TLA+
Le langage de spécification formelle de Leslie Lamport pour les systèmes concurrents — on décrit ce que le système doit faire, et le model checker vérifie qu'il ne peut pas aboutir à un état invalide.
Fondé sur la logique temporelle des actions. TLC est un model checker qui explore de façon exhaustive toutes les transitions d'état possibles. Amazon Web Services l'utilise pour la conception de S3, DynamoDB et EBS — et y a trouvé des bugs de conception avant l'implémentation. MongoDB, Cosmos DB et Microsoft Azure aussi. Courbe d'apprentissage raide — Lamport a lui-même écrit le manuel (Specifying Systems). Apalache est un vérificateur concurrent. PlusCal est une syntaxe de pseudo-code qui se transpile en TLA+.