LayerZero Verifies Critical Piece of Jolt Virtual Machine

LayerZero Research has completed formal verification of Jolt's bytecode expansion process, which transforms raw RISC-V instructions into Jolt's internal representation before zero-knowledge proving. This critical step in the Jolt virtual machine ensures that every proof built on top of it is valid.

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. Out of 67 expandable RISC-V instructions, 60 were fully proven, while the remaining seven were not provable due to specific edge cases that have been documented in a published paper.

The verification process took approximately 2.5 months and utilized AI tools, including Claude and Codex, to accelerate proof generation. Human engineers wrote the critical definitions and initial proof templates, with AI tools helping generate similar proofs for structurally repetitive instructions.