Le 22 octobre 2026, Anthropic a publié un compte rendu d’un travail mené avec Theorem : Claude a contribué à produire des preuves formelles d’absence de plantage pour 239 points d’entrée répartis dans 123 bibliothèques OSS-Fuzz. Ces preuves portent sur des entrées de moins de 64 Mo et sur un modèle précis de binaire RISC-V sous Linux. Elles ne couvrent pas, à elles seules, le comportement entier des bibliothèques.
La vérification formelle consiste à définir une propriété mathématique pour un programme, puis à prouver que le programme modélisé la respecte. Ici, la propriété examinée était l’absence de plantage pour les points d’entrée retenus, sous les hypothèses fixées pour l’expérience.
Comment la preuve est construite
Anthropic décrit un processus en trois étapes : des tests fuzz existants sont transformés en spécifications, Claude génère le code de preuve, puis le noyau Rocq vérifie cette preuve par rapport à la spécification. Le fuzzing consiste à faire exécuter un programme sur de nombreux entrées générées pour repérer des erreurs dans les cas testés. Une preuve formelle vise, elle, tous les comportements couverts par le modèle et la propriété définis.
Theorem a fourni les sémantiques des instructions RISC-V et des processus Linux utilisées dans ce modèle. Le vérificateur Rocq contrôle que la preuve découle de la spécification ; ce contrôle ne garantit pas que la spécification décrit tous les comportements réels ou toutes les exigences d’une bibliothèque.
Ce que couvrent les 239 points d’entrée
La propriété porte sur des entrées de moins de 64 Mo et sur un binaire RISC-V statique, monothread, doté d’un budget mémoire fixe et exécuté selon le modèle de processus Linux retenu. Anthropic rapporte une longueur médiane de 18 000 instructions RISC-V pour les binaires concernés.
Les 239 points d’entrée ne représentent pas toutes les voies d’accès aux 123 bibliothèques : Anthropic précise que tous les points d’entrée de chaque bibliothèque n’ont pas été vérifiés et que les points retenus ne couvrent pas nécessairement tout son comportement. Le résultat porte donc sur une propriété précise de chemins sélectionnés, dans cette configuration, et non sur une certification générale des bibliothèques.
Les bogues signalés pendant les tentatives de preuve
Anthropic indique que Claude a aussi corrigé des bogues rencontrés pendant le travail, puis que les spécifications ont été régénérées sur le code modifié. Parmi les exemples rapportés, un décompresseur subissait un sous-débordement de compteur pouvant provoquer une écriture hors limites avec une disposition rare des données d’entrée, autour de 20 Mo. Un décodeur d’images présentait une lecture hors limites avec une entrée de 64 Mo et plus de 2 Go de mémoire.
Anthropic signale également une lecture hors limites qui nécessitait une séquence particulière d’appels sur deux descripteurs du même fichier, ainsi que la redécouverte de CVE-2026-56132 dans libexpat avec une entrée profondément imbriquée. Un autre bogue concernait la logique d’une fonction limitant les fichiers qu’une application pouvait charger.
Pourquoi une preuve formelle ne certifie pas une bibliothèque entière
Une preuve vérifiée établit que le programme modélisé satisfait la propriété écrite dans la spécification, sous les hypothèses du modèle. Le résultat dépend donc aussi de la justesse de cette spécification et des sémantiques de la machine et du système d’exploitation. Le modèle de l’expérience principale décrit des binaires statiques monothreads sur RISC-V ; il ne représente pas automatiquement toutes les configurations de déploiement, notamment celles reposant sur d’autres architectures ou sur l’édition de liens dynamique.
La couverture compte aussi. Du code non atteint depuis les points d’entrée vérifiés reste en dehors de ces preuves, et un appelant peut utiliser une bibliothèque d’une manière qui n’est pas couverte par la propriété. Anthropic précise par ailleurs qu’AddressSanitizer, l’outil d’exécution utilisé pour détecter certains problèmes de mémoire dans du code C et C++, ne repère pas tous les défauts de sûreté mémoire.
Ce que l’annexe ajoute sur les preuves et Python
L’annexe distingue environ un milliard de lignes Rocq générées au fil des tentatives des quelque 180 millions de lignes intégrées aux preuves qui ont passé le contrôle. Une preuve achevée typique comptait environ 600 000 lignes réparties sur quelque 1 400 fichiers ; sa vérification pouvait prendre de 30 minutes à plusieurs heures de calcul CPU.
Dans une étude distincte, Verus a vérifié les 17 niveaux d’un interpréteur Python écrit en Rust par rapport à la sémantique formelle du projet. La comparaison avec CPython était empirique : Anthropic rapporte un comportement identique dans 99,95 % de plus de 1,7 million de programmes générés. Ce résultat décrit les programmes comparés ; il ne constitue pas une preuve d’équivalence pour tous les programmes Python.
