Towards a verified Jolt zkVM

Galois is excited to announce that we are kicking off a project to verify the frontend of the Jolt zkVM, with financial support provided by a grant from the Ethereum Foundation. 

Zero-knowledge virtual machines (zkVMs) emulate program executions in ZK, enabling verifiers to validate a program’s execution faster than it takes to rerun the computation – improving scalability and privacy. These powerful virtual machines have numerous use cases: from quickly validating smart contract transactions on blockchains to proving that a piece of software has a vulnerability without revealing the triggering exploit. 

One key benefit is that zkVMs make it possible for developers to automatically convert a program written in a high level language like C or Rust into a ZK statement. Manually writing ZK statements requires extensive cryptography expertise, and the process is tedious and error prone. By contrast, zkVMs make ZK much more accessible and reduce the odds of making mistakes that introduce security vulnerabilities. 

While zkVMs eliminate the need for developers to write correct ZK statements themselves, it is vital that the ZK statements that zkVMs produce are correct. Mistakes would result in security vulnerabilities, allowing attackers to produce bogus proofs. In short, the whole value proposition of zkVMs depends on guaranteed reliability and correctness. This project will formally verify that the frontend statements produced by the Jolt zkVM conform to a golden specification of the RISC-V semantics.

Jolt is one of the most promising zero-knowledge virtual machines (zkVMs), offering state of the art prover times with succinct proof sizes and verifier times. Jolt’s ZK statements enforce the execution of a RISC-V machine and are composed of R1CS constraints, indexed lookup tables, and memory checks. Recent work verified the lookup tables for each machine instruction. This project extends the previous work by verifying the entire Jolt frontend statement including the R1CS constraints and memory checks. In particular, we aim to mechanically prove in Lean 4 that Jolt’s frontend statements match the semantics of the RISC-V machine as defined in Sail.

Acknowledgements

Thank you to the Ethereum Foundation for funding this work! This effort will help secure the Ethereum ecosystem wherever Jolt is used to scale performance of layer 2 and eventually layer 1 systems. During this project, Galois will be collaborating with the developers of Jolt, the University of Cambridge, and Lindy Labs.