TLA+

TLA+, acronyme de « Temporal Logic of Actions » (« logique temporelle des actions » en anglais), est un système de méthode formelle pour les algorithmes parallèles et distribués. C'est un langage de spécification formel utilisé pour la conception, la modélisation, la documentation et la vérification de programmes, en particulier les systèmes distribués et concurrents. Le pseudo-code du langage TLA+ est considéré comme exhaustivement testable. Il peut servir à générer des représentations visuelles (blueprints) de systèmes logiciels.