Case study
Formal Verification for Ethereum's EIP-8282
A formal verification engagement for the Ethereum Foundation's EIP-8282 builder deposit and builder exit predeploys. We proved three guarantees directly against the pinned EVM bytecode at sys-asm@83f9801. The interactive report contains the protocol map, proof boundary, and linked evidence.
- Client
- Ethereum Foundation
- Verified guarantees
- 3
- Date
- September 2026
Overview
Our approach
We first review the implementation to understand where the system can fail and what the protocol requires. Once those questions are settled, we apply formal verification: mathematically proving the pinned bytecode correct against its formal specification and stated assumptions, with no covered failure modes left.
About EIP-8282
What EIP-8282 changes
With ePBS (EIP-7732), block builders become their own staked role on Ethereum. EIP-8282 gives them two dedicated contracts: one to deposit stake and join, and one to exit.
Both contracts are built into the protocol at fixed addresses. They take paid requests from users, queue them, and pass them to the consensus layer at the end of each block, the same way validator withdrawals already work (EIP-7002).
Why formal verification
Why the Ethereum Foundation chose formal verification
A classic audit can find bugs and attack paths, but it cannot guarantee that none remain. Formal verification proves specified properties for every covered input under explicit assumptions.
That matters for EIP-8282: the builder deposit contract sits at the boundary between user requests, execution clients, and Ethereum's consensus layer. A bug in how it admits, records, or returns deposits could make protocol behaviour inconsistent. These compact, assembly-native predeploys are well suited to machine-checked proofs.
EIP-8282 has no Solidity source: its low-level sys-asm/geas implementation runs directly as EVM bytecode. The Ethereum Foundation therefore chose to verify the frozen bytecode itself, without adding compiler or decompiler assumptions. We used AI-assisted Lean workflows, with the Lean kernel checking the final proofs.
Methodology
How the bytecode was formally verified
We spent most of the effort deciding exactly what to prove. The guarantees had to be simple enough for reviewers to read while still capturing the contracts' intended behaviour. We then built the proofs with substantial AI assistance and used the Lean kernel to check their correctness.
- 01
Understand the EIP and its implementation
We read EIP-8282 alongside its reference implementation in sys-asm to understand how the two contracts accept paid requests, queue them, and pass the oldest requests to the consensus layer.
ResultWe agreed with the Ethereum Foundation on the exact implementation to verify: sys-asm commit 83f9801 and the two predeploy addresses.sys-asm @ 83f9801
- 02
Resolve the places where the EIP text and code differed
Three points in the published text did not match the bytecode: only the exit contract starts inhibited, a SYSTEM call with calldata still drains the queue before setting the inhibitor, and inhibition is reversible.
ResultThe Ethereum Foundation confirmed the intended behaviour, and the EIP text was updated in a reviewed pull request.EIP PR #12120
- 03
Write the guarantees in English first
We chose three guarantees: admission, drain and control. We wrote them in plain English so reviewers could judge whether we were proving the right things before any Lean was written.
ResultThe guarantees were approved by Matt Garnett at the Ethereum Foundation and became the three properties summarized below.
- 04
Translate the guarantees into reviewable Lean statements
Each English clause became a precise Lean statement about a completed call to the pinned bytecode. The proof report shows the statement, explains its definitions, and links to the source that was proved.
ResultA consistency check confirms that the Lean text displayed in the report is the text that was proved.Guarantee registry
- 05
Prove the bytecode meets the guarantees
We proved the guarantees directly on the runtime bytecode, with each proof checked by the Lean kernel. We also introduced six bytecode mutations to check that the guarantees caught representative bugs, and proved supporting results around the remaining limits.
Resultmake check passed on the pinned source, with six mutation refutations registered.Build receipt
Verification is only useful when people can inspect and discuss it. We made the report readable on purpose: English guarantees come first, each proof boundary is visible, and the source and build evidence are linked at the point where they matter. We chose an interactive web report instead of a PDF so reviewers can explore the protocol map, open each guarantee, and follow the evidence without wading through a wall of generated output.
Formal verification
Formal Verification Summary
These guarantees establish who can add or remove requests and how the contracts update their fees and counters. Each holds under the conditions listed in the report, and failed calls leave the queue and counters unchanged.
| Guarantee | Status | What it establishes |
|---|---|---|
| Submission admission | Proved | Only a well-formed, paid, non-inhibited user call can append exactly one authentic deposit or exit record and emit one matching log. |
| Queue consumption | Proved | A successful SYSTEM call returns the oldest records, up to the per-call cap, and removes exactly those records. User calls remove none. |
| Queue control and fees | Proved | The caller selects the user or SYSTEM path, fees and counters update as specified, and INHIBITOR disables user calls while keeping SYSTEM access available. |
The proof covers the pinned runtime, initialization, and stated execution assumptions. It does not claim that consensus-layer scheduling, request-list construction, BLS checks, or open activation and upgrade decisions are correct. The interactive report makes that boundary explicit.
Contact our team
We take 4 protocols per quarter. Formal verification demands deep focus. We'd rather verify fewer contracts well than many poorly.
Continue reading
Learn more
Open the EIP-8282 interactive report to explore the protocol map, guarantees, and proof boundary.
Read EIP-8282 and the proof repository.
Why this target was verified at the bytecode level.
What is a formal proof? A short introduction for non-specialists.