以太坊研究员用 Lean 形式化验证 FCR，并发现 Gloas 规范漏洞

以太坊基金会研究员 fradamt 介绍其形式化验证工作：以太坊快速确认规则（FCR）已在 Lean 中获得安全性证明，模型贴近共识规范，证明在 FCR 假设下已确认区块保持规范链。作者称大部分验证工作仅用 4-5 天，且智能体基本在无人监督下完成；随后将模型适配到即将到来的 Gloas 变更时，发现分叉选择改动引入的一处规范层面的细微漏洞，该漏洞已修复，修正后协议的形式化验证通过。作者认为形式化模型可让以太坊在加快升级、收紧分叉时间线的同时继续提高安全门槛。