TL;DR
動的なシステムの振る舞いを記述するための形式仕様言語。Leslie Lamport が作った。名前は Temporal Logic of Actions の略である。
なぜ必要か
並行システムや分散システムの、時間による変化を記述できる。これにより、競合状態、デッドロック、ライブロックなどを設計の段階で見つけられる。こうした設計の根本的な誤りは、コードになってからでは見つけにくく、直すのにも費用がかかる。
仕組み
TLA+ は単純な数学にもとづいている。主な特徴は次のとおり。
仕様は、システムの状態を表す変数（Variables）、パラメータを表す定数（Constants）、変数の型の制約を表す型不変条件（Type Invariants）、状態の変化を表すアクション（Actions）で書く。振る舞いは、初期状態と状態遷移で表す。
検証する性質は 2 つある。安全性（Safety Property）は「悪いことは起こらない」、活性（Liveness Property）は「良いことはいずれ起こる」という性質である。全体の動作は仕様（Specification）として定義する。
仕様を確かめる主な道具には、モデル検査器の TLC と、証明システムの TLAPS がある。IDE の TLA+ Toolbox や、Visual Studio Code の拡張機能も用意されている。
注意点
現在は TLA+ Foundation が管理している。