⚠️ This repository contains research artifacts. It is a work in progress and should not be used for any purpose.
risc0-lean4 is a formal model of the RISC Zero zkVM, written in the Lean Theorem Prover (version 4). Its long-term goal is to support formal security and soundness proofs for the RISC Zero ecosystem.
We have executable models for:
- ELF file handling
- RV32IM emulation
- SHA2-256
- Merkle tree parsing and inclusion proof verification
- The Baby Bear field (and its degree 4 extension)
- Number Theoretic transform (NTT)
- FRI verification
- Arithmetic circuit parsing and evaluation
- zkVM receipt parsing and verification
We are currently developing the meta-theory of these systems.
- Main verification logic
- Lean version: Verify.lean
- Rust version: verify/mod.rs
- Merkle verification
- Lean version: Merkle.lean
- Rust version: verify/merkle.rs
- FRI verification
- Lean version: Fri.lean
- Rust version: verify/fri.rs
This repository trails behind the zkVM repository. Precise version information can be found in Cargo.lock.
See the Quickstart guide.
First, check to see if lake is in your terminal's search path. If not, you either haven't installed Lean4 yet, or you haven't source'd the elan environment variables.
risc0-lean4$ source ~/.elan/envNow you can perform the build:
risc0-lean4$ lake buildThis repository includes various executables. These executables are currently used for testing, but will eventually be expanded to provide greater utility.
Verify a receipt generated by the zkVM:
risc0-lean4$ ./build/bin/zkvm-verify-lean4Run a zkVM guest (without proof):
risc0-lean4$ ./build/bin/zkvm-emu-lean4Read the headers of an ELF binary:
risc0-lean4$ ./build/bin/elf-dump-lean4$ lake -Kdoc=on update
$ lake -Kdoc=on build Zkvm:docsThe docs will be viewable at build/doc/index.html.