Claude produit des preuves de sécurité. Le périmètre compte autant que le résultat

Une IA peut-elle faire mieux que chercher des bugs dans un programme ? Anthropic et Theorem présentent le 22 octobre 2026 un travail où Claude produit des preuves vérifiées par un autre logiciel. Les partenaires annoncent des résultats sur 239 points d’entrée répartis dans 123 bibliothèques ouvertes. Le changement est intéressant. Sa portée exige toutefois de regarder exactement ce qui a été prouvé.

Tester des exemples et prouver une propriété sont deux démarches différentes

Un test exécute un programme sur certaines entrées. Le fuzzing multiplie les entrées pour tenter de provoquer une erreur. Une preuve formelle cherche à établir une propriété pour toutes les entrées couvertes par un énoncé. L’étude d’Anthropic part de programmes de test déjà utilisés dans OSS-Fuzz. Elle demande aux agents de construire les preuves correspondant aux propriétés retenues.

Claude écrit les étapes de raisonnement sous une forme que Rocq peut contrôler. Le noyau de ce vérificateur examine ensuite la preuve. L’intérêt vient de cette séparation entre la production et la vérification. Il ne suffit pas que le modèle affirme avoir démontré quelque chose. Sa sortie doit être acceptée par le système de preuve dans le cadre défini.

Les résultats concernent des binaires et des propriétés précises

Les partenaires travaillent sur des programmes compilés pour une architecture RISC-V dans un environnement Linux modélisé. La configuration étudiée utilise notamment des binaires statiques et des limites de ressources. Ce n’est pas une preuve applicable sans changement à toutes les versions du code source. Un programme compilé pour une autre architecture ou avec une autre bibliothèque système sort de ce périmètre.

Le dépôt public des preuves décrit ce que ses résultats permettent d’affirmer. Il compare une version ordinaire du programme à des versions équipées de détecteurs d’erreurs. Sous les limites prévues, ces versions doivent conserver les mêmes comportements observables sans atteindre les erreurs couvertes. Les sorties et l’état final des fichiers font notamment partie des observations.

L’absence de certaines erreurs ne signifie pas l’absence de tout bug

Une fuite de mémoire ou un résultat faux peut échapper aux propriétés vérifiées. La preuve ne concerne que le code atteint par le point d’entrée étudié. Elle ne couvre pas automatiquement toute la bibliothèque. Le dépôt précise aussi que les preuves publiées de ce type n’excluent pas une exécution qui ne se termine jamais. Démontrer la terminaison exige un autre énoncé.

Les budgets mémoire et les restrictions sur les entrées font partie des hypothèses. On ne peut pas les retirer du résultat lorsqu’on le résume. Le modèle Linux utilisé dans Rocq indique lui-même ses limites. Il décrit une partie du système et conserve des hypothèses qu’il ne contrôle pas. Une preuve mathématique correcte reste tributaire de la pertinence de ce modèle pour le programme réel.

Un résultat de recherche du fournisseur avec des éléments publics

Les chiffres de 239 points d’entrée et 123 bibliothèques viennent du travail présenté par Anthropic avec Theorem. Ils ne constituent pas une reproduction indépendante menée ici. Une partie des preuves et des outils est publiée pour permettre leur examen. Le dépôt public présente un sous-ensemble du travail annoncé. Il ne faut donc pas confondre la taille de l’étude et le nombre de résultats effectivement disponibles dans cette publication de code.

L’étude explique aussi que certains programmes ont été corrigés avant la construction d’une preuve. La propriété porte alors sur le programme modifié. Les auteurs décrivent des contrôles destinés à éviter qu’une correction simplifie artificiellement le problème. Cette difficulté rappelle une question centrale. Il faut vérifier que le logiciel prouvé correspond toujours au comportement que l’on voulait préserver.

Une ouverture aux mainteneurs avec des conditions

Le programme OSS Verify de Theorem propose une prise en charge sans frais à des projets ouverts éligibles. Il s’adresse à leurs mainteneurs principaux et donne la priorité aux dépendances critiques pour la sécurité. Le passage vers l’environnement de compilation prévu fait partie des contraintes. L’offre ne garantit ni un délai identique pour tous les projets ni une preuve complète de leur fonctionnement.

L’apport de ce travail tient à la possibilité de faire contrôler une affirmation produite par une IA. Ça déplace la discussion vers la propriété exacte et ses hypothèses. Notre article sur l’élargissement de Claude pour la cybersécurité présente une autre approche de la recherche de vulnérabilités. Détecter une faille et démontrer qu’une classe d’erreurs est exclue restent deux contributions complémentaires.