TLA+ 能检查什么和不能检查什么

Claude Code 发明者 Boris Cherny 提到 Opus 可用 TLA+ 查找代码竞态条件，引发对形式验证的热议。TLA+ 擅长检查安全属性（不变式、动作属性）和活性属性（<>P、[]<>P 等），但无法表达不可形式化的属性、多步属性、浮点数操作、真实时间，以及"存在某行为满足P"这类可达性属性和超属性。