Claude prouve la sécurité de 123 bibliothèques au niveau du code RISC-V

Anthropic et Theorem ont publié les résultats d'un projet dans lequel Claude a rédigé, en mode autonome, des preuves formelles de correction pour du code open source réel. Le modèle a prouvé l'absence de plantage pour 239 points d'entrée dans 123 bibliothèques issues de Google OSS-Fuzz. Les preuves ne portent pas sur les sources, mais sur les instructions RISC-V compilées, et totalisent environ 180 millions de lignes en Rocq. Un tel travail exigeait jusqu'ici des années d'efforts de spécialistes pointus. On ne l'appliquait donc que là où une erreur coûte trop cher, par exemple dans l'avionique d'Airbus.

Le test de fuzzing comme spécification toute prête

Le principal obstacle de la vérification formelle est qu'il faut d'abord expliquer ce que signifie « correct ». Pour un décodeur PNG, la RFC 2083 existe. Pour un éditeur de texte ou un navigateur, il n'y a pas de spécification claire. Les chercheurs ont contourné le problème : ils ont repris les tests de fuzzing existants des développeurs et transformé la condition « le test ne plante jamais » en spécification formelle. Celle-ci est décrite au-dessus d'un modèle de l'exécution de n'importe quel binaire RISC-V sous Linux.

Un fuzzer teste un nombre énorme d'entrées semi-aléatoires, mais ne garantit pas une couverture complète. La preuve, elle, apporte une garantie : si Claude a prouvé que le test ne plantera sur aucune entrée de moins de 64 Mo, le fuzzing de ce point d'entrée sur RISC-V ne trouvera plus rien. OSS-Fuzz compile les programmes C et C++ avec AddressSanitizer, de sorte que tout accès mémoire incorrect compte comme un plantage. La propriété prouvée inclut donc automatiquement la memory safety, première source de vulnérabilités.

Ce qui a été obtenu

Le projet a duré quelques semaines. Le critère de réussite : Claude écrit la preuve, c'est le noyau de Rocq qui la vérifie, et un humain n'a pas besoin de relire des centaines de milliers de lignes. Trois éléments restent à croire sur parole : les modèles formels de RISC-V et des processus Linux, la formulation exacte des théorèmes, et Rocq lui-même.

• 123 bibliothèques OSS-Fuzz, 239 points d'entrée
• environ 180 millions de lignes de Rocq, preuve type d'environ 600 mille lignes
• binaire médian : 18 000 instructions RISC-V
• garantie : sortie correcte, sans erreur mémoire ni échec d'assertion, sur toute entrée jusqu'à 64 Mo
• hypothèses : binaire statique monothread, budget mémoire fixe, RISC-V et Linux

Les auteurs soulignent eux-mêmes que cela ne signifie pas l'absence de bugs dans les bibliothèques. Les erreurs restantes peuvent se cacher dans les composants de confiance ou hors de la propriété prouvée. En revanche, la surface à vérifier se réduit : pour couvrir de nouveaux projets, il n'est pas nécessaire d'agrandir la base de confiance.

Des bugs que le fuzzer n'aurait pas trouvés

Quand une preuve n'aboutissait pas, Claude corrigeait le code, la spécification était régénérée et le modèle prouvait alors la nouvelle version. Des centaines d'erreurs ont ainsi été mises au jour. Le fuzzer n'en aurait presque certainement pas détecté beaucoup, car il mute de petites entrées, généralement jusqu'à 1 Mo. Exemples :

• underflow d'un compteur dans une copie d'un décompresseur, menant à une écriture hors des limites d'un buffer, uniquement sur des entrées d'environ 20 Mo à la structure rare
• lecture hors limites dans un décodeur d'images, qui exige une entrée de 64 Mo ou plus et plus de 2 Go de mémoire
• lecture hors limites dans une autre bibliothèque, après une séquence d'appels précise via deux descripteurs du même fichier
• redécouverte de CVE-2026-56132 dans libexpat, qui nécessite une imbrication profonde
• erreur logique sans plantage : la fonction de limitation des fichiers chargés ne fonctionnait pas toujours

Un effet secondaire compte aussi : même une tentative de preuve qui échoue met au jour de vrais défauts. Par ailleurs, les tests de fuzzing vérifient souvent des propriétés de haut niveau, par exemple un encodage-décodage sans perte. Pour l'algorithme de compression LZO, le test affirme que la décompression des données compressées restitue l'original. Si la propriété est violée, le programme plante : prouver l'absence de plantage revient alors à prouver la propriété elle-même. Pour cpp-httplib, Claude a dû exclure séparément un dépassement de pile dû à une récursion profonde dans le destructeur de std::set.

Ce qu'il faut en retenir pour les équipes

Le contexte est tendu : plus de 1000 vulnérabilités ont été révélées récemment dans le noyau Linux, et les modèles assemblent de mieux en mieux des chaînes d'exploits à partir de petits bugs. À titre de comparaison, l'implémentation du noyau seL4 a demandé deux personnes-années, et sa vérification vingt. Si le coût des preuves baisse à mesure que les modèles gagnent en capacités, et si les preuves existantes peuvent être réutilisées d'une base de code à l'autre, l'économie du sujet change.

Anthropic publie une partie des preuves, les modèles de RISC-V et de l'OS, ainsi que les spécifications des tests qu'il n'a pas réussi à prouver. Theorem propose d'exécuter le même pipeline sur d'autres projets open source et publie un Claude skill pour la vérification en autonomie. Les développeurs qui ont un jour essayé les méthodes formelles avec des modèles plus faibles, puis y ont renoncé, ont intérêt à reconsidérer la question. Le plus raisonnable est de commencer par un projet qui dispose déjà de bons tests de fuzzing : la spécification y est presque prête. En parallèle, les auteurs testent les mêmes méthodes sur zlib et sur la vérification de l'équivalence comportementale d'un interpréteur Python écrit en Rust.