Wu has learned that Verity, the formal verification team, has announced the completion of formal verification for EIP-8282 for the Ethereum Foundation. Utilizing AI-assisted Lean proof processes, the team directly performs mathematical verification on the EVM bytecode, with the Lean kernel checking the proof results. This verification covers three key attributes of block builder staking and contract exit: request submission, queue processing, and fee and control logic. During the verification process, three inconsistencies were found between the EIP documentation and the actual code, which were subsequently revised. EIP-8282 is a supporting proposal for the Ethereum ePBS (EIP-7732) mechanism, and its proofs do not cover consensus layer scheduling and BLS checks. [https://www.(wublock123.com)/news/verity-formal-verification-eip-8282-ethereum-doc-code-mismatch-71725](https://www.wublock123.com)/news/verity-formal-verification-eip-8282-ethereum-doc-code-mismatch-71725)