Boris Cherny：我使用 Opus 5.5 通过 Lean 形式化验证了 Claude Agent SDK
我使用 Opus 5.5 通过 Lean 形式化验证了 Claude Agent SDK。几个简短的提示 = 16 个 PR 修复了各种 bug 和竞态条件。视频附上。
TLA+ 也效果很好。我有时会结合 Lean 和 TLA+ 来查找数据流、并发和状态管理方面的问题。
我对这两种语言都不太熟悉，但 Claude 在两者上都表现出色。这种方法对于形式化建模你的代码并发现人类可能不会注意到的 bug 非常有用。
形式化验证是编程的未来（或者至少是 bug 发现的未来）吗？
Opus 制作了一张信息图
给研究形式化方法的人补充一些细节——Claude 实际上做的事情大致是：
- 为程序建立模型，针对复杂的状态机或容易出现竞态条件的代码部分。
- 在模型中寻找反例。这些是疑似缺陷。
- 复现这些缺陷。
- 修复代码中的缺陷。
并不是整个代码库都经过了形式化验证（至少目前还没有！……），而是对最棘手的代码部分建模、查找反例，然后进行修复。
对照原文
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)?
Opus made an infographic https://t.co/w9fMWqB7HA
More details for the formal methods people -- what's happening is Claude is doing something like: 1. Building a model of the program, targeting a tricky state machine or race-prone part of the code 2. Finding counter-examples in the model. These are suspected bugs 3. Reproducing the bugs 4. Fixing the bugs in the code It's not that the whole codebase is formally verified (yet!..), more that the hairiest parts of the code are modeled, checked for counter-examples, and fixed.