EthSystemsがプライバシープールの形式検証を完了、仕様からSepoliaのバイトコードまでをカバー

PANews 10月27日付 —— イーサリアムの機関向けプライバシー技術機関であるEthSystemsは、プライバシープール（shielded pool）の形式検証を完了したと発表した。検証範囲は文書化された仕様から、Sepoliaテストネット上で動作するバイトコードにまで及ぶ。検証はレイヤーごとに異なるツールを使用した。モデル、回路、ハッシュにはLean、コントラクトにはHalmosとKontrol、ウォレットにはAeneasとVerusを用い、検証器とデプロイはバイト単位の再構築によって照合した。二重使用と価値保存はLeanの定理として機械検証されている。検証では計6件の問題が発見され、うち3件は検証ツール自体に起因するものだった。チームは同時に、依然として依存している仮定も列挙した。ハッシュに衝突が存在しないこと、検証器が偽の証明を拒否すること、コントラクトの挙動がモデルと一致することである。