Researchers who catalogued 141 security flaws in zero-knowledge proof systems between 2018 and 2024 found 99 of them in the circuits, the sets of mathematical constraints that decide whether a proof is accepted. Almost nine in ten of the 141 broke soundness, the guarantee that a prover cannot convince a verifier of something false, according to a study presented at USENIX Security 2024. A soundness bug does not crash a system or trigger an alert. It lets a false statement pass as true. Every application that trusts the proof then inherits the error without knowing it.

CertiK has now completed a mathematical proof that this cannot happen in zkWasm, the zero-knowledge virtual machine built by Delphinus Lab that proves a WebAssembly program ran correctly without revealing the computation behind it. Working in the Coq proof assistant, CertiK's researchers translated zkWasm's Halo2 circuit logic into formal definitions and built machine-checked proofs of two properties. The first is soundness: every computation trace the circuits accept is a valid run of the underlying Wasm program. The second is knowledge soundness: a prover cannot construct a valid proof for an execution that did not happen.

The proofs cover zkWasm's full instruction set, from arithmetic and bitwise operations to memory access, control flow and function calls. They also span every major component of the machine, from instruction execution to memory consistency and call-stack integrity, which CertiK describes as one of the most comprehensive formal verifications yet applied to a zkVM in production. The firm has documented the methodology and proof architecture in a technical blog series and published the theorem statements in its zkwasm-fv repository.

Why zkVM Circuits Carry the Most Risk

A zkVM lets developers write ordinary programs and get a proof that they ran correctly, without hand-building a custom circuit for every application. That convenience is why zkVMs now sit under rollups, cross-chain bridges and privacy-preserving applications. It also concentrates risk. Every program proved on zkWasm passes through the same circuits, so a single missing constraint weakens every proof built on top of it at once. The USENIX study found that 95 of its 99 circuit bugs broke soundness. Many came from constraints that were missing altogether or that translated the intended logic into constraints incorrectly, the kind of flaw a test suite rarely exercises because the honest path through the program still works.

The Rising Cost of Code-Level Flaws

The money exposed to code-level mistakes keeps growing. CertiK's own incident tracking puts Web3 security losses at $1.84 billion across 751 incidents in 2023, $2.45 billion in 2024 and $3.35 billion in 2025, a year that included the $1.45 billion supply-chain attack on Bybit. Code vulnerabilities accounted for 240 of 2025's 630 incidents. The first half of 2026 brought another $1.31 billion, about 28 percent more than the same period a year earlier once the Bybit outlier is set aside. Zero-knowledge systems raise the ceiling on that exposure. A flaw in one protocol's contract drains that protocol, while a soundness flaw in a zkVM that settles a rollup or a blockchain's blocks would let an attacker prove any state they liked.

How CertiK Built the Proof

zkWasm records a program's execution in a set of tables that the circuits then check against one another. The execution table holds one row for every step the program takes. Separate tables track memory, globals and the stack, the call frames that let functions return to the right place and the bitwise and range checks that keep numbers within bounds.

CertiK modelled each table and its constraints in Coq, reusing the WasmCert-Coq specification of WebAssembly where it could, then proved that any set of rows satisfying the constraints describes a legitimate execution. In its published figures, about 6,000 lines of Rust circuit definitions inside a 22,000-line codebase required 11,880 lines of Coq definitions and 21,200 lines of proofs, a total of 33,080. That is roughly five and a half lines of machine-checked reasoning for every line of circuit code. Every one of those lines is checked by the proof assistant rather than by a reviewer's judgement.

What the Proofs Caught That Audits Missed

The effort paid for itself before it was finished. CertiK first reported verifying zkWasm's circuits in April 2024 and later that spring described two critical bugs it had found along the way. The first, caught during an audit, sat in the instruction that loads a single byte from memory: the circuit forced only some of the unused upper bits to zero, so a malicious prover could slip arbitrary data into a load. The second was found only by the formal proofs. zkWasm tracked function calls and returns with a single counter, which meant a frame containing two returns looked identical to a frame containing a call and a return. An attacker could inject a fake return into a valid execution. In CertiK's example, that let a token balance increase three times instead of once. The code matched its design exactly. The design itself was wrong, which is why a line-by-line review could not see it. The fix counts calls and returns separately so that every frame has exactly one of each.

Completeness of the proofs matters as much as their existence. In October 2025 the Ethereum Foundation's zkEVM team reviewed the formal verification of another zkVM, SP1 Hypercube. It found complete and correct Lean proofs for 51 of the 62 RISC-V opcodes that had been claimed, warning that specifications and security goals are easy to get subtly wrong. Coverage of the full instruction set and of the machine's supporting components is therefore the part of CertiK's result that carries the most weight.

Where Formal Verification Goes Next

The largest buyer of this kind of assurance is about to be Ethereum itself. The Ethereum Foundation plans for validators to check zkVM proofs of each block instead of re-executing every transaction. Its zkEVM team has set security milestones of 100-bit provable security by the end of May 2026 and 128-bit by the end of the year, with proof sizes capped at 600 KiB and then 300 KiB. Proving has already become fast enough to matter: the same team reports latency falling from 16 minutes to 16 seconds and costs dropping 45 times. Alexander Hicks, who works on the Foundation's zkEVM formal verification project, expects optional proving on Ethereum after the Glamsterdam upgrade and mandatory proving in 2027 or very early 2028. He has said every zkVM in contention should have its RISC-V circuits formally verified well before that date.

zkWasm proves WebAssembly rather than RISC-V, but the method carries over. CertiK has presented its zkWasm work as the foundation for verifying RISC-V zkVMs: model each table in a proof assistant, state what a correct execution means and prove that the constraints admit nothing else. The approach comes from the company's academic roots. CertiK was founded by computer scientists from Yale University and Columbia University whose earlier research produced CertiKOS, a formally verified operating system kernel. The firm now serves more than 5,500 enterprise clients across audits, penetration testing, custody reviews and formal verification.

Most security work on zero-knowledge systems still ends with a report that lists the problems a reviewer found. A completed formal proof ends with a statement about every execution the circuits will ever accept, checked line by line by a machine. As rollups, bridges and eventually Ethereum's own blocks come to rest on zkVM proofs, that kind of statement is likely to move from a differentiator to an expectation. zkWasm is now one of the few production zkVMs that can make it in full.

Don’t forget to like and share the story!