EthSystemsがプライバシープールの形式的検証を完了、Sepoliaバイトコードをカバー

イーサリアムのプライバシー技術機関であるEthSystemsは、プライバシープールの形式的検証を完了したと発表しました。検証の範囲は、文書の仕様からSepoliaテストネットのバイトコードまで広がっています。検証プロセスでは、さまざまなツールが使用され、モデル、回路、ハッシュにはLeanが、契約にはHalmosとKontrolが、ウォレットにはAeneasとVerusが使用され、検証者とデプロイはバイト単位の再構築によって確認されました。二重支払いと価値保存はLean定理証明器によって検証されました。検証中に6つの問題が発見され、そのうち3つは検証ツール自体に起因しています。チームは、ハッシュの衝突がないこと、検証者が偽造証明を拒否すること、契約の動作がモデルと一致することなど、依然として依存している仮定を列挙しました。