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.