用 Opus 5.5 和 Lean 形式化验证 Claude Agent SDK，产出 16 个修复 PR

AI 导读

bcherny 用 Opus 5.5 借助 Lean 对 Claude Agent SDK 做形式化验证，几条简短提示词换来 16 个修复各类 bug 和竞态条件的 PR。

正文 · 原文

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)?

来源：bcherny · x.com