Formally Verifying the OpenVM RISC-V Extension

We’ve partnered with Nethermind Research to formally verify the functional correctness of the OpenVM RV32IM extension in Lean, supported by an Ethereum Foundation grant. Alongside this, we are introducing provable 100-bit security on the Axiom Proving API with the new OpenVM 1.5.0 release. With these developments, we aim to provide developers stronger ZK security assurances backed by formal methods, and we are committed to maintaining them as standard guarantees going forward.

Using Lean, this work proves that OpenVM’s RISC-V implementation matches the official SAIL specifications and correctly constrains execution and memory consistency, which goes beyond previous formal verification efforts for zkVMs. As a result, we can give users greater assurance that the ZK proofs generated by OpenVM are correct. Notably, the verification process, which covered all 45 RV32IM opcodes, uncovered no ZK circuit bugs, a testament to the robustness of our previous security work. To learn more about the methodology and security assumptions behind the verification, read the OpenVM blog post and the full verification report.

In conjunction with the formal verification, we are moving to provable security for OpenVM. OpenVM 1.5.0 featuring 100 bits of provable security is available today on the Axiom Proving API, and we will maintain this standard for OpenVM 2.0. This ensures that proofs generated by the Axiom Proving API provide security guarantees backed by mathematical theorems rather than conjectures.

Looking ahead, we will continue to invest in formal verification to offer developers the strongest possible security guarantees. We are actively collaborating with teams across the ecosystem to implement ZK for applications using OpenVM and deploy them on the Axiom Proving API. If you’re interested, get in touch!