RecodeX 重构消息，形式化验证团队 Verity 宣布，已为以太坊基金会完成 EIP-8282 的形式化验证。该工作借助 AI 辅助的 Lean 证明流程，直接对 EVM 字节码进行数学验证，并由 Lean 内核检查证明。验证过程中发现 3 处文档与代码不一致之处。