CertiK says it has completed formal verification of zkWasm, a zero-knowledge virtual machine (system proving computations without revealing them) for WebAssembly programs, using machine-checked proofs written in the Coq proof assistant. The open-source project from Delphinus Lab allows developers to prove that a WebAssembly program ran correctly without disclosing its computation. The verification covers circuit soundness and knowledge soundness across arithmetic and bitwise operations, memory access, control flow and function calls. CertiK translated zkWasm’s Halo2 circuit logic into Coq and developed about 33,000 lines of code, including roughly 21,000 lines of proofs. The company says the process uncovered and resolved correctness issues, while its site identifies two soundness bugs involving a missing memory-load constraint and missing constraints on the Return instruction. The formal guarantee is limited to the Halo2 circuits and their relationship to WebAssembly semantics; Rust table-building code, the Wasmi interpreter, Halo2 itself, external calls, instruction decoding and some constraint-generating Rust remain outside the proved scope or are trusted. Public materials expose definitions and theorem statements but replace proofs with placeholders. CertiK has not said whether the proofs will be released, which zkWasm version was verified or what changed since its April 2024 technical work. The effort comes as other teams pursue zkVM verification, including an Ethereum Foundation project with a $20 million budget, a Certora grant for autoprecompiles and Nethermind’s Lean-based work on Halo2 constraints.