Opus 5.5做Lean形式化验证：几句prompt修出16个bug修复PR

HamelHusain · x · 2026-09-23

Claude 团队的 bcherny 用 Opus 5.5 对 Claude Agent SDK 做 Lean 形式化验证，几段简短 prompt 就产出 16 个修复 bug 和竞态条件的 PR。他也用 TLA+，有时两者结合检查数据流、并发与状态管理问题；自称对两门语言都不熟，但 Claude 对两者都很擅长。

Hamel Husain 转发了 shreya 的评论：这种「让 agent 形式化验证并修 bug」的做法正成为新的「让 LLM judge 修 LLM 输出」——难点在于让形式化描述对人和 agent 都「正确」（可解释、可表达、可扩展），软件开发方式正迎来新一轮学习期。