EthSystems завершила формальну верифікацію приватного пулу

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