Google DeepMind publie AlphaProof Code : des agents ont prouvé en Lean la sécurité du code compilé de Signal
Google DeepMind a détaillé le 10 novembre AlphaProof Code, un système d'agents qui a produit environ 6,5 millions de lignes de preuves Lean sur le code machine de libsignal, la bibliothèque de référence du protocole Signal. Les preuves couvrent la poignée de main post-quantique PQXDH et le Triple Ratchet, avec des hypothèses et des limites précisées dans l'article technique.
La démonstration était évoquée en une ligne lors du lancement de Gemini 4 Carbon ; elle est désormais documentée. Google DeepMind a publié le 10 novembre un billet et un article technique sur AlphaProof Code, un système d’agents qui a prouvé mathématiquement des propriétés de sécurité du code de libsignal, la bibliothèque de référence du protocole Signal. Ce protocole chiffre aussi, dans des variantes, WhatsApp, Messenger et Google Messages.
Ce qui a été prouvé
L’originalité tient au niveau de la preuve. La plupart des vérifications de protocoles s’arrêtent à leur conception. Ici, les chercheurs ont compilé libsignal avec le compilateur Rust standard pour des processeurs AArch64 (Arm 64 bits) sous Linux, puis prouvé que ce code machine respecte les propriétés attendues. Ces preuves couvrent la poignée de main post-quantique PQXDH et le Triple Ratchet : confidentialité persistante, authentification, sécurité après la compromission temporaire d’un appareil et secret de la poignée de main.
Les chiffres donnent l’échelle : environ 6,5 millions de lignes de preuves écrites en Lean, un langage de preuve dont le noyau vérifie chaque étape. Elles reposent sur environ 26 000 lignes de spécifications et de description du processeur qu’il faut, elles, considérer comme fiables. Le travail a pris quatre semaines à une équipe de cinq personnes. L’article rappelle que la vérification du micronoyau seL4 avait demandé vingt années-personnes, et celle du compilateur CompCert six.
Comment les agents travaillent
AlphaProof Code répartit le travail comme une équipe de recherche. Des humains décident quoi prouver et relisent chaque spécification, rédigée avec l’aide de plusieurs modèles. Des agents propulsés par Gemini Carbon écrivent ensuite les preuves de façon autonome. Un agent « gardien » n’accepte une preuve que si Lean la valide contre une copie de la spécification approuvée : la fiabilité du résultat ne dépend donc pas de celle des agents. Selon Google DeepMind, les agents ont ensuite audité leur propre travail et n’ont signalé qu’environ 1 % du code de preuve pour une relecture humaine.
Pour vérifier que le système distingue un code sûr d’un code fautif, l’équipe a réintroduit deux vrais bogues, corrigés depuis, dans une copie isolée de libsignal. Dans les deux cas, le système a produit une preuve vérifiée que la version boguée n’était pas sûre. Le directeur technique de Signal, Ehren Kret, cité dans le billet, y voit une « avancée majeure ». Les artefacts de vérification sont publiés en source ouverte.
Les limites, écrites noir sur blanc
L’article technique est précis sur ce qu’il ne garantit pas. Les preuves symboliques supposent une cryptographie parfaite et ne disent rien du secret calculatoire des octets. Les bornes calculatoires ne valent pas face à un adversaire quantique. La génération des clés n’est pas vérifiée. La description du processeur couvre 467 instructions et 31 appels système, mais ne modélise ni les threads, ni les signaux, ni l’édition de liens dynamique. Enfin, le résultat fait confiance au noyau de Lean, aux primitives cryptographiques et aux contrats de certaines routines appelées par le programme.
Notre lecture
La vérification formelle a toujours eu un défaut : elle coûte trop cher pour presque tous les logiciels. AlphaProof Code montre que des agents peuvent produire l’essentiel des preuves, tant que des humains fixent ce qu’il faut prouver et que Lean vérifie tout le reste. C’est un changement de méthode plus qu’un exploit isolé : la confiance passe des agents, faillibles, à un vérificateur mécanique. Mais le résultat porte sur un périmètre précis, un petit programme de test en ligne de commande, une architecture et des hypothèses cryptographiques assumées. La primauté revendiquée et le coût réel en calcul restent à examiner par d’autres équipes, d’autant que Google DeepMind ne dit pas si l’outil lui-même sera proposé à d’autres. Pour les éditeurs de logiciels critiques, la question devient concrète : qui écrira et relira les spécifications, désormais le principal travail humain ?
Sources
- Google DeepMind — Introducing AlphaProof Code: a breakthrough in verifying complex software at depth (10 novembre 2026) Source primaire
- Google DeepMind — AlphaProof Code: Verifying Signal's Security at the Machine-Code Level (article technique et développement Lean) Source primaire
- The Register — Google DeepMind melds humans and AI agents to vet Signal's secure messaging techniques Source secondaire
Une source primaire émane directement de l'entreprise, du laboratoire ou de l'organisme concerné. Une source secondaire rapporte l'information sans en être l'auteur : nous la signalons comme telle. Une erreur ? Consultez notre politique de correction.
