用 Opus 5.5 与 Lean 形式化验证 Claude Agent SDK
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.
Boris Cherny 用 Opus 5.5 结合 Lean 对 Claude Agent SDK 做形式化验证，几个简短提示词就产出 16 个 PR，修复了多个 bug 和竞态条件。他还常把 Lean 与 TLA+ 结合，排查数据流、并发和状态管理问题。他表示自己并不熟悉这两种语言，但 Claude 很擅长，这种方法能发现人难以察觉的 bug。
正文
当前显示原文，中文全文译文尚未就绪。
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)?