L’IA fera de la vérification formelle une pratique grand public

• 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
  1. Une baisse rapide du coût de la vérification formelle
  2. Une hausse de la demande de vérification pour garantir la fiabilité du code généré par l’IA
  3. 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