以太坊研究员推进 Etheorem 项目，用数学形式化证明解决多客户端共识分歧风险

BiRun 讯，据 Ethresearch 论坛贴文，来自 Ethereum Protocol Fellowship（EPF）与 Invisible Garden 的研究团队公布了 Etheorem 项目最新进展。该项目旨在通过定理证明语言 Lean 4 构建一套完全可执行的以太坊共识规范，利用严格的数学形式化验证替代传统的代码测试，从根源上排查逻辑漏洞，以避免多客户端在实现规范时因理解偏差而引发链分叉事故。目前该规范已通过 Fulu、Gloas（包含 ePBS 机制）及 Heze 三个未来硬分叉版本的全部测试向量，涵盖状态转换与分叉选择等核心环节。所有逻辑均由 Lean 内核独立进行数学验证，正在为以太坊未来的复杂升级建立高安全标准的底层验证框架。