Boris Cherny 用 Opus 5.5 结合 Lean 形式化验证 Claude Agent SDK
Anthropic 的 Boris Cherny 拿 Opus 5.5 写 Lean 验证 Claude Agent SDK，几条提示词修出 16 个 bug，并发代码排查可以抄这个思路。
Boris Cherny 使用 Opus 5.5 通过 Lean 语言对 Claude Agent SDK 做形式化验证，只用几条简短提示词就生成了 16 个修复 bug 和竞态条件的 PR。
他还表示 TLA+ 同样适用，有时会将 Lean 和 TLA+ 结合起来排查数据流、并发和状态管理问题。他自述并不精通这两种语言，但 Claude 能熟练使用，这种方式能发现人工难以察觉的 bug。
If you’re looking for ways to try Opus 5.5 and Claude Tag in Slack… Boris Cherny @bcherny I used Opus 5.5 to formally verify the Claude Agent SDK using Lean. A couple short prompts = 16 PRs fixing various bugs and race conditions. Video attached. TLA+ also works well. I sometimes combine Lean and TLA+ to look for issues around data flow, concurrency, and state mgmt. I don't know either language well, but Claude is excellent at both. This approach is super useful for formally modeling your code and finding bugs that a human probably wouldn't have spotted. Is formal verification the future of coding (or at least, bug finding)?
本条情报归属 AITOP「技巧」核心栏目，重点聚焦北美前沿实验室与硅谷科技巨头。在跨区域产业观察坐标中，该动态直接关联「AI 开发者工具链、Coding Agent 与工程化实践」研究主线，反映出当前技术演进与商业落地的最新风向。涉及核心实体与技术议题包括：Opus 5.5、Claude Agent SDK、Lean、TLA+，读者可通过下方标签进入对应专题页查阅历史脉络与关联对比。
信源核验说明：本文原始线索采编自「cat」（@_catwu），经 AITOP 多维评分管线结构化提炼。
