If this call ever fails, the block is invalid

Since the Prague upgrade, execution-layer requests for validator exits and partial withdrawals go through a 504-byte contract written by hand 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. A post on Ethereum Research reports two properties of the deployed bytes, proved in Lean 4.

The first is that 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. The theorem carries no premise about storage, and the gas cost is computed exactly from the state. A companion theorem shows that valid histories keep the canonical code installed.

The second concerns order. Requests leave in exactly the order they arrived: over any valid history since deployment, the committed submissions equal the emitted withdrawal requests followed by the entries still queued. Both results are stated against Jaune, an executable semantics of the EVM and of 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, propositional extensionality, choice and quotient soundness.

The contract was not unexamined before. It had been through four audits and a loop-bounded Halmos check before deployment. What the proof adds is reach: it ties the bytes actually deployed to the protocol's own block processing with exact gas, and follows requests from submission to delivery across every valid history rather than across the bounded runs a model checker explores. For a component whose failure invalidates the block, that is the difference between tested and proven.