Anthropic affirme que Claude a prouvé des propriétés de sécurité dans 123 bibliothèques open source

Anthropic a indiqué que ses modèles Claude pouvaient produire des preuves formelles des propriétés de sécurité dans du code compilé à travers 123 bibliothèques open source, un résultat que l’entreprise a décrit comme une étape vers la réalisation de la vérification logicielle formelle à une échelle bien plus large. Dans un article de recherche publié le 22 octobre 2026, Anthropic a indiqué que le travail a également révélé des bugs qui étaient restés inobservés pendant des années.

Preuves et contexte

Selon Anthropic, Claude a prouvé que 239 points d’entrée de ces bibliothèques 123 ne planteraient pas sur une entrée inférieure à 64 Mo dans les conditions modélisées du projet. La société a indiqué que les preuves étaient appliquées au niveau du code assembleur sur des binaires RISC-V et utilisaient la sémantique formelle de Theorem pour le comportement des processus RISC-V et Linux. Anthropic a indiqué que l’effort couvrait des logiciels open source réels, y compris des bibliothèques de l’initiative OSS-Fuzz de Google, et qu’il représente, à sa connaissance, la première utilisation à grande échelle de IA pour appliquer une vérification formelle aux logiciels de production au niveau du code assembleur.

La société a indiqué que les épreuves avaient été générées sur plusieurs semaines et que Claude corrigeait également des bugs rencontrés durant le processus. Parmi les exemples listés figuraient une écriture hors limites déclenchée par une disposition rare de 20 Mo, une lecture hors limites dans un décodeur d’image nécessitant une entrée de 64 Mo et plus de 2 Go de mémoire, un plantage lié à une séquence d’appels particulière sur deux handles de fichiers, et une redécouverte de CVE-2026-56132 dans libexpat. Anthropic a également indiqué que l’effort a révélé des bugs logiques qui ne faisaient pas planter le logiciel, notamment un cas où une restriction d’accès aux fichiers n’était pas toujours appliquée.

La société a indiqué que les démonstrations sont conditionnelles et n’impliquent pas que le logiciel soit exempt de bugs. Sa propre section sur les limitations précise que les garanties dépendent d’hypothèses modélisées, y compris des binaires statiques monothread avec un budget mémoire fixe fonctionnant sous RISC-V Linux, et que le travail ne couvre pas tous les points d’entrée ni toutes les façons dont le logiciel peut être utilisé en production. Anthropic a indiqué que l’incertitude restante se concentre dans les composants de confiance : la sémantique RISC-V et Linux, les énoncés théorèmes et le vérificateur de preuves Rocq.

Pourquoi cela compte

Anthropic a présenté ce travail comme une preuve que les LLM peuvent réduire le coût de la vérification formelle, qui a historiquement nécessité des efforts très spécialisés et a généralement été limitée à des systèmes critiques pour la mission. Le post indique que les modèles plus grands nécessitaient moins de jetons pour certaines tâches de vérification, tandis que les composants de preuve partagés réduisaient la duplication entre projets connexes. L’entreprise a également indiqué qu’elle prévoyait de publier un sous-ensemble des preuves et que Theorem offrira le même pipeline pour d’autres projets open source.

La recherche est cohérente avec des travaux industriels plus larges montrant que la vérification formelle peut compléter les tests plutôt que de les remplacer. Mais comme le note Anthropic lui-même, la valeur d’une preuve dépend toujours de la correspondance de la spécification et du modèle machine à la réalité, et de nombreuses hypothèses de déploiement restent hors du champ des affirmations vérifiées.