180 millions de lignes de preuves formelles, 123 bibliothèques open source et 239 points d’entrée vérifiés : Anthropic affirme avoir franchi un seuil inédit avec Claude et Theorem. Le système a travaillé directement sur des binaires compilés en RISC-V et produit des preuves contrôlées par le noyau de Rocq, un assistant de preuve formelle.
L’enjeu dépasse la démonstration technique. Si cette méthode devient suffisamment abordable et reproductible, les développeurs pourraient vérifier des propriétés de sécurité qui échappent aux tests classiques. Mais le résultat ne signifie pas que 123 bibliothèques sont exemptes de tout bug : les preuves portent sur des propriétés précises, dans un environnement et sous des hypothèses déterminés.
180 millions de lignes Rocq pour 239 points d’entrée
Le projet porte sur 239 points d’entrée répartis dans 123 bibliothèques open source issues de l’écosystème OSS-Fuzz. Claude a généré environ 180 millions de lignes de preuves en Rocq, avec une moyenne d’environ 600 000 lignes par preuve. Les binaires vérifiés comptaient une longueur médiane de 18 000 instructions RISC-V.
Anthropic indique que les travaux ont été réalisés sur plusieurs semaines avec une intervention humaine limitée. Claude a généré les preuves et corrigé certains bugs détectés pendant le processus, tandis que le noyau de Rocq a vérifié leur validité. Cette séparation est essentielle : le modèle peut produire un raisonnement erroné, mais une preuve rejetée par le noyau ne devient pas valide pour autant.
| Élément vérifié | Résultat publié |
|---|---|
| Bibliothèques open source | 123 |
| Points d’entrée | 239 |
| Preuves produites | Environ 180 millions de lignes Rocq |
| Taille médiane des binaires | 18 000 instructions RISC-V |
| Taille typique d’une preuve | Environ 600 000 lignes |
| Limite d’entrée étudiée | 64 Mo |
Le choix du niveau assembleur distingue cette expérience de nombreuses approches qui vérifient uniquement le code source. La preuve porte sur les instructions compilées, c’est-à-dire sur une représentation plus proche de ce que le processeur exécute réellement.
À retenir : Claude n’a pas simplement analysé du code et signalé des risques. Il a généré des objets mathématiques que Rocq a ensuite contrôlés indépendamment.
Pourquoi vérifier le binaire plutôt que le seul code source
La vérification formelle consiste à démontrer mathématiquement qu’un programme respecte une spécification donnée. Un test montre qu’un logiciel fonctionne sur les cas exécutés ; une preuve formelle cherche à établir une propriété pour l’ensemble des entrées couvertes par le modèle et les hypothèses retenues.
Dans cette expérience, les propriétés concernent notamment l’absence de crash et certaines violations de sûreté mémoire. Claude a travaillé sur des binaires RISC-V, avec des modèles formels des instructions de cette architecture et de la sémantique des processus Linux fournis par Theorem.
Cette approche apporte un avantage concret : elle vérifie le résultat compilé plutôt qu’une intention exprimée uniquement dans le code source. Elle réduit ainsi le risque de laisser de côté des effets liés à la compilation ou à l’exécution, même si elle ne supprime pas la nécessité de définir correctement le modèle matériel, le système d’exploitation et les hypothèses d’environnement.
La portée reste donc précise. Une preuve d’absence de crash pour des entrées allant jusqu’à 64 Mo ne démontre pas l’absence de toutes les vulnérabilités, ni la conformité à toutes les exigences fonctionnelles. Elle établit la propriété qui a été formalisée, dans le cadre qui a été modélisé.
Ce que la preuve établit
- Une propriété de sécurité spécifiée mathématiquement.
- La validité de cette propriété pour le code et l’environnement couverts par le modèle.
- La cohérence de la démonstration après contrôle par le noyau de Rocq.
Ce qu’elle n’établit pas
- L’absence de tout bug dans une bibliothèque.
- La sécurité de fonctions qui ne figurent pas dans les points d’entrée étudiés.
- La conformité automatique à toutes les spécifications métier.
- La sécurité d’une nouvelle compilation si ses hypothèses diffèrent de celles de la preuve.
Cette distinction sera déterminante pour les équipes de développement. La vérification formelle ne remplace pas les tests, le fuzzing, l’analyse statique et la revue de code. Elle ajoute une garantie plus forte sur des propriétés ciblées.
Des bugs anciens détectés par une chaîne de preuve automatisée
Anthropic affirme que le projet a permis de détecter des centaines de bugs, dont certains étaient restés invisibles pendant des années. La démarche part de points d’entrée déjà associés à des tests de fuzzing, puis transforme les propriétés recherchées en spécifications formelles que Claude tente de démontrer.
Le fuzzing explore automatiquement un grand nombre d’entrées, souvent conçues pour provoquer des comportements inattendus. La preuve formelle change la nature du contrôle : au lieu de dépendre uniquement des cas générés et exécutés, elle cherche à établir une propriété générale sur l’espace d’entrées défini.
Cette combinaison explique l’intérêt du projet. Le fuzzing aide à trouver des contre-exemples concrets ; la preuve formelle tente ensuite de démontrer qu’aucun contre-exemple ne subsiste dans le périmètre choisi. Lorsqu’une preuve échoue, l’échec peut révéler un défaut dans le logiciel, une spécification trop ambitieuse ou un modèle incomplet.
Une source consacrée au projet rapporte notamment la redécouverte d’une vulnérabilité identifiée comme CVE-2026-56132 dans libexpat. Ce type de résultat illustre le rôle de la méthode : remettre en évidence des problèmes anciens en les soumettant à une vérification systématique au niveau du binaire.
La valeur opérationnelle ne tient toutefois pas au nombre de lignes produites. Une preuve de plusieurs centaines de milliers de lignes n’est utile que si sa spécification est pertinente, si le modèle couvre correctement l’exécution et si les conditions de validité sont comprises par les mainteneurs.
Ce que Claude change pour le travail quotidien des développeurs
Le principal changement concerne le coût humain de la formalisation. Jusqu’ici, produire une preuve pour du logiciel réel demandait souvent des spécialistes des méthodes formelles, capables de traduire une propriété de sécurité en logique et de guider le prouveur à travers les cas difficiles.
Dans l’expérience d’Anthropic, Claude prend en charge une grande partie de cette construction. Il traduit le comportement du programme en obligations de preuve, propose des étapes de raisonnement et corrige certains défauts découverts en chemin. Le noyau de Rocq conserve le rôle d’arbitre final.
Pour un développeur, la conséquence la plus concrète pourrait être l’apparition d’un nouveau type de contrôle dans la chaîne de livraison :
- le code est compilé dans un environnement défini ;
- des propriétés de sécurité sont formulées ;
- Claude génère une preuve ;
- Rocq vérifie cette preuve ;
- la preuve est associée au binaire et à ses hypothèses ;
- toute modification du code déclenche une nouvelle vérification.
Cette logique ressemble davantage à un contrôle de compilation qu’à une analyse ponctuelle. Une preuve attachée à un artefact logiciel peut devenir une condition de publication, au même titre qu’un test obligatoire ou qu’une analyse de vulnérabilités.
Les compétences qui prennent de la valeur
L’automatisation ne supprime pas le besoin d’expertise. Elle déplace le travail vers la définition des propriétés, la sélection des hypothèses et l’interprétation des échecs. Les équipes devront notamment savoir distinguer un bug réel d’une limite du modèle ou d’une spécification mal formulée.
Les développeurs devront également suivre les dépendances entre le code, le compilateur, l’architecture cible et l’environnement d’exécution. Une preuve obtenue pour un binaire RISC-V ne se transfère pas automatiquement à une autre architecture ou à une autre chaîne de compilation.
Le rôle du développeur évolue donc vers une supervision de la garantie. Claude peut produire une grande quantité de raisonnement formel, mais l’équipe reste responsable de la question la plus importante : la propriété prouvée correspond-elle réellement au risque que le logiciel doit éviter ?
glibc, OpenSSL et cURL deviennent les prochaines cibles
Anthropic et Theorem annoncent vouloir rendre la vérification formelle aussi courante que les tests standards. Leur feuille de route vise notamment glibc, OpenSSL et cURL, trois composants largement utilisés dans les systèmes et les applications.
Ces projets représentent un changement d’échelle. Les 123 bibliothèques étudiées constituent une démonstration importante, mais la vérification de composants fondamentaux pose des exigences plus élevées : surface de code étendue, compatibilité historique, nombreuses architectures, contraintes de performance et dépendances profondes.
La cible est néanmoins cohérente. glibc fournit une partie essentielle de l’environnement d’exécution de nombreux systèmes Linux. OpenSSL intervient dans la cryptographie et les communications sécurisées. cURL est intégré à une multitude d’outils et de services. Une amélioration vérifiée dans ces composants pourrait avoir un effet largement supérieur à celui d’un correctif limité à une application.
Theorem travaille également sur OSS Verify, un programme destiné aux projets open source. Le service vise à proposer une vérification de propriétés de sécurité ou à fournir les correctifs nécessaires avant la preuve. Cette orientation pourrait réduire la barrière d’entrée pour des mainteneurs qui ne disposent pas d’une équipe spécialisée en méthodes formelles.
Le passage à des bibliothèques centrales exigera toutefois des preuves plus riches que l’absence de crash sur un ensemble de points d’entrée. Les objectifs pourraient inclure la préservation de propriétés mémoire, le respect de contrats d’interface, la sûreté de certaines opérations cryptographiques et la stabilité de comportements compatibles avec les versions précédentes.
Le coût élevé reste le principal frein
La génération automatisée ne rend pas la vérification gratuite. Anthropic décrit les preuves comme coûteuses à produire, malgré une intervention humaine limitée. Le volume de 180 millions de lignes donne une indication de l’effort computationnel et de la complexité des objets générés, mais il ne constitue pas à lui seul un prix commercial.
Le coût se répartit entre plusieurs postes : calcul nécessaire à la recherche de preuves, stockage des artefacts, modélisation des instructions et du système, maintenance des spécifications et nouvelle vérification à chaque évolution du code. Une équipe doit également conserver la traçabilité des hypothèses et des versions utilisées.
La taille des preuves pose un autre problème. Environ 600 000 lignes par preuve en moyenne peuvent rendre la maintenance difficile si chaque changement mineur provoque une reconstruction complète. Les prouveurs et les modèles devront donc devenir plus efficaces, tandis que les formats de preuve devront rester vérifiables et exploitables dans le temps.
La confidentialité est également centrale pour les entreprises. Faire analyser du code propriétaire par un modèle externe peut entrer en conflit avec les exigences de secret industriel, les règles de conformité et les contrats clients. L’utilisation de modèles déployés dans un environnement contrôlé ou de preuves produites localement pourrait devenir une condition d’adoption.
La question économique se résume à un arbitrage : le coût de la preuve doit rester inférieur au coût attendu d’une vulnérabilité, d’une interruption de service ou d’un rappel de produit. Pour les composants critiques, cette équation peut être favorable. Pour une application interne peu exposée, les tests traditionnels resteront probablement plus adaptés.
À retenir : l’automatisation réduit le temps d’écriture des preuves, mais elle ne supprime ni le coût du calcul ni celui de la modélisation.
Une garantie plus forte, mais jamais universelle
La démonstration d’Anthropic répond à une limite historique de la vérification formelle : son application à des logiciels réels, compilés et suffisamment volumineux pour être utiles en production. Les 123 bibliothèques et les 239 points d’entrée montrent qu’un modèle peut désormais contribuer à cette tâche à une échelle supérieure à celle d’un petit composant pédagogique.
L’expérience ne transforme pas pour autant chaque sortie de Claude en preuve fiable. La fiabilité vient du contrôle par Rocq et de la précision des modèles, pas du seul fait que le texte a été généré par une IA. Un modèle peut aussi produire une preuve valide d’une propriété trop faible ou mal alignée sur le risque réel.
Les développeurs devront donc adopter une lecture en trois niveaux :
- vérifier que la spécification décrit bien le comportement attendu ;
- vérifier que le modèle couvre le matériel et l’environnement visés ;
- vérifier que la preuve a été contrôlée par un noyau indépendant et reproductible.
Cette discipline rapproche la vérification formelle des pratiques de sécurité existantes. Un rapport d’analyse statique n’est pas une garantie absolue ; une suite de tests ne couvre pas toutes les entrées ; une preuve formelle ne couvre pas davantage les propriétés qui n’ont pas été exprimées. La différence tient à la force de la garantie pour le périmètre effectivement défini.
La transparence des artefacts sera donc déterminante. Les projets devront publier les spécifications, les hypothèses, les versions du compilateur, les modèles utilisés et les procédures de reproduction. Sans ces éléments, une preuve difficile à auditer risque de devenir un simple label marketing.
Notre avis : la preuve formelle entre dans la boîte à outils
La démonstration Claude-Theorem marque une avancée crédible pour les développeurs : 180 millions de lignes Rocq, 123 bibliothèques, 239 points d’entrée et une vérification au niveau du binaire constituent une échelle difficile à atteindre manuellement. Le progrès le plus important n’est pas la quantité de texte générée, mais la possibilité de transformer une partie du travail de formalisation en processus automatisé et contrôlé.
Dans les six prochains mois, l’adoption la plus réaliste concernera les composants critiques, les bibliothèques de sécurité et les points d’entrée déjà ciblés par le fuzzing. Les équipes ne remplaceront pas leurs tests ; elles chercheront plutôt à ajouter des preuves sur les fonctions dont une défaillance aurait les conséquences les plus coûteuses.
Anthropic et Theorem devront encore démontrer que la méthode reste maintenable sur glibc, OpenSSL et cURL, avec des changements fréquents, plusieurs architectures et des exigences de compatibilité élevées. Si elles y parviennent, la preuve formelle pourrait passer du statut d’expertise spécialisée à celui de contrôle standard dans les chaînes de développement.
La question décisive ne sera alors plus de savoir si une IA peut écrire des preuves, mais quelles propriétés chaque équipe acceptera de rendre obligatoires avant de livrer son prochain binaire.