用 Opus 5.5 形式化验证 Agent SDK：几条 prompt 修出 16 个 PR

LingmingZhang · x · 2026-09-24

开发者 Boris Cherny 用 Claude Opus 5.5 配合 Lean 对 Claude Agent SDK 做形式化验证，仅用几条简短 prompt 就产出 16 个修复各类 bug 和竞态条件的 PR；他还常把 Lean 与 TLA+ 结合，用来发现数据流、并发与状态管理中的隐患。他自认对两种语言都不熟，但模型表现出色，认为这是发现人类难以察觉的 bug 的实用方法。

形式化验证研究者 Grigore Rosu 转发并提出更大胆的展望：形式化验证将回归其本来的定位——达成目的的手段。他描绘了「Intent Computing」的三步图景：AI 从人类意图同时生成代码、规格与证明；规格以自然语言反馈给人类审批，人类不再直接接触代码；引擎产出可独立校验的证明，保证产物与意图一致。一句话：AI 是新的计算机，意图是新的编程语言。