# TLA+ 能检查什么、不能检查什么

> 原标题：What TLA+ can and can't check

- 来源：Hacker News 首页
- 发布时间：2026-09-30T13:57:06.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/elpm059yedke2w0ihbxswr2nk
- 原文：https://buttondown.com/hillelwayne/archive/what-tla-can-and-cant-check/

## 摘要

TLA+ 可验证不变量、动作属性和活性等安全性属性，但无法表达可达性属性与超属性，例如证明游戏可获胜、或节能模式比普通模式更省电。它也无法原生定义跨两步以上的属性、浮点运算和真实时间，只能基于逻辑时间。作者提醒，形式化方法无法一劳永逸解决智能体软件开发问题，若属性无法写成逻辑公式，任何形式化方法都无能为力。