Anthropic affirme que Claude a prouvé que les bibliothèques open source 123 ne peuvent pas planter
Anthropic et Theorem ont utilisé Claude pour écrire 180 millions de lignes de preuves vérifiées par machine montrant que le code testé par fuzzing dans 123 bibliothèques open-source ne peut pas planter, et ont découvert au passage des bugs longtemps cachés.
Anthropic affirme que Claude a prouvé mathématiquement que le code testé par fuzzing dans 123 bibliothèques open-source ne peut pas planter sur une entrée inférieure à 64 Mo, et a trouvé au passage des bogues que des années de tests avaient manqués.
Le travail, publié par Anthropic le 22 octobre En collaboration avec la startup de vérification formelle Theorem, ce projet couvre 239 points d'entrée du projet OSS-Fuzz de Google. Anthropic le qualifie de premier effort à grande échelle visant à utiliser l'IA pour vérifier formellement des logiciels de production au niveau du code assembleur.
Des tests aux preuves
Le fuzzing consiste à soumettre un programme à un grand nombre d'entrées aléatoires pour identifier les points faibles, mais il est impossible de tester toutes les entrées. Anthropic a formalisé chaque test de fuzzing existant en une règle : “ ce test ne plante jamais ”, et Claude a prouvé que cette règle est valable pour toutes les entrées inférieures à 64 Mo.
Les démonstrations fonctionnent sur du code machine RISC-V compilé et non sur du code source. En quelques semaines, Claude a écrit environ 180 millions de lignes de démonstrations dans l'assistant de démonstration Rocq, soit environ 600 000 lignes pour un programme typique. Aucune intervention humaine n'est requise : le vérificateur Rocq valide automatiquement chaque démonstration.
Tests de bogues manqués
À chaque échec d'une épreuve, Claude décelait un bug, le corrigeait et recommençait. Selon Anthropic, cette démarche a permis de mettre au jour des centaines de bugs, dont une écriture hors limites dans un décompresseur qui n'apparaissait que sur des fichiers d'environ 20 Mo avec une configuration rare, ainsi que la redécouverte d'une faille connue dans l'analyseur XML libexpat.
Lors de tests distincts, Claude a prouvé que le code zlib du noyau Linux est conforme aux spécifications du format. De plus, en tentant de vérifier un lecteur PDF largement utilisé, il a découvert en une semaine autant de failles de sécurité que celles généralement signalées en une année. Plus de détails sont disponibles dans le annexe technique.
Ce que cela ne prouve pas
Anthropic précise que “ formellement vérifié ” ne signifie pas « sans bogues ». Les preuves supposent des binaires RISC-V monothread et liés statiquement sous Linux, alors que la plupart des déploiements réels s'exécutent sur x86 ou ARM. Les contrôles de mémoire utilisés ne détectent pas tous les bogues liés à la sécurité mémoire, et tous les points d'entrée de chaque bibliothèque n'ont pas été couverts.
Le coût est l'autre obstacle : les preuves peuvent nécessiter des centaines de millions de jetons. Anthropic indique que Claude Opus 5.5 a résolu la moitié d'un benchmark de 36 tâches avec environ 40% de jetons en moins qu'Opus 5, et que les agents partageant les preuves ont utilisé 17% de jetons en moins.
Pourquoi c'est important
L'IA devient très performante pour détecter les bugs, car Failles de PHP2Shell Des preuves ont été présentées cette semaine. Les démonstrations permettent de montrer que des catégories entières de bogues n'existent tout simplement pas. Theorem a publié un Claude compétence pour les responsables de projets open source qui souhaitent inscrire leurs projets, et il estimations que 95% du code machine dans l'écosystème logiciel Nix pourrait être vérifié d'ici la fin de 2027 pour environ 134 millions de dollars.
