用 Claude 形式化验证 Agent SDK：几条 prompt 产出 16 个修 bug PR
shyamalanadkat · x · 2026-09-23
Meta 工程师 bcherny 分享用 Opus 5.5 + Lean 对 Claude Agent SDK 做形式化验证，几条简短 prompt 就生成 16 个修复 bug 和竞态条件的 PR，并附演示视频。他还提到 TLA+ 同样好用，且常把两者结合来排查数据流、并发和状态管理问题——自己并不精通这两门形式化语言，但模型很擅长。
转发者 xennygrimmato 由此提出观点：形式化验证是编程的未来，过去的瓶颈是人类手动用 Lean 之类语言精确表达意图太繁琐，而前沿模型让这个瓶颈消失了。
所属事件: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