用 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，几句 prompt 修出 16 个 PR(13 条相关)→
「编程与Agent」频道最新
- 把 Astra 思考调成 extra high,它开始过度工程化单元测试 — astralmatrix · 2026-09-24
- Antithesis 赞助,O'Reilly 免费放出工程团队 AI 规模化指南 — blaizedsouza · 2026-09-24
- Zilliz CTO:Agent 让企业数据层问题无处遁形 — No_Engineer_1224 · 2026-09-24
- $0.072/时的16GB云VM跑Android模拟器+Chrome,常驻Agent工作流新选择 — cem2ran · 2026-09-24
- 10 次重跑均到关键区域却无一复现发现：全自主 agent 脆弱性实录 — rohanpaul_ai · 2026-09-24
- 把 Jev 接进 Mythic：用大模型给红队命令的 OPSEC 强度打分 — dyn___ · 2026-09-24