一句话看懂：Claude Code 作者 Boris Cherny 用 Opus 5.5 配合 Lean 形式化验证 Claude Agent SDK，几段简短提示词就换来 16 个修复 bug 与竞态条件的 PR，他还常把 Lean 与 TLA+ 组合使用。这提供了一个新信号：形式化验证正从学术工具变成日常找 bug 的工程手段。
事件核心：发生了什么
Boris Cherny 在 X 上分享了一次实验：他用 Opus 5.5 对 Claude Agent SDK 做形式化验证，工具是 Lean，另配合 TLA+ 检查数据流、并发与状态管理相关问题。据其描述，整个过程只需几段简短提示词，最终产出 16 个合并请求（PR），修复内容包括各类 bug 和竞态条件，并附有视频记录。他坦言自己并不精通 Lean 和 TLA+ 这两门形式化语言，但 Claude 在两者上都表现良好。帖子发布于 2026 年 9 月 22 日，浏览量约 110 万次。
为什么重要
形式化验证长期被视作高门槛领域，需要专门人才和大量时间，通常只出现在航空、芯片、数据库等对正确性要求极高的场景。这次实验的关键点不在“AI 又写了代码”，而在于大模型开始承担形式化建模这一环：把并发、状态流转、数据流等抽象问题写成可机器证明的模型，再由求解器找出反例。若这条路走通，SDK、Agent 框架、分布式组件等复杂软件可能多出一条新的质量保障路径，与单元测试、模糊测试形成互补。目前公开信息显示，这仍是一次个人驱动的实践，尚不足以证明可大规模替代人工验证。
对用户/开发者/创作者的影响
对开发者而言，更现实的价值是“找 bug”而非“完全证明正确”。如果你在写并发逻辑、状态机、Agent 编排或 API 协议，可以尝试让模型先生成 TLA+ 或 Lean 模型，再针对反例定位问题；竞态条件、边界状态这类靠人工审查容易漏掉的问题，正是形式化方法的强项。对使用 Claude Agent SDK 的团队，这 16 个 PR 意味着 SDK 的稳定性可能直接受益。对普通用户和创作者，短期影响间接：底层工具更稳，AI 应用的崩溃和异常行为会更少。需要提醒的是，模型生成的验证模型本身可能出错，结果仍需人工复核，且这类工作会显著消耗推理算力。
AI 工具推荐
想把多个 AI 模型放在一个入口？
GamsGo AI 集成 ChatGPT、DeepSeek、Gemini、Claude、Midjourney、Veo 等常用模型，适合写作、绘图、视频和日常 AI 工作流。
推广链接：通过此链接购买，我可能获得佣金，不影响你的价格。
值得关注的后续
一是这 16 个 PR 是否被合入主线、修复问题的严重程度是否有公开说明；二是 Lean/TLA+ 这类形式化验证能否被封装进 CI 流程，变成开发者可日常调用的能力；三是其他厂商的编码模型是否会跟进支持形式化语言，以及 Anthropic 是否会把该能力产品化。Cherny 抛出的问题也值得持续跟踪：形式化验证会成为写代码的常规环节，还是仅限于 bug 发现这一细分场景。
