N環球 
Claude rédige 180 millions de lignes de preuves mathématiques : première vérification formelle massive de logiciels open source par l’IA
Recherche officielle d’Anthropic : avec Theorem, Claude a vérifié formellement des propriétés de sécurité au niveau assembleur RISC-V sur 123 bibliothèques open source et 239 points d’entrée — et déterré des centaines de bogues ayant échappé à des billions de tests automatisés.
Pourquoi c’est important
La vérification formelle était un luxe réservé à des experts pendant des années — écrire le micronoyau seL4 a pris 2 années-personnes, le vérifier en a pris 20. Anthropic vient de montrer qu’un modèle de pointe peut le faire pour plus d’une centaine de bibliothèques open source réelles en quelques semaines, tout en déterrant des bogues ayant survécu à des « billions » d’exécutions de tests automatisés.
Lire l’article
Anthropic l’a annoncé sur sa page de recherche officielle le 22 octobre : en collaboration avec la société de vérification logicielle Theorem, Claude a vérifié formellement des propriétés de sécurité au niveau assembleur RISC-V sur 123 bibliothèques open source réelles issues du programme OSS-Fuzz de Google, couvrant 239 points d’entrée. L’entreprise y voit « le premier effort à grande échelle d’utilisation de l’IA pour appliquer la vérification formelle à des logiciels de production au niveau du code assembleur ».
L’échelle est saisissante : environ 180 millions de lignes de preuves Rocq, une preuve typique avoisinant 600 000 lignes, couvrant des binaires d’une longueur médiane de 18 000 instructions RISC-V — le tout accompli en quelques semaines. Le noyau Rocq vérifie chaque preuve de façon indépendante, sans relecture manuelle ligne à ligne.
La méthode convertit les tests de fuzzing existants en spécifications mathématiques : pour toute entrée de moins de 64 Mo, un binaire RISC-V statique monothread sous Linux doit toujours se terminer normalement, sans violation de sécurité mémoire. Quand Claude soupçonnait un bogue en cours de preuve, il corrigeait directement le code puis reprouvait la nouvelle spécification.
Des centaines de bogues ont ainsi refait surface, dont un dépassement inférieur de compteur dans une copie de décompresseur provoquant une écriture hors limites (déclenchable uniquement par des entrées d’environ 20 Mo à la disposition rare et spécifique), une lecture hors limites dans un décodeur d’images, et la redécouverte de CVE-2026-56132 dans libexpat — certaines vulnérabilités sommeillaient depuis des années.
Anthropic reconnaît elle-même les limites : une vérification formelle réussie ne signifie pas l’absence de bogues — les preuves ne couvrent que des binaires RISC-V statiques monothread, alors que la plupart du code tourne sur x86/ARM. Elle a publié un sous-ensemble des preuves sur GitHub pour vérification indépendante, et Theorem propose d’appliquer le même pipeline à d’autres projets open source.
Les résultats annexes sont notables aussi : l’implémentation zlib du noyau Linux a été prouvée conforme à la RFC 1950 au niveau du binaire x86, et un large sous-ensemble d’un interpréteur Python écrit en Rust a affiché un taux de conformité comportementale de 99,95 % avec CPython sur plus de 1,7 million de programmes aléatoires.
💬 Commentaires
Aucun commentaire. Soyez le premier !