Claude vérifie formellement 123 bibliothèques open source
Anthropic indique que Claude a produit 239 preuves couvrant 123 bibliothèques du projet OSS-Fuzz de Google, avec le partenaire Theorem.
Anthropic a annoncé le 22 octobre que Claude avait servi à vérifier formellement les propriétés de sécurité de 123 bibliothèques open source enregistrées dans le projet OSS-Fuzz de Google, en collaboration avec Theorem, spécialiste des preuves formelles. L'information a été rapportée par aitimes.com.
Le modèle a mené à bien les preuves de 239 points d'entrée de test répartis sur ces 123 bibliothèques. L'objectif : établir que les tests se terminent sans plantage pour toutes les entrées inférieures à 64 Mo, sans erreur de sûreté mémoire ni échec d'assertion.
Les preuves générées totalisent 180 millions de lignes au format de l'assistant de preuve Rocq ; une preuve médiane couvre un binaire d'environ 18 000 instructions RISC-V. Claude a par ailleurs détecté des centaines de bugs pendant le processus, corrigé le code puis re-prouvé les corrections, notamment un sous-dépassement de compteur dans un décompresseur et une lecture hors limites dans un décodeur d'images. Les travaux ont aussi redécouvert la CVE-2026-56132 dans la bibliothèque d'analyse XML libexpat.
Anthropic présente cette opération comme la première vérification à grande échelle par IA des propriétés de sécurité d'un logiciel de production au niveau du code assembleur. L'entreprise a publié une partie des preuves et le modèle utilisé, et Theorem propose son accompagnement pour appliquer la même démarche à d'autres projets open source.
La vérification formelle a longtemps été réservée aux logiciels critiques, comme l'avionique ou les noyaux de systèmes d'exploitation, en raison du temps et de l'expertise qu'elle exige : en 2025, la vérification du micro-noyau seL4 avait demandé environ 20 années-personnes, pour 2 années-personnes de mise en œuvre. Anthropic cite aussi d'autres essais, dont une preuve au niveau binaire montrant que l'implémentation de compression zlib du noyau Linux est conforme à sa spécification.
Un test comparatif entre Opus 5.5 et Opus 5
Dans une expérience distincte, Opus 5.5 a résolu la moitié de 36 tâches de vérification en consommant environ 40 % de tokens de moins qu'Opus 5, et la collaboration entre agents a réduit l'usage de tokens de 17 %.
En bref
Qu'a annoncé Anthropic le 22 octobre ?
La vérification formelle des propriétés de sécurité de 123 bibliothèques open source d'OSS-Fuzz par Claude, avec Theorem, soit 239 preuves.
Quels bugs ont été trouvés pendant les preuves ?
Des centaines de bugs, dont un sous-dépassement de compteur dans un décompresseur, une lecture hors limites dans un décodeur d'images, et la redécouverte de la CVE-2026-56132 dans libexpat.
Les preuves sont-elles publiées ?
Anthropic a publié une partie des preuves et le modèle utilisé ; Theorem propose son aide pour appliquer la méthode à d'autres projets.