用 Opus 5.5 + Lean 形式化验证 Agent SDK，几个 prompt 产出 16 个修 bug PR
julianweisser · x · 2026-09-23
开发者 Boris Cherny(引用推文)分享了一个亮眼工作流：用 Claude Opus 5.5 对 Claude Agent SDK 做基于 Lean 的形式化验证，仅几条简短 prompt 就产出 16 个修复各类 bug 与竞态条件的 PR；他还提到 TLA+ 也很有效，常把 Lean 与 TLA+ 组合来排查数据流、并发与状态管理问题，自己并不精通这两种语言但 Claude 写得很好。转发者评论称软件验证正迅速成为值得投入的方向，围绕它还有大量工具链空白可建。
所属事件:几句 prompt 让 Opus 用 Lean 验证 Agent SDK，修出 16 个 PR(7 条相关)→
「编程与Agent」频道最新
- 开发者用 Opus 5.5 做 Lean 形式化验证,几条提示修出 16 个 bug — jimmykoppel · 2026-09-23
- Rogo 创始人:记忆压缩是企业 agent 最未解的难题 — rohanpaul_ai · 2026-09-23
- 告别巨型 Prompt:Graph Engineering 用图结构编排 AI Agent 工作流 — Pavan_Belagatti · 2026-09-23
- 让编码 Agent 在 PR 里附上火焰图，性能回归一目了然 — DanielLockyer · 2026-09-23
- 开发者实测新模型 Sol 6 擅长目标导向任务,让其通宵跑任务 — gregmushen · 2026-09-23
- Theorem 团队:用 Lean 形式化验证 AI 沙箱,全自动验证距落地仅数月 — ctjlewis · 2026-09-23