TLA+ 能验证什么，不能验证什么

📋 概述

Claude Code 的作者 Boris Cherny 提到 Opus 能用 TLA+ 找出代码里的竞态条件，随后全网开始热议形式化验证。作为长期教授和推广 TLA+ 的人，作者感到兴奋，但也很担心这波狂热：很多人说形式化方法将一劳永逸地解决智能体软件开发的问题，这是胡说。已经有很多文章谈过 TLA+ 在保证能力上的局限，比如正确的设计不会自动变成正确的代码，所以本文聚焦另一个限制——要验证一个性质，首先得有一个可被表达的性质。文章由此讨论哪些性质是 TLA+ 连表达都做不到的，包括如何用行为序列、状态与 []P、P-next 等时序算子来表述系统。