用 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(18 条相关)→
「编程与Agent」频道最新
- Opus 5.5 纯代码搞定 Blender 建模绑定，作者封装成首个开发 skill — TAbrodi · 2026-09-24
- 一条 prompt 让 agent 自己核算账单：价格涨还是用量涨？ — gethackteam · 2026-09-24
- Opus 5.5 单条 prompt 一次生成 C/C++ 版 90 年代 demoscene 演示 — dreamwieber · 2026-09-24
- 用 Sonnet 3.7 起步、Opus 5.5 重构：AI 生成 Rummy 500 游戏免费上线 — AIandDesign · 2026-09-24
- Garry Tan:创业公司获客正被 agent 双向重塑 — garrytan · 2026-09-24
- Pattern MCP 让 AI Agent 按设计规范选组件而非重复造轮子 — DonR954 · 2026-09-24