Introducing zkvmBlast: Differential Fuzzing for Ethereum's zkVMs

Today we are introducing zkvmBlast, a zkVM-agnostic differential fuzzer for RISC-V zkVMs. It takes one program, runs it across many zkVMs and a reference simulator, and reports every important disagreement. It looks mainly for two kinds of bugs: soundness bugs, where a prover can convince a verifier of something false, and completeness bugs, where a valid program cannot be proved at all. The same setup also catches executor-correctness bugs, where the zkVM's own execution diverges from the RISC-V specification before any proving happens. The work was partially funded by the Ethereum Foundation.

The campaigns so far have surfaced seven distinct completeness and correctness bugs across SP1, Pico, and OpenVM, all responsibly disclosed, plus a reproduction of a known RISC0 soundness bug. This post describes what zkVMs are, why their correctness is becoming critical for Ethereum, why completeness deserves more attention than it currently gets, and what zkvmBlast does about it. We will follow up with deeper posts on the individual techniques developed for zkvmBlast.

zkVMs and their role on Ethereum's future

A zkVM (zero-knowledge virtual machine) lets you write a program in a normal language like Rust, compile it to a standard instruction set (almost always RISC-V today), and produce a succinct proof that the program ran and produced a given output. Anyone can verify that proof succinctly (i.e., cheaply), without re-running the program. If you want a proper introduction, we have written two: zkVM Security: What Could Go Wrong? and Projects That Shaped Modern zkVMs.

Until recently zkVMs were an application-layer component, e.g., a rollup, a bridge, or a coprocessor could use a zkVM to compress computation. That is changing. The Ethereum Foundation is pushing the "snarkification" of Ethereum itself, a direction Vitalik Buterin laid out in "The Verge", where an ordinary block is proved with a validity proof so that verifying the chain no longer requires re-executing every transaction. The main requirement is "real-time" proving: proving the vast majority of mainnet blocks inside a slot, on modest hardware.¹

This is no longer a distant idea. Ethproofs, an Ethereum Foundation project, is a public leaderboard that tracks proofs of real mainnet blocks across zkVMs and provers, measuring latency and cost the way L2BEAT tracks rollups. Alongside it, the EF's zkEVM team runs its own benchmarking effort aimed at worst-case, adversarial blocks rather than average ones. Both efforts lean on Ere², a library that puts many zkVMs behind a single compile/execute/prove interface.

What could go wrong: soundness, completeness, and executor correctness

Two properties matter for the proof system itself, and they fail in opposite directions. A third concern sits underneath both: soundness and completeness ask whether the proof system faithfully reflects what the zkVM executed, and executor correctness asks whether what it executed was RISC-V at all.

Soundness is the classic target, and rightly so. In an Ethereum setting a soundness bug is catastrophic: a malicious prover could get the network to accept a proof for an invalid state transition, forging balances or state roots. Most zkVM security work, including the fault-injection research we build on, aims here. We have found our share of these too, for instance in Jolt and OpenVM.

Completeness gets far less attention, and that is exactly why we leaned into it. A completeness bug sounds benign: a program simply fails to prove. But consider what that means once proving is on Ethereum's critical path.

Figure 1. A completeness bug is a liveness risk. The block is valid and every node executes it cleanly, but the prover cannot produce the proof the protocol now demands, so proving stalls on a legitimate block.

Suppose a block is completely valid. Every node executes it and the state transition is correct. Now the prover is asked to prove that execution and cannot, because some instruction the block happens to use trigger a crash in the zkVM. In snarkified Ethereum where blocks must carry validity proofs, and no honest prover can produce the required proof for a legitimate block, then finality cannot get reached. This is a liveness failure, and it does not require a malicious prover: it can happen by accident, or an attacker can craft a transaction whose execution deliberately hits the completeness bug, leading to a denial-of-service against the entire network.³

Completeness bugs also tend to hide on the edges of the RISC-V specification, the corner cases where a naive-looking implementation shortcut silently diverges from the spec.

Executor correctness is a root cause rather than an outcome, and the consequences depend on further checks done by the proof system. Soundness and completeness describe what a user ends up observing. Given a divergent trace (i.e. a trace that is not executed according to RISC-V semantics):

The third row is still not harmless. Developers iterate against the executor, because executing is fast and proving is expensive. An executor that silently accepts what the specification forbids tells them their program is fine, and the truth surfaces much later, possibly with a difficult to interpret failure that is not linked to the original issue (for instance a cumulative-sum mismatch deep inside the proving stack, or, on OpenVM, as a verification failure after prove has already printed a success message). Fortunately, every executor-correctness bug we found lands in that third row: none produced an accepted proof of a divergent execution (soundness) and none rejected a program the specification called valid (completeness).

Formal verification efforts focus on soundness so far

The strongest tool we have for zkVM correctness has, so far, mostly looked in one direction. The Ethereum Foundation's Verified zkEVM project is a multi-team effort to formally verify zkVMs against the RISC-V specification, with the ambitious goal of bug-free zk(E)VMs by 2027. We contribute to that ecosystem through our own Clean framework for verifying circuits and multi-AIR systems in Lean.

But the formal verification of zkVM constraints has, up to now, almost entirely targeted soundness. A typical theorem proves that satisfying a chip's constraints implies the corresponding RISC-V instruction executed correctly, so no false proof can be produced. The reverse direction, that a correct execution can always be proved, is the completeness property, and it is usually left out of scope: it requires reasoning about the prover's witness generation rather than the constraints alone, which is a much larger and less explored target.

The gap is not hypothetical. When Succinct and Nethermind formally verified the core of SP1 Hypercube, the effort established soundness for the RV64 opcodes but, by its own account, set completeness aside. A misaligned-target JALR bug then fell straight through that gap: a jump whose target address has its low bit set is valid and well-defined under the spec, yet the prover crashes or the verifier rejects. The EF's own writeup calls it "a completeness bug which, in practical terms, could be a denial-of-service vector," and notes it was outside the scope of the verification effort, highlighting the need to augment formal methods with other techniques to ensure prover uptime. This is exactly the class zkvmBlast is built to surface; our RISC-V enumeration even carries a dedicated probe for misaligned jump targets of this kind.

What zkvmBlast does

zkvmBlast is a differential-testing framework. The core idea is simple and old, if you run the same program through several independent implementations plus a trusted reference, they should all agree, and any disagreement is a candidate bug. What makes it work for zkVMs is doing this across the whole stack, from a high-level Rust guest down to individual RISC-V instructions, and adding oracles that can see not just crashes but wrong results and unprovable executions.

Figure 2. zkvmBlast at a glance. A range of program sources feed two differential harnesses, which drive a shared set of zkVM executors alongside the Spike reference simulator (in green). A differential oracle compares every executor against the reference: agreement is the healthy outcome, and any disagreement is classified as a completeness, executor-correctness, or soundness bug.

The framework has four moving parts, kept deliberately decoupled so a new program source, a new zkVM, or a new oracle can be added without requiring any further changes.

Program sources (seeds). The fuzzer is only as good as its seeds, so we generate them through different approaches to cover most of zkVMs' infrastructure. On the Rust side: a corpus gathered and mutated from real-world algorithm code and compiler tests, our zkRustSmith fork of RustSmith for random Rust programs, full Reth Ethereum blocks executed inside the guest, and precompile-exercising programs. On the RISC-V side: random Cascade-style RV32IM programs, a hand-built spec-isolation corpus that pins down individual specification corners, and an adapted Skeletal Program Enumeration approach that systematically enumerates instruction variants. The RISC-V seed corpus is released as its own repository, riscv-seeds-lab.

Executors. Every program is emitted into the format each target expects and run side by side. On the Rust path we cover SP1, RISC0, OpenVM, Pico, and Zisk through Ere; on the RISC-V path we cover SP1, RISC0, OpenVM, Pico, and Airbender against the Spike reference simulator, which serves as ground truth for what a correct RISC-V machine should do. Note that we have adapters for RISC-V programs to efficiently fuzz those zkVMs.

Differential oracle. Disagreements are caught at several levels, such as whether programs terminate the same way (success, trap, or timeout), whether they reach the same final register state, whether a program the reference accepts can actually be proved, and, on the soundness oracle, whether a corrupted execution still produces a proof a verifier accepts.

Fault injection. The differential oracle only ever sees what an honest run produces, but a soundness bug needs a dishonest prover, so we simulate one. The harness patches witness generation to inject a single controlled fault into an otherwise normal proving run, leaves the constraint system untouched, and hands the resulting proof to an independent, unpatched verifier. If that verifier still accepts and the public values differ from the clean run, the constraints failed to pin down something they should have, and that is a soundness bug. The faults themselves are small and targeted, for instance corrupting an ALU result, redirecting a register write, tampering with a fetched instruction word or the program counter, or altering the value a memory read returns, each aimed at a different part of the constraint system. The design follows Arguzz, with ELF inputs rather than CircIL-derived product programs. For now we have only experimented adding faults to SP1, OpenVM and Risc0, given that instrumenting the prover implies patching its source code and is highly architecture dependent (as opposed to the differential testing described above, which implies only matching the expected binary format for the candidate programs).

A design goal throughout was low-effort adoption. A zkVM team can point the harness at its own guest programs, drop in a new backend through Ere, and use the whole thing as a CI job that fails on any unexplained divergence.

What we have found so far

Below are the findings we can share now as we have already triage them and share them with the teams. All were responsibly disclosed to the affected teams; some are already fixed.

Every completeness and executor-correctness finding is stopped somewhere in the pipeline, usually by a prover that fails or hangs, and in one case only by the verifier, after prove has already reported success. The soundness row is the only one marked Not caught, which is exactly what makes it a soundness bug: nothing in the pipeline objects at all. Three findings are worth a closer look, one completeness bug and two executor-correctness bugs whose divergent traces the proof system refused downstream.

Writing a nonzero result to x0. The RISC-V specification fixes register x0 at zero, so any write to it is discarded. An interpreter follows the spec and drops the write. But a prover that computes the raw ALU result on one chip and separately constrains x0 to zero on another produces an unsatisfiable constraint whenever the discarded result happens to be nonzero, so a valid program cannot be proved.

li   t0, 7
li   t1, 3
add  x0, t0, t1    # result 10 is discarded; x0 stays 0 per the spec

This is valid RISC-V that Spike runs to a clean halt, yet SP1 v6.0.2 and Pico v1.3.0 rejected it at proving time. SP1 has fixed it upstream.

Misaligned instruction fetch. A branch or jump to a target that is not four-byte aligned must raise an instruction-address-misaligned trap. OpenVM, Pico, and SP1 v6 instead continue silently at the misaligned address during execution. The divergence is caught downstream, but not during execution: Pico's prover panics with Regional cumulative sum is not zero, raised by a consistency check buried inside it, SP1 v6 retries a shard indefinitely on a GKR cumulative sum mismatch, and OpenVM generates a proof, prints App proof completed!, and only fails at cargo openvm verify with stark verification error: challenge phase error. None of these messages hints at a misaligned jump.

auipc t0, 0         # t0 = address of this instruction
addi  t0, t0, 6     # target = that address + 6, which is 2 mod 4
jalr  zero, t0, 0   # jalr clears bit 0, but 6 is even, so the target stays 2 mod 4
                    # spec: trap with instruction-address-misaligned
                    # OpenVM, Pico, and SP1 v6: continue at the misaligned PC

Misaligned word load/store in OpenVM. The spec allows two behaviors for a misaligned data access: trap, or perform the access with the correct result. For lw and sw, OpenVM does neither. It silently rounds the address down to the nearest four-byte boundary and reads or writes the wrong bytes, while the same module handles the halfword variants correctly. Given a buffer whose first four bytes are 01 02 03 04:

lw   t0, 1(a0)     # spec: trap, or return the bytes at offsets 1..4 (0x00040302)
                   # OpenVM: silently returns 0x04030201 (offset 0)

The prover refuses to build a trace for the misaligned access, panicking with unaligned memory access not supported: LOADW, shift: 1, so the wrong value is never certified. The executor is the only stage where this looks like a working program.

None of these classes are covered by the standard riscv-tests suite, which is why generating targeted tests out of the specification, rather than only reusing existing ones, mattered.

Conclusion

zkVMs are on their way to becoming part of Ethereum's trusted computing base. When they get there, every gap between a zkVM and the RISC-V specification is a gap in Ethereum's security or liveness. zkvmBlast is our attempt to close those gaps systematically: one program, many zkVMs, a trusted reference, and an oracle strong enough to see soundness failures, executors that quietly diverge from the specification, and, crucially, the completeness bugs that could lead to chain halts. The result is a reusable framework that a zkVM team can adopt with little effort and keep running in CI, and a first batch of real findings to show it works.

If you build or depend on a zkVM and want it fuzzed, hardened, or audited, we would love to work with you. Reach out at zksecurity.xyz/contact.

Acknowledgements

This work was partially funded by the Ethereum Foundation, whose support made the project possible. We also thank Cody Gunton for valuable feedback and brainstorming throughout the work.