The EIP-7002 contract.

The protocol’s own code

What the contract does.

A user submits a 56-byte request — a validator’s public key and an amount — with a fee, and the contract queues it, with the caller, at raw storage offsets. At the end of every block the client calls the contract from the reserved system address 0xffff…fffe; the contract removes up to sixteen requests from the head of the queue, returns them as the block’s withdrawal requests, which the block header commits to, and updates an excess counter that sets the next fee through fake_exponential(1, excess, 17). A fault here could drop, duplicate or reorder exits, or invalidate blocks.

With no compiler, no ABI and no selector dispatch, the contract also tests whether the method depends on a compiler’s conventions. It needed no extension of the certificate checker. The model the bytes are proved to refine is transcribed from the EIP’s text and pseudocode, not read off the bytes. Its initial state is what deployment leaves: the excess set to an inhibitor, 2²⁵⁶ − 1, that blocks submissions until the first system call, and an empty queue.

Totality

A system call that cannot fail.

Whatever the contract’s storage holds, as long as its canonical code is installed, the client’s end-of-block call succeeds without error, at an exact, state-dependent cost that never exceeds 210,000 gas — against the 30,000,000 the protocol supplies. The statement has two hypotheses: a covered fork, and the code.

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).error = none ∧
    (systemProtocolOutput benv).gasLeft = systemTransactionGas - systemProtocolGas benv ∧
    systemProtocolGas benv ≤ 210000 ∧
    (systemProtocolOutput benv).returnData = (systemProtocolPost benv).output ∧
    (systemProtocolOutput benv).refundCounter = (systemProtocolPost benv).refundCounter

Its history form, history_checked_system_totality, needs only that the canonical code is installed at a checkpoint: after any configured history from there, the call still succeeds. No history removes the code, and nothing a history does to this contract’s storage can make its end-of-block call fail and the block invalid — in Jaune’s semantics.

FIFO from deployment

Submissions in, requests out.

After canonical deployment, every committed submission is, in order, either a withdrawal record published by the blocks or an entry still in the contract’s final queue. The statement reads directly:

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

These lists are concrete observations. submissions reads committed calls, including calls inside transactions and excluding reverted effects. emissions reads the actual type-1 block requests. remainingQueue reads the live entries between the head and tail in final contract storage. All three use records containing the caller, public key and amount, so equality preserves every field, order and multiplicity.

theorem history_fifo
    {cfg : ChainConfig} {checkpoint final : BlockChain}
    (deployment : DeploymentHistory cfg checkpoint)
    (admission : deployment.Admission)
    (history : ConfiguredHistoryTrace cfg checkpoint final)
    (otherInstalled : OtherSystemCodeInstalled checkpoint.state)
    (senders : history.NoSenderAt systemAddress)
    (authorities : history.NoAuthorityAt systemAddress)
    (avoid : ∀ root ∈ history.rawFrames,
      root.sevm.codeAddress = none → root.sevm.currentTarget ≠ systemAddress)
    (occurrences : (submissions history).length ≤ wordOccurrenceCap) :
    HistoryFifo history

deployment identifies the actual committed canonical creation transaction and the same chain’s preactivation prefix. Its admitted Cancun execution establishes the initial storage and runtime code; these are proved consequences, not separate starting-state assumptions. The subsequent history covers Prague, Osaka, BPO1 and BPO2, including an empty history.

The remaining premises are explicit. The other three system contracts must have their canonical code at the modern checkpoint. Transactions and authorizations exclude the system address, no entered creation targets it, and its code is empty at the post-deployment boundary. The Cancun prefix also requires canonical beacon code at later block openings. The modern history contains at most 2²⁵⁴ committed submissions. There is no hash premise or per-frame entry condition, and the theorem does not authenticate historical block inclusion.

A companion bounds delivery: an entry at position q when a block’s requests are computed is emitted exactly ⌊q/16⌋ blocks later, counting that block as zero, in every admitted extension that long. Nothing submitted later overtakes it (block_word_delivery_from_deployment). The runtime emits at most sixteen entries per block and uses the fee its word arithmetic computes.

Statements that can fail

The system-address premise is not decorative.

A closed theorem builds a two-block history from an independently supplied checkpoint that places, at the system address, a contract that calls the queue from inside a user transaction and drains it before the block’s own system call — and FIFO fails (systemEmpty_loadBearing_witness). This witness does not supply the canonical deployment required by the headline. As far as we know, putting code at that address would take a signature by its key or a 160-bit Keccak preimage, but Blanc does not prove this, and the premise stays.

Refinement and liveness

Every successful frame, classified.

A successful frame at this code is exactly one of three things, with exact storage, logs and return bytes: the system call’s dequeue; a submission — not static, from a caller other than the system address, with 56 bytes of input and a value covering the fee the bytecode computes; or a fee read. While the excess holds the inhibitor, no user call succeeds. Which failure a rejected call meets is not stated (exec_frame_effect). The contract’s balance never decreases, and the committed submissions add exactly their values to it (history_balance_nondecreasing).

After any history that leaves the contract active, a submission paying at least the EIP’s fee and started with more than the 2,300-gas stipend beyond its cost executes at exactly 1,258 + 87·k gas plus its storage accesses, where k counts the iterations of the fee loop; a fee read costs 180 + 87·k plus one read (history_submission_nat_live).

Specification against bytes

The fee the bytes compute.

The EIP specifies its fee as Python pseudocode over unbounded integers. The bytecode computes the same series in 256-bit words, whose intermediate products can overflow. Two pre-deployment audits noted that its fee therefore departs from the EIP’s once the excess passes 2,892: one judged such an excess unreachable under current settings; the other, noting that a higher block gas limit might bring it within reach, rated the finding informational. Blanc states the agreement exactly.

theorem word_fee_le_nat {excess : B256} {iterations : Nat} {output : B256}
    (run : WordFakeExponential.Run excess 17 1 17 0 iterations output)
    (model : Blanc.WithdrawalRequest.State) (excessEq : model.excess = excess.toNat) :
    (output / (17 : B256)).toNat ≤ Blanc.WithdrawalRequest.fee model

theorem word_fee_eq_iff_natFeeDomain {excess : B256} {iterations : Nat}
    {output : B256}
    (run : WordFakeExponential.Run excess 17 1 17 0 iterations output)
    (model : Blanc.WithdrawalRequest.State) (excessEq : model.excess = excess.toNat) :
    (output / (17 : B256)).toNat = Blanc.WithdrawalRequest.fee model ↔
      NatFeeDomain excess iterations

The bytecode’s fee never exceeds the EIP’s, and equals it exactly when no intermediate value of the series wraps. Then a closed theorem builds a three-block configured history from an independently supplied checkpoint, in which a submission is committed after paying 2²⁴⁵ wei: at least the fee the bytecode computes at an excess of 2,893, about 3.2·10⁷³ wei, but less than the EIP’s, about 8.1·10⁷³ wei (nat_fee_guarantee_refuted). This refutes that fee guarantee for the checkpoint model; it does not provide a canonical deployment witness or a mainnet exploit. FIFO uses the fee the bytecode computes.

The divergence begins only where the EIP’s own fee is out of any account’s reach. By direct computation, outside the proofs, the two fees agree at every excess below 2,893, and at 2,892 the fee is already about 7.6·10⁷³ wei, more than 10⁴⁷ times all the ether in existence. The wrapped arithmetic does yield a fee of 1 wei near an excess of 2²⁵², but every model state a history reaches from deployment has its effective excess plus its count bounded by the number of submissions, so that excess would take about 2²⁵² of them. The counterexample reaches its excess with 2,895 submissions in one block, on a synthetic Prague chain whose block gas limit, 2²⁹, is about nine times mainnet’s; the retained mainnet scan through block 26,141,229 recorded a peak excess of 666, on 19 December 2025.

The seventh question

Mainnet, when Prague began.

The contract was deployed before Prague, but its use began only when Prague activated, so all of it lies in forks Jaune covers. At block 22,431,083, the last before Prague, three providers report that its storage held exactly the model’s initial state — the inhibitor in the excess slot, zeros in the count, head and tail — with the same storage root it had at deployment, 549,694 blocks earlier; that it had logged no request; that the four system contracts held their canonical code; and that the system address held none.

These observations support the connection to mainnet, but do not authenticate its history inside Lean. The current FIFO headline instead derives the initial storage and runtime from canonical Cancun deployment and its admitted prefix. Applying it to mainnet still relies on the historical execution being a configured one in Jaune and on the stated environmental conditions. The constructor result establishes the runtime and initial storage without a hash premise (deploy_initial).

Stated, so it is not inferred

Not claimed.

• How the consensus layer processes the requests, including whether the caller is entitled to act on the validator it names.
• Whether the fee parameters are economically sound.
• That the chain produces the later blocks the delivery bound speaks of; distance is counted in configured blocks.
• Which failure a rejected call meets, or its gas.
• Storage growth: dequeued slots are left in storage, and nothing is proved about them.
• Transaction-level liveness; anything beyond 2²⁵⁴ committed submissions.

The claim map’s EIP-7002 section lists every theorem with its premises, file and line.

Context

Earlier work.

Before deployment, four audits commissioned by the Ethereum Foundation examined the Pectra system contracts, and a loop-bounded Halmos check compared this contract’s bytecode with references written from the EIP’s pseudocode. We know of no earlier proof about this contract that is unbounded in the excess and in the history, or that follows a request from its submission to the block that emits it.