Jolt’s 60 Verified Instructions Clarify What a zkVM Proof Really Covers

LayerZero has released Jolt-QED, a Lean-based formal-verification project for the Jolt zero-knowledge virtual machine. The immediate result is not a claim that the entire zkVM is formally verified. It is a proof that 60 of Jolt’s 67 expandable RISC-V instructions faithfully implement their corresponding RISC-V semantics.

That distinction matters because Jolt does not prove the original RISC-V program directly. Its tracer first rewrites instructions that are not convenient for the proving system into sequences of Jolt instructions. The resulting program is then executed and proved. If that rewrite changes the program’s meaning, a cryptographically valid proof could still attest to the wrong computation.

The Jolt-QED paper models both the RISC-V reference machine and the Jolt instruction set in Lean. It also describes a process for extracting bytecode expansions from the Rust implementation so that the statements being proved correspond to the implementation’s instruction definitions. For the verified instructions, the formal claim is semantic equivalence: starting from the same machine state, the expanded sequence reaches the same final RISC-V state as the original instruction.

This is a valuable security boundary for zkVM builders. Testing and fuzzing can find concrete mismatches, but they cannot establish that no mismatch exists across every input. Formal proofs can provide that stronger result for the exact model and assumptions they cover. The project’s repository makes those assumptions visible instead of presenting formal verification as an unlimited security guarantee.

The limitation is material: seven of the 67 expandable instructions remain unproven. The repository also marks the downstream Jolt constraints, sumchecks, reductions, and commitment scheme as unfinished or in progress. In other words, the new result strengthens one link in the proof chain; it does not independently establish the soundness of every component that produces or verifies a Jolt proof.

For ICP developers evaluating a zkVM-based component, the practical lesson is to request a trust-surface map, not just a benchmark. Check which guest instructions are supported, whether the translation layer is proven equivalent to the reference ISA, which compiler and generated models are trusted, and whether the deployed binary matches the verified source. A proof system can be mathematically sound while a pre-proof translation step still targets the wrong computation.

Jolt-QED therefore represents a useful shift in ZK engineering: verification claims are becoming modular, inspectable artifacts. The most meaningful question is no longer simply whether a zkVM is “formally verified,” but which transformation has been verified, against which specification, and what remains outside the proof.