Efficient Branch-and-Bound Testing and Verification of zkVMs
Hideaki Takahashi, Suman Jana, Junfeng Yang
cs.CR
Sep 14, 2026 · v1
TL;DR
Formally verifies in Lean 4 the injectivity and cardinality-preservation of the trace canonicalizers used by the ZEBRA zkVM verifier, at the algorithmic specification level.
Abstract
Zero-knowledge virtual machines (zkVMs) enable verifiable execution of general-purpose programs by translating virtual machine semantics into algebraic constraints over execution traces. The correctness of these constraints is critical: a single incorrect constraint can admit forged proofs (under-constrained) or reject valid executions (over-constrained). Existing approaches do not provide meaningful guarantees at production scale: fuzzers and unit tests often miss bugs, SMT solvers struggle with the size and nonlinearity of constraints, and theorem provers require substantial manual effort. We present ZEBRA, a fully automated verification and bug-detection framework: for a given program and input, the constraint must admit exactly one valid execution trace - no more and no fewer. This reduces zkVM verification to a solution-set cardinality problem over a canonical trace space, where redundancies such as null-row padding and non-deterministic permutations are eliminated prior to counting. To compute cardinality tractably, ZEBRA lifts analysis from finite-field witnesses to an integer interval lattice, exploiting a structural sparsity property of zkVM constraints: across 5 real-world zkVMs, constraints utilize only 14.0% of their theoretical connectivity capacity on average. This sparsity enables tight interval propagation with limited approximation error. ZEBRA performs a parallel branch-and-bound search that either produces a concrete counter-example or certifies the absence of violations within a bounded region. We evaluate ZEBRA on five real-world zkVMs. ZEBRA discovers 11 zero-day bugs; 6 have already been independently confirmed and 3 have been fixed by developers. Compared to SMT-based verification, ZEBRA is 51.5x faster, verifies 16.5 percentage point more instances, and its range verification provides up to 63x efficiency gain over repeated single-input verification.
Problem
zkVM correctness depends on algebraic constraints over execution traces. A single wrong constraint can admit forged proofs (under-constrained) or reject valid executions (over-constrained). Fuzzers, SMT solvers and manual theorem proving do not scale to production zkVMs.
Approach
ZEBRA reduces zkVM verification to checking that a given program and input admit exactly one canonical execution trace. Canonicalizers first remove redundancies such as padding rows and permutations. Trace cells are lifted to integer intervals, exploiting the sparsity of zkVM constraints, and a parallel branch-and-bound search runs over them. The canonicalizers' injectivity and cardinality preservation are formally verified in Lean 4 at the specification level. The engine itself is about 4,500 lines of Rust.
Results
Across five Plonky3-based zkVMs (Pico, SP1, Sphinx, Valida, Ziren), ZEBRA found 11 zero-day bugs; 6 were confirmed and 3 fixed. It is 51.5x faster than SMT-based verification and verifies 16.5 percentage points more instances. Range verification gives up to a 63x gain over repeated single-input verification.
