EVM Track
Verification of Ethereum execution guest program deployed on a zkVM correctly implements the EVM specification at the level of the RISC-V instructions.
Overview
With uncertainty regarding client diversity, the status of each client with respect to use with zkVMs and the variance in language specific verification tooling, this track has ultimately focused on the feasibility of implementing an execution guest program with natively verified RISC-V assembly, either via the use of a proof assistant as macro assembler or via verified compilation.
Verification Goals
Selected Resources
Grants
evm-asm
Intended to support the development of formally verified Ethereum execution guest programs for zkVMs, exploring macro assembly in Lean and verified compilation.
Awarded to: zkSecurity
Certified compilation
Intended to support research on certified compilation methods in the Rocq ecosystem together with tools for high-assurance cryptography.
Awarded to: Aarhus University
Development of an EVM in Rocq
Intended to support the development of a canonical, maintainable, and validated EVM specification in Rocq.
Awarded to: KTH Royal Institute of Technology
Verification of revm and Lean backend for K
Intended to support verification of revm compiled to RISC-V against KEVM together with development of a Lean backend for K.
Awarded to: Runtime Verification
Repositories
Verified-zkEVM/evm-asm
Verified macro assembler building the EVM guest bottom-up from a machine-checked RV64 core (experimental prototype)
- EVM
Verified-zkEVM/CompPoly
- EVM
Verified-zkEVM/iris-lean
- EVM
pirapira/stateless-pancaketh
Experimental Ethereum stateless guest implementation in Pancake.
- EVM
Talks and Videos
October 2025
pq2-05: e2e Formal Verification
- EVM
October 2025
Comparing ZK Constraints - Keccak, Plonky3 - Rust/Rocq
- EVM
- zkVM
March 2025
Q1 2025: EVM Track update
- EVM
Papers
OOPSLA 2025
Certified Decision Procedures for Width-Independent Bitvector Predicates
Siddharth Bhat, Léo Stefanesco, Chris Hughes, Tobias Grosser.
- EVM
OOPSLA 2025
Interactive Bitvector Reasoning using Verified Bit-Blasting
Henrik Böving, Siddharth Bhat, Luisa Cicolini, Alex Keizer, Léon Frenot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark Barrett, Tobias Grosser.
- EVM
Articles
January 2026 · Formal Land
Formal verification of the Keccak precompile from Plonky3
- EVM
- zkVM