EVM Track
Verifying that the EVM guest program executed inside a zkVM correctly implements the EVM specification, with the assurance carried down to the RISC-V the prover actually runs.
Overview
Verification Goals
Selected Resources
Grants
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