Anthropic et Theorem ont fait produire à Claude des preuves formelles sur du code existant, couvrant 123 bibliothèques. L’opération a mis au jour des centaines de bugs et nourrit l’ambition de banaliser la vérification formelle par l’IA, malgré des contraintes strictes et un coût de calcul élevé.
Validité limitée et coût de calcul élevé annoncés
Anthropic précise qu’un logiciel « vérifié formellement » n’est pas exempt d’erreurs. Les preuves générées ne sont valables que dans des conditions strictes : une architecture de processeur donnée, des programmes mono-thread et des entrées inférieures à 64 Mo. En réalité, les bibliothèques concernées fonctionnent sur des matériels et configurations variés. Chaque preuve nécessite des centaines de millions de tokens, et Anthropic ne communique pas le coût total du projet. Même lorsque la preuve complète échoue, Anthropic indique que la tentative permet de découvrir de véritables bugs. Lors de la vérification d’un lecteur PDF largement utilisé, l’équipe a identifié en une semaine autant de failles de sécurité qu’en une année habituelle de signalements pour ce logiciel. Dans un autre cas, Claude a détecté une erreur logique restée inaperçue pendant plus de dix ans.
Résultats obtenus sur 123 bibliothèques open-source
En quelques semaines, Claude a généré environ 180 millions de lignes de code de preuve couvrant 123 bibliothèques open-source, en s’appuyant sur des programmes de test issus du projet OSS-Fuzz de Google. Le modèle a permis d’identifier plusieurs centaines de bugs qui n’avaient pas été découverts par les méthodes de test traditionnelles. Pendant la production des preuves, Claude a eu la possibilité d’apporter lui-même des corrections aux défauts repérés, dont un grand nombre ne se manifestent que dans des cas très particuliers, comme des fichiers d’entrée extrêmement grands ou des modes d’accès inhabituels, d’après les chercheurs.
Vous codez avec l’IA ?
Outils, agents et nouveautés dev IA décryptés, chaque soir en 5 min. Gratuit.
Inclus dès l'inscription : notre sélection des meilleurs guides & comparatifs IA.
Choisissez votre rythme
Gratuit · Pas de spam · Désabonnement en 1 clic
Méthode employée et degré d’autonomie revendiqué
Plutôt que de produire du code neuf, Claude a traduit des tests de plantage en problèmes mathématiques, analysé le code machine compilé, puis généré des preuves détaillées. Un vérificateur indépendant, Rocq, contrôle automatiquement ces preuves. Selon Anthropic, la procédure requiert très peu d’examen humain, et les chercheurs parlent d’une génération de preuves « entièrement autonome ». Les outils et fondations formelles ont cependant été conçus par des ingénieurs de Theorem. Ce dispositif a été mis en place par l’équipe Frontier Red Team d’Anthropic avec Theorem, pour appliquer Claude à la vérification mathématique de code existant.
Un contexte historiquement coûteux pour la vérification formelle
La vérification formelle exhaustive est historiquement très coûteuse. Par exemple, la preuve du petit noyau seL4 a nécessité 20 années-hommes, ce qui a limité cette approche à des usages extrêmes comme certains logiciels avioniques d’Airbus. L’initiative d’Anthropic vise un problème central des logiciels générés par l’IA, tout en reconnaissant des limites pratiques strictes.
Réutilisation des preuves, gains d’efficacité et prochaines cibles
Un test plus restreint a montré que les preuves générées sont réutilisables. Le modèle Opus 5.5 parvient à résoudre la moitié des preuves tout en utilisant environ 40 % de tokens de moins qu’Opus 5. Anthropic indique que la vérification formelle par IA devrait bientôt devenir aussi accessible que les tests classiques, et Theorem vise déjà des composants critiques comme glibc, OpenSSL et cURL. Anthropic ambitionne d’étendre cette méthode, présentée comme un levier supplémentaire pour l’automatisation des logiciels.
