Claude prouve 239 programmes sans plantage, mais sous conditions strictes

Anthropic et la société Theorem affirment avoir fait un pas vers la vérification formelle à grande échelle. Selon Anthropic, Claude a démontré, en quelques semaines, que 239 points d'entrée de 123 bibliothèques open source ne plantent sur aucune entrée de moins de 64 Mo. Les preuves portent sur le code assembleur RISC-V, et non sur le code source. L'entreprise y voit, à sa connaissance, le premier effort de cette ampleur sur des logiciels de production. Elle publie aussi un sous-ensemble des preuves.

Transformer des tests en spécification

La vérification formelle consiste à prouver mathématiquement qu'un programme respecte des règles définies. Elle est restée réservée aux cas extrêmes, comme le code avionique d'Airbus : d'après Anthropic, vérifier le noyau seL4 a demandé 20 années-personnes, contre deux pour l'écrire.

Le premier obstacle est de définir ce que « correct » veut dire. L'équipe a contourné le problème en convertissant les tests de fuzzing existants, issus de l'initiative OSS-Fuzz de Google, en spécification : « ce test ne plante jamais ». Si Claude le prouve, le fuzzing de ce point d'entrée ne trouvera plus rien sur RISC-V.

Les preuves, écrites en Rocq, totalisent environ 180 millions de lignes. Une preuve typique en compte environ 600 000, pour des binaires de 18 000 instructions en médiane. Selon Unite.AI, l'annexe d'Anthropic précise que Claude a écrit près d'un milliard de lignes, dont 180 millions seulement ont passé le vérificateur. Ce dernier rend la relecture humaine quasi inutile : il suffit de faire confiance aux modèles formels de RISC-V et de Linux, aux énoncés des théorèmes et au vérificateur lui-même.

Des bugs que le fuzzing aurait peu de chances de trouver

Claude pouvait corriger lui-même les bugs rencontrés avant de poursuivre sa preuve. Anthropic évoque des centaines de défauts. Selon Unite.AI, on y trouve une écriture hors limites déclenchée par une entrée d'environ 20 Mo avec une disposition rare, ou une lecture hors limites dans un décodeur d'image exigeant 64 Mo d'entrée et plus de 2 Go de mémoire. Les fuzzers mutent en général de petites entrées, plafonnées à 1 Mo, ce qui explique ces angles morts.

Autres résultats : un bug logique présent depuis plus de dix ans et, pendant la vérification d'un lecteur PDF très répandu, autant de bugs de sécurité en une semaine que ce qui est habituellement signalé en un an. The Decoder relaie ces chiffres, qui proviennent d'Anthropic et ne sont pas vérifiés de façon indépendante.

D'autres expériences ont été menées. Claude a prouvé l'implémentation de zlib du noyau Linux conforme à la RFC 1950, directement sur le binaire x86. Il a aussi écrit un interpréteur Python en Rust, prouvé avec Verus. Sur 1,7 million de programmes aléatoires, son comportement est identique à celui de CPython dans 99,95 % des cas.

« Vérifié » ne veut pas dire « sans bug »

Anthropic insiste sur les limites. Les preuves supposent un binaire statique, monothread, à budget mémoire fixe, sur CPU RISC-V avec Linux et la bibliothèque musl. La plupart des utilisateurs emploient x86 ou ARM avec glibc. De plus, AddressSanitizer ne détecte pas toutes les erreurs mémoire, et tous les points d'entrée n'ont pas été vérifiés.

Selon Anthropic, un vérificateur de preuves ne peut pas dire si la spécification correspond à la réalité, ce qui explique que « vérifié » ne signifie pas « sans bug ». Crypto Briefing abonde : selon ce média, une preuve ne vaut que par la propriété prouvée, et tout défaut de spécification subsiste.

Le coût est un autre point. Les preuves peuvent demander des centaines de millions de jetons, et The Decoder note qu'Anthropic ne donne pas le coût total du projet. Sur 36 petites tâches, Opus 5.5 résout la moitié d'entre elles avec environ 40 % de jetons en moins qu'Opus 5. Quand les agents peuvent se copier leurs preuves, ils en consomment 17 % de moins.

Ce qui est proposé aux projets open source

Selon Unite.AI, Theorem propose gratuitement le même procédé aux projets open source éligibles via son programme OSS Verify. Les mainteneurs reçoivent une preuve Rocq pour chaque cible de fuzzing, et les bugs trouvés leur sont signalés en privé, sans délai de divulgation. Une preuve peut demander plusieurs jours. La feuille de route de Theorem vise l'ensemble de l'écosystème Nix, dont glibc, OpenSSL et cURL. Reste à savoir si d'autres équipes parviendront à reproduire ces résultats, point que Crypto Briefing juge déterminant.