Verity Finds Three Documentation-Code Mismatches in Ethereum EIP-8282

Verity completed formal verification for the Ethereum Foundation’s EIP-8282 builder staking deposit and exit contracts, finding three mismatches between the proposal’s documentation and its code.

The review used AI-assisted Lean proofs to verify EVM bytecode, with Lean’s kernel checking the proof results. It covered request submission, queue processing, and fee and control logic.

EIP-8282 is a companion proposal to EIP-7732, which describes Ethereum’s ePBS mechanism. The verification did not cover consensus-layer scheduling or BLS checks. The EIP was revised after the mismatches were found.