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