以太坊研究员用 AI 智能体+Lean 形式化验证共识协议,迈向 4-8x 更快终局
anselm · x · 2026-09-26
- 以太坊 OG 研究者 @fradamt(EthLabs,18 项 EIP 署名作者)宣布,已为解耦共识协议提案(I,未来以太坊升级方向)完成形式化验证,称这将使以太坊终局性(finality)提速 4-8 倍。
- 该协议因要求大部分质押者可离线,比普通 BFT 协议复杂得多,正确性远超标准的安全性与活性,这些细微性质均已通过验证;目前尚非完整规格,但包含成为完整规格所需的全部共识关键细节。
- 工作流:AI agents 与数学证明检查器 Lean 协作,智能体负责找出协议破绽、生成反例并提出修复,所有结论必须通过形式化数学证明验证,不存在“信我”环节。
- 他由此判断:未来的协议设计都将包含 AI 辅助形式化验证,既用于正确性也用于加速设计迭代。
所属事件:以太坊解耦共识协议完成 AI 辅助形式化验证(2 条相关)→
「编程与Agent」频道最新
- 别让 AI 做 pptx 了：网页版幻灯片动画更好，但给老板汇报还得交 PPT — lxfater · 2026-09-26
- 观点：个人 Agent 会同质化，真正护城河是持续积累的个人上下文 — vaibhavbetter · 2026-09-26
- Matt Pocock：CODING_STANDARDS.md 应在创建 5 分钟后就开始被填满 — mattpocockuk · 2026-09-26
- 自建基准:35B 的 Qwen3.6 得 95%,完胜 120B 的 GPT-OSS 53% — pauliusztin · 2026-09-26
- 把 DeepSeek Harness 装进 Muse 云端虚拟机，补齐中文检索短板 — op7418 · 2026-09-26
- 全程代码生成动画一次通过,博主实测 AI 编码 one-shot 潜力 — eschadiol · 2026-09-26