LayerZero Research completes formal verification of Jolt bytecode expansion
The team used the Lean theorem prover to formally verify 60 of 67 RISC-V instructions over roughly 2.5 months, marking a key milestone in zkVM correctness.
Formal verification is the software equivalent of a mathematical proof. Instead of testing whether code behaves correctly under a set of conditions, you prove it must behave correctly under all conditions. LayerZero Research just finished doing it for a critical piece of Jolt, their zero-knowledge virtual machine built for RISC-V architecture.
The specific component now verified is bytecode expansion, the process that transforms raw RISC-V instructions into Jolt’s internal representation before any zero-knowledge proving happens. If that transformation is wrong, every proof built on top of it is suspect.
What actually got verified, and how
The team used Lean, a formal theorem-proving assistant, to check the correctness of bytecode expansion against a trusted RISC-V reference model called LeanRV64D, which is itself derived from the Sail RISC-V specification.
Out of 67 expandable RISC-V instructions, 60 were fully proven. The remaining seven were not provable due to specific edge cases that the team has documented in a published paper. The whole bytecode expansion verification effort took approximately 2.5 months.
One notable detail about the process: the team used AI tools, including Claude and Codex, to accelerate proof generation. Human engineers wrote the critical definitions and initial proof templates, and AI tools helped generate similar proofs for structurally repetitive instructions.
The news moving money, markets, and the world—before your day starts.
Daily. Free. Join 34,000+ readers across crypto, finance, and policy.
Why Jolt and why this matters now
Jolt originated from research by a16z crypto, which has also done prior formal verification work on related components using ACL2, a separate theorem-proving system. The a16z lineage gives Jolt an unusual pedigree for an open-source zkVM: it was designed with academic rigor from the start, built around lookup arguments via a protocol called Lasso and sumcheck protocols.
LayerZero has taken Jolt further, integrating it into their Zero chain with additions including GPU acceleration and post-quantum safety features marketed under the name Akita and LatticeJolt.
LayerZero describes the broader project as targeting full correctness of the Jolt zkVM, covering both completeness and soundness. Bytecode expansion verification is one stage in that larger program, which the team has structured into sequential phases.
The competitive context for formal zkVM verification
The fact that LayerZero’s formal verification program connects to prior a16z work using ACL2 signals continuity of effort rather than a one-time exercise. Multi-institution, multi-tool verification projects build a more robust credibility case than any single audit or proof run.
What to watch next is whether the remaining stages of Jolt’s formal verification program proceed on a similar timeline, and how the seven unverified instructions get handled, whether through future proofs as tooling improves or through architectural workarounds that avoid the problematic edge cases.