Announcement ↗

OpenVM is end-to-end formally verified

Machine-checked theorems in Lean 4 covering all of OpenVM, from soundness of the SWIRL proof system to the recursion and RISC-V circuits.

Read the announcementLearn more ↓
WHAT WE VERIFY

Formally verified in Lean 4

HEURISTICIf the OpenVM verifier accepts a proof, the claimed RISC-V program really executed and produced the claimed output.
THEOREMIn the random permutation model, if a series of OpenVM app proofs are accepted, then there exists a RISC-V execution trace of the committed program producing the claimed output, up to a quantitative soundness error.
THEOREMIn the random permutation model, if a family of SWIRL recursion proofs is accepted, then there exist child proofs accepted by the SWIRL verifier at the layers immediately below, up to a quantitative soundness error.
CHECKED IN LEANTRUSTED
COMPILED
RISC-V guest program
CHECKED IN LEAN
VERIFIEDVM Circuits
VERIFIEDRecursion Circuits
VERIFIEDFiat-Shamir Transform
VERIFIEDSWIRL IOP Soundness
TRUSTED BASE
Lean 4 kernelThe minimal formal proof checker, which has multiple independent implementations.
The ISA specificationWe use a Lean backend for RISC-V converted from the official Sail model.
Hash function securityThe Poseidon2 hash used in SWIRL is assumed to be built on a good deterministic proxy for a random permutation.
PROOF BLUEPRINT

How the formal verification fits together

Composing results about each component into an end-to-end verification

SWIRLStraightline round-by-round knowledge soundness for SWIRL.READ →Fiat-ShamirApplying the BCS transform to get a non-interactive proof system.READ →VM CircuitsCircuit correctness for every extension, including RISC-V.READ →Recursion & AggregationCombining SWIRL proofs with a recursive verifier.READ →Certified OpenVM VerifierCompiling the Lean verifier into an executable binary.READ →E2E CompositionPutting everything together for OpenVM as a whole.READ →
SWIRLREAD →Straightline round-by-round knowledge soundness for SWIRL.Fiat-ShamirREAD →Applying the BCS transform to get a non-interactive proof system.BUILDS ON: SWIRLVM CircuitsREAD →Circuit correctness for every extension, including RISC-V.Recursion & AggregationREAD →Combining SWIRL proofs with a recursive verifier.BUILDS ON: FIAT-SHAMIRCertified OpenVM VerifierREAD →Compiling the Lean verifier into an executable binary.BUILDS ON: FIAT-SHAMIRE2E CompositionREAD →Putting everything together for OpenVM as a whole.BUILDS ON: VM CIRCUITS · RECURSION & AGGREGATION · CERTIFIED OPENVM VERIFIER
COMPONENTSTATEMENT LINESPROOF LINESTHEOREMS
SWIRL103,167199,6606,426
Fiat-Shamir30,481490,2179,783
VM Circuits7,843495,23124,365
Recursion & Aggregation9,777853,25722,544
Certified OpenVM Verifier1762480
End-to-End Composition1,24728,160997
Total152,6912,066,77364,115
PROOF STATS: AGGREGATE
152,691STATEMENT LINES
2,066,773PROOF LINES
64,115THEOREMS
CHECK THE LEAN PROOFS

Machine-checked proofs

Our proofs are verified by the Lean kernel, a minimal type checker with multiple independent implementations, ensuring logical correctness.

We audit the proofs with the gold standard Lean comparator, confirming that every theorem is stated using a small trusted core of definitions and that its proof relies only on Lean's standard axioms. This rules out statement tampering or usage of hidden assumptions.

Visit each proof blueprint page to check correctness of the statements.

CERTIFIED VERIFIER

Integrated into OpenVM

The certified Lean verifier is compiled to a C binary and integrated into OpenVM 2.1.0, meaning the zero-knowledge proof verifier now has formal correctness guarantees. Read about the compilation process.

VERIFY OPENVM PROOFS IN CERTIFIED MODE
$ cargo openvm verify stark --certified
LEARN MORE

Announcement

Announcement blog postwww.axiom-staging.xyz/blog/openvm-fv ↗