OpenVM is Now End-to-End Formally Verified

We are excited to announce that OpenVM is now the first end-to-end formally verified zero-knowledge virtual machine (zkVM). OpenVM 2.1.0 ships with a certified STARK verifier compiled from a reference verifier written in Lean whose soundness we formally prove. We prove in Lean that if this reference verifier accepts a proof, then the committed RISC-V program really executed and produced the claimed output. Our proofs connect the reference verifier to every layer of the OpenVM stack and heuristically compose to give the final result.

Verifying the whole stack, rather than individual components, is what makes this guarantee meaningful. Bugs in ZK systems often hide at the boundaries between components, such as between a circuit and the proof system that checks it, or between an interactive proof system and its Fiat-Shamir transform, and verifying components in isolation cannot rule them out. Because our theorems connect every part of OpenVM into a single statement about the system as a whole, the only gaps that remain are the explicitly stated assumptions and heuristic steps we describe below.

We undertook this formal verification effort because frontier AI poses a growing cybersecurity risk. This year alone, AI agents breached Hugging Face, escaped KVM isolation, and found a 13-year-old Chrome sandbox escape. ZK systems are no exception: our AI auditor found a soundness vulnerability in the stwo-cairo proof system that partial formal verification had not covered. End-to-end formal verification closes gaps like this one and provides a guarantee that holds up against arbitrarily powerful AI attackers.

In the rest of this post, we explain the scope of our formal verification, the security guarantees it provides and their limitations, and the benefits for users. To learn more about the verification, check out the explainer website.

Why End-to-End Formal Verification Matters

This release completes the end-to-end formal verification of OpenVM soundness. Formal verification proves that a given class of bugs cannot exist by providing a mathematical guarantee that a given system follows a desired specification. Critically, this guarantee remains robust as attack tools improve, since it is based on machine-checkable logic rather than human or AI code auditing. For that reason, it anchors the highest-assurance security work, from the seL4 kernel in defense systems to the SL5 standard for secure deployment of frontier AI.

Formal verification is difficult to do well and has well-known pitfalls: it can leave parts of the system unverified, verify a model that differs from the code running in production, or prove a specification that does not say what was intended. We address the last issue with expert human review of theorem statements and all definitions going into them, while the first two are prevented by the end-to-end coverage of our verification approach.

A typical limitation of ZK formal verification efforts is covering only the proof system or the ZK circuits, leaving Fiat-Shamir bugs out of scope. These bugs are some of the most dangerous and difficult to find. Both Plonky3 and stwo-cairo had soundness bugs where a value was left out of the Fiat-Shamir transcript, and in stwo-cairo the bug sat just outside circuits that had been formally verified in Lean. By covering the full ZK proving stack, our approach provides formal guarantees against this type of vulnerability.

Another common issue is a discrepancy between the model of the system covered by formal verification and what is actually deployed. To address this issue, we compile the Lean reference verifier itself into the certified verifier that ships in OpenVM 2.1.0 and extract circuit constraints directly from the production verifying keys. This gives us confidence that our formal results apply to the verifier that users actually run in OpenVM.

How We Did It

We applied the extraction, specification, and proving framework from our prior verification work to every layer of OpenVM, from SWIRL and Fiat-Shamir through VM execution, recursion, and the shipped verifier:

Extraction: We programmatically extracted the polynomial constraints of the VM, recursion, and aggregation circuits in OpenVM's standard configuration from their verifying keys into Lean, so the Lean model is exactly the set of constraints the production verifier enforces.
Specification: We specify the RISC-V semantics followed by programs proven by OpenVM by converting the official Sail model to Lean. For the recursion, we use an executable reference verifier for SWIRL written in Lean for which we prove cryptographic soundness. We compile this into a certified verifier integrated into OpenVM to ensure that our specification matches what is running in production.
Proving: We developed a multi-agent system based on frontier models to generate the Lean proofs connecting the extracted constraints to the specification.

Writing the proofs at this scale would historically have been out of reach. For a sense of the cost, the landmark seL4 microkernel, about 8,700 lines of C, took roughly 25 person-years to design, implement, and verify. With our multi-agent system, our small team completed the end-to-end verification in four months.

Every proof is checked by the Lean kernel, which has multiple redundant implementations. For AI-generated proofs, we must also defend against the known risk of reward hacking, where an agent might introduce new assumptions or maliciously modify the statement of a theorem instead of proving the intended statement. We therefore also audit every proof with the Lean comparator, the gold standard for checking Lean proofs, which confirms in an isolated build that each theorem matches its human-reviewed published statement, contains no sorry, and relies only on Lean's standard axioms.

In total, the verification comprises 64,115 theorems with no sorry placeholders. The theorem statements rely on 152,691 total lines of definitions, which should be reviewed by a reader seeking to trust the verification. These theorems are proven using 2,066,773 lines of proofs, which are machine-checked by Lean and can be ignored by the reader. These break down by component as follows:

Component	Statement lines	Proof lines	Theorems
SWIRL	103,167	199,660	6,426
Fiat-Shamir	30,481	490,217	9,783
VM Circuits	7,843	495,231	24,365
Recursion & Aggregation	9,777	853,257	22,544
Certified OpenVM Verifier	176	248	0
End-to-End Composition	1,247	28,160	997
Total	152,691	2,066,773	64,115

What We Verified

OpenVM produces a single final STARK proof attesting to the execution of a RISC-V program. We prove a theorem in Lean for each layer of the proving stack and compose them heuristically into the following end-to-end conclusion:

If the OpenVM verifier accepts a proof, then the committed RISC-V program really executed and produced the claimed output, up to a quantitative soundness error.

This holds for every program, input, and proof, providing broader coverage than traditional audits or testing, and establishes 100 bits of provable security for OpenVM's default parameters. Below, we summarize each component and how the results compose.

SWIRL IOP Soundness

SWIRL is the proof system underlying OpenVM 2.0 and later. We prove in Lean that its interactive form satisfies straightline knowledge soundness with an explicit error bound, a strong notion that preserves security when removing interaction and supports our analysis of proof recursion. This required formalizing the full protocol, down to the coding-theory results it rests on.

Fiat-Shamir

OpenVM makes SWIRL non-interactive using the BCS transform, the version of the Fiat-Shamir transform for IOPs: it commits to each oracle with a Merkle tree and replaces the verifier's random challenges with a hash of everything sent so far. We prove in Lean that this preserves knowledge soundness in an idealized hash model.

Applying this to SWIRL gives knowledge soundness of the non-interactive SWIRL protocol. We then prove that the resulting verifier is equivalent to the SWIRL reference verifier that OpenVM actually runs. This rules out missing components in the Fiat-Shamir transform, such as a prover message that is never absorbed into the transcript.

VM Extension Circuits

OpenVM's VM circuits constrain the execution of RISC-V instructions and of OpenVM's extensions, which accelerate hashing and elliptic curve operations. We prove that any witness satisfying their constraints, extracted directly from the production verifying keys, follows the RISC-V semantics of the official Sail specification. Combined with the Fiat-Shamir result, this shows that accepted app proofs imply a real RISC-V execution of the committed program producing the claimed output.

Recursion and Aggregation Circuits

OpenVM aggregates app proofs recursively into a single STARK proof, with each aggregation circuit verifying the proofs one layer below. Their specification is the SWIRL reference verifier, together with additional logic connecting adjacent proofs. We prove that whenever an aggregation proof is accepted, the proofs one layer below are accepted by the reference verifier and describe the same VM execution.

Putting it all Together

Composing these results, the certified verifier checks the final proof with the reference verifier, the recursion theorem unwinds it layer by layer down to the app proofs, and the VM theorem turns those into a RISC-V execution with the claimed output.

Each step is a Lean theorem, but composing them across recursion relies on standard heuristics, since no widely accepted theoretical framework yet covers soundness of recursive proofs. Limitations details exactly where these heuristics enter.

Integrating Into OpenVM

OpenVM 2.1.0 ships a certified verifier compiled from the reference SWIRL verifier as part of the OpenVM CLI. We produce this by compiling the reference verifier from Lean to C, and it verifies unmodified OpenVM STARK proofs. This provides high confidence that our formal verification applies to the OpenVM verifier that is used in practice. In certified mode, the CLI first checks that the proof targets OpenVM's canonical standard configuration, then runs the reference verifier on the final recursive STARK and checks the VM public values.

To try it, install the OpenVM CLI with the certified verifier enabled and run it against a RISC-V OpenVM STARK proof:

cargo install cargo-openvm --features certified-verifier
cargo openvm verify stark --certified

Limitations

Like any formal verification, ours rests on a set of assumptions and covers a specific scope. Users should be aware of these limitations when relying on the verification and using OpenVM.

Three assumptions underlie any result proven in Lean, including ours:

The Lean kernel. Every result assumes the soundness of the Lean kernel that checks the proofs. Our proofs are checked on Lean v4.34.0, which includes fixes for the soundness bugs found by recent AI-assisted bug hunts (postmortem) and has no known soundness issues as of this writing.
Correctness of the specification. A theorem is only as meaningful as the definitions it is stated in. The guarantee assumes that the specification in our formalization, including the reference verifier, the security definitions, and the RISC-V semantics converted from the official Sail specification, correctly captures its intent, as do the Mathlib definitions it builds on.
The Lean-to-C compiler. The certified verifier is compiled from Lean to C, so the Lean-to-C compiler and the C toolchain that builds the binary are trusted.

Beyond these, the OpenVM verification has the following specific limitations:

Completeness. We prove soundness, meaning false statements are rejected. We do not prove completeness, meaning that every honest proof verifies.
Heuristic steps. Three steps, all part of composing the component theorems, rest on standard heuristics rather than theorems: composing the recursion layers into one end-to-end statement; applying Fiat-Shamir security in the recursive setting, where each aggregation circuit computes the hash in-circuit instead of querying an oracle; and transferring bounds proven in the ideal permutation model to the concrete Poseidon2 hash.
Non-standard configurations. Only OpenVM's canonical standard configuration with default parameters is verified.
Onchain verification. The Halo2 wrapper and the EVM verifier used for onchain verification are outside the scope of this release.

What's Next

For users, this verification provides formal assurances that certain classes of common vulnerabilities cannot occur, which becomes increasingly important as OpenVM is used for more critical and higher-stakes applications.

At Axiom, we believe securing high-assurance software with formal verification is critical in an era of AI-enabled attacks, and it is the direction we are building toward. We see this release as one of the first instances of an industry-wide trend: formal verification of large-scale production software, long considered too costly, is becoming viable with the right approach and expert supervision.

End-to-end formal verification is now part of our ongoing security posture for OpenVM. Future releases will ship with updated proofs so the certified verifier tracks production code. To learn more about the release, explore the explainer website.

If you are considering formal verification for your own high-assurance software, we would be glad to talk about how our approach could apply. Please get in touch. To follow our work, join the developer Telegram and follow us on X.