Executive Summary

[palinatolmach]

Project Overview and Goals

This project review documents Runtime Verification's comprehensive formal verification work for the Ethereum Foundation's zkEVM Formal Verification project, delivered in August 2025. The Ethereum Foundation launched this initiative to achieve the highest possible level of assurance for zkEVMs, with the ultimate goal of creating bug-free zero-knowledge Ethereum Virtual Machines.

The overarching goal of the project was to establish mathematical equivalence between zkEVMs used for execution and formal models that have been tested against the EVM conformance test suite, providing the rigorous verification foundation needed for safe zkEVM deployment, and addressing the challenge that many RISC-V based zkEVM approaches rely on REVM (Rust-based EVM implementation) compiled to RISC-V.

Key Deliverables

1. Lean 4 Backend (klean Tool)

• Repository: runtimeverification/k (pyk.klean module)
• Purpose: Bridge between K Framework and Lean 4 theorem proving ecosystems
• Achievement: Developed command-line tool that generates Lean 4 programs from kompiled K definitions, enabling translation of EVM specifications into theorem-provable format for enhanced verification rigor. The technical innovation of exporting K definitions to Lean 4 proved successful, providing broader ecosystem value by making K semantics accessible to the Lean 4 community.

2. EVM Equivalence Verification Framework

• Repository: runtimeverification/evm-equivalence
• Purpose: Mathematically prove equivalence between Runtime Verification's KEVM and Nethermind's EvmYul models
• Achievement: Established formal proof methodology for opcode-by-opcode equivalence verification, providing mathematical guarantees that different EVM implementations behave identically—crucial for zkEVM trustworthiness

3. EVM Opcode Summarization System

• Repository: runtimeverification/evm-semantics
• Purpose: Generate atomic, single-step execution rules for EVM opcodes to accelerate verification
• Achievement: Created comprehensive summarization framework covering 68 EVM opcodes with 7,225 lines of standardized summary rules, dramatically improving symbolic execution efficiency for zkEVM verification

4. zkEVM Testing and Verification Workflow

• Repository: runtimeverification/zkevm-harness
• Purpose: Formally verify real-world EVM implementations (REVM) through RISC-V compilation and zero-knowledge toolchains
• Achievement: Implemented end-to-end pipeline that compiles Rust EVM code to RISC-V using RISC Zero and SP1 toolchains, then performs both concrete and symbolic verification using K Framework

5. RISC-V Semantics for zkEVM Verification

• Repository: runtimeverification/riscv-semantics
• Purpose: Enable formal verification of complex zkEVM implementations compiled to RISC-V architecture
• Achievement: Implemented complete RISC-V instruction set coverage and semantic optimizations, which crucial because REVM verification relies on compiling REVM to RISC-V, which in turn requires formal verification-ready RISC-V semantics.

Infrastructure Components Delivered

REVM ↔ KEVM Verification Infrastructure

• RISC-V semantics
• zkEVM harness supporting RISC Zero and SP1 compilation toolchains
• Comprehensive test suite covering all major EVM opcode categories

Cross-Framework Verification Capabilities

• klean tool enabling K Framework to Lean 4 translation
• Support for equivalence verification between KEVM and CLEAR models
• Extensible architecture for additional formal verification frameworks

Automated Verification Systems

• EVM opcode summarization reducing complex multi-step operations to atomic rules
• Scalable CI pipeline architecture for continuous re-verification
• Performance optimizations enabling practical verification of large-scale systems

Impact on zkEVM Ecosystem

This work directly addresses Runtime Verification's stated mission to "show that the EVMs used for zkEVM execution are correct." The delivered infrastructure provides:

• Mathematical Guarantees: Formal proofs that different zkEVM implementations behave equivalently
• Practical Verification: Tools for verifying real-world zkEVM implementations like those used by major projects
• Ecosystem Standardization: Common verification frameworks promoting consistency across zkEVM development
• Scalable Infrastructure: Systems capable of handling the complexity of production zkEVM verification

The project establishes the rigorous formal verification foundation necessary for the zkEVM ecosystem to achieve the Ethereum Foundation's goal of bug-free implementations, while maintaining the security and compatibility guarantees essential for Ethereum's scaling through zero-knowledge rollups.