用 Opus 形式化验证 Claude Agent SDK:数条提示产出 16 个修 bug PR
jfiance · x · 2026-09-24
工程师 Boris Cherny 分享用 Opus 5.5 对 Claude Agent SDK 做形式化验证的经验:只用几条简短提示,就让模型用 Lean 写出规范并产出 16 个修复 bug 与竞态条件的 PR。他还表示 TLA+ 同样好用,有时会把 Lean 和 TLA+ 结合使用,分别排查数据流、并发与状态管理方面的问题。
要点:
- 作者并不精通 Lean 或 TLA+,但 Claude 对两者都很擅长,降低形式化验证门槛
- 这种方法能发现人工很难察觉的 bug,适合对代码做形式建模
- 转发者 @sushant94 评价这是「形式化验证已成为工程师实用工具」迄今最清晰的案例,称其团队已在生产引擎上运行这套循环
- 作者发问:形式化验证会成为编码(至少是找 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