CertiK Completes Formal Verification of zkWasm zkVM in Coq

CertiK has completed a formal verification of zkWasm, the zero-knowledge virtual machine from Delphinus Lab that proves correct execution of WebAssembly programs. Working in the Coq proof assistant, researchers proved soundness and knowledge soundness across the full instruction set; about 6,000 lines of Rust circuit code required 33,080 lines of Coq definitions and proofs.

• Soundness and knowledge soundness proved for all zkWasm instructions
• 6,000 lines of Rust circuits required 33,080 lines of Coq proofs
• Formal methods caught a bug allowing fake function returns
• USENIX 2024: 99 of 141 zk-system flaws were in circuits