Verity 为以太坊完成 EIP-8282 形式化验证，发现 3 处文档与代码不一致

吴说获悉，形式化验证团队 Verity 宣布，已为以太坊基金会完成 EIP-8282 的形式化验证，利用 AI 辅助 Lean 证明流程，直接对 EVM 字节码进行数学验证，并由 Lean 内核检查证明结果。此次验证涵盖区块构建者质押存入及退出合约的三项关键属性，包括请求提交、队列处理及费用与控制逻辑。验证过程中还发现 EIP 文档与实际代码存在三处不一致，随后进行了修订。EIP-8282 是以太坊 ePBS（EIP-7732）机制的配套提案，相关证明不涵盖共识层调度及 BLS 检查等环节。