Anthropic avance un résultat spectaculaire sur un vieux rêve de l'informatique. Dans des travaux publiés le 22 octobre, l'entreprise explique que Claude, épaulé par les outils de la start-up Theorem, a produit des preuves formelles établissant qu'un vaste ensemble de code open source réel ne plante pas dans les conditions testées par ses propres développeurs. La vérification formelle restait jusqu'ici l'apanage de l'avionique, des noyaux de systèmes d'exploitation et des logiciels justifiant des années de travail d'experts. Selon Anthropic, les modèles de langage la mettent désormais à la portée de bibliothèques ordinaires.
Tout part des tests de fuzzing du programme OSS-Fuzz de Google. Un fuzzer bombarde un point d'entrée de très nombreuses entrées modifiées et signale celles qui provoquent un plantage, y compris les erreurs mémoire repérées par AddressSanitizer. Cette exploration ne peut jamais être exhaustive. Les chercheurs ont donc converti chaque harnais en énoncé mathématique : le programme compilé ne plante pour aucune entrée de moins de 64 Mo. Il revenait à Claude de le démontrer dans l'assistant de preuve Rocq, à l'aide des modèles formels des instructions RISC-V et du comportement des processus Linux fournis par Theorem.
D'après le billet, Claude a bouclé en quelques semaines les preuves de 239 points d'entrée répartis dans 123 bibliothèques. L'ensemble représente environ 180 millions de lignes de Rocq, une preuve type atteignant quelque 600 000 lignes pour un binaire d'environ 18 000 instructions. Inutile de les relire, assure l'entreprise, puisque le noyau de Rocq contrôle mécaniquement chaque étape. La confiance se réduit aux modèles RISC-V et Linux, aux énoncés exacts des théorèmes et au vérificateur lui-même. Les garanties reposent aussi sur des hypothèses, notamment un binaire statique à fil d'exécution unique et à mémoire fixe.
Ces tentatives de preuve ont aussi servi de chasse aux bugs. Chaque fois qu'il rencontrait un plantage atteignable, Claude corrigeait le code puis reprenait, et Anthropic indique que la démarche a révélé des centaines de défauts. Parmi eux figurent une écriture hors limites dans un décompresseur embarqué, déclenchée seulement par des entrées d'environ 20 Mo, une lecture fautive dans un décodeur d'images exigeant un fichier de 64 Mo et plus de 2 Go de mémoire, ainsi que la redécouverte d'une faille connue de libexpat. Les fuzzers, qui plafonnent généralement les entrées vers 1 Mo, n'atteindraient presque jamais ces cas.
Des expériences annexes vont plus loin encore. Claude a rédigé une spécification formelle du format zlib décrit par la RFC 1950 et démontré que le code zlib du noyau Linux s'y conforme, cette fois sur des binaires x86. Il a également écrit en Rust un interpréteur couvrant une large part de Python, prouvé sa conformité à un modèle universitaire de CPython avec l'outil Verus, et obtenu un comportement identique sur 99,95 % de 1,7 million de programmes aléatoires. Sur un lecteur PDF très répandu, il aurait trouvé en une semaine autant de failles de sécurité qu'on en signale habituellement en un an.
Le coût reste le principal frein, certaines preuves engloutissant des centaines de millions de tokens. Anthropic rapporte que Claude Opus 5.5 a résolu la moitié d'un banc d'essai de 36 tâches de vérification avec environ 40 % de tokens en moins qu'Opus 5, et que des agents partageant un espace de preuves réutilisables ont encore économisé 17 %. Theorem compte proposer la chaîne à d'autres projets open source et a publié une feuille de route visant l'écosystème Nix, dont glibc, OpenSSL et cURL.
Anthropic publie les nouveaux modèles de confiance, les preuves complètes des harnais qui n'ont exigé aucun correctif et les spécifications de ceux restés non prouvés, en retenant tout ce qui pourrait dévoiler des failles non corrigées. L'entreprise rappelle qu'une preuve ne vaut que par sa spécification : si le modèle de la machine est faux, un code vérifié peut tout de même défaillir. Aucun chercheur indépendant n'a encore eu le temps d'auditer ces éléments, si bien que les chiffres restent pour l'instant ceux de l'entreprise.