开发者用 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 在两者上都表现出色，这种方法对形式化建模非常实用。
所属事件:Anthropic 开发者用 Opus 5.5 + Lean 形式化验证 Agent SDK，修出 16 个 bug(16 条相关)→
「编程与Agent」频道最新
- 不想用终端和贵订阅，求 GUI 友好的 Claude Code 替代品 — Dev-in-the-Bm · 2026-09-24
- 给 AI 群聊装上连体激发式记忆,结果它们自发成立了业委会 — liminal_bardo · 2026-09-24
- 开发者实测：不用 Jev API，本地 embedding 方案更快更私密 — allisonmaybe · 2026-09-24
- 让 Copilot CLI 与 Grok Build 开会共识,跨框架审阅新玩法 — DanWahlin · 2026-09-24
- Robinhood 已推 MCP 与托管智能体账户,Schwab 两项皆无 — MartinGTobias · 2026-09-24
- OpenRSI 招募贡献者:用你的研究出题考核前沿 Agent — ChengleiSi · 2026-09-24