Vérification formelle avec Claude : preuves pour 123 bibliothèques open source

Le 22 octobre, l’équipe Frontier Red Team d’Anthropic, avec la société Theorem, a publié une étude dans laquelle Claude a écrit des preuves formelles de sécurité pour 123 bibliothèques open source du projet OSS-Fuzz. Les preuves portent sur le code RISC-V compilé, et non sur le code source. Selon les auteurs, c’est la première vérification formelle de logiciels de production au niveau assembleur, à l’aide de l’IA, à cette échelle.

Comment fonctionne la vérification formelle avec Claude ?

La vérification formelle est une preuve mathématique qu’un programme possède une propriété donnée pour toutes les entrées possibles, et pas seulement pour celles que quelqu’un a testées. Le problème, c’est qu’elle demandait jusqu’ici des années de travail d’experts. Une comparaison tirée de l’étude : la vérification du noyau seL4 a pris environ 20 années-personnes, son écriture deux.

Le pipeline de l’étude se présente ainsi :

1. Le point de départ, ce sont les tests de fuzzing existants d’OSS-Fuzz (un projet de Google qui bombarde sans relâche les bibliothèques de données aléatoires).
2. La bibliothèque et son test sont compilés en un exécutable RISC-V.
3. À partir de la sémantique du processeur RISC-V et d’un processus Linux fournie par Theorem, une spécification est générée automatiquement : le programme doit toujours se terminer normalement, sans erreur mémoire ni assertion échouée.
4. Claude écrit la preuve, et le vérificateur Rocq confirme qu’elle satisfait la spécification.
5. Quand Claude tombe sur un bug, il corrige le code, la spécification est régénérée et la preuve est reconstruite de zéro.

La garantie couvre toute entrée de moins de 64 Mo ainsi que toute réponse du système et toute disposition mémoire modélisées (en supposant un programme statique, monothread, sur RISC-V et Linux).

Quels chiffres Anthropic a-t-il donnés ?

1. 239 points d’entrée dans 123 bibliothèques.
2. Au total, environ 180 millions de lignes de preuves en Rocq ; une preuve typique compte environ 600 000 lignes et porte sur un programme d’une médiane de 18 000 instructions RISC-V.
3. L’ensemble a pris quelques semaines.
4. Sur 36 petites tâches, Opus 5.5 en a prouvé la moitié en consommant environ 40 % de tokens en moins qu’Opus 5, et les agents travaillant dans un espace partagé ont consommé 17 % de moins que seuls.

Détail curieux : la preuve pour cpp-httplib a exigé de montrer que l’arbre rouge-noir de libc++ a une profondeur bornée logarithmiquement, car c’était le seul moyen d’exclure un dépassement de pile dans le destructeur de std::set.

Quels bugs Claude a-t-il trouvés ?

Selon les auteurs, le processus a mis au jour des centaines de bugs qui avaient survécu à des années de fuzzing. Exemples tirés de l’article :

1. Un dépassement par le bas d’un compteur dans un décompresseur, menant à une écriture hors tampon, mais seulement avec une entrée d’environ 20 Mo à la structure rare.
2. Une lecture hors tampon dans un décodeur d’images, nécessitant une entrée de 64 Mo et plus de 2 Go de mémoire.
3. Une lecture hors tampon qui n’apparaissait qu’avec une séquence précise d’appels sur deux descripteurs du même fichier.
4. La redécouverte de CVE-2026-56132 dans libexpat (elle nécessitait une entrée profondément imbriquée).
5. Un bug logique : une fonction limitant l’accès aux fichiers ne fonctionnait pas toujours, alors que rien ne plantait.

S’y ajoutent trois expériences supplémentaires. Claude a écrit une spécification formelle de la RFC 1950 et prouvé sur des binaires x86 que le zlib du noyau Linux l’implémente correctement. Il a aussi construit en Rust un interpréteur d’un sous-ensemble de Python qui, sur 1,7 million de programmes aléatoires, s’est comporté comme CPython dans 99,95 % des cas. Enfin, une tentative de vérifier un lecteur PDF populaire a trouvé en une semaine autant de failles de sécurité qu’on en signale habituellement en un an.

C’est la même direction qu’avec PHP2Shell et Claude Mythos chez Bank of America : les modèles d’IA trouvent des bugs que les humains et les outils classiques ont manqués pendant des années. Sauf que cette fois, cela ne se termine pas seulement par un correctif, mais par une preuve.

À quoi faire attention ?

D’abord, à ce que signifie « vérifié ». Les auteurs l’écrivent clairement : la vérification formelle ne signifie pas un code sans bugs (en version originale « »Formally verified« does not mean »bug-free.« »). Une preuve ne vaut que ce que valent la spécification, les modèles de RISC-V et de Linux, et le vérificateur Rocq lui-même.

Ensuite, au périmètre. Les preuves portent sur des binaires RISC-V statiques et monothreads avec musl, alors que la plupart d’entre nous exécutent du code sur x86 ou ARM avec glibc. Elles ne couvrent pas non plus le code mort, ni les cas où c’est le programme appelant la bibliothèque qui corrompt la mémoire.

Enfin, au coût. Certaines preuves peuvent engloutir des centaines de millions de tokens, ce que les auteurs eux-mêmes désignent comme la principale limite.

Une partie des preuves est déjà sur GitHub (oss-verify-proofs), avec la sémantique de RISC-V et de Linux. Le reste attend, car il pourrait révéler des bugs non corrigés.

FAQ

Qu’est-ce que la vérification formelle ?

C’est une preuve mathématique, vérifiée par un programme, qu’un code possède une propriété donnée pour toutes les entrées, par exemple qu’il n’écrit jamais hors d’un tampon. Les tests et le fuzzing ne vérifient que des cas choisis.

Les bibliothèques vérifiées sont-elles exemptes de bugs ?

Non. La preuve garantit l’absence de plantage uniquement dans le modèle décrit (RISC-V, Linux, entrée de moins de 64 Mo, un seul thread). Des bugs peuvent se cacher dans la spécification, dans le modèle de la machine ou en dehors de ce périmètre.

Puis-je faire vérifier mon projet ?

Theorem gère OSS Verify, un programme gratuit pour une sélection de projets open source. Le mainteneur du projet le soumet via une pull request contenant les fichiers project.yaml, Dockerfile et build.sh, comme pour OSS-Fuzz. Il faut s’attendre à migrer le build vers des binaires statiques riscv64.