TLA+ : ce qu'il vérifie et ce qu'il ne peut pas
Original : What TLA+ can and can't check
Pourquoi c'est important
L'IA générative relance l'intérêt pour la vérification formelle, mais sans en clarifier les limites réelles.
Suite à l'annonce que Claude Opus peut utiliser TLA+ pour détecter des race conditions, l'enthousiasme autour des méthodes formelles explose. Hillel Wayne, éducateur TLA+ de longue date, tempère : vérifier une propriété exige d'abord de savoir l'exprimer — et TLA+ a des angles morts réels.
Boris Cherny, inventeur de Claude Code, a révélé qu'Opus était capable d'utiliser TLA+ pour trouver des race conditions. Internet s'est immédiatement enflammé : les méthodes formelles allaient « résoudre » le développement logiciel agentique. Hillel Wayne, auteur de plusieurs formations TLA+, intervient pour calmer le jeu.
TLA+ découpe un système en comportements — des séquences d'états. On peut exprimer des propriétés booléennes sur ces états, et les composer avec trois opérateurs temporels : `[]P` (« toujours P »), `<>P` (« éventuellement P ») et `P'` (« P dans l'état suivant »). Ces combinaisons permettent de vérifier des invariants de sécurité (« rien de mauvais n'arrive jamais ») et des propriétés de vivacité (« quelque chose de bon finit par arriver »).
Mais le point central de Wayne : pour vérifier une propriété, encore faut-il pouvoir l'énoncer. TLA+ ne peut pas exprimer certaines classes de propriétés — notamment celles liées aux performances, aux coûts, ou à des comportements émergents difficiles à formaliser. Un design correct en TLA+ ne garantit pas non plus un code correct. La nuance est de taille quand on parle de systèmes agentiques autonomes.