Anthropic affirme que Claude a rédigé des preuves formelles démontrant que 123 bibliothèques open source ne peuvent pas planter

En collaboration avec Theorem, Anthropic affirme avoir utilisé Claude pour prouver des propriétés de sécurité au niveau assembleur (RISC-V) dans plus de 100 bibliothèques open source utilisées dans le monde réel. L’entreprise présente ce travail comme la première utilisation à grande échelle de l’IA pour vérifier formellement des logiciels en production à ce niveau.

Selon Anthropic :

• Ce qui a été prouvé : pour 239 points d’entrée de tests de fuzzing répartis dans 123 bibliothèques OSS-Fuzz, les programmes se terminent toujours normalement, sans erreur de sûreté mémoire ni assertion échouée, quelle que soit l’entrée de moins de 64 MB. Cela vaut sous certaines hypothèses : un binaire statique monothread avec une limite mémoire fixe, exécuté sur un processeur RISC-V sous Linux. Les preuves représentent environ 180 millions de lignes de Rocq, vérifiées par le vérificateur de preuves Rocq.
• Comment : le test de fuzzing existant de chaque bibliothèque a été transformé en spécification (« ce test ne plante jamais »), puis Claude a rédigé la preuve en corrigeant au passage les bogues découverts. Anthropic affirme que cela a permis de trouver des centaines de bogues, y compris des cas qu’un fuzzer aurait probablement eu du mal à atteindre, comme une écriture hors limites nécessitant une rare entrée de 20 MB, ainsi qu’une redécouverte de CVE-2026-56132 dans libexpat.
• Autres expériences : Claude a prouvé que l’implémentation de zlib du noyau Linux correspond à une spécification de la RFC 1950 au niveau du binaire x86, et a créé un interpréteur Python en Rust dont le comportement correspondait à CPython dans 99,95 % de 1,7 million de programmes aléatoires. Anthropic indique également que les tentatives de vérification formelle d’un lecteur PDF très répandu ont révélé en une semaine autant de bogues de sécurité qu’on en signale généralement en un an.
• Coût : les preuves peuvent nécessiter des centaines de millions de tokens. Sur 36 petites tâches de vérification, Anthropic affirme qu’Opus 5.5 en réussit la moitié avec environ 40 % de tokens en moins qu’Opus 5, et que des agents partageant leurs preuves ont eu besoin de 17 % de tokens en moins.

Anthropic publie une partie des preuves ainsi que les sémantiques de RISC-V et de Linux. Theorem propose d’exécuter le même pipeline pour d’autres projets open source et publie un skill Claude pour vérifier votre propre code. Anthropic précise que cela ne prouve pas que les bibliothèques sont exemptes de bogues : les bogues restants se trouveraient dans les composants de confiance ou hors du périmètre des preuves.