Opus 5.5 用 Lean 形式化验证 Agent SDK：几句 prompt 修出 16 个 bug
hargup13 · x · 2026-09-23
- 有开发者用 Claude Opus 5.5 对 Claude Agent SDK 做形式化验证：几句简短 prompt 生成了 16 个 PR，修复了各类 bug 和竞态条件。
- 他完全不懂 Lean 这门语言，但 Claude 两种语言都写得很熟练；TLA+ 同样好用，他有时把 Lean 和 TLA+ 组合使用，分别排查数据流、并发与状态管理问题。
- 方法价值：形式化建模代码能发现人类很难发现的 bug，作者认为这可能是编程（至少是找 bug）的未来；转发者更断言形式化验证是软件开发的近期方向，并预告一个能让 Lean 跑在更多场景的项目。
所属事件:Opus 5.5+Lean 形式化验证 Agent SDK 修出 16 个 bug(19 条相关)→
「编程与Agent」频道最新
- Plurai 发布 Agent 仿真测试插件:数字孪生让 Agent 先在虚拟世界翻车 — nikola_mr64990 · 2026-11-12
- Agent 说「Done」不等于真做完:Plurai 仿真核验实际行为 — nikola_mr64990 · 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