Today we are announcing that the functional correctness of the OpenVM RV32IM extension has been formally verified in Lean by Nethermind Research with support from an Ethereum Foundation grant. This marks the first step in incorporating formal methods into the OpenVM development process, which we intend to maintain as a standard component of our ongoing security strategy.
This verification ensures that the statements proven in ZK by OpenVM match the official SAIL specification for RISC-V by proving that OpenVM polynomial constraints exactly codify RV32IM opcode functionality. No ZK circuit bugs were found in OpenVM’s implementation of RISC-V opcodes in the course of verification, giving users a formal assurance that there are no missing constraints that could lead to critical soundness vulnerabilities.
In addition to covering all 45 RV32IM opcodes, this work also verified correctness of execution and memory consistency, going beyond previous formal verification efforts for zkVMs. We assumed the correctness of the LogUp multiset consistency arguments in OpenVM, which will be the subject of future formal verification work.
What was verified
To formally verify the OpenVM RV32IM extension, Nethermind first built tooling to extract the underlying polynomial constraints from each OpenVM AIR written in the Plonky3 ZK frontend. This resulted in a representation of the constraints as polynomial equations in Lean. Nethermind then proved that these polynomials imply the functional relation between opcode inputs and outputs as codified in the standard SAIL specification for RISC-V.
The result of the process was Lean proofs covering all 45 RV32IM opcodes, spanning:
ALU opcodes (27): ADD, ADDI, SUB, XOR, XORI, OR, ORI, AND, ANDI, SLT, SLTI, SLTU, SLTUI, SLL, SLLI, SRL, SRLI, SRA, SRAI, MUL, MULH, MULHU, MULHSU, DIV, DIVU, REM, REMU
Control-flow opcodes (10): AUIPC, BEQ, BNE, BLT, BGE, BLTU, BGEU, LUI, JAL, JALR
Memory manipulation opcodes (8): LW, LH, LHU, LB, LBU, SW, SH, SB
These proofs ensure that there are no missing or conflicting constraints in the opcode circuits, which implies functional correctness of OpenVM’s handling of RISC-V, including memory and execution consistency. This verification focused on the OpenVM frontend and assumed the correctness of the LogUp multiset equality argument and underlying proof system comprising the OpenVM backend. These will be the focus of future verification efforts as we expand the scope of formal methods in OpenVM.
We are open-sourcing the verification infrastructure and artifacts:
The verification tooling to extract Plonky3 constraints from OpenVM chips is available at Nethermind’s forks of OpenVM and STARK-backend. In future work, these will be merged into the main OpenVM repos
The Lean proofs for each RV32IM opcode are available open-sourced here
The full verification report can be found here
We plan to accompany future releases with updates to this verification infrastructure to ensure OpenVM remains continuously formally verified.
OpenVM is moving to provable security
In tandem with this milestone, OpenVM is making a broader move toward provable security. Today we are announcing a new OpenVM 1.5.0 release with 100 bits of provable security, available on GitHub under MIT and Apache 2.0 dual-license. The upcoming OpenVM 2.0 release will also feature 100 provable bits of security, and we are actively working towards 128 bits of provable security. Together, these efforts push OpenVM toward a future where the strength and correctness of its security are backed by rigorous formal methods without reliance on conjectures.
To stay up to date with new OpenVM developments, join our developer Telegram and follow us on X. Until then, you can find our open-source code on GitHub – see you there!