上周克劳德代码（Claude Code）发明者鲍里斯·切尔尼（Boris Cherny）称奥普斯（Opus）用TLA+（TLA+）找到代码竞态条件，全网热议形式化验证。作者作为TLA+长期教育者与倡导者感兴奋，但冷静下担忧，因多人称形式化方法将彻底解决智能体软件开发问题，实乃谬论。TLA+保证性弱点已多谈，如正确设计不自动转正确代码，故作者想说另一局限：验证属性需先有属性。

上周 Claude Code 发明者 Boris Cherny 提到 Opus 能用 TLA+ 在代码中找到竞态条件，现在网上所有人都在讨论形式化验证。TLA+ 非常擅长设计复杂的并发系统并确保无 bug，这真令人兴奋！但面对这股新热潮我很担忧，看到很多人说形式化方法将一劳永逸地解决智能体软件开发问题，这纯属胡扯。

关于 TLA+ 在能保证什么方面的弱点已谈得够多，比如正确的设计不会自动转化为正确的代码。于是聚焦另一局限：要验证一个属性，我们得先有属性可验证！那么 TLA+ 甚至无法表达哪些属性？

TLA+ 能检查什么

TLA+ 将系统划分为一组行为，每个行为是一系列状态，比如“灯1是绿的，然后黄，然后红”。在每个状态中，我们可以表达常规的布尔表达式，比如“灯4是绿的”或“所有灯都是红的”。我们还可以用三个“时序”逻辑运算符来修饰表达式：

• []P（“总是 P”）：在当前状态及之后每个状态中 P 都为真时成立。例：[](at_most_one_green) 表示此后每个状态都不超过一个绿灯。
• P'（“P 素数”）：在下一状态 P 为真时成立。例：light="green" && light'="red" 表示灯从绿变红。
• <>P（“最终 P”）：在当前状态或至少一个未来状态 P 为真时成立。例：<>(light4 = "yellow") 表示灯4现在是黄或将来某时是黄。

当我们说 P 是系统属性，是指它在每个行为的初始状态为真。所以若检查属性 []P，意味着 []P 在每个初始状态为真，根据“总是”的定义，P 从该初始状态起每个未来状态都为真，即在每个行为的每个状态都为真。我们称之为不变量，是 TLA+ 检查的最基础属性之一。

我们也可将 [] 与素数组合得到动作属性。[](x' >= x) 表示 x 的新值总是大于等于旧值。另一个有趣的是 [](P => P')：一旦 P 为真就再不会为假。实际 TLA+ 因“停顿不变性”稍复杂，但这是额外细节。动作属性与不变量都是安全属性，大致指“坏事永不发生”。

顺便说，活性是“好事总会发生”。所有活性属性基于 <>。单独 <>P 仅指“P 在每个行为至少一个状态为真”，通常太弱不算好系统属性。但组合后能构造更有趣的活性属性：

• []<>P：在每一个状态，P 在至少一个未来状态为真。可表示恢复机制，如“若节点重新选举领导，它们最终会就领导达成一致”。
• <>[]P：在某时刻 P 变为真并永远保持。很适合展示算法以正确结果终止。
• [](P => <>Q)：对每个 P 为真的状态，都存在 Q 为真的未来状态。可展示 P 最终引发 Q，或“所有入队消息最终都在读者历史中”。解析公式有点绕，所以有语法糖 P ~> Q（P 导致 Q）。

还有其他运算符如 ENABLED 和 <<A>>_v 能玩出别的花样，但我们检查的多是不变量、动作属性和活性。还有精化，它是安全与活性的结合，自成一题。

TLA+ 不能做什么

从明显的开始：如果你不知如何将属性表示为逻辑公式，TLA+ 帮不了你，任何形式化方法也帮不了。若无法形式化“鸟”的概念，就无法证明应用能识别鸟。不幸的是，很多我们在意的重要属性属于此类。

其次，过于具体的事。TLA+ 安全属性作用于单个状态（不变量）或单步（动作属性）。无法原生定义跨两步或多步的属性，如“按 delete 再按 undo 恢复原状”，或“按 power 后十步内开机”。也无法定义浮点操作或真实时间（仅逻辑时间）上的属性。

现在说我最感兴趣的局限。TLA+ 属性隐式地对所有行为量化。我说检查 []P 是“P 在每个状态为真”，实际指“对所有行为，[]P 对该行为初始状态为真”。TLA+ 能查的系统属性必须对每个单独行为都为真。

这排除了什么？比你想的多得多！

其一，无法做“存在行为使 P 为真”。所以不能说 P 可能，即便实际没达到。例如证明游戏可赢，这叫可达性属性。更高级的如“从每个初始状态可达 P”或“从任何 Q 为真状态可达 P”。

我们也无法定义针对一组行为的属性，称为超属性。假设建模手机硬件，想验证节能模式总比普通模式耗电少。属性是“任何操作序列在节能模式耗电不多于常规”。要反驳，需给我两个除起始模式外完全相同的行为，且常规模式耗电更少。单个行为不够，所以在 TLA+ 中无法自然检查。超属性看似小众，却涵盖大量安全属性和所有统计属性（“95分位响应时间5ms”）。

最后，稍偏学术的，无法定义针对整个状态空间的属性。例如不能说从状态 X 到 Y 只有一条路径。不知实际多有用。这类“元属性”可能有意义，我只不知具体。

"TLA+" 能“做”什么

我说 TLA+ 不能做这些有点简化了。意思是若你写规格且直接对应想建的系统，TLA+ 不能将这些表达为系统属性。但可用辅助变量模拟两步属性，如将状态变更存入 state_history 序列并定义为该序列上的不变量。可用自组合模拟某些超属性，即自组合规格的每个行为是实际系统的两个行为。主要模型检查器 TLC 能用新 REACHABLE 关键字检查最基本可达性，用 TLCGet 查某些状态空间属性。Andrew Helwer 有篇神文讲用公平性和“机器闭包”模拟“总是可达”。

这些是有用 hack，但仍是 hack。每个都需聪明才智且有严重缺陷。辅助变量毁精化，自组合让状态空间指数级膨胀等。Hack 不能很好与其他特性组合，也覆盖不了想表达属性的所有精妙处。最糟的是让模型奇怪混乱，不对应实际系统。

也可用侧重不同的工具。CTL 能做可达性，PRISM 做概率属性等。它们牺牲了 TLA+ 擅长的，且当然都处理不了逻辑上无法表达的属性。

TLA+ 很擅长摘低垂果实——不变量和活性覆盖许多在意的事，且它表达检查得相当好。用 TLA+ 查 vibe code 潜力大（陷阱也多）。但很多东西它甚至无法表达，更别提检查。

社区普遍强调形式化验证与测试不足以将实现完全托付给大模型，人类工程师仍需真正理解系统；同时在 TLA+ 的语法易用性和文章技术细节上存在少数人的质疑与批评。

认为形式化验证无法替代人工理解，不能把实现全交给大模型

• 靠写测试或形式验证来把实现甩给概率性模型是逃避，构建者必须自己弄懂系统（较多人） > 概率猜测机器救不了他们，人们无法逃避真正理解所构建事物的需要。（@adamddev1）

认为编程语言缺陷加剧验证难度，闭图语义语言可桥接模型与实现

• 现有语言允许表达部分图使验证技术挑战大，若语言仅暴露闭图语义或可缩小模型与实现的鸿沟（少数人） > 我的看法是只暴露闭图语义的语言有助于弥合模型与实现间的差距。（@rrook）

认为 TLA+ 语法怪异且手工转译易错，整体评价不高

• TLA+ 语法奇特需配套专门子语言，且形式模型通过后仍需手工转为真实代码并可能引入错误（少数人） > TLA+ 语法超级怪异，而且最终还得手工转换成真实语言难免出错。（@IshKebab）

质疑文章关于可达性的表述，认为 TLA+ 本可证明可赢性

• 文章称可达性表述奇怪，但模型检查“永不赢”不变量失败即间接证明存在可行行为，无需另说（少数人） > 证明游戏可赢只需模型检查“永远不可赢”不变量并失败即可，何须另说？（@lou1306）

有价值的补充

• Quint 是基于动作时序逻辑的可执行规范语言，配有友好工具链，适合对 TLA+ 感兴趣者尝试（@sourdecor）
• TLA+ 不擅长建模弱内存或非顺序一致语义，转译后默认顺序一致，手工建模易错；Rust 的 miri 与 loom 可查部分非顺序行为（@singron）
• 形式方法包括 TLA+ 无法防止未验证硬件固件的侧信道，也难以发现浮点算术非结合性等问题（@westurner）
• 社区另有汇总贴讨论互联网发现 TLA+ 后的实践与未来动向（@ChrisArchitect）