用 Opus 5.5 以 Lean 形式化验证 Claude Agent SDK,16 个 PR 修出竞态 Bug

blaizedsouza · x · 2026-09-23

开发者 bcherny 分享用 Opus 5.5 对 Claude Agent SDK 做形式化验证的经历:几条简短 prompt 就产出 16 个修复各类 Bug 和竞态条件的 PR。他表示自己并不精通 Lean 或 TLA+,但 Claude 对两者都很擅长,他有时会把 Lean 和 TLA+ 结合,用于检查数据流、并发与状态管理问题。

其核心主张是:形式化方法将成为 agentic coding 的基石,但有一条规则——agent 可以负责写证明,定理(规格)必须由人来陈述。这种「人定定理、AI 写证明」的流程能发现人类很难察觉的代码缺陷,适合对代码做形式化建模与找 Bug。