Efficient Branch-and-Bound Testing and Verification of zkVMs

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 missing or 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 bugdetection framework grounded in a precise correctness criterion: for a given program and input, the constraint system must admit exactly one valid execution trace-no more (soundness) and no fewer (completeness). 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 realworld zkVMs, constraints utilize only 14.0% of their theoretical connectivity capacity on average. This sparsity enables tight interval propagation with limited over-approximation error. ZEBRA performs a parallel branch-and-bound search that, unlike fuzzing, either produces a concrete counterexample or certifies the absence of violations within a bounded input region.

We evaluate ZEBRA on five real-world zkVMs. ZEBRA discovers 11 previously unknown vulnerabilities, including critical flaws enabling control-flow hijacking and proof forgery-none detected by a state-of-the-art fuzzer; 6 have already been independently confirmed and 3 have been fixed by developers. Compared to SMTbased verification, ZEBRA is 51.5× faster, verifies 16.5 percentage point more instances, and its range verification provides up to 63× efficiency gain over repeated single-input verification.

• Security and privacy → Software security engineering; Cryptanalysis and other attacks.