Les spécifications formelles sont des outils d’incident, pas des preuves académiques

Il y a un moment, dans tout incident réel, où la salle cesse de parler de fonctionnalités et commence à parler de temps.

Le temps d’arrêter l’hémorragie. Le temps de comprendre dans quel état se trouve le système. Le temps de décider si un redémarrage améliore la situation ou élargit le blast radius. Le temps de répondre à la seule question que votre « vous » de demain vous reprochera d’avoir ignorée : « Si nous ne faisons rien, que se passe-t-il ensuite ? »

À cet instant, la plupart des systèmes distribués se transforment en concours de récits. Chacun a une histoire plausible. Aucune n’est réfutable assez vite.

C’est pour cela que je reviens sans cesse aux spécifications formelles. Pas comme un test de pureté. Comme un outil d’incident.

Hillel Wayne l’a dit sans détour dans sa récente conversation sur les méthodes formelles : les méthodes formelles ne servent pas seulement à prouver qu’un programme est correct ; elles servent à rendre les parties critiques d’un système suffisamment précises pour pouvoir raisonner dessus. Cette précision fait la différence entre « on pense » et « on sait », surtout quand le système est distribué, automatisé et sous charge.

Le vrai problème n’est pas le bug. C’est l’état que vous ne savez pas expliquer.

La plupart des équipes savent déjà corriger un bug. Vous trouvez le repro, vous patchiez, vous livrez. Les problèmes difficiles apparaissent quand le système a plusieurs « writers », du travail asynchrone, des retries, des pannes partielles et des timeouts qui interagissent.

Ajoutez maintenant des agents.

Un workflow agentic, ce n’est pas seulement du code qui s’exécute. C’est du code qui décide, puis agit — et crée encore plus d’état. S’il appelle des services externes, déclenche des paiements, passe des ordres, met à jour des entitlements clients, chaque action devient un maillon d’une chaîne que vous devrez peut-être justifier plus tard.

Quand cela dérape, le mode de défaillance est rarement « ça a crashé ». Le mode de défaillance, c’est : « ça a continué, mais dans une mauvaise réalité ».

• Deux workers pensent tous les deux « posséder » le même job.
• Un retry transforme une action « once-only » en action « at-least-once ».
• Un humain lit un dashboard en eventual consistency et prend une décision sur la base d’un état fantôme.
• Un agent lit un contexte périmé et exécute avec assurance une action valide… au mauvais moment.

Les tests classiques couvrent mal ces situations, parce que vous ne pouvez pas énumérer les interleavings qui comptent. L’observabilité aide à voir ce qui s’est passé, mais après coup. « On a des logs » n’équivaut pas à « on a un modèle ».

Les specs formelles, surtout TLA+, vous obligent à définir le système comme une machine à états : quel état existe, quelles transitions sont permises, ce qui doit toujours rester vrai. Ce n’est pas académique. C’est, à ma connaissance, la seule manière de rendre lisible le comportement distribué.

Le déterminisme n’est pas un détail d’implémentation. C’est une exigence business.

Dans les systèmes proches du trading et des paiements, l’objectif n’est pas « zéro incident ». L’objectif, c’est : « des dommages bornés, des résultats explicables et une reprise rapide ». Vous pouvez vivre avec la panne d’un composant. Vous ne pouvez pas vivre avec le fait de ne pas savoir ce qu’il a fait.

Dans les faits, le déterminisme recouvre quatre points :

1. L’idempotence est explicite : vous décidez quelles actions peuvent être répétées sans risque et vous encodez la clé qui les rend sûres.
2. L’ordre est intentionnel : vous choisissez où l’ordre compte (par compte, par portefeuille, par client) et où il ne compte pas.
3. La responsabilité est unique : un endroit décide, les autres observent. Si plusieurs endroits décident, vous modélisez l’arbitrage.
4. Les invariants ne se négocient pas : vous définissez ce qui ne doit jamais arriver, même pendant des retries, des backfills ou des pannes partielles.

C’est le même changement de posture qui rend les systèmes d’IA (intelligence artificielle) plus sûrs. Pas parce que l’IA serait magique, mais parce qu’elle est probabiliste. Si vous laissez des composants probabilistes écrire directement dans votre « vérité financière » ou votre system of record, vous perdez la capacité à rejouer et à défendre les résultats. Gardez-les dans la narrative layer, et maintenez la truth layer déterministe. (Cette séparation est proche de ce que j’ai défendu dans LLMs Belong in the Narrative Layer, Not in the Financial Truth Layer.)

Les specs formelles se situent précisément à cette frontière. Elles permettent de figer le cœur déterministe et ses invariants, pour que le reste du système puisse être créatif sans devenir dangereux.

Ce que TLA+ vous apporte quand l’incident met tout le monde sous pression

La valeur la plus sous-estimée de TLA+ n’est pas le model checker. C’est la discussion qu’il impose.

Quand vous rédigez une spec, l’ambiguïté n’a plus d’endroit où se cacher. Vous ne pouvez pas dire « le worker prend le job ». Vous devez préciser quand il est éligible, qui peut le réclamer, et ce qui se passe si deux workers essaient. Vous ne pouvez pas dire « on réconciliera plus tard ». Vous devez définir la transition de reconciliation et ce qu’elle a le droit de modifier.

Sous pression, cette précision paie de trois manières très concrètes :

• Auditabilité : vous pouvez relier les événements observés aux transitions autorisées. Si quelque chose s’est produit et n’existe pas dans le modèle, vous avez un vrai défaut, pas un mystère.
• Capacité de reprise : vous pouvez concevoir à l’avance les « repair moves ». Backfill, replay, compensation et chemins de freeze sont aussi des transitions. Si vous ne les avez jamais modélisés, vous les improviserez quand cela coûtera le plus cher.
• Maîtrise du blast radius : les invariants disent clairement ce que vous pouvez relâcher sans danger et ce que vous devez protéger à tout prix. Cette clarté vaut mieux que l’héroïsme.

Cela rejoint l’insistance de Wayne : les méthodes formelles deviennent de plus en plus praticables, et des outils comme TLA+ sont utilisés parce qu’ils aident les équipes à raisonner sur des comportements complexes, pas parce qu’ils promettent un logiciel parfait. Dans un contexte business, c’est ce cadrage pragmatique qui compte. Vous n’achetez pas de la certitude. Vous achetez moins d’inconnues inconnues. (Voir à nouveau la discussion.)

Un schéma vécu : l’incident où « on ne peut pas savoir » est la panne

J’ai construit des automatisations de trading où le code n’était pas la partie la plus inquiétante. Le plus inquiétant, c’était le contrat invisible entre composants : qui a le droit d’agir, sous quelles conditions, et comment on sait qu’une action est définitive.

Un type d’incident revenait sans cesse, quels que soient les systèmes et les équipes : localement, le système faisait ce qu’il était « autorisé » à faire ; globalement, il trahissait l’intention. Un retry partait après un timeout, un accusé de réception arrivait trop tard, deux services n’étaient pas d’accord sur le fait qu’une transition d’état avait été committée. La panne n’était pas l’indisponibilité. La panne, c’était l’incertitude.

Quand vous ne pouvez pas déterminer si une transition d’état a eu lieu, vous ne pouvez pas avancer en sécurité. Vous vous figez. Des humains lancent des scripts manuels. Certains proposent de redémarrer des queues et de redéployer des services, parce que ce sont les seuls leviers visibles. Pendant ce temps, le système continue à dériver.

Une spec formelle n’aurait pas empêché chaque échec. Mais elle aurait rendu deux points impossibles à ignorer :

• Les invariants exacts qui définissent un comportement « suffisamment correct ».
• Les transitions exactes qui constituent des manœuvres de reprise sûres, y compris celles qui sont interdites.

C’est cela que je veux dire quand j’affirme que c’est un outil d’incident. Un moyen de réduire la part d’improvisation.

Adopter les specs formelles sans en faire du théâtre

Vous n’avez pas besoin d’un programme de vérification formelle à l’échelle de l’entreprise. Vous avez besoin d’un seul périmètre étroit où l’ambiguïté coûte cher.

Voici un pattern qui fonctionne dans des équipes réelles :

1) Choisir un « truth workflow » et tracer la frontière

Choisissez un workflow où un état erroné est pire qu’une indisponibilité. Exemples : entitlements, état de facturation, cycle de vie d’un ordre, positions de portefeuille, payouts, effets de bord irréversibles.

Définissez ce qui se trouve dans le cœur déterministe (machine à états, invariants, transitions) et ce qui reste à l’extérieur (UI, analytics, raisonnement de l’agent, recommandation).

2) Écrire la spec avant la prochaine réécriture, pas après l’incident

Une spec écrite en post-mortem devient souvent de la documentation. Une spec écrite avant la construction devient du design.

Restez petit. Si c’est trop grand pour être model-check, c’est trop grand pour servir d’outil d’aide à la décision.

3) Modéliser les mouvements d’échec comme des transitions de premier ordre

La plupart des systèmes modélisent le happy path puis « gèrent les erreurs ». Cela ne suffit pas.

• Que signifie « freeze » en termes d’état ?
• Comment reprendre sans appliquer deux fois les actions ?
• À quoi ressemble une compensation, et à quoi ne doit-elle jamais toucher ?

C’est le même état d’esprit que pour construire des déploiements d’IA qui composent : vous définissez un chemin contrôlé de la réalité actuelle vers la réalité cible, avec de la réversibilité lorsque c’est possible. (Voir aussi : Build on the Stack You Have: The Rollout Pattern That Makes AI Compound.)

4) Transformer les invariants en contrôles runtime et en runbooks

Une spec qui vit dans un repo sans jamais influencer le comportement en production finit oubliée.

Choisissez 3 à 5 invariants et implémentez-les sous forme de :

• Assertions runtime ou garde-fous aux frontières.
• Alertes qui réveillent des humains sur violation d’invariant, pas sur des symptômes bruyants.
• Étapes de runbook qui se réfèrent à l’invariant : quoi vérifier, quoi geler, quoi rejouer.

5) Utiliser la spec comme gouvernance du changement

Tout changement qui affecte le truth workflow doit d’abord mettre à jour la spec. C’est une forme légère de contrôle du changement : elle ne ralentit pas les équipes, elle évite des retours en arrière coûteux.

Les dépassements de budget en logiciel viennent souvent du fait de construire deux fois la mauvaise chose. Ici, la dynamique est la même : l’ambiguïté est un centre de coûts. (Si vous voulez l’angle gouvernance plus large, voir Budget overruns are rarely a surprise. They are a governance choice.)

Mon point de vue : l’IA ne fera pas disparaître le besoin de specs. Elle renchérira le coût de leur absence.

Une idée tentante plane derrière la vague actuelle : les modèles écriront le code, et peut-être même le vérifieront. Wayne aborde la question de savoir si l’IA pourrait faire entrer les méthodes formelles dans le mainstream ; je suis d’accord sur la direction, pas sur l’interprétation paresseuse. (Voir l’entretien.)

Si l’IA réduit le coût de production du logiciel, elle réduit aussi le coût de production de modes de défaillance subtils. Les systèmes agentic multiplient les effets de bord. Les systèmes distribués multiplient les interleavings. Ensemble, ils multiplient le nombre d’histoires plausibles pendant une panne.

Les specs formelles sont ce qui permet de garder une partie du système ennuyeuse. Déterministe. Auditable. Récupérable. Ce n’est pas un luxe. C’est la fondation qui permet d’aller vite partout ailleurs.

Utilisez TLA+ là où « on ne peut pas savoir » deviendrait votre pire incident. Si vous ne pouvez pas expliquer l’état, vous ne maîtrisez pas le système.

C’est mon opinion, et je n’ai encore jamais vu une équipe regretter d’avoir rendu son truth workflow lisible.