Claude a prouvé l'absence de plantage dans 123 bibliothèques open source

Jeudi 22 octobre 2026, Anthropic a publié avec la société Theorem un travail qui change d'échelle la vérification formelle du logiciel : Claude a prouvé mathématiquement que 239 points d'entrée de 123 bibliothèques open source ne plantent jamais, pour toute entrée de moins de 64 Mo, directement sur le code machine compilé. En chemin, il a trouvé et corrigé des centaines de bugs que des milliards de tests n'avaient pas vus.

La vérification formelle en deux mots

Un test vérifie qu'un programme se comporte bien sur les cas essayés. Une preuve formelle démontre qu'il se comporte bien sur tous les cas possibles, et un logiciel indépendant (ici Rocq, l'ancien Coq) vérifie la démonstration ligne par ligne. Le problème, jusqu'ici, c'était le coût : Anthropic rappelle qu'écrire le noyau seL4 a demandé deux années-personnes, et le prouver vingt. La méthode restait réservée à quelques codes critiques, comme l'avionique d'Airbus.

Ce que Claude a prouvé

L'équipe est partie des tests de fuzzing du programme OSS-Fuzz de Google. Un fuzzer bombarde un point d'entrée d'entrées aléatoires pour le faire planter ; Claude devait prouver qu'aucune entrée ne le ferait planter, ce qui rend le fuzzing de ce point d'entrée inutile.

• 239 points d'entrée dans 123 bibliothèques, prouvés en quelques semaines ;
• aucune erreur mémoire détectée par AddressSanitizer ni assertion ratée, pour toute entrée de moins de 64 Mo ;
• les preuves portent sur le binaire RISC-V compilé, pas sur le code source ;
• environ 180 millions de lignes de preuve Rocq, soit en général 600 000 lignes pour un binaire médian de 18 000 instructions.

Personne n'a besoin de relire ces millions de lignes : le vérificateur Rocq s'en charge. Il faut seulement faire confiance au modèle mathématique du processeur RISC-V et de Linux, à l'énoncé des théorèmes et à Rocq lui-même.

Les bugs trouvés en chemin

Quand une preuve échoue, c'est souvent qu'il y a un bug. Claude a donc corrigé le code, puis repris la preuve. Anthropic cite notamment :

• un dépassement de compteur dans un décompresseur, qui menait à une écriture hors limites, mais seulement sur des entrées d'environ 20 Mo à la structure très précise ;
• une lecture hors limites dans un décodeur d'images, qui exigeait une entrée de 64 Mo et plus de 2 Go de mémoire ;
• une autre lecture hors limites déclenchée par une suite d'appels précise sur deux accès au même fichier ;
• la redécouverte de la faille CVE-2026-56132 de libexpat, qui demandait une entrée très imbriquée ;
• un bug de logique sans plantage : une option qui doit restreindre les fichiers qu'une application peut charger n'était pas toujours appliquée.

Ce sont des cas qu'un fuzzer, qui travaille d'habitude sur des entrées de moins de 1 Mo, avait très peu de chances de trouver.

Les autres essais

• zlib dans le noyau Linux : Claude a écrit une spécification formelle du format (RFC 1950), puis prouvé que l'implémentation du noyau la respecte, cette fois sur le binaire x86. Même exercice sur une demi-douzaine d'autres bibliothèques, avec quelques bugs mineurs non exploitables.
• Un interpréteur Python en Rust, prouvé conforme à une description académique de CPython avec l'outil Verus. Sur 1,7 million de programmes générés au hasard, il se comporte comme CPython dans 99,95 % des cas.
• Un lecteur PDF très répandu : en une semaine, autant de failles de sécurité trouvées que ce qui est d'habitude signalé en un an. Anthropic évoque aussi un bug de logique resté caché plus de dix ans dans une autre application critique, sans la nommer.

Le coût, et ses limites

Une preuve peut consommer des centaines de millions de tokens. Anthropic note que Claude Opus 5.5 réussit la moitié de 36 petites tâches de vérification avec environ 40 % de tokens de moins qu'Opus 5, et que des agents qui partagent leurs preuves en dépensent 17 % de moins que seuls.

Anthropic insiste aussi sur ce que « prouvé » ne veut pas dire :

1. Prouvé ne veut pas dire sans bug. La preuve vaut pour le modèle de la machine : un binaire RISC-V statique, monothread, lié à musl. La plupart des gens utilisent ces bibliothèques sur x86 ou ARM avec glibc.
2. Tout n'est pas couvert. AddressSanitizer ne voit pas toutes les erreurs mémoire, tous les points d'entrée n'ont pas été prouvés, et un programme peut toujours mal utiliser une bibliothèque.

Ce qui est publié

Anthropic publie une partie des preuves (celles qui ne révèlent pas de bug non corrigé), ainsi que les modèles de RISC-V et de Linux utilisés. Theorem propose de faire tourner la même chaîne pour d'autres projets open source, publie un skill Claude pour démarrer, et vise à terme l'écosystème Nix, glibc, OpenSSL et cURL compris.

L'enjeu dépasse la recherche : les IA trouvent désormais des failles plus vite qu'on ne les corrige, comme on l'a vu cette semaine avec la faille critique de GitLab ou les failles de PHP. Prouver l'absence de certains bugs devient une défense crédible. Côté OpenAI, la preuve formelle progresse aussi en mathématiques : voir les 722 manuscrits vérifiés en Lean.