LayerZero Research completes formal verification of Jolt bytecode expansion

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, includin...