Contexte et intérêt de TLA+
Le tweet viral de Boris Cherny a généré près d’un million de vues et a relancé l’intérêt pour TLA+ (Temporal Logic of Actions), un langage de modélisation formelle créé il y a plus de trente ans. La communauté l’utilise pour décrire les comportements possibles d’un système et les propriétés qui doivent toujours ou éventuellement être respectées. L’exemple phare présenté dans l’article est l’élection de leader parmi trois ordinateurs : aucune configuration ne doit produire deux leaders simultanément et un leader doit finir par être élu.
Mécanismes de model checking et limites
Le modèle TLA+ se compose d’états (instantanés) et d’actions (transitions). Le vérificateur standard, TLC, explore exhaustivement les états d’un modèle fini : pour trois nœuds, il y a 38 états, alors que le même modèle avec neuf nœuds dépasse le million d’états. Cette explosion combinatoire montre que le model checking reste limité aux instances finies. De plus, TLC ne garantit pas la conformité du code réel au modèle ; il ne vérifie qu’une abstraction.
Les propriétés de sécurité (□ P) et de vivacité (◇ P) sont exprimées avec les opérateurs classiques : □ P signifie « toujours », ◇ P « éventuellement », et P ⇝ Q « P conduit à Q ». Un contre‑exemple de sécurité apparaît dès que l’on autorise un ordinateur à voter deux fois : le vérificateur renvoie une exécution de six étapes où deux leaders coexistent.
□ (¬ (leader1 ∧ leader2)) // aucune double‑leadershipIntégration avec les systèmes de preuve modernes
Pour dépasser les limites de TLC, les auteurs évoquent Verus, un environnement où spécification, preuve et implémentation Rust cohabitent dans le même langage. Leur pipeline a transformé plus de 16 000 paires spécification/propriété TLA+ en plus de 3 000 preuves vérifiées par Verus, illustrant la faisabilité d’une chaîne de vérification complète.
Le système de preuve natif de TLA+, TLAPS, peut prouver des propriétés générales, mais son automatisation reste restreinte, surtout pour les arguments de vivacité. Ainsi, la combinaison de model checking (pour les cas concrets) et de preuves formelles (pour les cas généraux) constitue la pratique recommandée.
Perspectives d’automatisation par IA
Les chercheurs de Reasonable entraînent des modèles d’IA capables de générer, transformer et vérifier des spécifications. Un agent a déjà utilisé Opus 5.5 pour modéliser des parties du Claude Agent SDK en TLA+ et en Lean, démontrant que les agents peuvent passer du modèle à la preuve puis au code réel. L’objectif à long terme est un « loop » unique où la spécification, l’implémentation et la vérification sont synchronisées automatiquement, réduisant les écarts entre modèle et produit.
Des entreprises comme AWS, MongoDB, Datadog ou Kafka utilisent déjà TLA+ pour valider des protocoles critiques, mais elles restent conscientes des trois réserves majeures : portée finie du model checking, besoin de preuves pour les tailles arbitraires, et dissociation entre modèle et implémentation.
