La vérification formelle, qui consiste à prouver mathématiquement qu'un code se comporte comme spécifié, est depuis longtemps la référence en matière de sécurité, et trop coûteuse pour presque tout le monde. Anthropic donne un repère parlant : le noyau seL4 a demandé deux années-personnes d'écriture et 20 de vérification. Avec la société de vérification Theorem, Anthropic rapporte aujourd'hui que Claude a produit de telles preuves à une échelle impensable il y a quelques années.
L'astuce a été d'éviter d'écrire les spécifications à la main. L'équipe a pris des tests de fuzzing du programme OSS-Fuzz de Google, de petits points d'entrée où tout plantage compte comme un bogue, et a transformé chacun en énoncé formel : le binaire RISC-V compilé ne plante jamais, y compris sur les erreurs mémoire détectées par AddressSanitizer, pour toute entrée de moins de 64 Mo. En quelques semaines, Claude l'a prouvé pour 239 points d'entrée dans 123 bibliothèques, en corrigeant au passage les bogues trouvés. Les preuves, surtout écrites dans l'assistant de preuve Rocq, totalisent environ 180 millions de lignes, une preuve typique comptant quelque 600 000 lignes pour un binaire de 18 000 instructions en médiane. Personne n'a besoin de les lire ; le vérificateur de Rocq les valide.
Les bogues sont le bénéfice immédiat. Plusieurs étaient de ceux qu'un fuzzer trouve rarement, comme une écriture hors limites dans un décompresseur qui n'apparaissait qu'avec des entrées d'environ 20 Mo à la structure bien précise. D'autres expériences ont prouvé le zlib du noyau Linux par rapport à une version formelle de la RFC 1950 et vérifié un interpréteur Rust pour un sous-ensemble de Python, conforme à CPython sur 99,95 % de 1,7 million de programmes aléatoires. Le coût baisse aussi : sur 36 petites tâches, Claude Opus 5.5 en a prouvé la moitié avec environ 40 % de tokens en moins qu'Opus 5, et le partage de preuves entre agents a fait économiser 17 %.
Pour les mainteneurs, c'est la preuve la plus solide à ce jour que des garanties vérifiées par machine pourraient devenir courantes pour les bibliothèques répandues, comme l'est devenu le fuzzing. Theorem propose de faire tourner la chaîne pour d'autres projets open source et a publié une skill Claude.
Les auteurs sont prudents sur les limites, et les lecteurs doivent l'être aussi. Vérifié ne veut pas dire sans bogue. Les preuves portent sur des compilations RISC-V mono-fil, liées statiquement à musl, alors que la plupart des utilisateurs font tourner ces bibliothèques sur x86 ou ARM avec glibc. AddressSanitizer ne détecte pas toutes les erreurs mémoire, tous les points d'entrée n'ont pas été couverts, et un programme appelant peut encore mal utiliser une bibliothèque. Une preuve peut en outre coûter des centaines de millions de tokens, et c'est là le vrai frein à une application à tout l'écosystème.