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

Researchers have mathematically proven the security of zkWasm, a zero-knowledge virtual machine developed by Delphinus Lab. A formal verification process, conducted in the Coq proof assistant, confirms two critical properties of zkWasm: soundness and knowledge soundness. Soundness ensures that only valid computations are accepted, while knowledge soundness guarantees that provers cannot generate proofs for non-existent executions.

The verification covers the entire instruction set of zkWasm, including arithmetic, bitwise operations, memory access, control flow, and function calls. It also encompasses all major components of the machine, such as instruction execution, memory consistency, and call-stack integrity. This extensive coverage sets the formal verification apart from previous efforts applied to zkVMs in production.

Zero-knowledge virtual machines (zkVMs) have gained popularity due to their convenience, allowing developers to write standard programs and receive proof of correct execution without creating custom circuits for each application. However, this convenience also concentrates risk, as any weakness in the shared circuits can weaken all proofs built on top of them simultaneously.

The USENIX Security 2024 study found that 99 out of 141 security flaws in zero-knowledge proof systems were related to the circuits, with nearly 95% of the bugs breaking soundness. Many of these flaws stemmed from missing constraints or incorrect translations of intended logic into constraints, which often go undetected by standard test suites since the honest path through the program still functions.

As code-level mistakes continue to rise in cost, the potential exposure from flaws in zero-knowledge systems escalates. A single protocol's vulnerability can drain the entire protocol, while a soundness flaw in a zkVM used to settle rollups or blockchain blocks could allow attackers to prove any desired state. CertiK's formal verification of zkWasm's circuits provides a critical layer of assurance against such risks, ensuring the integrity and reliability of zkVM-based applications.