EIP-8282 adds two small contracts, one for builder deposits and one for builder exits. This report audits the bytecode intended for deployment through formal methods.
We spent most of our effort deciding exactly what to prove. We wanted guarantees that were simple to read and captured the contracts’ intended behaviour. We then built the proofs with substantial AI assistance and used the Lean kernel to check their correctness.
We started by reading EIP-8282 alongside its reference implementation in sys-asm. We wanted to understand how the two contracts accept paid requests, queue them, and pass the oldest requests to the consensus layer.
Result We agreed with Matt Garnett (EF) on the exact implementation to verify: sys-asm commit 83f9801 and the two predeploy addresses.sys-asm @ 83f9801
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 it sets the inhibitor, and inhibition is reversible. Felix Lange (EF) confirmed all three are intended and explained the upgrade path behind them.
Result A pull request to the EIP, reviewed by Nico Flaig.EIP PR #12120
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. Getting these statements right took longer than proving them.
Result Approved by Matt Garnett before any Lean was written. They are the three cards below.
We translated each English clause into a precise Lean statement about a completed call to the pinned bytecode. Each card shows that statement, explains its definitions, and links to the source we proved.
Result A script checks that the Lean text shown on this page is the text that was proved.Guarantee registry
We proved the guarantees directly on the runtime bytecode, with each proof checked by the Lean kernel. We then introduced six bytecode mutations to check that the guarantees caught those bugs, and proved supporting results around the remaining limits.
Result make check passed on the pinned source; six mutation refutations registered.Build receipt
Thomas Marchand and Benjamin Flores (LFG Labs). Matt Garnett (guarantees) and Felix Lange (intended behaviour), Ethereum Foundation. Nico Flaig (EIP text), ChainSafe. Authors: Cayman, Nico Flaig, Felix Lange and Justin Traglia.
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 its card. Failed calls leave the queue and counters unchanged.