ZkVM verification made faster and more reliable with ZEBRA
Efficient Branch-and-Bound Testing and Verification of zkVMs
Cryptography and Security
Summary
Verifying the correctness of zero-knowledge virtual machines (zkVMs) is very important because even one small mistake can let hackers cheat or block valid programs. The authors created ZEBRA, a tool that automatically checks if zkVM constraints produce exactly one valid execution for given inputs, ensuring correctness. It uses a clever method to count possible executions much faster than existing tools, helping find bugs that previous testing missed. ZEBRA successfully found and helped fix real bugs in multiple zkVM implementations.
What this means in practice
- •For blockchain developers: Detect and fix subtle correctness bugs in zkVM implementations to improve security and reliability of blockchain smart contracts.
- •For security testing teams: Automate verification of cryptographic software to find critical vulnerabilities faster and with less manual effort.
Authors
Hideaki Takahashi, Suman Jana, Junfeng Yang
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.