End-to-end formally verifying OpenVM

Duration: NaN:NaN:NaN

Speaker: Yi Sun

Type: Lightning Talk

Expertise: Some familiarity with the topic

Event: Devcon

Date: Nov 2026

Real-time proving makes it possible to verify Ethereum execution as blocks are produced, but performance alone is not enough: the entire proving stack must correctly connect program execution to the final proofs. This talk presents Axiom’s end-to-end formal verification effort for OpenVM. We explain how we use Lean to prove soundness of the SWIRL proof system, verify that the production Rust verifier faithfully implements its mathematical specification, and establish correctness of the RISC-V virtual machine and recursive verifier circuits. We will discuss how these proofs compose into a single assurance story, where the main trust boundaries remain, and the engineering techniques required to verify a zkVM running in production. Attendees will leave with a concrete blueprint for formally verifying a complex real-world cryptographic system.