Contexte et enjeux
Le code logiciel reste truffé de défauts, même après des campagnes de tests intensives. Le noyau Linux, largement considéré comme l’un des systèmes les plus éprouvés, a récemment vu plus de 1 000 vulnérabilités publiées. Face à la capacité croissante des modèles d’IA à identifier et exploiter des failles, les méthodes traditionnelles de défense deviennent insuffisantes. La vérification formelle, qui consiste à démontrer mathématiquement l’absence de bugs selon un jeu de règles, offre une garantie de sécurité, mais son coût historique la cantonne aux projets critiques : la mise en œuvre du noyau seL4 a nécessité 2 person‑years de code et 20 person‑years de preuves.
Méthodologie et portée des preuves
Anthropic a mobilisé le modèle Claude, couplé à la plateforme Theorem, pour automatiser la génération de preuves sur 123 bibliothèques open‑source. Chaque preuve repose sur la transformation du jeu de tests existant en spécification : le modèle encode la règle « tous les tests passent ». Les hypothèses de vérification sont strictes : exécution d’un binaire statique monothread sur un CPU RISC‑V1, avec un budget mémoire fixe, sous Linux, et pour tout entrée inférieure à 64 Mo. Sous ces contraintes, Claude a démontré que les programmes terminent sans erreurs de sécurité mémoire ni assertions échouées. Le processus a également mis en évidence des bugs non détectés malgré des trillions d’exécutions de tests.
Analyse des résultats et limites
Le taux de couverture dépasse les 100 preuves validées, ce qui constitue, selon les auteurs, la première démonstration à grande échelle de vérification formelle au niveau assembleur pour du code de production. La taille des preuves dépasse souvent le code source, mais Claude a pu gérer la complexité grâce à son aptitude à parcourir des millions de lignes de code. Cependant, les hypothèses restrictives limitent la portée : la preuve ne s’applique qu’à des binaires monothread, à une architecture RISC‑V1 et à des entrées limitées à 64 Mo. Toute variation (multithreading, autre architecture, entrées plus volumineuses) nécessite une nouvelle preuve.
Perspectives
Anthropic publie un sous‑ensemble des preuves et les sémantiques RISC‑V/Linux afin que la communauté puisse les vérifier et les réutiliser. Theorem propose d’étendre la chaîne d’outils à d’autres projets et met à disposition une « Claude skill » pour aider les développeurs à initier leurs propres vérifications. Les auteurs anticipent que, à mesure que les modèles gagnent en intelligence, le coût de rédaction des preuves continuera de diminuer, rendant la vérification formelle accessible au-delà des seules applications critiques.
