用 Opus 5.5 + Lean 形式化验证 Claude Agent SDK，几个 prompt 提出修复 16 个 bug 的 PR
spikedoanz · x · 2026-09-24
开发者 bcherny 用 Opus 5.5 配合 Lean 定理证明器，对 Claude Agent SDK 做形式化验证，短短几个 prompt 就产出 16 个 PR，修复了多种 bug 和竞态条件。
要点：
- 他还常配合 TLA+，用来排查数据流、并发与状态管理问题，有时两者结合使用
- 他自称对 Lean/TLA+ 都不熟，但 Claude 在两者上都表现出色
- 结论：形式化建模代码非常适合发现人工难以察觉的 bug
被引用的推文则在调侃这种验证的「薛定谔状态」：问 Claude 是否验证了程序，它说验证了，但它验证的可能只是它想象中一个更小、更听话的程序——最后程序果然有 bug。这既是梗，也点出了形式化验证依赖中模型「自我幻觉」的真实风险。
所属事件: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