Méthodes formelles TLA+ et Coq (Rocq), où elles valent leur coût

Méthodes formelles TLA+ et Coq (Rocq), où elles valent leur coût

Les méthodes formelles remplacent « ça a passé les tests » par une vérification mécanique d’une propriété énoncée en mathématiques. Le titre réunit deux outils qui ne répondent pas à la même question : TLA+ (Temporal Logic of Actions, le langage de spécification de Leslie Lamport) explore les comportements d’une conception, Coq (renommé Rocq Prover en 2025) démontre un théorème sur un programme ou un algorithme. La position défendue ici : ça rapporte énormément sur une petite fraction d’un système, et presque rien sur le reste.

Explication de la marmotte

Avant d’ouvrir un pont, personne ne se contente d’y faire rouler trois camions pour voir si ça tient : on calcule qu’il tiendra, quelle que soit la charge prévue. Les méthodes formelles font pareil pour un logiciel dont la panne coûterait trop cher : passer de « on a essayé, ça marchait » à « on a démontré que ça ne peut pas arriver ».

→ Lire l’explication complète de la marmotte

TLA+ et Coq : exploration d’états contre assistant de preuve

Première famille : la spécification vérifiée par exploration d’états. On décrit le système comme une machine à états (des variables, un état initial, des actions qui font passer d’un état au suivant), puis un outil parcourt les états atteignables et vérifie qu’une propriété tient dans chacun. Autour de TLA+ gravitent quatre outils à ne pas confondre :

• TLC, le vérificateur de modèles livré avec TLA+, énumère explicitement les états d’un modèle borné ;
• PlusCal est un langage d’allure algorithmique, traduit vers TLA+, pour ceux que la notation mathématique brute rebute ;
• Apalache est un vérificateur symbolique : il confie la question à un solveur SMT (Satisfiability Modulo Theories) au lieu d’énumérer, et vise d’abord les invariants ;
• TLAPS (TLA+ Proof System) vérifie des preuves écrites à la main, donc sans borne sur le modèle, au prix d’un effort d’un autre ordre.

Seconde famille : l’assistant de preuve. Coq, développé à l’Inria (Institut national de recherche en informatique et en automatique), est à la fois un langage de programmation fonctionnel et une logique. On y écrit des définitions, on énonce un théorème, on construit la preuve pas à pas, et un petit noyau vérifie chaque étape. Rien n’est exploré : la preuve vaut pour toutes les entrées, y compris une infinité.

Les voisins, une phrase chacun. Isabelle/HOL (Higher-Order Logic) est un assistant de preuve en logique d’ordre supérieur, celui dans lequel est prouvé le micronoyau seL4 (un noyau à capacités, justement). Lean est un assistant de preuve à types dépendants, très porté par la communauté mathématique. Alloy modélise des structures relationnelles et les analyse sur des instances bornées. La méthode B raffine une spécification abstraite jusqu’au code en déchargeant des obligations de preuve à chaque étape. Et HACL* (High Assurance Cryptographic Library) est écrite en F*, pas en Coq : la confusion est fréquente.

	TLA+ (TLC, Apalache)	Coq / Rocq Prover
Ce qu’on écrit	Une machine à états abstraite, des invariants et des propriétés temporelles	Des définitions, des programmes fonctionnels, des théorèmes et leurs preuves
Ce qu’on obtient	Un contre-exemple (une trace d’exécution fautive), ou l’absence de violation dans le modèle borné	Une preuve vérifiée par le noyau, valable pour toutes les entrées ; éventuellement du code extrait
Objet vérifié	La conception, jamais le code	L’algorithme ou le programme écrit dans Coq, sous une spécification donnée
Effort	Quelques jours à quelques semaines pour un protocole, accessible à un ingénieur motivé	Des mois à des années, compétence rare, preuve souvent bien plus longue que le code
Limite principale	Explosion combinatoire, modèle borné, écart total avec le code	Coût, spécification qui peut être fausse, base de confiance en aval
Retour le plus rentable	Trouver un défaut de conception avant d’écrire une ligne	Garantir un composant petit, stable et critique

Ce que TLC et Apalache vérifient, et les hypothèses du modèle

Une spécification TLA+ ne vaut que par ses hypothèses, et elles sont toutes écrites par un humain. Le réseau perd-il des messages ? Les duplique-t-il, les réordonne-t-il ? Un nœud qui tombe redémarre-t-il avec son état disque ou vierge ? Les horloges dérivent-elles ? Chaque réponse est une action présente ou absente du modèle. Une panne non modélisée est une panne contre laquelle rien n’est vérifié : le vérificateur ne devine pas ce qu’on a oublié de lui dire, et un modèle où le réseau est fiable prouve la correction d’un protocole qui n’existera jamais en production.

Deux classes de propriétés, deux niveaux de difficulté :

• la sûreté (« rien de mauvais n’arrive ») : jamais deux leaders pour un même mandat, jamais deux valeurs décidées. Un contre-exemple est une trace finie, donc lisible et rejouable ;
• la vivacité (« quelque chose de bon finit par arriver ») : toute requête finit par recevoir une réponse. Elle n’a de sens que sous des hypothèses d’équité (une action possible en permanence finit par être exécutée), et un contre-exemple est une exécution infinie qui boucle.

En pratique, on vérifie surtout la sûreté. La vivacité coûte plus cher à explorer, les optimisations par symétrie de TLC ne s’y appliquent pas sans risque, et ses hypothèses d’équité sont précisément ce qu’un réseau réel ne promet pas. Pour un protocole de consensus, elle dépend d’hypothèses de synchronie détaillées dans la page sur le consensus distribué et la tolérance byzantine.

Reste l’explosion combinatoire. Le nombre d’états croît exponentiellement avec le nombre de nœuds, de messages en transit et de valeurs possibles. On vérifie donc un modèle borné : trois nœuds, deux valeurs, un nombre plafonné de pannes. Le résultat s’énonce « aucune violation dans ces bornes », et l’extrapolation à cinquante nœuds repose sur un pari empirique (la plupart des défauts de conception se manifestent sur de petites instances), pas sur un théorème. Pour lever la borne, il faut un invariant inductif vérifié par Apalache ou une preuve TLAPS, et le budget change d’ordre de grandeur.

Le raffinement mérite une mention : TLA+ permet de montrer qu’une spécification détaillée implémente une spécification abstraite, en exhibant la correspondance entre leurs états. C’est la bonne manière de descendre par paliers vers le système réel, mais le dernier palier reste une spécification, pas du code.

Côté réalisations, les références sont publiques et sobres. L’article de Newcombe et al., « How Amazon Web Services Uses Formal Methods » (revue Communications of the ACM, 2015), rapporte que TLA+ a révélé sur des systèmes distribués en production des défauts de conception subtils que ni les tests ni les revues n’avaient trouvés. Paxos dispose d’une spécification TLA+ de Lamport, Raft de la sienne, écrite par son auteur. Aucun de ces textes ne prétend que le code est prouvé.

Ce que Coq (Rocq Prover) prouve : théorème, extraction et base de confiance

Coq prouve qu’un objet défini dans Coq satisfait un énoncé écrit dans Coq. Les trois réalisations de référence montrent la portée et la forme du résultat :

• CompCert (Xavier Leroy) est un compilateur C dont la preuve établit la préservation sémantique : le code assembleur produit se comporte comme le programme source, pour les programmes sans comportement indéfini ;
• Fiat Cryptography génère du code d’arithmétique sur les corps finis des courbes elliptiques, accompagné de sa preuve de correction ; ce code est intégré à BoringSSL ;
• le théorème des quatre couleurs (Georges Gonthier) a été entièrement vérifié en Coq, ce qui rappelle que l’outil est d’abord un vérificateur de mathématiques.

Pour passer de la preuve au binaire, deux voies. L’extraction traduit le programme Coq vers un langage fonctionnel comme OCaml, qu’on compile ensuite normalement. L’autre voie consiste à prouver un générateur ou un compilateur, puis à faire confiance à ce qu’il émet (c’est la logique de CompCert et de Fiat Cryptography).

Dans les deux cas, la preuve s’arrête quelque part, et ce qui se trouve au-delà forme la base de confiance, ou TCB (Trusted Computing Base) : le noyau de vérification de Coq, les axiomes ajoutés au développement, le mécanisme d’extraction, le compilateur du langage cible, l’environnement d’exécution, le système, le matériel. CompCert lui-même laisse hors preuve le préprocesseur, l’assembleur et l’éditeur de liens. Un théorème admis sans preuve (Admitted) ou un axiome incohérent suffit à rendre tout démontrable, y compris le faux : la première vérification d’un développement tiers consiste à lister ses hypothèses, pas à admirer sa taille.

Reste le piège le plus sournois, parce qu’il porte tous les signes extérieurs de la rigueur : la spécification fausse mais prouvée. Un tri prouvé « renvoie une liste triée » sans que l’énoncé exige les mêmes éléments en sortie est correct, démontré, et renvoie volontiers la liste vide. La preuve garantit la cohérence entre l’énoncé et l’objet. Elle ne dit rien de la cohérence entre l’énoncé et le besoin. Relire la spécification reste un travail humain, et c’est le plus rentable de toute la chaîne.

De la spécification au code exécuté : où se loge chaque écart

Le schéma suivant se lit de haut en bas : chaque flèche est une traduction, et chaque crochet indique ce qu’aucune preuve en amont ne couvre.

L’écart 3 est celui que TLA+ ne ferme jamais. Les palliatifs existent : vérifier des traces d’exécution réelles contre la spécification, générer des cas de test à partir du modèle, placer les invariants en assertions dans le code. Ils réduisent l’écart, ils ne le prouvent pas nul.

L’écart 4 est le terrain des compilateurs prouvés, et aussi celui de la compilation reproductible, qui répond à une autre question : le binaire livré provient-il bien de ce source ? Les deux sont complémentaires.

L’écart 5 concentre ce qu’un attaquant vise en premier face à du code prouvé. Une preuve de correction fonctionnelle porte sur la relation entre entrées et sorties. Le temps d’exécution, la consommation, les accès au cache n’apparaissent pas dans l’énoncé, donc pas dans la garantie : le temps constant est une propriété distincte, à obtenir et à vérifier séparément (voir les attaques par canaux auxiliaires). Même chose pour la configuration : un protocole prouvé pour une majorité de trois nœuds sur cinq ne promet rien si le quorum est réglé à deux, et une primitive prouvée appelée avec un paramètre réutilisé reste une primitive mal utilisée. La page lire une garantie sans la surinterpréter traite ce réflexe côté preuves cryptographiques ; il vaut à l’identique ici.

Où TLA+ et Coq rapportent, et où ils coûtent pour rien

Le compromis central : on achète une garantie exhaustive sur un objet précis, on la paie en compétences rares, en temps, et en rigidité (toute modification de l’objet prouvé oblige à reprendre la preuve). Le calcul n’est favorable que si l’objet est petit, stable, critique, et doté d’une propriété qu’on sait écrire.

Ça rapporte sur :

• les protocoles distribués (réplication, élection, verrous, transactions), parce que leurs défauts naissent d’entrelacements que l’intuition humaine n’énumère pas ;
• les machines à états de sécurité (cycle de vie d’une clé, session d’authentification, révocation), où un état inattendu est une élévation de privilège ; les modèles de la page Bell-LaPadula et Biba et de la sécurité par capacités sont précisément des propriétés de ce type ;
• les noyaux et hyperviseurs, dont tout le reste dépend ;
• les compilateurs, parce qu’un défaut s’y propage à tout ce qu’ils produisent ;
• les primitives cryptographiques, où une retenue mal propagée passe tous les tests aléatoires et se révèle sur une entrée choisie.

Ça ne rapporte pas sur le code métier ordinaire : règles de gestion qui changent chaque trimestre, écrans, assemblage de services. La spécification y serait aussi longue et aussi fausse que le code, et elle serait périmée avant la fin de la preuve. Sur ce terrain, un système de types sérieux, des tests de propriétés et la revue font le travail. La sécurité mémoire de Rust relève d’ailleurs de la même famille, en version légère : un système de types est une vérification formelle limitée à une classe de propriétés, qui élimine une classe entière de défauts à la compilation sans qu’on ait à écrire de preuve.

L’arbre ci-dessous donne l’outil selon la question posée.

La dernière branche est la plus sous-estimée. Pour la plupart des organisations, la bonne décision n’est pas de prouver quoi que ce soit en Coq, mais de consommer des composants prouvés par d’autres et d’écrire du TLA+ sur ses propres protocoles. Le rapport coût sur bénéfice de TLA+ en phase de conception est sans équivalent ; celui d’une preuve Coq maison ne se justifie que si le composant est le produit lui-même.

Côté réglementaire, trois ancrages sûrs. Les niveaux hauts des Critères Communs, EAL6 et EAL7 (Evaluation Assurance Level), demandent une conception vérifiée de façon semi-formelle puis formelle. En avionique, le référentiel DO-178C de certification des logiciels embarqués est accompagné du supplément DO-333, consacré aux méthodes formelles. Et le pilotage automatique de la ligne 14 du métro parisien a été développé avec la méthode B. Hors de ces contextes, aucune case à cocher n’impose une preuve : la décision reste une décision d’ingénierie, ce qui est plutôt une bonne nouvelle.

Exemple : boucle de vérification TLA+ d’une élection de leader

Cas d’école : une élection de leader par mandats numérotés, à trois nœuds, sur un réseau qui perd, duplique et réordonne les messages. La propriété de sûreté s’écrit en une ligne : pour tout mandat, au plus un nœud se considère leader, soit un invariant vérifié sous la forme Spec => []UnSeulLeaderParMandat.

La trace fautive typique : un nœud accorde son vote, tombe avant de l’avoir écrit sur disque, redémarre sans mémoire, vote une seconde fois pour un autre candidat dans le même mandat. Deux majorités, deux leaders. Ce scénario demande une panne placée entre deux instructions précises ; un test d’intégration peut tourner très longtemps sans le produire, alors que le vérificateur, sur un modèle de cette taille, le sort rapidement avec la suite exacte des événements.

La dernière ligne du schéma n’est pas décorative. Un invariant trop faible, ou une action jamais activable à cause d’une garde mal écrite, donne un modèle où tout passe parce que rien ne se passe. Casser volontairement la spécification et constater que l’outil proteste est le seul moyen de savoir que le feu vert veut dire quelque chose. Un vérificateur qui ne trouve rien du premier coup est une raison de s’inquiéter, pas de fêter.

Prérequis et conditions d’exploitation d’une spécification formelle

Avant de commencer, il faut disposer de trois choses. Une propriété énonçable en une phrase précise (« jamais deux détenteurs du verrou » passe, « le système est sûr » ne passe pas). Un périmètre découpé : on spécifie le protocole de réplication, pas la plateforme. Et quelqu’un qui maîtrise le protocole autant que l’outil, car la difficulté est dans le choix de l’abstraction, pas dans la syntaxe. Côté plateforme : TLC s’exécute sur une machine virtuelle Java et consomme mémoire et cœurs sans modération ; Apalache s’appuie sur un solveur SMT ; un développement Coq dépend d’une version précise de l’outil et de ses bibliothèques, à figer.

En exploitation, une spécification se traite comme du code :

• elle vit dans le dépôt, à côté de ce qu’elle décrit, et toute modification du protocole passe d’abord par elle ;
• la vérification tourne en intégration continue sur un modèle réduit, et périodiquement sur un modèle large ;
• les bornes et hypothèses du modèle sont documentées en tête de fichier : ce sont elles qui définissent la portée de la garantie, et ce sont elles qu’un auditeur doit lire ;
• les invariants prouvés sont repris en assertions et en sondes de supervision, pour détecter en production une violation que le modèle excluait (ce qui signale une hypothèse fausse, information précieuse) ;
• pour Coq, la liste des axiomes du développement est contrôlée à chaque version, et la montée de version de l’outil est planifiée : elle casse régulièrement des preuves.

Le mode de défaillance le plus courant n’a rien de technique : la spécification écrite une fois, vérifiée une fois, puis laissée de côté pendant que le code évolue. Elle continue de passer au vert en décrivant un système qui n’existe plus, ce qui en fait le document le plus rassurant et le moins vrai du dépôt.

FAQ

TLA+ prouve-t-il que le code est correct ?

Non. TLA+ vérifie une conception décrite à part, dans son propre langage. Le lien avec le code repose sur la discipline : relecture croisée, assertions reprenant les invariants, vérification de traces d’exécution contre la spécification. Un défaut d’implémentation (verrou oublié, écriture non synchronisée sur disque) reste entièrement possible sous une spécification irréprochable.

Coq et Rocq Prover sont-ils deux outils différents ?

C’est le même. Coq a été renommé Rocq Prover en 2025 ; la littérature, les bibliothèques et la plupart des projets cités ici portent encore l’ancien nom, d’où l’usage des deux.

Faut-il commencer par TLA+ ou par Coq ?

Par TLA+, dans presque tous les cas. L’investissement se compte en semaines, le retour arrive dès la première trace fautive, et la démarche s’applique aux protocoles que toute architecture distribuée contient. Coq se justifie quand il faut une garantie sur toutes les entrées d’un composant de calcul, et qu’aucun composant déjà prouvé ne fait l’affaire.

🐝 Ce qui arrive si on s’en passe

Sans spécification vérifiée, un protocole distribué n’est validé que sur les entrelacements que les tests ont eu la chance de produire. Les scénarios rares (panne entre deux écritures, message retardé au-delà d’un changement de mandat) restent inexplorés jusqu’à ce que la production les rencontre, sous forme de données divergentes entre réplicas ou de deux détenteurs d’un même verrou. Un attaquant capable de retarder ou de rejouer des messages peut chercher délibérément ces états. Sans énoncé écrit, il manque aussi la référence permettant de dire si un comportement observé est un défaut ou non, et chaque évolution du protocole se décide sans moyen de vérifier qu’elle préserve les propriétés d’origine. Côté calcul, une erreur arithmétique sur une entrée précise survit indéfiniment aux tests aléatoires.

🦫 Explication de la marmotte 🍫

Tester un programme, c’est l’essayer sur quelques cas. Les méthodes formelles cherchent à couvrir tous les cas, et il existe deux façons de s’y prendre. La première consiste à décrire le fonctionnement prévu sous forme de situations possibles et de passages d’une situation à l’autre, puis à laisser un outil parcourir toutes les situations atteignables. S’il en trouve une interdite, il donne la suite exacte d’événements qui y mène, et on corrige la conception. Comme le nombre de situations grossit très vite, on se limite à une version réduite du système : le résultat ne vaut que pour cette version réduite. La seconde façon consiste à écrire une démonstration mathématique, étape par étape, qu’un outil contrôle ligne à ligne. Elle vaut pour tous les cas sans limite, mais demande des mois de travail spécialisé. Dans les deux cas, on ne vérifie que ce qu’on a écrit. Si la description oublie une panne, ou si la règle à respecter est mal formulée, l’outil valide quelque chose de faux. Il reste aussi des étapes non vérifiées entre la description et la machine réelle : le programme réellement écrit, sa traduction en instructions, le matériel, les réglages. Voilà pourquoi on réserve ces méthodes aux petites parties d’un système dont tout le reste dépend.

À lire aussi

• Vérifier un protocole cryptographique avec Tamarin ou ProVerifCe que vérifient réellement Tamarin et ProVerif sur un protocole cryptographique, lequel choisir selon la question posée et comment lire un résultat annoncé comme prouvé.
• Non-interférence et contrôle de flux d'information en pratiqueCe que le contrôle de flux d'information et la non-interférence ajoutent au contrôle d'accès, leurs variantes, leurs limites et leur usage en architecture de sécurité.
• Lire une certification FIPS 140-3 ou Critères Communs d'un HSMCe que garantissent réellement les certifications FIPS 140-2, FIPS 140-3 et Critères Communs d'un module cryptographique matériel, comment lire un certificat et quel niveau exiger à l'achat.

Pages voisines

La citent

• Non-interférence et contrôle de flux d'information en pratique
• Vérifier un protocole cryptographique avec Tamarin ou ProVerif
• Langages informatiques : histoire, inventeurs et usages
• Lire une certification FIPS 140-3 ou Critères Communs d'un HSM

Méthodes formelles TLA+ et Coq (Rocq), où elles valent leur coût

Elle cite

• Consensus distribué et tolérance aux pannes byzantines
• Modèles Bell-LaPadula, Biba et Clark-Wilson
• Sécurité par capacités contre ACL
• Attaques par canaux auxiliaires et secrets
• Rust et la sécurité mémoire par construction, garanties et limites
• Vérifier une chaîne de compilation reproductible
• Comment concevoir la sûreté cyber automobile et aéronautique
• Common Criteria