开发者用 Claude Opus 5.5 以 Lean 形式化验证 Agent SDK，产出 16 个修 bug PR
bcherny · x · 2026-09-24
工程师 bcherny 分享用 Claude Opus 5.5 对 Claude Agent SDK 做形式化验证的完整方法：只需几条简短 prompt，就产出了 16 个修复 bug 与竞态条件的 PR。他的具体工作流是：
- 让 Claude 为程序建模，瞄准状态机复杂或易出竞态的代码部分；
- 在模型中寻找反例，即疑似 bug；
- 复现这些 bug；
- 在代码中修复。
他强调这不是把整个代码库形式化验证（至少目前不是），而是只对最棘手的部分建模、查反例、修复。他还提到 TLA+ 同样好用，有时会把 Lean 和 TLA+ 结合使用，覆盖数据流、并发与状态管理的问题；并表示自己并不精通这两门语言，但 Claude 在两者上都表现出色，这种方法对形式化建模非常实用。
所属事件:Opus 5.5+Lean 形式化验证 Agent SDK 修出 16 个 bug(19 条相关)→
「编程与Agent」频道最新
- 两人小公司用 46 个 AI Agent 运营：审批门禁、哈希锁文件与翻车复盘 — dkovl · 2026-11-12
- LlamaIndex 让 AI Agent 渗透测试自家 LlamaParse，四天暴露四条经验 — llama_index · 2026-11-12
- Manhattan 字体 v0.0.1：每个字母都是一个 Python 函数 — allanyu_ · 2026-11-12
- 用 Backplane「提示词造出」任意扩展卡,网友呼吁扩展口回归标配 — _Stocko_ · 2026-11-12
- Agent 会话跑了 51 分钟烧 24.8 万 token,网友直呼还在干活 — _Stocko_ · 2026-11-12
- 可视化 AI Agent 团队协作：每个 Agent 一间「房间」，共享知识库 — LiorAloni11 · 2026-11-12