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