[ethresear.ch] [Security] Lean verification of EIP-7002: system-call success and FIFO requests

Since Prague, execution-layer requests for validator exits and partial withdrawals go through a 504-byte contract at 0x00000961Ef480Eb55e80D19ad83579A64c007002, hand-written for the geas assembler. At the end of every block the protocol makes a system call to it, and that call is consensus-critical: EIP-7002 requires a block whose call fails to be invalidated.

We proved two properties of the deployed runtime bytes in Lean 4:

1. The system call always succeeds, whatever the contract’s storage holds, and uses at most 210,000 of the 30,000,000 gas it is given.
2. Requests leave in exactly the order they arrived. Over any valid history since the contract’s deployment, the committed submissions are exactly the emitted withdrawal requests followed by the entries still queued.

Both are stated against Jaune, an executable semantics of the EVM and block processing, also written in Lean, and cover the Prague, Osaka, BPO1 and BPO2 forks. The proofs use no axioms beyond Lean’s standard three: propext, Classical.choice and Quot.sound.

Before deployment, the contract had already been examined by four audits and a loop-bounded Halmos check. The results here connect the deployed bytes to Jaune’s block processing, with exact gas, and follow requests from submission to delivery across histories.

The system call succeeds

The statement is short enough to quote. It has no premise about storage:

theorem checked_system_totality {benv : Benv} (fork : CoveredFork benv.stat.fork)
    (installed : benv.state.getCode withdrawalRequestPredeployAddress = Blanc.withdrawalRequestCode) :
    processCheckedSystemTransaction benv withdrawalRequestPredeployAddress [] =
      .ok ((systemProtocolPost benv).state, systemProtocolOutput benv) ∧
    (systemProtocolOutput benv).gasLeft = systemTransactionGas - systemProtocolGas benv ∧
    systemProtocolGas benv ≤ 210000

Here processCheckedSystemTransaction is the checked system-call routine that Jaune’s block processing uses. It returns .ok only when the call ends without error; otherwise it rejects the block. So under a covered fork, with the canonical code installed, the call succeeds. Its gas cost systemProtocolGas benv is computed exactly from the state and never exceeds 210,000. (checked_system_totality)

A companion theorem shows that valid histories under the covered forks keep the canonical code installed. (history_canonical_code)

Requests are first in, first out

The FIFO theorem, history_fifo, concludes HistoryFifo history:

def HistoryFifo {cfg : ChainConfig} {checkpoint final : BlockChain}
    (history : ConfiguredHistoryTrace cfg checkpoint final) : Prop :=
  submissions history = emissions history ++ remainingQueue history

Each of the three lists is read directly off the execution history:

• submissions lists every committed submission call to the contract, including calls made from inside transactions, with its caller and calldata. A submission is committed if it succeeds and no enclosing call rolls it back.
• emissions lists the withdrawal requests (request type 1) that the blocks actually output, in block order and in order within each block.
• remainingQueue reads the live queue from the contract’s final storage, from the stored head pointer up to the stored tail.

All three produce records in the same 76-byte format (caller, public key, amount), so equality compares every field. Because the equation compares lists, it respects order and multiplicity: the same request submitted twice counts twice. And because it holds for every valid history, it holds after every block, starting from the empty history. So no committed submission is ever lost, duplicated, reordered, or emitted before it was submitted.

Two further results describe how the queue is served:

• Service rule. Each block emits the first min(16, queue length) entries, and every committed submission paid at least the fee the bytecode computes. (That fee is not always the EIP’s; see The fee below.) (block_word_fifo)
• Delivery bound. Suppose an entry is at zero-based position q in the queue when block B computes its requests. Then it is emitted exactly \lfloor q/16 \rfloor blocks after B (in B itself if q < 16), and later submissions cannot delay it. This holds in any extension of the history that runs that long and still meets the premises; it does not claim that the chain will produce those blocks. (block_word_delivery_from_deployment)

What the FIFO theorem assumes

Every history is valid under Jaune’s configured block processing. Each block also satisfies a balance bound: all execution-layer balances before the block, plus the block’s incoming consensus-layer withdrawal credits, sum to less than 2^{256} wei. There is no hash premise.

The remaining premises fall into three groups. Several concern the system address 0xfffffffffffffffffffffffffffffffffffffffe (0xff…fe below), which the protocol uses as the caller of its system calls.

• Deployment. The history begins with the contract’s own deployment: a Cancun block containing the canonical CREATE transaction, with the canonical creation code, zero value, enough gas and no address collision. The rest of that block, and every block until activation, runs Cancun. In that stretch none of the blocks’ transactions is sent from the system address (the protocol’s own system calls are not transactions, so they are unaffected) and no contract creation runs at it, even one that reverts. The system address has no code right after the deployment transaction, and each later block starts with the canonical EIP-4788 beacon-roots code already in place.
• After activation. Every block runs Prague, Osaka, BPO1 or BPO2 under the same valid chain configuration. At activation, the other three system contracts (EIP-2935, EIP-4788 and EIP-7251) hold their canonical code. Throughout, no block transaction is sent from the system address, no EIP-7702 authorization is signed by it, and no contract creation runs at it, even one that reverts.
• Capacity. There are at most 2^{254} committed submissions after activation. This bound only keeps counters and queue addresses from wrapping in 256-bit arithmetic during the proof; the contract enforces no such limit.

The contract’s starting state is not assumed. A deployment bridge proves it: at activation the contract holds its canonical runtime and its post-deployment storage (an empty queue; count, head and tail zero; and excess 2^{256}-1, the inhibitor value that blocks submissions until the first system call). It also proves that no submissions were committed before activation: Cancun makes no system call to the contract, so the excess stays at the inhibitor, and every call from any other caller reverts. The one starting fact it does not derive is that the system address has no code. Deployment cannot establish that, so it is assumed right after deployment and carried forward to activation.

That condition is not a formality. A machine-checked counterexample puts code at the system address; a user transaction triggers that code, which then calls EIP-7002. EIP-7002 recognises the system call only by its caller, so it treats this call as the system call and drains the queue before the block’s real one. The counterexample meets every other premise of the earlier form of the theorem, which started from an assumed post-deployment state rather than from deployment. So the condition cannot be dropped from that earlier theorem. The counterexample does not start from a canonical deployment, though, and it does not show that mainnet can reach such a state.

The theorem is about execution histories; it does not authenticate any mainnet transaction or state root. For the earlier form, the verification package of a related paper (see below) records what three RPC providers reported at block 22,431,083, the last before Prague: EIP-7002’s storage was still in its post-deployment state, with an empty queue and the excess at the inhibitor; each of the four system contracts (EIP-2935, EIP-4788, EIP-7002 and EIP-7251) held its canonical code; the system address held no code. These observations match the earlier form’s starting premises but are not authenticated state proofs. Applying either form to mainnet also depends on Jaune’s fidelity to Ethereum, which fixture tests support but these proofs do not establish.

The fee

The EIP specifies fake_exponential over unbounded integers. The bytecode computes it in 256-bit words, which can overflow. Two pre-deployment audits flagged this: Blackthorn L-8 and Sigma Prime PEC-03. We proved that the bytecode’s fee never exceeds the EIP’s, and that the two are equal exactly when no intermediate value of the calculation wraps.

The gap can be exercised. A machine-checked three-block history meets the premises of the earlier form of the FIFO theorem, yet commits a submission that paid less than the EIP’s fee. So a guarantee that every submission paid the EIP fee would be false, which is why the FIFO results refer to the fee the bytecode computes. This history, however, does not start from a canonical deployment, similar to the drain counterexample.

It is also far from mainnet. The witness runs a synthetic Prague chain and reaches an excess of 2,893 with 2,895 submissions in one block, whose gas limit is 2^{29}. Each pays only 1 wei, because a block’s fee is set by the excess left by the previous block, here zero; the excess then rises by the number of submissions above the target of two. The underpaying submission, in the next block, pays 2^{245} wei, about 5.65\times10^{55} ETH, from an initial allocation vastly larger than mainnet’s entire supply. It refutes the universal fee guarantee; it does not show that such an underpayment can happen on mainnet.

By direct computation, outside the proofs, the two fees agree at every excess up to 2,892. For scale, the related paper’s verification package records a mainnet excess of 666 on 19 December 2025. Sigma Prime noted that optimisations or a higher block gas limit might make the overflow threshold reachable. Reaching the threshold would not be enough, though: at excess 2,893 even the bytecode’s lower fee is about 3.2\times10^{55} ETH, so no real account could pay it.

What this does not say

• Nothing about Amsterdam or later forks. The results cover only blocks that run Cancun before activation and the four covered forks after it.
• Nothing about how the consensus layer processes the requests, including whether the caller is entitled to act on the validator or when a requested exit or withdrawal completes.
• Nothing about whether the fee parameters are economically sound, or about storage growth. Dequeued slots stay in storage.
• No transaction-level liveness theorem. There are frame-level ones: once the inhibitor is cleared, a submission from any caller other than the system address succeeds at an exact cost if it pays at least the EIP’s fee, carries 56 bytes of input, is not static, and has more than 2,300 gas beyond its cost. Fee equality is not required, since paying the EIP’s fee also covers the bytecode’s. This says nothing about whether the transaction is admitted or included.
• No corresponding totality or FIFO theorem for the EIP-7251 contract.

Evidence and artifacts

Every Lean result above is at one source revision: Blanc 7954405c, with Jaune ff22ec80, using Lean v4.35.0. Besides the theorems linked above, it contains the frame-level submission liveness theorem.

The pinned Jaune’s README reports its strict current-mainnet fixture lane over the execution-specs release [email protected]: all 4,968 files of its manifest pass, with no expected-failure allowance. That is a result for that source and fixture snapshot, not a claim about all Ethereum execution behavior.

The axiom audit walks dependencies from scratch. It does not rely on #print axioms, whose imported-inductive reporting bug affects the completeness of the report, though not kernel soundness. The audit bounds the axioms used, but it cannot show that the statements capture the intended protocol properties.

A related paper, arXiv:2610.19764v1, covers this contract (§4.5 and Appendix F.5) among eight deployed artifacts; this post covers only EIP-7002, because its failure invalidates a block. The paper is based on an older snapshot of the corpus: Blanc 5048a51f with Jaune 2737c8eb, using Lean v4.34.0. The FIFO theorem here is newer than the paper’s, which started from an assumed post-deployment state rather than from deployment. Its verification package, Zenodo DOI 10.5281/zenodo.23351349, records that snapshot’s checks, including a leanchecker replay and the mainnet observations cited above.

AI agents wrote the proofs and statements under my direction and helped draft this post. Corrections are welcome, especially on the definitions of the three lists in the FIFO equation, the assumptions and the connection to mainnet.

Questions

1. Is there a route to code or a transaction at the system address that the premises miss?
2. For future forks, which system contracts or properties would be most valuable to verify before their bytecode is finalized for deployment, and what evidence would client teams need to use those results?
3. For those following the client FV thread and the client TCB thread: Jaune is an executable EL semantics in Lean, with the fixture coverage above, and the results here carry over to mainnet only insofar as Jaune agrees with the clients. Where might it diverge from them, and which behaviours would you test first to find out?