Jolt QED: Formally Verifying Jolt Bytecode Expansion In Lean

See A16z summer series for a brief talk about the work given by Quang Dao. A less formal but equally detailed, and sometimes more up to date blog series about the work can be found here.

Abstract#

In this work, we formally verify using the Lean4 proof assistant, that jolt zk-VM’s bytecode expansion process faithfully emulates a RISC-V CPU. Prior work translated the official Sail specification of RISC-V into Lean. We extend this model to define the Jolt ISA in Lean. We then write a transpiler to automatically extract Jolt’s bytecode expansions into Lean from their Rust definitions. Finally, we prove these expansions equivalent to their corresponding RISC-V instructions. Additionally, this lays the groundwork for proving the upstream components of Jolt are complete and sound.