TLA+（時間論理 of アクション）は、システムを振る舞いの集合としてモデル化し、各振る舞いは状態の列である。時間論理演算子を使って、不変条件（例えば []P はあらゆる状態で P が成り立つことを意味する）やアクション特性（例えば [](x' >= x) は x の新しい値が常に古い値以上であることを表す）を表現できる。生存性特性（「何か良いことがいつか起こる」と主張する）は <> 演算子から構築され、<>[]P（最終的に P が永遠に真となる）や P ~> Q（P が Q を導く）などの例がある。これらの特性はすべての可能な振る舞いに対して評価され、普遍的に成り立つことを保証する。

根本的な制限として、TLA+ は振る舞いについての存在量化を必要とする性質を表現できない。たとえば、ゲームが勝ちうることを証明するために必要な「P が真となる振る舞いが存在する」ような到達性特性は言語のスコープ外である。同様に、TLA+ は振る舞いの集合に対する性質であるハイパープロパティを表現できない。たとえば、エネルギー節約モードがあらゆる可能なアクションシーケンスにおいて通常モードより常に少ないエネルギーを使用することを確認するのは、2 つの異なる振る舞いを比較する必要があり、これがハイパープロパティの例である。

回避策は存在する — 状態履歴を保存するための補助変数の使用、複数の振る舞いをモデル化する自己構成、TLC モデルチェッカーにおける REACHABLE キーワードと TLCGet の活用など — しかし、これらは重大な欠点をもたらす。補助変数は精緻化を複雑にし、自己構成は状態空間の指数関数的な爆発を引き起こし、これらの技術はしばしばごちゃごちゃしたモデルを生み出し、実際のシステムに直接対応しなくなる。CTL や PRISM などの他のツールはこれらの性質の一部を扱えるが、TLA+ が得意とする安全性と生存性の検証において弱さを抱えるトレードオフとなる。