TLA+ est un langage de spécification formelle développé par Leslie Lamport. Il est utilisé pour la conception, la modélisation, la documentation et la vérification de programmes, en particulier de systèmes concurrents et de systèmes distribués. TLA+ est considéré comme un pseudocode exhaustivement testable, et son utilisation est assimilée à l'élaboration de plans pour les systèmes logiciels ; TLA est un acronyme pour Temporal Logic of Actions (logique temporelle des actions).
