L’IA fera de la vérification formelle une pratique grand public
(martin.kleppmann.com)- La vérification formelle (formal verification) est une méthode qui consiste à prouver mathématiquement qu’un code satisfait toujours sa spécification, mais elle est longtemps restée cantonnée à un domaine limité centré sur la recherche
- Quelques grands systèmes, comme le microkernel seL4, ont bien été développés avec vérification formelle, mais son coût élevé et sa grande difficulté l’ont rendue presque absente de l’industrie
- Récemment, des outils d’assistance au code fondés sur les LLM ont montré des résultats non seulement pour le code d’implémentation, mais aussi pour la rédaction de scripts de preuve dans plusieurs langages, ce qui laisse entrevoir un profond changement dans l’économie de la vérification
- Si l’IA peut automatiser à la fois la génération de code et la preuve de correction, le développement pourrait évoluer vers une approche plus fiable que la revue de code humaine
- L’automatisation de la vérification formelle apparaît comme une technologie clé pour garantir la fiabilité logicielle à l’ère de l’IA, et son adoption à grande échelle dépendra probablement davantage d’un changement culturel que de limites techniques
État actuel et limites de la vérification formelle
- Des langages et outils orientés preuve comme Rocq, Isabelle, Lean, F*, Agda permettent de démontrer mathématiquement qu’un code satisfait sa spécification
- Le noyau du système d’exploitation seL4, le compilateur C CompCert ou encore la pile de protocoles cryptographiques Project Everest en sont des exemples représentatifs
- Pourtant, dans l’industrie, la vérification formelle est très peu utilisée
- Dans le cas de seL4, la vérification de 8 700 lignes de code C a nécessité 20 années-personnes et 200 000 lignes de code Isabelle
- Chaque ligne d’implémentation demandait 23 lignes de preuve et une demi-journée de travail humain
- À l’échelle mondiale, on estime à quelques centaines le nombre de spécialistes capables d’écrire ce type de preuves
- D’un point de vue économique, pour la plupart des systèmes, le coût de la vérification dépasse les pertes causées par les bugs, ce qui limitait fortement sa viabilité pratique
Comment l’IA change l’économie de la vérification formelle
- Ces dernières années, les assistants de code fondés sur les LLM ont obtenu des résultats non seulement sur le code d’implémentation, mais aussi sur la rédaction de scripts de preuve
- Nature, Galois, arXiv et d’autres ont rapporté des cas où des LLM ont généré des preuves dans plusieurs langages
- Aujourd’hui, une supervision experte reste nécessaire, mais une automatisation complète semble envisageable dans les prochaines années
- Si le coût de la vérification chute fortement, la vérification formelle pourra être appliquée à un plus grand nombre de logiciels
- En parallèle, le code généré par l’IA nécessitera de garantir sa fiabilité par vérification formelle plutôt que par relecture humaine
- Si l’IA peut démontrer elle-même la correction de son code, celui-ci pourrait être préféré au code écrit manuellement
Complémentarité entre LLM et vérification des preuves
- Quand un LLM rédige des scripts de preuve, il peut produire des contenus erronés (hallucinations), mais le proof checker les rejette
- Le vérificateur repose lui-même sur un petit code validé, ce qui rend très difficile l’acceptation d’une preuve incorrecte
- La rigueur de la vérification formelle compense donc l’incertitude inhérente aux LLM
- Cette combinaison constitue une voie d’automatisation sûre pour garantir la fiabilité du code généré par l’IA
Nouveau défi : la justesse de la définition de la spécification
- Même dans un environnement de vérification automatisée, définir correctement la spécification (specification) reste le défi central
- Il faut s’assurer que les propriétés démontrées correspondent bien à celles que les développeurs voulaient réellement exprimer
- La rédaction de spécifications exige toujours de l’expertise et une réflexion attentive, mais elle reste bien plus simple et rapide que la rédaction manuelle de preuves
- L’IA pourrait aussi aider à la traduction des spécifications entre langage naturel et langage formel
- Il existe toutefois un risque de perte de sens, considéré comme gérable
Évolution attendue des méthodes de développement logiciel
- Les développeurs pourraient décrire les propriétés voulues du code sous forme de spécifications déclaratives, puis laisser l’IA générer à la fois l’implémentation et la preuve
- Dans ce cas, il ne serait plus nécessaire pour les développeurs d’examiner directement le code produit par l’IA, qui pourrait être utilisé sur la base de la confiance, comme le langage machine produit par un compilateur
- En résumé, trois évolutions sont attendues
- Une baisse rapide du coût de la vérification formelle
- Une hausse de la demande de vérification pour garantir la fiabilité du code généré par l’IA
- La précision de la vérification formelle viendra compenser la nature probabiliste des LLM
- Si ces facteurs se combinent, la vérification formelle a de fortes chances de devenir une technologie grand public de l’ingénierie logicielle
- À l’avenir, le principal facteur limitant pourrait être moins la technologie que la vitesse d’acceptation du changement culturel dans les équipes de développement
1 commentaires
Avis de Hacker News
Je pense que la vérification formelle (formal verification) révèle surtout sa valeur dans des domaines où l’implémentation est bien plus complexe que la spécification.
Par exemple, l’optimisation au niveau du bit dans les implémentations cryptographiques ou les passes d’optimisation des compilateurs.
Mais comme le code écrit par la plupart des développeurs (ou par l’IA) est déjà proche de la spécification grâce aux langages de haut niveau, je ne pense pas que les bénéfices de la vérification formelle y soient si importants.
Je doute même qu’écrire la spécification séparément soit plus lisible.
Aujourd’hui déjà, divers frameworks et bibliothèques abstraient les détails d’implémentation.
La vérification formelle peut certes offrir des garanties plus fortes, mais la plupart des gens ne veulent pas ce niveau de garantie, et je ne pense pas que l’IA fasse naître ce besoin
Certaines personnes prédisent que l’IA automatisera entièrement la vérification formelle, mais je vois un problème dans ce raisonnement.
Si l’IA peut prouver automatiquement des logiciels, alors il ne serait même plus nécessaire de vérifier des logiciels écrits par des humains.
L’IA pourrait elle-même concevoir des idées, les implémenter et décider du niveau de vérification.
Au final, la programmation et la vérification humaines pourraient en grande partie disparaître.
En pratique, il est possible pour les humains de concevoir des assistants de preuve, mais il est bien plus difficile de vérifier avec eux des programmes de grande taille.
Donc si une telle IA apparaissait, elle pourrait sans doute créer elle-même de nouveaux assistants de preuve.
Bien sûr, ce genre d’hypothèse relève davantage de la science-fiction et, tant qu’on ne sait pas clairement ce que l’IA rendra plus facile ou plus difficile, ce type de prédiction a peu de sens.
Lien vers une discussion connexe
Ce sera peut-être le point de bascule vers une phase complètement différente pour l’humanité
Pour obtenir des résultats utiles avec des agents de codage (Claude Code, Codex CLI, etc.), l’essentiel est de bien mettre en place un environnement où exécuter et valider le code qu’ils écrivent.
Les langages faciles à exécuter comme Python sont les plus adaptés, et pour du HTML+JS il faut des outils comme Playwright.
L’étape suivante, ce sont les suites de tests automatisées, puis les outils de qualité comme les formateurs de code, les linters et les fuzzers.
Les débogueurs sont utiles aussi, mais leur nature interactive les rend difficiles à exploiter pour des agents.
Je pense que les outils de vérification formelle font partie de ce spectre — les modèles actuels gèrent aussi très bien les langages de programmation spécialisés.
Si vous trouvez que les agents de codage ne servent pas à grand-chose, c’est probablement parce qu’il manque un bon environnement d’exécution et de test
En prenant Haskell comme exemple, si ça compile, alors dans la plupart des cas ça fonctionne correctement.
Si cette propriété est utile aux humains, elle le sera aussi pour les LLM.
Les property tests sont particulièrement bien adaptés aux LLM — ils couvrent une large zone d’erreurs avec peu de tests.
Quand on voit que la communauté mathématique essaie d’utiliser les LLM pour améliorer du code Lean, on peut penser qu’un développement logiciel s’appuyant sur des systèmes de types plus puissants est tout à fait possible
Le débogage n’est pas séquentiel, et le moment des causes et des effets s’y entremêle.
J’avais essayé ChatGPT autrefois pour traquer un bug multithread avec gdb, mais il ne faisait que répéter des suggestions triviales du type « ajouter des prints ».
Cela m’a rappelé que c’est au fond un domaine qui exige de l’expérience et de l’intuition
Demander à un ingénieur junior de travailler sans débogueur ni lanceur de tests n’aurait aucun sens.
Au final, il faudra probablement plus de ressources de calcul.
Claude implémente, et Codex ainsi que Gemini relisent.
Cette méthode coûte cher, mais c’est ce que j’ai trouvé de plus fiable pour réduire le biais envers soi-même (self-bias) et améliorer la qualité du code.
Des outils d’analyse statique aideraient aussi, mais j’ai l’impression qu’ajouter simplement plus d’outils ne suffit pas
Si le processus de vérification est automatisé, la vraie difficulté se déplace vers la définition précise de la spécification (specification).
Écrire la spécification est bien plus rapide et plus simple que produire la preuve elle-même, mais cela demande toujours de l’expertise et de la prudence.
Si la preuve formelle ne s’est pas généralisée dans le passé, ce n’est pas seulement à cause de sa difficulté, mais aussi parce que le modèle waterfall a disparu au profit du développement agile.
Au lieu d’écrire de longues spécifications, on a évolué vers une méthode d’itération rapide en fonction des besoins des utilisateurs
Il est peut-être temps de se mettre à OCaml.
Beaucoup d’assistants de preuve et de systèmes de vérification peuvent générer du code OCaml, et ADA/Spark mérite aussi d’être envisagé.
Quoi qu’il en soit, l’ingénierie logicielle va changer à l’ère de l’IA, mais nous devons produire des logiciels de meilleure qualité qu’aujourd’hui.
La vérification formelle aidera clairement à atteindre cet objectif
Ce n’est pas encore terminé, mais je partage mon projet expérimental.
Dans un monde où les textes centrés sur le code manquent, cela peut valoir le détour pour quelqu’un qui cherche une idée de hackathon intéressante.
Lien vers le projet py-mcmas
Les LLM ont tendance à bien résoudre les problèmes faciles à vérifier.
C’est pourquoi je divise la résolution en trois étapes.
1️⃣ J’écris d’abord un programme qui définit les conditions de réussite
2️⃣ puis je lui fais vérifier le problème initial
3️⃣ et enfin je vérifie moi-même
Cette approche existe chez moi depuis longtemps, mais désormais des modèles comme Opus ou GPT-5.2 l’exécutent bien même en mode autonome.
Article de blog connexe
Dans les domaines où la vérification prend du temps, cela peut au contraire augmenter la charge de validation pour les humains
On peut poser la question : « qui vérifie le programme de vérification ? »
Si c’est aussi le LLM qui l’écrit, on peut avoir l’impression d’une régression infinie (turtles all the way down).
ce qui est difficile, c’est de produire la preuve.
Il existe bien sûr des exceptions pour les propositions complexes, mais cela aide énormément à réduire les bugs
Même si la vérification formelle se démocratise, je ne pense pas que tout le monde se mettra à utiliser Lean ou Isabelle.
Elle se diffusera plutôt sous une forme où l’IA s’intègre naturellement aux workflows existants.
Par exemple, avec de la vérification de propriétés dans la CI, ou un bouton dans l’IDE du type « prouver l’invariant de ce module ».
La plupart des ingénieurs n’auront probablement jamais besoin de voir directement les scripts de preuve.
La vraie difficulté n’est pas que le LLM produise des preuves, mais de pousser les organisations à investir dans l’écriture de spécifications et de modèles.
Si l’IA facilite la proposition et la révision de spécifications, la vérification pourra s’installer naturellement comme un outil de refactoring, au même titre que les tests ou les linters
Certaines personnes se plaignent encore que GPT‑5.2 est incapable de compter correctement le nombre de
rdans « garlic ».Si c’est vraiment nécessaire, il suffit de demander au LLM d’écrire un script Python puis de l’exécuter.
C’est vrai, mais cela ne relève que d’un détail d’implémentation de la tokenisation et n’a presque aucun rapport avec l’utilité réelle.
On n’a presque jamais besoin d’utiliser un LLM pour compter les lettres dans un mot