EthSystemsはプライバシープールの形式的検証を完了し、規範をSepoliaバイトコードに適用しました。

イーサリアムの機関プライバシー技術機関 EthSystems は、そのプライバシープール（shielded pool）について、文書化された仕様から Sepolia テストネットでのバイトコードの実行までの形式的検証を完了したことを発表しました。検証は層ごとに異なるツールを使用して行われました：モデル、回路、ハッシュには Lean を、契約には Halmos と Kontrol を、ウォレットには Aeneas と Verus を、検証者とデプロイにはバイト単位の再構築による照合を使用しました。

二重支払いと価値保存は Lean 定理機械によって検証されました。検証中に6つの問題が発見され、そのうち3つは検証ツール自体に起因していました。チームは同時に依存している仮定を列挙しました：ハッシュの衝突がないこと、検証者が偽造証明を拒否すること、契約の動作がモデルと一致すること。