TLA+
Langage de modélisation formelle (états, transitions, invariants) utilisé pour prouver les propriétés de systèmes critiques.
Prouver, plutôt que tester
TLA+ est un langage de modélisation formelle créé par Leslie Lamport. Il décrit un système par ses états, ses transitions et ses invariants — des propriétés qui doivent rester vraies quelle que soit l'exécution. Plutôt que d'échantillonner des cas de test, on prouve mathématiquement que ces invariants tiennent.
AWS utilise TLA+ depuis des années sur ses services critiques : un invariant typique de DynamoDB garantit par exemple que les données sont répliquées sur trois zones de disponibilité. À l'échelle de l'hyperscaler — où un événement « un sur un milliard » se produit malgré tout plus de mille fois par heure — la preuve formelle est le seul filet qui résiste.
Un levier de contrôle à l'ère agentique
Dans un monde où les agents produisent du code à un rythme qui rend la relecture exhaustive impossible, la modélisation formelle redevient stratégique : on vérifie la divergence entre le code et le modèle par analyse statique et dynamique, et l'on borne les décisions des agents par un crible déterministe et prouvé. C'est l'une des réponses concrètes à la question « comment garder le contrôle sans tout relire ».
Questions fréquentes
À quoi sert TLA+ dans le développement agentique ?
TLA+ décrit un système par ses invariants et permet de prouver mathématiquement qu'ils tiennent. Face à du code massivement généré par IA, il sert à vérifier la divergence entre le code et son modèle et à borner de façon déterministe les décisions des agents — garder le contrôle sans tout relire.
