CertiKは、WebAssemblyプログラム向けのゼロ知識仮想マシン（計算内容を明らかにせずに計算を証明するシステム）であるzkWasmの形式検証を完了したと明らかにした。検証には、Coq証明支援系で記述した機械検査可能な証明を用いた。Delphinus Labが公開するオープンソースプロジェクトzkWasmにより、開発者は計算内容を開示せず、WebAssemblyプログラムが正しく実行されたことを証明できる。検証の対象は、算術・ビット演算、メモリアクセス、制御フロー、関数呼び出しにまたがる回路の健全性と知識健全性である。CertiKはzkWasmのHalo2回路ロジックをCoqに移植し、約3万3000行のコードを開発した。このうち約2万1000行が証明コードである。同社によると、この過程で正確性に関する問題を発見し、解決した。一方、同社のサイトでは、メモリーロード制約の欠落とReturn命令に対する制約の欠落という、2件の健全性バグが示されている。形式検証による保証は、Halo2回路とWebAssemblyセマンティクスの関係に限定される。Rustによるテーブル構築コード、Wasmiインタープリター、Halo2自体、外部呼び出し、命令デコード、一部の制約生成用Rustコードは、証明の対象外または信頼する要素として扱われる。公開資料には定義と定理の記述が掲載されているが、証明はプレースホルダーに置き換えられている。CertiKは、証明を公開するかどうか、どのバージョンのzkWasmを検証したのか、2024年4月の技術作業以降に何が変更されたのかを明らかにしていない。今回の取り組みは、他のチームもzkVMの検証を進める中で行われた。イーサリアム財団は2000万ドルの予算を組んだプロジェクトを進めており、Certoraは自動precompile向けの助成を実施し、NethermindはHalo2制約のLeanベースの取り組みを進めている。