用 Claude 形式化验证 Agent SDK:几条 prompt 产出 16 个修复 PR
JiaweiLiu_ · x · 2026-09-24
Anthropic 工程师 Boris Cherny 分享:他用 Opus 5.5 配合 Lean 对 Claude Agent SDK 做形式化验证,几条简短 prompt 就产出 16 个 PR,修复了多个 bug 和竞态条件。他有时也会结合 TLA+,用于排查数据流、并发与状态管理问题——并表示自己两种语言都不熟,但 Claude 都写得很好。
相关生态工作(TLA+ 社区与 Specula 团队):
- Specula:用 TLA+ 对系统代码建模,配合模型检查器找出数百个深层 bug 的 agentic 工具(GitHub 480 star)
- TLAPS-Bench:为重要系统/协议的 TLA+ 规约提供机器证明服务,已证明 2PC、Paxos、TCP 等经典协议
- 团队发现前沿 AI 写证明太强,不得不下架所有 proof-completion 任务;但从零证明真实系统代码的底层规约仍然很难
所属事件: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