CertiK Completes Formal Verification of zkWasm, Mathematically Proving the zkVM Sound

This story was originally published on HackerNoon at: https://hackernoon.com/certik-completes-formal-verification-of-zkwasm-mathematically-proving-the-zkvm-sound.
CertiK used the Coq proof assistant to prove zkWasm's circuits sound across its full instruction set, catching a design bug audits missed.
Check more stories related to programming at: https://hackernoon.com/c/programming. You can also check exclusive content about #certik, #web3, #ai-and-ml, #cybersecurity, #software-engineering, #technology, #good-company, #zkevm, and more.

This story was written by: @ishanpandey. Learn more about this writer by checking @ishanpandey's about page, and for more stories, please visit hackernoon.com.

CertiK has completed a formal verification of zkWasm, the zero-knowledge virtual machine for WebAssembly built by Delphinus Lab. Using the Coq proof assistant, it proved the zkVM's Halo2 circuits sound and knowledge sound across arithmetic, bitwise, memory, control-flow and function-call instructions. The work, which CertiK began in 2024, runs to more than 33,000 lines of machine-checked Coq and caught a critical design bug that auditing had missed. It arrives as Ethereum prepares to verify its own blocks with zkVM proofs, with the Ethereum Foundation targeting 128-bit provable security by the end of 2026.