Two weeks ago, we introduced Akita: a new, highly performant polynomial commitment scheme inside Jolt, the zk-VM underpinning Zero’s proving architecture. Today, we share another update: Jolt bytecode expansion has been formally verified using the Lean proving assistant.
We are releasing a repo of machine-checked proofs, and a preprint of the paper describing the process.
What Formal Verification delivers
Formal verification refers to the act of writing proofs of mathematical claims in a manner that can be automatically checked by a computer.
Loosely, the Jolt zk-VM takes a RISC-V guest program as input, and outputs an efficiently checkable proof that it ran every instruction of the guest program correctly. The Jolt CPU, however, only implements a strict subset of the RISC-V instructions, namely, those RISC-V instructions that satisfy certain decomposability conditions. Additionally, Jolt also supports a small set of decomposable instructions that are native only to the Jolt CPU, called virtual instructions. Together they form the Jolt instruction set. For each of the unimplemented non-decomposable RISC-V instructions, Jolt emulates them by executing a sequence of one or more Jolt instructions - a process referred to as bytecode expansion in the Jolt literature.
For Jolt proofs to be meaningful, it is imperative that the expanded programs faithfully simulate their RISC-V counterparts. Failure to do so, would imply that the Jolt proofs are vacuous. As Jolt is a foundational component of Zero’s proving stack, rather than simply testing equivalence against a random sample of test cases, we formally verify the equivalence claim for all inputs, something that would otherwise be computationally infeasible merely by fuzzing. Additionally, by representing the Jolt Instruction set in Lean, we also lay the foundations towards formally verifying the remaining components of Jolt, which is currently in progress.
Explore in detail
Given the extremely strong guarantees of proof assistants, it can be tempting to use formal verification as a broad umbrella to advertise unbounded security guarantees of a zk-VM. The details of course are subtle and require careful exploration. In the Github repo we document in detail the assumptions needed to prove theorems, their importance, how we wrote down the theorems in the first place, and explicitly outline the exact trust surface of what is assumed to be safe, and what is proven to be secure.
- Preprint - A self contained description of the entire process to be submitted for peer-review.
- Repo + Technical Blogs - Machine-checked proofs, as well as a detailed exploration of the formal verification process.