According to CoinMeta, Wu said that the formal verification team Verity announced that they have completed the formal verification of EIP-8282 for the Ethereum Foundation. They utilized AI to assist in the proof process of Lean, directly performing mathematical verifications on the EVM bytecode, with the Lean kernel checking the results of these verifications. This verification covered three key aspects of the contract for block builders' staking and withdrawal, including request submission, queue processing, and fee and control logic. During the verification process, it was also discovered that there were three inconsistencies between the EIP documentation and the actual code, which were subsequently revised. EIP-8282 is a supporting proposal for Ethereum's EPBS ( EIP-7732 ) mechanism, and the related proofs do not cover consensus layer scheduling and BLS checks, among other aspects.