以太坊基金会与形式化验证公司Verity合作，对管理区块构建者进入和退出机制的EIP-8282进行了数学检验。验证为提案的运行时字节码建立了三项已证明的保证，同时发现了一些需要研究人员处理的不一致之处。这项工作的意义，在于明确了哪些执行行为已有证明支撑，以及规范与实现之间还有哪些问题需要协调。
验证对象是构建者的进入与退出机制
EIP-8282创建于2026年5月22日，围绕区块构建者的生命周期设置专用合约，管理其存款与退出。区块构建者承担组装网络区块的工作，因此，进入和退出规则关系到这一参与者群体如何与协议交互。
Verity于2026年9月完成验证，重点检查运行时字节码的正确性。运行时字节码是实际在链上执行的低层代码。直接检验这一层，可以把讨论推进到代码真正执行时的行为，而不只停留在提案文字对机制的描述上。
这一范围也限定了结论：本次成果针对EIP-8282的特定执行行为，不能延伸为对以太坊整体安全性的保证，也不能据此认定提案已经部署。
三项保证覆盖两类调用，证明仍有边界
验证得出的三项保证，涉及用户提交的付费调用以及SYSTEM调用的相关场景。SYSTEM调用由协议自身发起，与普通用户发起的调用不同。对这两类路径分别检验，有助于确认不同调用来源下的代码行为是否符合被验证的要求。
但“三项保证”并不等于全部可能行为均已得到证明。形式化验证需要围绕明确的性质和条件展开，其结论适用于证明覆盖的范围。现有信息支持的判断是：相关调用路径中被证明的部分已有数学依据；对于这些性质之外的行为，不能直接套用同样的结论。
Verity还使用了六种字节码变异来检验所设性质。这类方法通常通过刻意修改代码，观察验证性质能否识别变化。它有助于检验这些性质对代码变化是否敏感，但六种变异本身不代表所有错误类型都被穷尽，也不能直接换算成某个安全覆盖率。
已证明的性质与发现的不一致可以同时存在
本次审查同时标出了需要以太坊研究人员处理的不一致之处。已证明的保证与这些问题并不矛盾：前者说明特定行为满足相应性质，后者提示仍有代码、规范或预期行为需要进一步对齐。
我们的判断是，这次验证最直接的价值是缩小后续讨论的范围。研究人员可以在已有证明的基础上，集中处理差异究竟来自实现、规范表述，还是对预期行为的理解。可能的处理路径包括修改代码、调整规范或澄清行为要求，但具体应采用哪一种，取决于对差异的进一步判断。
现有信息没有给出这些不一致的具体内容及严重程度，因此不足以把它们统一认定为可被利用的漏洞，也不足以认定其仅是文字问题。对开发者而言，关键是区分已经验证的性质与尚待解决的差异，避免把局部证明理解为整份提案已无争议。
后续重点是差异如何进入规范修订
EIP-8282的Last Call（最终征求意见）截止日为2026年11月1日，Verity在此前的9月完成验证。这一先后顺序意味着，验证发现具备在该轮征求意见结束前影响规范的时间条件，但不能据此认定相关问题已经解决，或最终规范已经按验证结果完成修改。
后续应观察研究人员如何回应每项差异、是否调整代码或规范，以及修订后的行为与已有证明之间能否保持一致。如果修改涉及原先证明所依赖的条件，还需要判断证明是否仍适用。相较于单看保证数量，问题的处置结果和证明适用范围，才更能体现这项工作对提案可靠性的实际贡献。
