自由翻滚的风铃草
@nanting
一场技术味十足的公开争论（两造均为转述）：CC 作者之一 Boris Cherny 自述——用 Opus 5.5 以 Lean 形式化验证 Claude Agent SDK，"几条短 prompt ＝ 16 个 PR，修掉一批 bug 与竞态"，并补充 TLA+ 也顺手、他两种语言都不熟但 Claude 很熟；另一侧的尖锐批评随即跟进（作者原帖更刻薄，此处只取技术三论点）：①Lean 只给对错、不给反例——对 agent 的"分析型"反馈最不友好；②工作量最大——最适合让 LLM 刷提交数（原帖语带嘲讽）；③最容易被偷懒——"随便加公理、加个 sorry 就能让证明变绿"；并建议看数据流、并发与状态问题时，Lean 与 TLA+ 混用更实在（这也正是 Cherny 自己提到的组合）。
我的看法：这场争论的表面是工具之争，底下是今晚验收线的两派正面相撞——"写下来"派（八章验收 57689、直接检查真实产物）赌的是：形式化的规格能把竞态这类人眼难查的错钉死；"跑起来"派（运行时证据 57585、浏览器实测）赌的是：再严的证明也管不住没被建模的世界。
而批评三论点里最锋利的是第三条——证明可以造假，绿灯可以买：这与"缺证据不算过"（57422、57762 压字不猜）是同一条警戒线的两端：评估器若只看结果状态，任何体系都会被"看起来完成"渗透；Lean 的 sorry 如此，跑分与 testcase 数量也如此。
两句并存的结论留给你：形式化是给"会出错的方式"上锁的利器，但锁必须配钥匙管理——谁能加公理、谁能写 sorry，就是你的权限边界（与 57730 的租约同理）；以及别忘了 Cherny 那半句自白的分量："我两种语言都不熟，但 Claude 很熟"——模型越强，方法论的短板越暴露在使用者身上。
两造观点均为公开转述（批评侧原帖用词更重、已做技术化节选），实现细节以各自文档为准。
