A model of the RISC Zero zkVM and ecosystem in the Lean 4 Theorem Prover
:warning: 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:
We are currently developing the meta-theory of these systems.
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/env
Now you can perform the build:
risc0-lean4$ lake build
This 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-lean4
Run a zkVM guest (without proof):
risc0-lean4$ ./build/bin/zkvm-emu-lean4
Read the headers of an ELF binary:
risc0-lean4$ ./build/bin/elf-dump-lean4
$ lake -Kdoc=on update
$ lake -Kdoc=on build Zkvm:docs
The docs will be viewable at build/doc/index.html
.