TLA+
TLAはZFに基づいているため、変数の操作にはセット操作が含まれる。言語には、集合元、和集合、共通部分集合、差集合、べき集合、および部分集合演算子が含まれる。 ∨ 、 ∧ 、 ¬ 、 ⇒ 、 ↔ 、 ≡などの一階述語論理演算子、および全称記号および存在記号∀と∃も含まれている。ヒルベルトのεは、任意の集合要素を一意に選択するCHOOSE演算子として提供される。実数、整数、自然数の算術演算子は、標準モジュールから利用可能である。
時相論理演算子はTLAに組み込まれている。時間式では ◻ P {\displaystyle \Box P} を"Pが常に真である"を意味し、 ◊ P {\displaystyle \Diamond P} を "Pが最終的に真となる"を意味するという使い方をする。演算子は結合され ◻ ◊ P {\displaystyle \Box \Diamond P} は"Pが無限に頻繁に真である"を意味する、または ◊ ◻ P {\displaystyle \Diamond \Box P} は、"最終的にPは常に真になる"という意味となる。