セキュリティ/形式検証の @Certora が Ethereum Foundation から 研究助成金を獲得 Powdr Labs の autoprecompiles を対象に、zkEVM 向け最適化の正当性検証を進めるとのことです
プロジェクト概要
Certora は、スマートコントラクトの挙動を仕様として書き、それが常に満たされるかを数理的にチェックする形式検証ツール群を開発しています。
Certora Prover は、コントラクト本体とルール（CVL）を入力とし、成立する場合は証明、破れる場合は具体的な反例（どの入力・状態遷移で壊れるか）を返すことができるオープンソースツールです。
仕様を先に書いて CI に組み込み、コミットごとに回すことが可能です。
今回の助成金は、Ethereum Foundation の zkEVM イニシアティブで使われる「autoprecompiles」を検証する研究に向けたもので、autoprecompiles は Powdr Labs が取り組む最適化で、zkEVM 上の暗号・算術演算を速くするために再利用される低レベルの回路コンポーネントを自動で推論して生成する仕組みだそうです。
Certora は、この取り組みで作る仕様・証明・検証フレームワークをオープンソース化し、zkEVM 実装やロールアップ開発者が再利用できる形で公開する方針とのことです。