Claude Code创造者Boris Cherny在社交平台上透露，团队利用Opus 5.5消灭了代码中的竞态条件，这迅速在工程界掀起了一场形式化验证热潮。不少开发者随即产生乐观判断，认为大模型配合严格的数学方法，已经彻底解决了智能体自主写代码时的并发缺陷。
但狂欢很快遭遇了冷水。图灵奖得主Leslie Lamport设计的TLA+长年被AWS等顶级架构团队用于分布式协议校验，其资深布道者Hillel Wayne随后发文直言，把形式化验证当成终结自主编程缺陷的银弹纯属无稽之谈。更重要的是，舆论场从一开始就误读了事实：在Cherny的实际工程流中，主力其实是定理证明器Lean，TLA+只是外围辅助，而形式化工具本身的数学盲区，远比代码补丁复杂得多。
还原16个PR的真相：Lean与TLA+的真实分工
引发技术圈震荡的源头是Cherny在2026年9月22日的一则披露。当时他使用Opus 5.5在Claude Agent SDK上完成了形式化验证工作，仅凭几个简短提示词，就自动生成了16个修复Bug与竞态条件的合并请求。大部分讨论将功劳悉数归于TLA+，然而一手记录显示，这套自动化修复的主力工具实为精于代码级交互式证明的Lean，TLA+仅用于辅助分析部分并发数据流与状态管理。
这种工具错位折射出工业界的普遍误解。TLA+的核心强项在于高层离散状态机建模，利用时序逻辑（TLA）验证并发架构的安全性与活性。相比之下，代码级逻辑证明需要Lean这类依赖类型系统的交互式证明器；若要校验静态配置与权限图谱，工程界通常会转向基于SAT求解的Alloy。三者在系统工程中各司其职，没有任何单一工具能够通吞全局。
- 结论.大模型并没有凭空发明验证逻辑，它只是降低了工程师编写Lean定理与TLA+模型的输入阻抗。
TLA+写不出的现实世界：超属性与概率死穴
即便把视角收窄到并发状态建模本身，TLA+也远非万能。要验证一个系统属性，前提是必须能用时序逻辑精确表达它。人类工程师对业务往往存在大量模糊直觉，一旦无法抽象为数理公式，任何形式化工具都无法介入。
更深层的障碍在于数学结构本身。TLA+天然以单轨迹为粒度进行全称量化检查，系统只校验每一条独立执行路径是否满足约束。这种机制导致它在数学上根本无法原生表达超属性。例如，在硬件节能模式下消耗功率必须低于标准模式这一命题，本质上需要同时对比两条不同的执行轨迹；同理，现代分布式系统最为关注的非干扰安全性和系统观测确定性，也全都属于单轨迹模型检查器无法触碰的超属性。
在工程细节上，TLA+的安全属性只作用于单状态或相邻单步。常见的交互逻辑如按下删除后再按撤销恢复原状，这类跨越两步及以上的多步变迁关系，无法直接写成动作属性，必须依靠工程师手动向规约中塞入辅助历史变量。同时，TLA+不处理概率模型，也无法度量微服务体系至关重要的95分位延迟。它运行在基于人工抽象步进与无卡顿不变性的逻辑时钟之上，完全剥离了真实世界的物理时间分布。
空真性陷阱与不可逾越的代码断层
除了数学工具本身的边界，大模型自主生成规约还会带来更隐蔽的系统风险：模型检查器亮起的绿灯，可能是毫无意义的假象。
学术界近期针对大语言模型生成TLA+规约的评测表明，AI极易写出空真属性或非承重断言。当模型生成的前置条件在逻辑上恒为假时，蕴涵式会自动判定为真，检查器随之放行。这种通过模型检验的规约根本没有对系统施加任何有效约束，反而向工程团队提供了危险的虚假安全感。
更为致命的是活性属性的检验机制。活性属性无法通过有限的状态序列判定违背，往往需要依赖套索循环反例，并且极度依赖弱公平与强公平等环境调度假设。一旦大模型为了促成证明，向规约中注入了过于严苛的公平性假设，该模型就彻底脱离了真实的操作系统调度器，证明结果在工业生产中毫无效用。
模型检查器亮起的绿灯，往往只是把未经约束的假设包装成了数学证明。
最终横亘在所有从业者面前的，是严峻的规约与代码断层。TLA+保证的仅仅是抽象设计在数学上的自洽性，它既不编译为机器指令，也不对生产代码提供直接的类型约束。哪怕规约在TLC模型检验中完全正确，也绝不等于生产代码忠实实现了这套数学模型。
- 风险.如果团队缺乏资深形式化专家做裁判门禁，任由智能体自主修改规约并通过检查，系统崩溃只是被推迟到了线上高并发触发的瞬间。
对于真正负责生产环境高并发系统的架构师而言，眼下最理性的做法不是盲信全自动形式化验证，而是建立起外部不可变裁判机制。让大模型去编写Lean代码片段或TLA+初稿，但必须由人类专家锁定核心规约与不变性条件，并配合跟踪验证工具核对真实代码执行轨迹。只有清醒认识到数学模型的死穴，这场由智能体掀起的工程演进，才不至于沦为另一场数字幻象。