EVM Equivalence

[JuanCoRo]

Executive Summary

This section provides a summary of the runtimeverification/evm-equivalence repository.

Project Overview and Significance

The evm-equivalence repository contains the formal proof of equivalence between two independent mathematical models of the Ethereum Virtual Machine (EVM): Nethermind's EvmYul and Runtime Verification's KEVM. This work aims to mathematically guarantee that these two distinct models of the EVM behave identically.This project provides an additional layer of trust, ensuring that different formal EVM models don't have any behavioral divergences.

Technology Stack

The project leverages a sophisticated stack of formal methods technologies to bridge two different verification paradigms:

• K Framework: A rewrite-based executable semantic framework. Runtime Verification's KEVM model, a complete formal specification of the EVM, is written in K. The K Framework excels at defining the operational semantics of a language—how it executes step-by-step.
• Lean 4: A functional programming language and interactive theorem prover based on dependent type theory. Nethermind's EvmYul model is written in Lean 4.
• klean Tool: A command-line utility from K's pyk library that serves as the bridge between the two ecosystems. It translates semantic rules from compiled K definitions (like those in KEVM) into corresponding Lean 4 code, enabling the comparison to be performed within a single proof environment.

Work Process and Methodology

The project employs a systematic, multi-stage methodology to prove equivalence on an opcode-by-opcode basis. This "divide and conquer" strategy makes the task of verifying the entire EVM more tractable. The workflow for each opcode can be summarized as follows:

• Code Generation: The klean tool is used to translate a specific K rule corresponding to an EVM opcode's semantics (e.g., the rule for ADD) into a Lean 4 representation. This generated code resides in the KEVM2Lean directory.
• EvmYul Summarization: Provide the necessary theorems capturing the computational content of the needed opcode within the EvmYul model.
• State Mapping: Provide the formal mapping between a state in the KEVM model and a corresponding state in the EvmYul model. The function providing the mapping defines precisely what it means for the two machines to be in an "equivalent" state.
• Equivalence Proof: The final proof is constructed entirely within Lean 4. The core of the proof for each opcode is to demonstrate that if the two models start in equivalent initial states, they will transition to equivalent final states after executing that opcode. This proves that the state equivalence property is an invariant preserved by the operation. The individual proofs are contained in files of the Equivalence folder.

A Tale of Two Formalisms: KEVM and EvmYul

The core challenge of the evm-equivalence project lies in bridging the gap between two distinct and powerful mathematical frameworks. The two EVM models in question, Runtime Verification's KEVM and Nethermind's EvmYul, are implemented using different languages and are based on different approaches to formal methods.

The K Framework and KEVM: Executable Specifications

The K Framework is a technology for defining and analyzing programming languages. Its philosophy is that a language's formal specification should be directly executable. K is a rewrite-based system where behavior is defined by transition rules of the form $s_1 \Rightarrow s_2$, describing how a program state $s_1$ evolves to $s_2$. A K definition includes syntax, state structure, and transition rules. A key advantage is that a single K definition can generate various language tools like interpreters and verifiers.
KEVM is the application of this framework to the EVM. It is a complete, executable formal specification of the EVM in K, validated against an extensive test suite containing tens of thousands of cases.

Lean 4 and EvmYul: A Proving Ground for Mathematics and Software

Lean 4 is a modern theorem prover and functional programming language used for mathematics formalization and software verification. It is based on the Calculus of Constructions, a dependent type theory, which allows for expressing precise properties about programs. Lean's credibility comes from a small, trusted proof-checking kernel that validates every proof, ensuring a high degree of correctness. Nethermind is using Lean 4 to construct EvmYul, an executable formal model of the EVM and its intermediate language, Yul. The goal is to build a provably correct EVM implementation using interactive theorem proving.

Blueprint and Documentation

For a more in-depth documentation of this project, please refer to the following:

• Blueprint of the project
• Project README.md
• Equivalence README.md