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

AI 导读

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

正文 · AI 翻译

我用 Opus 5.5 通过 Lean 对 Claude Agent SDK 进行了形式化验证。几条简短的提示词就生成了 16 个 PR，修复了各种 bug 和竞态条件。视频见附件。

TLA+ 也很好用。我有时会把 Lean 和 TLA+ 结合起来，排查数据流、并发和状态管理方面的问题。

这两种语言我都不太熟，但 Claude 在这两种语言上都非常出色。这种方法对于对代码进行形式化建模、发现人类可能不会注意到的 bug 非常有用。

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

来源：bcherny · x.com