英文原文

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 5.5，通过 Lean 对 Claude Agent SDK 进行了形式化验证。几个简短提示词就产生了 16 个 PR，修复了各种错误和竞态条件。附有视频。

TLA+ 也很有效。我有时会结合使用 Lean 和 TLA+，查找数据流、并发和状态管理方面的问题。

我对这两种语言都不熟悉，但 Claude 非常擅长二者。这种方法对于对代码进行形式化建模，以及发现人类可能注意不到的错误非常有用。

形式化验证会是编程（或者至少是查找错误）的未来吗？

线程续帖英文原文

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.

线程续帖中文翻译

给形式化方法从业者补充更多细节——实际发生的过程大致如下：

  1. 为程序建立模型，针对棘手的状态机或容易出现竞态的代码部分
  2. 在模型中查找反例。这些是疑似错误
  3. 复现这些错误
  4. 修复代码中的错误

并不是整个代码库都已经经过形式化验证（还没有！……），而是对最棘手的代码部分建模、检查反例并修复。