Certified OpenVM Verifier

OpenVM ships a certified verifier for its standard VM configuration, compiled from the Lean reference verifier to C. This applies its soundness and canonicity guarantees to all the STARK proofs you verify.

INTEGRATION FLOW

How the certified verifier works

The Lean executable invokes the reference verifier to check the final recursive STARK, then checks the VM public values.

TRY IT NOW

Run the certified verifier

Install the OpenVM CLI with the certified verifier enabled, then run it against a RISC-V OpenVM STARK proof.

BASH

$ cargo install cargo-openvm --features certified-verifier

$ cargo openvm verify stark --certified

Certified verifier accepted the proof

NOTE

Currently, only OpenVM's canonical standard configuration with default parameters is formally verified. This scope is checked before the certified verifier is launched.