Verity’s formal review of the Ethereum Foundation’s builder staking deposit and exit contracts identified three gaps between EIP-8282’s text and code, and the proposal was revised afterward.
The review examined Ethereum Virtual Machine (EVM) bytecode related to request submission, queue operations, and fee and control logic. AI tools helped produce proofs in Lean, and Lean’s kernel checked the results.
EIP-8282 is a companion proposal to EIP-7732, which sets out Ethereum’s ePBS mechanism. The review did not extend to consensus-layer scheduling or BLS checks.
