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

By Simon Yoon

Canonical URL: https://www.tokenpost.com/news/technology/54570
Published: 2026-11-11T22:29:35.000Z
Updated: 2026-11-11T22:29:35.000Z
Section: Technology

> The review used AI-assisted Lean proofs to verify EVM bytecode and covered request submission, queue processing, fee and control logic.

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.


