Verity完成以太坊EIP-8282形式化验证并发现3处文档与代码不一致
RecodeX 重构消息，形式化验证团队 Verity 宣布，已为以太坊基金会完成 EIP-8282 的形式化验证。该工作借助 AI 辅助的 Lean 证明流程，直接对 EVM 字节码进行数学验证，并由 Lean 内核检查证明。验证过程中发现 3 处文档与代码不一致之处。
事件追踪 · 持续发展中
EIP-8282形式验证
持续追踪EIP-8282形式验证相关报道与进展。
关注仅保存在当前浏览器和域名中，无需登录，不会自动跨设备同步。事件时间线
按最新发布排序以太坊基金会与Verity完成EIP-8282字节码形式验证，发现构建者合约不一致
RecodeX 重构消息，以太坊基金会与Verity对EIP-8282中构建者存款与退出合约的执行字节码进行了形式验证，确认了三项行为保证，同时发现研究团队需要解决的不一致之处。Verity在公开研究说明中介绍了这一对EIP-8282构建者存款与退出合约属性进行机器化核验的案例。形式验证指以数学方法确认代码是否满足既定条件。此次验证于2026年9月完成，覆盖用户提交调用与协议SYSTEM调用两条执行路径。