CertiK表示，已完成对zkWasm的形式化验证。zkWasm是面向WebAssembly程序的零知识虚拟机（一种无需披露计算内容即可证明计算结果的系统），其验证采用由Coq证明助手编写并经机器检查的证明。Delphinus Lab开源的这一项目允许开发者证明WebAssembly程序已正确运行，而无需披露其计算过程。此次验证涵盖算术和位运算、内存访问、控制流及函数调用等方面的电路完备性与知识完备性。CertiK将zkWasm的Halo2电路逻辑转换为Coq，并开发了约33,000行代码，其中约21,000行为证明代码。该公司表示，这一过程发现并解决了正确性问题；其网站则指出，项目涉及两个完备性漏洞，分别与缺失的内存加载约束和Return指令缺少约束有关。形式化保证仅限于Halo2电路及其与WebAssembly语义之间的关系；Rust表构建代码、Wasmi解释器、Halo2本身、外部调用、指令解码以及部分生成约束的Rust代码，仍在已证明范围之外或属于受信任部分。公开材料展示了定义和定理陈述，但以占位符替代了证明。CertiK尚未说明是否会公开这些证明、完成验证的是哪个zkWasm版本，或自2024年4月的技术工作以来有哪些变化。随着其他团队也在推进zkVM验证，这项工作应运而生，其中包括以太坊基金会一项预算为2,000万美元的项目、Certora一项面向自动预编译合约的资助，以及Nethermind基于Lean对Halo2约束开展的工作。