EthSystems завершила формальну верифікацію приватного пулу, охоплюючи байт-код Sepolia

Ethereum-приватна технологічна компанія EthSystems оголосила про завершення формальної верифікації свого приватного пулу, охоплюючи від письмових специфікацій до байт-коду на тестовій мережі Sepolia. У процесі верифікації було використано кілька інструментів: моделі, схеми та хеші використовували Lean, контракти – Halmos і Kontrol, гаманці – Aeneas і Verus, а верифікатори та деплоймент перевірялися шляхом побайтової реконструкції. Двійники та збереження вартості були перевірені за допомогою теоремної машини Lean. Під час верифікації було виявлено 6 проблем, з яких 3 виникли в самих інструментах верифікації. Команда також перерахувала припущення, від яких вона все ще залежить, включаючи відсутність колізій у хешах, те, що верифікатори відхилять підроблені докази, і що поведінка контрактів узгоджується з моделлю.