Anthropic et la société Theorem ont utilisé Claude pour produire des preuves formelles portant sur 239 points d’entrée de 123 bibliothèques open source. L’expérience représente environ 180 millions de lignes de preuves Rocq et vise à vérifier, au niveau du code assembleur RISC-V, que certains programmes ne peuvent pas planter dans les conditions testées.
La publication technique d’Anthropic, mise en ligne le 22 octobre, décrit un passage du test statistique à la preuve mathématique. Au lieu de lancer toujours plus d’entrées aléatoires avec un outil de fuzzing, les chercheurs transforment les tests existants en spécifications. Claude doit ensuite construire une preuve que le binaire compilé respecte ces propriétés pour toutes les entrées prévues par le modèle.
Des garanties ciblées sur 123 bibliothèques
L’équipe a travaillé sur des projets présents dans OSS-Fuzz, l’infrastructure de Google qui teste en continu des logiciels open source. Claude a prouvé des propriétés pour 239 points d’entrée répartis dans 123 bibliothèques. L’objectif principal consistait à montrer que les exécutables concernés ne déclenchaient ni erreur de sûreté mémoire ni assertion, pour des entrées allant jusqu’à 64 Mo.
Ces résultats ne signifient pas que les logiciels sont exempts de tout défaut. Les preuves s’appliquent à un cadre précis : binaires RISC-V, processus Linux modélisé, exécution mono-thread et budget mémoire défini. Une erreur dans les modèles formels, le vérificateur Rocq ou les hypothèses retenues resterait également hors du périmètre démontré.
Le volume est néanmoins inhabituel. Anthropic indique que les preuves totalisent environ 180 millions de lignes de Rocq, avec une médiane proche de 600 000 lignes par preuve. Le vérificateur de preuves contrôle mécaniquement leur validité, ce qui évite une relecture humaine ligne par ligne.
Claude a aussi trouvé puis corrigé des bogues
La tentative de preuve a révélé des erreurs que le fuzzing avait peu de chances d’atteindre. Anthropic cite notamment un dépassement de compteur menant à une écriture hors limites avec une entrée d’environ 20 Mo, ainsi qu’une lecture hors limites exigeant une entrée de 64 Mo et plus de 2 Go de mémoire. Claude a proposé des correctifs avant de reprendre la construction des preuves.
Les auteurs publient un sous-ensemble des preuves, les modèles RISC-V et Linux utilisés, ainsi qu’un skill Claude destiné à aider les développeurs à appliquer la méthode à d’autres projets. Cette ouverture doit permettre une vérification indépendante des artefacts et des hypothèses.
Notre analyse
Le résultat déplace la question de la sécurité assistée par IA. Un modèle ne sert plus seulement à repérer des anomalies ou à suggérer un correctif : il produit ici un objet mathématique qu’un noyau de preuve peut accepter ou rejeter. Cette séparation est importante, car la confiance ne repose pas uniquement sur la réponse du modèle.
La portée reste toutefois étroite et le coût élevé. Anthropic évoque des centaines de millions de jetons pour certaines campagnes. La méthode ne remplace donc ni la revue de code ni les tests, mais elle pourrait rendre la vérification formelle accessible à davantage de composants critiques si les preuves deviennent moins coûteuses et réutilisables.
