TLA+

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 ».