Anthropic avait fait vérifier son code par l'IA, un autre labo y trouve des bugs
— AGENTS
GenProof a repris six bibliothèques déjà certifiées par Claude pour Anthropic et y a trouvé des erreurs bien réelles, sans invalider les preuves initiales. Le problème ne vient pas des démonstrations mais de ce qu'on avait choisi de démontrer.
Anthropic avait fait grand bruit en annonçant que son IA Claude avait démontré mathématiquement la sécurité de plus de cent bibliothèques open source, du genre de celles qui font tourner la moitié d'internet. Un nouveau laboratoire, GenProof, vient de reprendre six de ces bibliothèques, dont OpenSSL et zlib, et y a trouvé des bugs bien concrets, certains touchant Redis ou le noyau Linux.
La nuance compte et elle est vertigineuse pour quiconque vend de la fiabilité garantie par preuve mathématique. Une démonstration peut être parfaitement valide et vérifier la mauvaise chose. Anthropic prouvait qu'un programme ne plante pas, pas qu'il renvoie le bon résultat. Un bug dans Redis a ainsi rendu des données illisibles après une mise à jour, sans jamais provoquer d'erreur d'exécution que la preuve initiale aurait pu capter.
Aucun graphiste, monteur ou directeur artistique n'ouvre un fichier de preuve Lean le matin. Mais les logiciels de compression, de chiffrement ou de stockage qui plantent rarement et tiennent les pipelines créatifs reposent précisément sur ce genre de briques auditées en silence. Quand une entreprise affiche des garanties mathématiques sur son code, la question devient : garanties sur quoi, exactement.
GenProof propose aussi deux outils, QuickProof pour écrire des spécifications en C sans jargon mathématique, et QuickMaths pour faire collaborer plusieurs agents sur des démonstrations dans Lean, avec un score de 72 % sur une évaluation de cent vingt-huit problèmes de recherche. L'intérêt réel se loge ailleurs que dans ce chiffre : ce sont des agents qui abandonnent une piste bloquée pour en explorer une autre, et un vérificateur indépendant qui contrôle chaque résultat avant de le valider.
La limite tient en une phrase simple. Un vérificateur garantit qu'une preuve correspond à son énoncé, jamais que l'énoncé correspond à ce que l'utilisateur attendait vraiment. Écrire la bonne spécification devient le métier qui compte, bien plus que générer des milliers de lignes de démonstration. Les discours sur la sécurité garantie par preuve mathématique méritent désormais une question précise avant d'être crus sur parole : quelle propriété exacte a été vérifiée, et laquelle a été oubliée.