Boris Cherny 用 Opus 5.5 加 Lean 形式化验证，产出 16 个修 bug PR
AccBalanced · x · 2026-09-25
Claude Code 创作者 Boris Cherny 用 Opus 5.5 对 Claude Agent SDK 做形式化验证：几条简短 prompt 就产出 16 个修复真实 bug 与竞态条件的 PR，而他自己并不熟悉 Lean。
验证发现的实际 bug 包括：会话阶段中沙箱网络请求与权限提示可同时解决、导致会话永久等待；重试循环与 token 截断守卫互相冲突形成死循环；流式响应可能在消息中途结束却被记为成功，无报错也无成本记录。
他还表示 TLA+ 同样好用，有时会将 Lean 与 TLA+ 结合，一次性检查数据流、并发与状态管理。他认为这种「老技术遇上更快的作者」的方法对形式化建模代码、发现人工难以察觉的 bug 极为实用，并提问：形式化验证会是编程（或至少找 bug）的未来吗？
所属事件:Opus 5.5+Lean 形式化验证 Agent SDK 修出 16 个 bug(19 条相关)→
「编程与Agent」频道最新
- Plurai 发布 Agent 仿真测试插件:数字孪生让 Agent 先在虚拟世界翻车 — nikola_mr64990 · 2026-11-12
- Agent 说「Done」不等于真做完:Plurai 仿真核验实际行为 — nikola_mr64990 · 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