AlphaProof Code vérifie des propriétés de sécurité de Signal avec 6,5 millions de lignes Lean

Une IA qui signale une faille peut attirer l’attention. Une IA qui contribue à produire une preuve mathématique contrôlée par un noyau de vérification va plus loin : elle permet d’établir, propriété par propriété, ce que garantit réellement le code qui protège des conversations privées.

D’une détection automatisée à une preuve vérifiable

Dévoilé le 10 novembre 2026, AlphaProof Code, le système de Google DeepMind, a été utilisé pour vérifier des propriétés de sécurité de libsignal, l’implémentation de référence du protocole Signal. L’objectif n’était pas simplement d’inspecter le code à la recherche d’erreurs, mais de démontrer formellement que certaines propriétés restent vraies dans l’implémentation étudiée.

La distinction est importante. Une analyse automatisée classique peut identifier des comportements suspects, des chemins d’exécution inhabituels ou des vulnérabilités potentielles. La vérification formelle, elle, traduit une propriété de sécurité en énoncé mathématique, puis cherche à établir que cet énoncé est respecté par le programme dans les conditions définies.

Dans le cas présent, les agents d’AlphaProof Code ont généré environ 6,5 millions de lignes de preuves Lean. Ces preuves ont ensuite été contrôlées par le noyau du système de preuve Lean. Ce noyau constitue le dernier arbitre : il ne se contente pas d’évaluer la plausibilité d’une démonstration produite par un modèle, il vérifie que les règles formelles ont bien été respectées.

L’IA n’a donc pas reçu le dernier mot sur la validité de ses propres résultats. Son travail a consisté à explorer et construire les démonstrations ; la validation finale repose sur un mécanisme formel indépendant des intuitions ou des probabilités du modèle.

Vérifier le code au plus près de son exécution

L’un des aspects les plus significatifs du projet tient au niveau auquel la vérification a été menée. Les travaux se sont appuyés sur des spécifications, mais aussi sur la sémantique machine-code en AArch64, l’architecture 64 bits utilisée par de nombreux processeurs mobiles et serveurs.

Cette approche cherche à réduire l’écart entre l’algorithme décrit par ses concepteurs et le programme effectivement exécuté par la machine. Vérifier uniquement une abstraction du protocole ne suffit pas toujours : une erreur peut apparaître lors de la compilation, dans la gestion de la mémoire, dans une opération arithmétique ou dans l’interprétation d’une instruction bas niveau.

En prenant en compte la sémantique du code machine, le dispositif tente de suivre la chaîne complète : la propriété de sécurité, le code de libsignal, puis les instructions correspondant à son exécution sur AArch64. Cette profondeur ne signifie pas que chaque composant de l’écosystème Signal est automatiquement couvert. Elle permet cependant de rapprocher la preuve du comportement concret du logiciel.

Pour un protocole de messagerie chiffrée, cette précision est déterminante. La confidentialité ne dépend pas seulement de la solidité théorique de la cryptographie. Elle repose aussi sur la fidélité de l’implémentation, la gestion des clés, les états du protocole et les garanties apportées par le code exécuté.

Une production massive, mais pas autonome

Le volume annoncé donne une idée de la difficulté du chantier : 6,5 millions de lignes de preuves pour établir les propriétés ciblées. Ce chiffre ne correspond pas à autant de lignes de code applicatif, mais aux éléments formels nécessaires pour décrire les comportements, lever les ambiguïtés et démontrer les théorèmes associés.

Google DeepMind précise toutefois que le travail a été guidé par des humains. Les chercheurs ont défini les objectifs, construit le cadre de vérification et orienté les agents dans les étapes difficiles. L’IA n’a pas transformé seule un dépôt logiciel en garantie mathématique complète.

Cette précision est essentielle, car une preuve formelle ne porte que sur ce qui a été spécifié. Les spécifications de confiance représentent environ 26 000 lignes, soit une fraction très réduite du volume total des preuves générées. Elles restent néanmoins un socle critique : si une propriété est mal formulée, trop faible ou incomplète, le système peut démontrer impeccablement quelque chose qui ne couvre pas le risque recherché.

Autrement dit, le noyau Lean peut certifier qu’une preuve est correcte au regard des définitions et des axiomes fournis. Il ne peut pas décider seul si ces définitions décrivent toutes les garanties attendues d’une messagerie sécurisée.

Ce que cette étape apporte à Signal

Signal indique que cette méthode étend nettement la portée des vérifications formelles menées auparavant sur son logiciel. Jusqu’ici, les analyses formelles appliquées aux protocoles cryptographiques portaient souvent sur des modèles abstraits, des composants isolés ou des propriétés précises. Le projet présenté avec AlphaProof Code vise une couverture plus proche de l’implémentation réelle et de son exécution.

La différence se mesure moins au nombre de problèmes trouvés qu’au type de résultat produit. Un outil d’analyse peut conclure qu’aucun défaut connu n’a été détecté dans un périmètre donné. Une preuve formelle établit qu’une propriété déterminée découle du modèle et du code vérifiés. Ce n’est pas une certification générale de sécurité, mais c’est une garantie beaucoup plus explicite et auditable.

Le rôle de l’IA est ici particulièrement intéressant. Les systèmes de preuve comme Lean exigent habituellement un travail considérable pour décomposer un objectif, choisir les lemmes utiles et gérer les détails techniques. Les agents peuvent accélérer cette recherche, générer des étapes intermédiaires et reprendre une démonstration après un échec. La validation, elle, reste confiée à un noyau dont le fonctionnement est plus restreint et plus facilement inspectable.

Une garantie ciblée, pas un certificat absolu

Il serait excessif de conclure que Signal est désormais « prouvé sûr » dans son ensemble. La démarche ne couvre que les propriétés sélectionnées, les composants étudiés et les hypothèses retenues. Elle ne remplace ni les audits, ni les tests, ni l’analyse des dépendances, ni la surveillance des vulnérabilités apparues après la vérification.

Elle ne traite pas non plus automatiquement les erreurs de conception situées en dehors des spécifications, les compromis opérationnels, les attaques contre le matériel ou les éléments qui ne figurent pas dans le modèle. La confiance est déplacée vers une base plus précise : spécifications, sémantique d’exécution, bibliothèques de preuve et noyau Lean.

C’est justement ce déplacement qui rend l’expérience importante pour l’ingénierie logicielle. Une IA générative peut produire du code plausible, mais une preuve contrôlée par un noyau impose une discipline différente : chaque étape doit être justifiable dans un cadre formel.

Le prochain jalon sera l’élargissement mesurable du périmètre : davantage de composants de libsignal, davantage de propriétés et, idéalement, la publication de résultats permettant à des tiers de reproduire ou d’auditer les preuves. À terme, l’enjeu ne sera pas de produire toujours plus de lignes Lean, mais de réduire les 26 000 lignes de spécifications de confiance, d’en clarifier les hypothèses et de démontrer que les garanties formelles couvrent les scénarios d’attaque les plus importants.