Anthropic a annoncé que son modèle Claude peut générer automatiquement des preuves de vérification formelle pour du code existant. Lors d’un test portant sur 123 bibliothèques du projet OSS‑Fuzz de Google, Claude a produit environ 180 millions de lignes de preuve en quelques semaines. Les preuves ont été vérifiées par l’outil Rocq, et Anthropic affirme que le processus n’a quasiment pas nécessité de relecture humaine.
Ce que le système a réellement fait
Claude n’a pas écrit de nouveaux programmes. Il a plutôt transformé des cas de test de plantage en énoncés mathématiques, analysé le code machine compilé et produit des preuves formelles que le code respecte ces énoncés. Lorsque le modèle rencontrait un bogue, il était autorisé à corriger lui-même le code. En une semaine d’analyse d’un lecteur PDF populaire, Claude a découvert autant de failles de sécurité qu’on en signale habituellement en une année. Dans une autre bibliothèque, il a trouvé une erreur logique passée inaperçue pendant plus de dix ans.
Limites et coûts
Anthropic précise que les preuves ne sont valables que pour un programme monothread exécuté sur une architecture de processeur donnée, avec des entrées de moins de 64 MB. Les besoins en calcul sont élevés : certaines preuves nécessitent des centaines de millions de tokens, même si l’entreprise n’a pas révélé le coût total. Un test plus restreint a montré que le nouveau modèle Opus 5.5 peut produire la moitié des preuves avec environ 40 % de tokens en moins que son prédécesseur.
Pourquoi c'est important
Si l’IA peut vérifier automatiquement le code, les développeurs pourraient consacrer moins de temps à la recherche de bogues et à la relecture des correctifs, en particulier pour les logiciels critiques pour la sécurité. Toutefois, la méthode actuelle ne fonctionne que dans des conditions strictes concernant le matériel et les données d’entrée ; la plupart des applications courantes nécessitent donc encore des tests classiques.
