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

Heuristic
If the OpenVM verifier accepts a ZK proof, the claimed RISC-V program really executed and produced the claimed output.
Theorem
In 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.
Theorem
In 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.
Compiled
RISC-V guest program
Checked in Lean
Verified
VM Circuits
Verified
Recursion Circuits
Verified
Fiat-Shamir Transform
Verified
SWIRL IOP Soundness
Trusted base
Lean 4 kernel
The minimal formal proof checker, which has multiple independent implementations.
The ISA specification
We use a Lean backend for RISC-V converted from the official Sail model.
Hash function security
The 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

SWIRL

Straightline round-by-round knowledge soundness for SWIRL.

Read →

Fiat-Shamir

Applying the BCS transform to get a non-interactive proof system.

Read →

VM Circuits

Circuit correctness for every extension, including RISC-V.

Read →

Recursion & Aggregation

Combining SWIRL proofs with a recursive verifier.

Read →

Certified OpenVM Verifier

Compiling the Lean verifier into an executable binary.

Read →

E2E Composition

Putting everything together for OpenVM as a whole.

Read →

SWIRL

Straightline round-by-round knowledge soundness for SWIRL.

Read →

Fiat-Shamir

Applying the BCS transform to get a non-interactive proof system.

Read →Builds on: SWIRL

VM Circuits

Circuit correctness for every extension, including RISC-V.

Read →

Recursion & Aggregation

Combining SWIRL proofs with a recursive verifier.

Read →Builds on: Fiat-Shamir

Certified OpenVM Verifier

Compiling the Lean verifier into an executable binary.

Read →Builds on: Fiat-Shamir

E2E Composition

Putting everything together for OpenVM as a whole.

Read →Builds on: VM Circuits · Recursion & Aggregation · Certified OpenVM Verifier
Proof stats
Size of the Lean development by component
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
Statement lines
152,691
Proof lines
2,066,773
Theorems
64,115
Proof checking

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 ZK proof verifier now has formal correctness guarantees. Read about the compilation process.

$ cargo openvm verify stark --certified