Opus 5.5+Lean 形式化验证 Agent SDK 修出 16 个 bug

09-23，Anthropic 开发者 Boris Cherny（bcherny，Claude Code 创作者）分享了一种用大模型做形式化验证的实操方法：用 Claude Opus 5.5 对 Claude Agent SDK 进行 Lean 形式化建模，仅凭几条简短 prompt 就产出 16 个修复 bug 与竞态条件（race condition）的 PR。他本人并不精通 Lean 或 TLA+，验证工作主要由模型完成，说明形式化验证的门槛可能正被大模型显著降低。

已确认

• bcherny 于 09-23 分享该工作，@catwu、@andreisavu、@doodlestein、@TIME、@dyn 等独立帖子以及 @JiaweiLiu、@spikedoanz、@LingmingZhang、@HamelHusain、@julianweisser、@hargup13、@jimmykoppel、@shyamalanadkat、@blaizedsouza、@jfiance、@AccBalanced 的转发转述一致内容，部分附演示视频。
• 用 Opus 5.5 + Lean 对 Claude Agent SDK 建模，几条简短 prompt 产出 16 个修 bug PR，涉及多个 bug 与竞态条件；他展示了完整工作流：先让模型写规范建模、再验证找 bug、进而生成修复。
• 他表示 TLA+ 同样好用，常把两者结合用于检查数据流等。
• 他随后让 Opus 把这套形式化验证工作流制作成一张信息图，直观展示用大模型辅助形式化建模找 bug 的流程。
• @doodlestein（Jeffrey Emanuel）将其概括为一种形式化验证驱动的 agent 调试工作流。

为什么重要

• 形式化验证传统上需要 Lean、TLA+ 等证明语言的深厚功底，此前主要见于分布式系统与关键软件领域；如果不懂 Lean 的开发者也能借大模型完成这一流程，可能显著扩展形式化方法的适用范围。
• 该方法直接作用于 Anthropic 自家的 Agent SDK 并实际修出 bug，是「LLM 辅助形式化验证」从理论走向工程实践的直观案例。

2026-09-23 ~ 2026-09-25 · 19 条相关

• 用 Opus 5.5 + Lean 形式化验证 Claude Agent SDK，产出 16 个修 bug PR — TIME · 2026-09-23
• 【源头】几句 prompt 让 Opus 用 Lean 形式化验证 Agent SDK,产出 16 个修 bug PR — bcherny · 2026-09-23
• 【源头】Opus 顺手把 Lean 验证 Agent SDK 的过程做成了信息图 — bcherny · 2026-09-23
• Opus 5.5做Lean形式化验证：几句prompt修出16个bug修复PR — HamelHusain · 2026-09-23

另有 15 条近重复转述:hargup13 · andreisavu · _catwu · julianweisser · jimmykoppel · doodlestein · shyamalanadkat · blaizedsouza · JiaweiLiu_ · dyn___ · spikedoanz · bcherny · LingmingZhang · jfiance · AccBalanced