# LayerZero Labs Verifies 60 of 67 Jolt Bytecode Instructions in Lean

By Simon Yoon

Canonical URL: https://www.tokenpost.com/news/technology/23378
Published: 2026-09-23T15:47:13.000Z
Updated: 2026-09-23T15:47:13.000Z

LayerZero Labs has formally verified 60 of 67 expandable RISC-V instructions in Jolt’s bytecode-expansion stage, advancing but not completing the zero-knowledge virtual machine’s wider verification effort.

Jolt is a zero-knowledge virtual machine designed to prove program execution. Its bytecode-expansion component converts RISC-V instructions into the structured representation used by the proving system.

The completed work covered 60 instructions over approximately two and a half months. Seven instructions remain unproven, and the reasons are detailed in Section 7 of the preprint.

The proofs were written in Lean with LeanRV64D, a RISC-V reference model generated from forks of the official Sail RISC-V model and Sail compiler. AI agents assisted with repetitive proof-writing tasks, while humans wrote critical definitions and initial proof templates.

Formal verification uses a theorem prover to establish that software meets specified properties across the inputs covered by its model. For Jolt, the completed proofs apply to bytecode expansion rather than the entire zkVM.

The broader formal-verification project remains ongoing. Its remaining stages include Jolt constraints, sumchecks, reductions and the commitment scheme.