TLA+ 形式化验证的能力与表达边界解析

TLA+ 能够有效表达和验证状态不变量、动作属性与活性等安全属性，但无法原生表达不可逻辑化的概念、多步属性、实时/浮点约束、可达性及跨行为的超属性。针对近期因 Claude Code 借其检测竞态条件而引发的形式化验证狂热，作者指出形式化方法无法一劳永逸解决智能体软件开发问题，正确的设计也无法自动转化为无缺陷的代码。