Verity completed formal verification of EIP-8282 for the Ethereum Foundation. It used AI-assisted Lean proofs to mathematically verify EVM bytecode, covering three key properties of builder staking deposit and exit contracts. It found three inconsistencies between the EIP document and code, which were revised.
吴说获悉，形式化验证团队 Verity 宣布，已为以太坊基金会完成 EIP-8282 的形式化验证，利用 AI 辅助 Lean 证明流程，直接对 EVM 字节码进行数学验证，并由 Lean 内核检查证明结果。此次验证涵盖区块构建者质押存入及退出合约的三项关键属性，包括请求提交、队列处理及费用与控制逻辑。验证过程中还发现 EIP 文档与实际代码存在三处不一致，随后进行了修订。EIP-8282 是以太坊 ePBS（EIP-7732）机制的配套提案，相关证明不涵盖共识层调度及 BLS 检查等环节。