Claude vérifie formellement 123 bibliothèques, révélant des bugs que les tests rataient

Une IA peut désormais faire davantage que signaler une entrée dangereuse ou proposer un correctif. Selon Anthropic, Claude a contribué à construire des preuves formelles montrant que 123 bibliothèques open source respectent certaines propriétés de sécurité, avec une vérification indépendante par le noyau de Rocq.

De la détection de bugs à la démonstration mathématique

Dans un article publié le 22 octobre 2026, Anthropic décrit un travail mené avec l’entreprise Theorem autour de bibliothèques open source utilisées pour traiter, parser ou transformer des données. L’objectif n’était pas seulement de rechercher des comportements anormaux, mais de démontrer formellement que certains programmes ne produisent pas de résultats incorrects dans les conditions définies.

Le projet couvre 239 points d’entrée répartis entre les 123 bibliothèques. Ces points d’entrée correspondent aux fonctions ou interfaces par lesquelles un programme reçoit des données. Les preuves produites couvrent notamment des entrées allant jusqu’à 64 Mo, une taille suffisamment importante pour dépasser les exemples de test classiques et les cas artificiels généralement utilisés dans les suites de validation.

La différence avec une campagne de tests est fondamentale. Un test montre qu’un logiciel fonctionne sur un ensemble de cas sélectionnés. Une preuve formelle cherche à établir qu’une propriété reste vraie pour toutes les entrées relevant du périmètre défini. Ce périmètre peut concerner l’absence de dépassement mémoire, la validité d’un résultat ou le respect d’une spécification précise.

Il ne s’agit donc pas d’une certification générale de chaque bibliothèque. Une preuve ne garantit que les propriétés effectivement spécifiées, dans les hypothèses retenues. Mais elle permet de remplacer une confiance fondée sur l’accumulation d’exemples par une démonstration vérifiable mécaniquement.

Claude génère, Rocq vérifie

Le rôle de Claude se situe principalement dans la production et l’assemblage des éléments nécessaires à la preuve. Le modèle peut analyser le code, proposer des lemmes, générer des scripts et identifier les étapes manquantes dans un raisonnement formel. La validation finale, elle, ne repose pas sur l’IA.

Les preuves ont été contrôlées par le noyau de Rocq, un assistant de preuve auparavant connu sous le nom de Coq. Ce logiciel applique les règles logiques du système formel et refuse une démonstration incohérente. Cette séparation est essentielle : Claude peut se tromper, produire une preuve incomplète ou formuler un raisonnement erroné, mais le noyau ne valide que les objets qui respectent les règles spécifiées.

Le corpus atteint environ 180 millions de lignes de Rocq. Le chiffre donne une idée de l’ampleur du travail, mais aussi de sa complexité. Une preuve formelle à grande échelle ne consiste pas à traduire mécaniquement un programme en équations. Elle exige de décrire précisément le comportement attendu, de formaliser les structures de données, de gérer les cas limites et de relier le code réellement exécuté à cette spécification.

L’IA intervient ainsi dans une zone où le coût humain constitue depuis longtemps un frein majeur. Les méthodes formelles sont réputées puissantes, mais leur déploiement demande des spécialistes capables de naviguer entre programmation, logique et sémantique des langages. L’automatisation de certaines tâches répétitives peut réduire ce coût, sans supprimer la nécessité d’un cadre formel correctement défini.

Des bugs passés entre les mailles des tests

Le projet n’a pas seulement produit des certificats de conformité. Il a également permis de découvrir et de corriger des bugs qui avaient résisté à des milliers de milliards d’exécutions de tests.

Cette observation illustre une limite connue des approches statistiques. Même une campagne de test massive peut ne jamais atteindre une combinaison rare de valeurs, de tailles d’entrée et d’états internes. Un programme peut fonctionner correctement sur une quantité presque inimaginable de cas tout en échouant sur une configuration particulière.

Les bibliothèques de traitement de données sont particulièrement exposées à ces scénarios. Les erreurs peuvent dépendre d’un seuil numérique, d’un format inhabituel ou d’un enchaînement précis entre plusieurs fonctions. Dans ce contexte, l’analyse formelle cherche moins à multiplier les exemples qu’à examiner la logique générale du programme.

La portée exacte des corrections reste toutefois liée aux propriétés vérifiées. Une preuve portant sur un dépassement de tampon ne démontre pas nécessairement l’absence d’une erreur de logique métier, d’une fuite d’information ou d’une vulnérabilité dans une dépendance externe. La formalisation réduit un ensemble de risques ; elle ne transforme pas automatiquement une bibliothèque en composant exempt de toute faille.

Le véritable enjeu : rendre la preuve exploitable

La performance la plus significative n’est peut-être pas le volume de code vérifié, mais la capacité à appliquer ces méthodes à un ensemble large de projets existants. Les logiciels open source sont rarement conçus dès l’origine pour être prouvés formellement. Leur code peut contenir des optimisations, des interfaces historiques et des comportements implicites difficiles à décrire dans une spécification.

La production de 180 millions de lignes de preuves montre aussi le coût potentiel d’une telle démarche. Ces artefacts doivent être maintenus lorsque le code évolue, lorsque les compilateurs changent ou lorsque la spécification est affinée. Une preuve qui devient impossible à reconstruire après chaque mise à jour perd une partie de sa valeur opérationnelle.

Le modèle le plus crédible repose donc sur une combinaison : l’IA accélère l’exploration et la rédaction des preuves, tandis que des outils déterministes et des ingénieurs vérifient les hypothèses, les interfaces et les résultats. Le noyau de Rocq joue ici le rôle d’un arbitre technique indépendant du modèle qui a généré les scripts.

Cette architecture répond aussi à une question de confiance. Il ne suffit pas d’affirmer qu’une IA a « trouvé » une preuve. Il faut pouvoir l’examiner, la rejouer et vérifier que le mécanisme chargé de l’accepter est suffisamment restreint et auditable. La valeur du résultat tient précisément à cette chaîne de contrôle.

Vers des bibliothèques vérifiées à grande échelle

L’expérience menée par Anthropic et Theorem suggère une évolution concrète du développement logiciel : les assistants d’IA pourraient rendre accessibles des techniques jusque-là réservées à des composants critiques, comme les compilateurs, les systèmes embarqués ou certains protocoles cryptographiques.

Le prochain jalon sera la reproductibilité. Il faudra mesurer combien de bibliothèques peuvent être vérifiées dans des conditions comparables, combien de temps les preuves demandent à être régénérées après une modification et quelle part du code reste couverte lorsque les projets évoluent. Il faudra aussi publier clairement les spécifications retenues et les limites de chaque preuve.

Avec 123 bibliothèques, 239 points d’entrée et des entrées allant jusqu’à 64 Mo, le projet fournit une démonstration d’échelle. Sa portée réelle se jugera sur la maintenance : si les preuves survivent aux mises à jour courantes et continuent de révéler des bugs que les tests manquent, l’IA aura franchi une étape importante, non pas en remplaçant la vérification humaine, mais en rendant la vérification formelle plus praticable.

Source : Anthropic, « Formal verification »