Ce qui a réellement été prouvé
La Frontier Red Team d’Anthropic, avec Theorem, a publié le 22 octobre les résultats d’une tentative d’utiliser Claude pour la vérification formelle à grande échelle. L’équipe a repris des tests de fuzzing existants d’OSS-Fuzz, de Google, a traité chaque test comme une propriété que le code doit satisfaire, l’a compilé en assembleur RISC-V, et a fait écrire à Claude des preuves vérifiées par machine que le binaire obtenu ne plante jamais.
La propriété est étroite et précise : pour toute entrée inférieure à 64 Mo, le programme ne plantera pas sur une erreur de sûreté mémoire ni sur une assertion échouée. Les preuves supposent un binaire statique monothread doté d’un budget mémoire fixe, tournant sur un processeur RISC-V sous Linux, et font confiance au vérificateur Rocq, aux sémantiques RISC-V et de processus Linux de Theorem, ainsi qu’au matériel et au compilateur OCaml sous-jacents.
Les chiffres
Sur 123 bibliothèques libres, Claude a prouvé que 239 points d’entrée sont exempts de plantage selon cette spécification. Les preuves totalisent environ 180 millions de lignes de Rocq. Une preuve type fait quelque 600 000 lignes, pour une longueur médiane de binaire d’environ 18 000 instructions RISC-V. Le travail a pris quelques semaines.
Anthropic ne dit pas combien de points d’entrée ont été tentés au total : les chiffres ne permettent donc aucun taux de réussite. L’entreprise indique publier les preuves des tests qui n’ont demandé aucun correctif, et les spécifications de ceux qu’elle n’a pas réussi à prouver.
Des centaines de bogues sont apparus en chemin, et Claude les a corrigés, ce qui régénérait les spécifications. Parmi les exemples cités : un dépassement inférieur de compteur dans un décompresseur provoquant une écriture hors limites seulement sur un agencement rare d’environ 20 Mo d’entrée, une lecture hors limites dans un décodeur d’images exigeant une entrée de 64 Mo et plus de 2 Go de mémoire, et une redécouverte de CVE-2026-56132 dans libexpat. L’un d’eux était une restriction de fichiers pas toujours appliquée : un bogue logique qui ne plante jamais, latent depuis plus de dix ans.
La triche évidente, et ce qu’ils en ont fait
Le dispositif comporte une faille que l’équipe nomme elle-même. Claude pouvait rendre un théorème démontrable en réécrivant le programme pour qu’il ne plante jamais. Anthropic indique avoir pénalisé les correctifs modifiant le comportement, accordé un crédit supplémentaire pour la démonstration des entrées qu’un correctif change, et journalisé et audité chaque correctif.
Le problème ouvert, c’est le coût
Sur un banc de 36 petites tâches de vérification bâties à partir de vrai code OSS-Fuzz, avec trois tentatives indépendantes dotées chacune de cinq millions de jetons, Opus 5.5 en a prouvé la moitié avec environ 40 % de jetons en moins qu’Opus 5. Les agents autorisés à copier les preuves des autres depuis un espace partagé ont consommé 17 % de jetons en moins et achevé 34 des 36, contre 32 pour les agents travaillant seuls.
Anthropic est explicite sur les limites. « Formellement vérifié » ne veut pas dire exempt de bogues : un vérificateur ne peut confirmer que la spécification correspond à la réalité, et des bogues peuvent subsister dans la spécification, le modèle de machine ou la base de confiance. Les preuves portent sur des binaires RISC-V liés à musl, alors que la plupart des déploiements tournent en x86 ou ARM avec une glibc liée dynamiquement. Et une seule preuve peut coûter des centaines de millions de jetons, ce que l’entreprise qualifie de problème ouvert majeur.
Par ailleurs, Claude a rédigé une spécification à partir du RFC 1950 et prouvé que l’implémentation zlib du noyau Linux la respecte au niveau du binaire x86. Anthropic dit avoir répété l’opération pour environ six autres bibliothèques très utilisées. Savoir si ce travail x86 se généralise est ce qu’il faudra suivre.
