Claude vérifie mathématiquement 123 bibliothèques logicielles et découvre des centaines de bugs

Anthropic et Theorem utilisent Claude pour produire des preuves formelles sur 123 bibliothèques open source et détecter des bugs échappant aux tests.

Des milliards de tests ne suffisent pas toujours à garantir qu'un programme fonctionnera correctement. Certains défauts nécessitent une combinaison d'événements trop rare pour être rencontrée, même après plusieurs années de vérifications automatisées. Anthropic et l'entreprise spécialisée Theorem ont utilisé Claude pour produire des preuves mathématiques portant sur 239 points d'entrée de 123 bibliothèques open source, afin de garantir l'absence de certains plantages dans des conditions précisément définies. L'expérience a mobilisé plusieurs agents pendant quelques semaines, généré environ 180 millions de lignes de preuves formelles et révélé des centaines de bugs, dont certains avaient échappé à des milliers de milliards d'exécutions de tests. Quand les tests ne suffisent plus à trouver les bugs

Dans le développement logiciel, la recherche d'erreurs repose largement sur l'exécution de tests. Les équipes définissent des scénarios, vérifient les résultats et cherchent à provoquer des comportements inattendus. Le fuzzing automatise une partie de ce processus en soumettant à un programme un grand nombre d'entrées aléatoires ou modifiées. Cette technique est notamment utilisée par OSS-Fuzz, le projet de Google consacré à la détection continue de vulnérabilités dans les logiciels open source.

Le fuzzing peut révéler des erreurs de mémoire, des plantages ou des violations de propriétés définies par les développeurs. Mais son efficacité dépend des entrées générées et des chemins d'exécution réellement explorés. Même après des milliards de tentatives, rien ne garantit qu'un ensemble particulier de données, susceptible de provoquer une défaillance, aura été testé.

La vérification formelle répond à un problème différent. Elle consiste à transformer le comportement d'un programme et certaines exigences en objets mathématiques, puis à démontrer que ces exigences sont satisfaites dans toutes les situations couvertes par le modèle. Plutôt que d'exécuter un nombre fini d'exemples, elle cherche à établir une propriété valable pour tout un ensemble d'entrées.

Cette méthode existe depuis longtemps, mais sa mise en œuvre exige une expertise considérable. Anthropic rappelle notamment que le noyau du système d'exploitation seL4 avait nécessité environ deux années-personnes de développement, contre vingt pour sa vérification formelle. La rédaction des preuves, souvent bien plus volumineuses que le code étudié, limitait jusqu'ici leur utilisation aux systèmes où les exigences de sécurité justifiaient un investissement exceptionnel. Transformer les tests existants en propriétés mathématiques

Pour éviter d'avoir à rédiger manuellement une spécification complète de chaque logiciel, les chercheurs ont exploité les tests de fuzzing déjà maintenus par les développeurs. Chaque test définit un point d'entrée : une partie du programme capable de recevoir des données et de déclencher une erreur lorsqu'une propriété importante n'est pas respectée.

Anthropic et Theorem ont converti ces tests en spécifications formelles. Dans leur configuration principale, la propriété recherchée revient à démontrer qu'un programme compilé ne provoquera aucun plantage pour une entrée inférieure à 64 Mo, quelles que soient les données reçues et les réponses du système d'exploitation prises en compte par le modèle. Cette garantie englobe notamment certaines erreurs d'accès mémoire détectées par AddressSanitizer et les assertions présentes dans les tests.

Le travail s'effectue au niveau du code machine RISC-V, et non simplement sur le code source. Les bibliothèques et leurs tests sont compilés, puis leurs instructions sont traduites en une représentation mathématique à l'aide des modèles d'exécution développés par Theorem. Claude reçoit cette représentation, les propriétés à démontrer et les outils nécessaires pour construire la preuve.

Cette approche permet de travailler directement sur le comportement du programme compilé, sans exiger que les bibliothèques soient réécrites dans un langage de programmation conçu pour la vérification. Les preuves sont rédigées avec Rocq, anciennement Coq, un assistant de preuve capable de vérifier mécaniquement que chaque étape satisfait les règles logiques attendues. 180 millions de lignes de preuves vérifiées automatiquement

L'expérience porte sur 239 points d'entrée appartenant à 123 bibliothèques intégrées à OSS-Fuzz. Les chercheurs annoncent environ 180 millions de lignes de preuves Rocq, produites sur quelques semaines. Une preuve typique atteint près de 600 000 lignes et porte sur un binaire contenant une médiane de 18 000 instructions RISC-V.

Le volume est considérable, mais il ne nécessite pas une relecture humaine ligne par ligne. Claude construit les preuves ; le noyau de vérification de Rocq contrôle ensuite qu'elles démontrent effectivement les propriétés formulées. Les auteurs peuvent ainsi utiliser une IA générative pour produire un raisonnement volumineux tout en confiant la validation logique à un logiciel spécialisé.

La garantie repose néanmoins sur plusieurs éléments de confiance : la formulation exacte des propriétés, les modèles mathématiques du processeur et du système d'exploitation, ainsi que le vérificateur Rocq. Une preuve acceptée établit que le programme respecte la propriété définie dans cet environnement modélisé, pas qu'il est universellement exempt de défauts.

Anthropic publie une partie des preuves et des composants techniques permettant de les vérifier ou de les réutiliser. Les éléments susceptibles de révéler des vulnérabilités encore non corrigées ne sont pas rendus publics. Theorem propose également d'appliquer cette méthode à d'autres projets open source. Des bugs cachés dans des situations presque impossibles à tester

La construction des preuves a elle-même permis de découvrir des anomalies. Lorsqu'un agent ne parvenait pas à démontrer qu'un programme ne pouvait pas planter, il pouvait explorer les conditions responsables de l'échec, identifier un défaut et proposer une correction.