Le Frontier Red Team d'Anthropic a publié le 22 octobre une étude dans laquelle Claude a rédigé des preuves formelles pour 239 points d'entrée de 123 bibliothèques open source : tant que l'entrée fait moins de 64 Mo, ces programmes ne plantent pas. Les preuves portent directement sur les exécutables RISC-V compilés, avec pour partenaire Theorem, une société d'outils de vérification formelle. Selon Anthropic, c'est la première fois qu'une IA mène à grande échelle une vérification formelle au niveau assembleur sur des logiciels de production.
Toutes ces bibliothèques proviennent du projet OSS-Fuzz de Google, c'est-à-dire ces composants de base qui tournent depuis longtemps sur la plateforme de fuzzing ; on y trouve de la compression, du décodage d'images et de l'analyse HTTP. L'ensemble du chantier a pris quelques semaines.
Transformer le fuzzing en théorèmes
La méthode comporte trois étapes. D'abord, l'équipe a réécrit la suite de tests de fuzzing existante de chaque bibliothèque sous forme de spécification formelle, qui dit en substance : « ce code de test ne plante pour aucune entrée ». La spécification repose sur les modèles de sémantique des instructions RISC-V et de sémantique des processus Linux fournis par Theorem.
Ensuite, Claude rédige la preuve, que le vérificateur de preuves Rocq contrôle pas à pas.
« Claude writes the proof; the Rocq kernel checks it against the specification. » (Claude écrit la preuve ; le noyau Rocq la vérifie par rapport à la spécification.)
La troisième étape traite le cas où la preuve ne passe pas. Une preuve qui bloque signale souvent un vrai défaut dans le code ; Claude modifie alors lui-même le code, la spécification est régénérée et la preuve reprend. L'équipe admet que cette étape se prête au « reward hacking » : le modèle pourrait modifier le programme à la légère pour que la preuve aboutisse. Les correctifs ont donc été assortis d'une pénalité, il faut prouver la plage d'entrées qu'un correctif affecte, et chacun est consigné puis audité à la main.
Une preuve typique compte environ 600 000 lignes. Au final, il ne reste à croire que les modèles de sémantique de RISC-V et de Linux, l'énoncé du théorème lui-même et le vérificateur Rocq.
Les failles débusquées en cours de preuve
Plusieurs centaines de failles ont été trouvées et corrigées en chemin, dont certaines que le fuzzing aurait du mal à faire apparaître. L'article en cite quelques-unes : un dépassement par le bas d'un compteur dans un décompresseur, qui ne se déclenche qu'avec certaines entrées d'environ 20 Mo ; une lecture hors limites dans un décodeur d'images, qui exige 64 Mo d'entrée et plus de 2 Go de mémoire ; et une autre lecture hors limites qui demande que deux handles opèrent sur le même fichier dans un ordre précis. La CVE-2026-56132 de libexpat a également été redécouverte.
La preuve de cpp-httplib comportait un obstacle supplémentaire : la récursion lors de la destruction d'un std::set peut provoquer un débordement de pile. Pour l'écarter, l'équipe a prouvé au niveau du code machine que l'algorithme d'équilibrage de l'arbre rouge-noir de libc++ maintient la profondeur de l'arbre à une échelle logarithmique.
La même étude comprend aussi quelques expériences annexes. Claude a écrit en Rust un sous-ensemble de Python et a prouvé avec Verus qu'il respecte la sémantique de CPython ; sur 1,7 million de programmes aléatoires, son comportement coïncide avec celui de CPython dans 99,95 % des cas. Il a aussi généré de lui-même une sémantique d'instructions x86 qui, en exécution pas à pas, permet de démarrer l'espace utilisateur d'Ubuntu, et il a relevé au passage plusieurs centaines d'erreurs dans la documentation de référence officielle.
À mettre en regard de seL4
La vérification formelle n'a rien de nouveau dans l'industrie ; la difficulté a toujours été la main-d'œuvre. On cite souvent le micronoyau seL4 : environ dix mille lignes de C, pour un effort de preuve généralement évalué à une vingtaine d'années-personnes. Le compilateur CompCert suit une voie similaire, peaufiné pendant des années par une petite équipe. Ces projets ont en commun peu d'objets, de longs cycles et une forte densité d'experts.
L'échelle d'Anthropic cette fois : 123 bibliothèques en quelques semaines ; en comparaison grossière, la structure de coût par unité de travail a pris une autre forme, l'humain passant de la rédaction des preuves à la définition des spécifications et à la relecture des correctifs. Le coût s'est déplacé vers les tokens : l'article indique qu'une preuve complète peut consommer des centaines de millions de tokens. Sur les 36 petites tâches, chaque tâche donnait à un seul agent trois essais avec un budget de 5 millions de tokens chacun ; lorsque les agents ont été autorisés à réutiliser les preuves des autres, les tokens nécessaires ont encore baissé de 17 %.
La solidité des garanties n'est pas non plus du même ordre. seL4 prouve la correction fonctionnelle ; ici, on prouve seulement « ne plante pas », un périmètre bien plus étroit.
Les trous au-delà de la preuve
Les limites que dresse Anthropic elle-même sont assez précises. Les preuves portent sur des binaires RISC-V mono-thread, liés statiquement et utilisant musl libc, alors que la plupart des utilisateurs font tourner des versions x86 ou ARM avec glibc liée dynamiquement. AddressSanitizer ne détecte pas à lui seul toutes les erreurs de sécurité mémoire, certains points d'entrée ne sont pas couverts, et la corruption de mémoire causée par un mauvais usage de la bibliothèque côté appelant échappe elle aussi à la preuve.
« “Formally verified” does not mean “bug-free.” » (« Formellement vérifié » ne veut pas dire « sans bug ».)
L'écart entre la spécification et la machine réelle est l'endroit où cette voie risque le plus de dérailler. Rocq et les modèles de sémantique doivent eux aussi être durcis, ce que l'article qualifie de « loin d'être anodin ». L'équipe estime que la vérification formelle deviendra une étape courante du développement de logiciels sûrs ; quant à savoir quand ces preuves couvriront des environnements de déploiement courants comme x86 et glibc, l'article ne donne aucune échéance.
Sources : article de recherche du Frontier Red Team d'Anthropic, CocoLoop ; la page de recherche d'Anthropic a servi à recouper le nombre de bibliothèques, de points d'entrée, de lignes de preuve et la base de comparaison des tokens.