Show

Scroll

Core

Ethereum

Lean

<img width="1920" height="1080" src="https://blockchainreporter.net/wp-content/uploads/2025/12/certik6.webp" alt="certik" style="float: right; margin-left: 5px;" title="CertiK Says Coq Proofs Show zkWasm's Core Circuits Are Sound 12">
<p><a href="https://www.certik.com/" rel="noopener noreferrer nofollow">CertiK</a> says it has finished formally verifying zkWasm, a zero-knowledge virtual machine for WebAssembly programs, with machine-checked proofs written in the Coq proof assistant. The company announced the result on September 28, though the project isn’t new. Its <a href="https://www.certik.com/resources/blog/advanced-formal-verification-of-zero-knowledge-proof-blockchains" rel="noopener noreferrer nofollow">technical blog series</a> on the work goes back to April 2024, when CertiK first described a full verification of the zkWasm circuits.</p>
<p>zkWasm lets a developer prove that a WebAssembly program ran correctly without revealing the computation. The open-source project comes from Delphinus Lab. Everything built on it trusts the circuits, the constraint systems that decide what counts as a valid run. Miss one constraint and a dishonest prover may get a false execution accepted, quietly undermining every proof that depends on it. CertiK, which says it has worked with more than 5,500 enterprise clients, pitches formal verification as a step past audits and testing. In practice that means a proof checker confirms the code meets a mathematical specification for every input, not just the ones someone thought to try.</p>
<h2 id="what-certik-says-it-proved">What CertiK says it proved</h2>
<p>According to the release, the proofs establish two properties. The first is soundness: every accepted execution trace corresponds to a valid run of the Wasm program. The second, which CertiK calls knowledge soundness, is that a prover can’t produce a valid proof for an incorrect execution. The work covers arithmetic and bitwise operations, memory access, control flow and function calls. In 2024 CertiK called the project the world’s first complete formal verification of a zkVM. The new release settles on one of the most comprehensive efforts on a production zkVM so far.</p>
<p>The method was to translate zkWasm’s Halo2 circuit logic into Coq and prove statements about the translation. CertiK’s public README says the translation was done by hand and kept close to the Rust source to limit errors. The internal development runs to about 33,000 lines of Coq, roughly 21,000 of them proofs. (The Coq project has been renamed Rocq since 2025, though CertiK’s materials still use the old name.)</p>
<p>The release says subtle correctness issues turned up along the way and were resolved, without counting or grading them. CertiK’s site is more specific. It lists two soundness bugs in zkWasm: a missing constraint on a memory load, caught in manual review, and missing constraints on the Return instruction that allowed fake returns, caught by the proofs. Either could let a malicious prover get an invalid proof past the verifier, CertiK says.</p>
<h2 id="other-teams-are-verifying-zkvms-too">Other teams are verifying zkVMs too</h2>
<p>CertiK isn’t alone here. The Ethereum Foundation runs a $20 million zkEVM formal verification project. One of its researchers noted in a 2026 workshop abstract that the push to verify core parts of zkVMs for Ethereum’s base layer has run for over a year, with many teams involved. Certora won a foundation grant in February to verify autoprecompiles, a circuit optimization. Nethermind, working in Lean instead of Coq, built tooling that pulls Halo2 constraints into a proof assistant and used it to find a critical bug in a Scroll Keccak-256 circuit. That circuit had since been deprecated, and Nethermind said the bug couldn’t have been exploited because Scroll’s prover is centralized.</p>
<h2 id="what-the-proofs-don-t-cover">What the proofs don’t cover</h2>
<p>CertiK’s own README lays out the limits. The goal is to show the circuits are sound with respect to WebAssembly semantics, and everything outside the Halo2 circuits is out of scope. That includes the Rust code that builds the tables, the Wasmi interpreter and Halo2 itself. The external-call instruction is skipped because it has no real constraints. Instruction-decoding logic was audited by hand instead of proved, and some Rust that generates constraints is assumed correct. So the guarantee covers the circuits, with the rest taken on trust.</p>
<p>Outsiders can’t check all of it yet. The public GitHub repository publishes the definitions and theorem statements, so readers can see what was claimed, but it replaces the proofs with placeholders. The announcement doesn’t say whether they’ll be released, which zkWasm version was verified, or what changed since 2024. Any guarantee about proofs also leans on Halo2 doing its job, and the README puts Halo2 outside the verified scope.</p>

CertiK Says Coq Proofs Show zkWasm’s Core Circuits Are Sound

Table of Contents

BlockchainReporter

Other articles published on Sep 28, 2026

Ripple confirms top Korean banks and RippleX leaders for XRP Seoul 2026 event

BDAG Price Recovery to $0.5 Possible in Oct? BlockDAG Price Prediction

Who Is Dfinity Founder Dominic Williams, and What's He Trying to Prove With ICP?

Bitget Hack: What We Know About The $351M Breach

What Does The GENIUS Act Actually Require Under US Crypto Policy?

Quant & Sei Network leads gains among crypto majors.

Join our free newsletter for daily crypto updates!