Formalizing FOCIL in Lean 4

AI 摘要

一句话摘要: 通过Lean 4形式化验证，确认FOCIL机制在以太坊标准假设下能实现“1-of-N诚实”抗审查性。 关键事实: 1. FOCIL（EIP-7805）的抗审查核心是：只要IL委员会中有一名非共谋诚实成员列出交易，即可强制其纳入规范区块。 2. 形式化证明从以太坊>2/3诚实验证者假设出发，推导出端到端安全定理，且未使用Classical.choice等公理。 3. 验证过程揭示了规范中三个值得讨论的细节问题（原文未具体展开）。 涉及主体: 以太坊（Ethereum）、FOCIL项目、作者rahulbarmann、EIP-7805。 可能影响: 为FOCIL在Hegotá升级中的部署提供数学严谨性背书，增强社区对以太坊抗审查能力的信心；形式化验证方法可能成为未来EIP安全审计的参考范式。 是否值得继续跟踪: 是。FOCIL是以太坊路线图关键升级，形式化验证结果直接影响其落地可行性，且作者计划后续扩展至活性证明和激励分析。 噪音/炒作风险: 低。该分析基于严格的形式化验证（Lean 4代码已开源），结论有数学证明支撑，非主观推测或营销内容。