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

Эфириум-организация по технологиям конфиденциальности EthSystems объявила о завершении формальной верификации своего конфиденциального пула (shielded pool), охватывающей от письменных спецификаций до байт-кода, работающего в тестовой сети Sepolia. Верификация проводилась с использованием различных инструментов по слоям: модели, схемы и хеши с помощью Lean, контракты с помощью Halmos и Kontrol, кошельки с помощью Aeneas и Verus, а верификаторы и развертывание проверялись посимвольно.

Двойные траты и сохранение стоимости были проверены с помощью теоремной машины Lean. В процессе верификации было обнаружено 6 проблем, из которых 3 возникли в самом инструменте верификации. Команда также перечислила предположения, от которых она по-прежнему зависит: хеши без коллизий, верификаторы будут отклонять поддельные доказательства, поведение контрактов соответствует модели.