Ethereum Advances Consensus Verification with Lean 4
The Ethereum research team is working on a project called 'Etheorem' to implement and mathematically verify consensus specifications for the Fulu, Gloas, and Heze upgrades using Lean 4. This initiative aims to minimize the risks associated with different interpretations of the same specifications by various clients.
Project Overview
Ethereum's research team is undertaking a significant project named 'Etheorem' that aims to implement and mathematically verify the consensus specifications for the Fulu, Gloas, and Heze upgrades using the Lean 4 proof assistant. This effort seeks to reduce the risk of chain splits that can occur when multiple clients interpret the same specifications differently.
Goals of Etheorem
The primary objective of Etheorem is to create a functional implementation of the Ethereum consensus specifications in Lean 4, moving beyond simple code testing to mathematically validate the core logic. The project has disclosed its progress through a post on the Ethereum Research Forum by the Ethereum Protocol Fellowship (EPF) and the Invisible Garden research team.
Technical Implementation
Etheorem has successfully implemented consensus specifications for the three upgrades. It can execute state transitions and fork choice logic, comparing its results with official Ethereum consensus test vectors. Key features of the upgrades include:
- Fulu: Specifications related to data availability sampling.
- Gloas: Elements concerning the execution payload auction structure (ePBS).
- Heze: Features aimed at resistance to censorship through inclusion list structures.
Verification Techniques
The project utilizes the SSZ (Simple Serialize) library, known as SizzLean, to validate critical properties necessary for consensus data serialization, deserialization, and Merkle tree computations. The verification checks if serialized data reverts to its original value, ensures that different values do not share the same encoding, and confirms that encoding sizes do not exceed predefined limits.
The initiative also focuses on reducing discrepancies between verified code and actual execution code by using the same specification definitions in both the verification and execution environments. However, it is important to note that this formal verification does not replace the entire Ethereum client ecosystem, and passing test vectors does not guarantee operational stability or readiness for formal release. The project plans to expand its scope of proof in the future.