TLA+能做什么，又做不了什么

What TLA+ can and can't check

最近Boris Cherny提到Claude Code能用TLA+发现竞态条件，这让形式化验证再次成为热点。作为TLA+的长期布道者，我既兴奋又担忧。兴奋的是大家开始关注复杂并发系统的设计，担忧的是有人误以为形式化方法能一劳永逸地解决Agent软件开发的所有问题。TLA+在验证不变量（invariants）和活性（liveness）属性方面非常强大，能确保“坏事不发生”和“好事终会发生”。但它的局限同样明显：无法表达需要跨多个步骤验证的属性，无法处理浮点数或物理时间，更无法直接验证涉及多个行为对比的超属性（hyperproperties），比如安全性中的非干涉性或统计属性。虽然可以通过辅助变量或自组合等技巧来“模拟”这些检查，但这些方法往往让模型变得复杂且难以维护。TLA+擅长摘取低垂的果实，但并非万能钥匙。