用 Opus 5.5 + Lean 形式化验证 Claude Agent SDK,几个 prompt 修出 16 个 PR
_catwu · x · 2026-09-23
Boris Cherny(Anthropic)分享:用 Opus 5.5 对 Claude Agent SDK 做形式化验证,只用几个简短 prompt 就产出 16 个 PR,修复了多个 bug 和竞态条件。他还常配合 TLA+,两者结合用于排查数据流、并发与状态管理问题;自称并不精通这两门语言,但 Claude 写得很好。他认为形式化建模能发现人类很难察觉的 bug,并提问形式化验证会否成为编码(至少是找 bug)的未来。catwu 提示可在 Slack 中试用 Opus 5.5 与 Claude Tag。
所属事件:Opus 5.5+Lean 形式化验证 Agent SDK 修出 16 个 bug(19 条相关)→
「编程与Agent」频道最新
- 两人小公司用 46 个 AI Agent 运营：审批门禁、哈希锁文件与翻车复盘 — dkovl · 2026-11-12
- 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