Quand l’IA prouve une propriété du code : le progrès réel et la garantie limitée
Anthropic et Theorem annoncent des preuves formelles sur 123 bibliothèques. Une avancée à lire avec ses hypothèses : certifier une propriété ne rend pas tout un service invulnérable.
Prêt à lire l’article.
Dans cet article
Le 22 octobre, Anthropic a présenté un travail avec Theorem dans lequel Claude produit des preuves de sécurité pour du code compilé. Selon l’entreprise, l’expérience couvre 123 bibliothèques ouvertes. Le résultat annoncé concerne certains programmes exécutés dans un environnement RISC-V et Linux modélisé, avec des limites explicites, notamment sur la taille des entrées. Il ne constitue pas une certification générale de ces logiciels.
Une preuve doit dire ce qu’elle prouve
Le dépôt public de Theorem permet de préciser le périmètre consultable : il documente des preuves pour 60 points d’entrée dans 25 bibliothèques. Ce sous-ensemble public ne doit pas être confondu avec le total annoncé par Anthropic. Les preuves sont contrôlées par Rocq et reposent sur un modèle d’exécution dont les auteurs décrivent les hypothèses et les limites. MIND AI MEDIA n’a pas réexécuté cette chaîne de vérification.
Un exemple fictif permet de comprendre l’enjeu. Une bibliothèque peut traiter correctement des fichiers dans les conditions prévues par une preuve, tandis que l’application qui l’utilise donne accès à ces fichiers au mauvais utilisateur. La première garantie ne répond pas à la seconde question. Une démonstration mathématique peut être rigoureuse et rester insuffisante pour juger un service entier.
Notre analyse : déplacer le travail de confiance
L’intérêt industriel serait de réduire le coût d’un travail jusqu’ici très spécialisé. Mais le gain utile ne se mesure pas seulement au nombre de lignes de preuve produites. Il faudrait aussi examiner le temps nécessaire pour définir la propriété recherchée, relire les hypothèses et refaire la vérification après une modification.
Pour une rédaction, une administration ou une PME qui achète un logiciel, cette annonce invite à poser des questions précises. Quelle version est couverte ? Quelles fonctions ont été examinées ? Quels composants restent en dehors du périmètre ? Comment la garantie sera-t-elle maintenue dans le temps ? Une réponse documentée vaut davantage qu’une étiquette générale de « logiciel sécurisé par IA ».
La projection reste conditionnelle : si ces méthodes deviennent plus accessibles, elles pourraient renforcer la maintenance des composants partagés. Elles ne supprimeraient ni la gestion des accès, ni les mises à jour, ni les erreurs de configuration. La preuve formelle apporte une forme particulière d’assurance ; sa valeur dépend de la clarté de ce qu’elle inclut et de ce qu’elle laisse ouvert.
Sources
Anthropic — étude du 22 octobre 2026.
Theorem — preuves publiques et limites du modèle. Sources consultées le 24 octobre. Annonce des auteurs, sans reproduction indépendante par notre rédaction.