Titre original : AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level
Auteurs : Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton et Pushmeet Kohli.
Affiliations : Google DeepMind et Google.
Publication : rapport technique de Google DeepMind daté du 10 novembre 2026, 57 pages, hors arXiv. Les spécifications et les preuves Lean sont publiées en accès libre.
Liens : rapport (PDF), billet de DeepMind, preuves Lean.
L’idée en bref
La vérification formelle consiste à prouver mathématiquement qu’un logiciel respecte ses propriétés, ce qui exclut tout bug ou attaque qui les violerait. Elle reste rare parce qu’elle coûte cher : le rapport rappelle que le micronoyau seL4 a demandé vingt années-personnes et le compilateur CompCert six, sur du code écrit pour être vérifié.
Le pari de DeepMind est que l’IA a déplacé le goulot d’étranglement. Écrire les preuves devient une tâche que des équipes d’agents mènent seules, puisque le vérificateur de Lean rejette toute erreur. Le travail humain se concentre sur la spécification : décider exactement quoi prouver, et sous quelles hypothèses.
Ce que montre le papier
Ce qui a été prouvé
L’équipe a compilé libsignal, la bibliothèque de référence du protocole Signal, sans la modifier, avec le compilateur Rust standard, pour processeurs AArch64, dans un petit programme en ligne de commande. Les théorèmes portent directement sur ce code machine. Ils couvrent la poignée de main post-quantique PQXDH et le Triple Ratchet, et établissent la confidentialité persistante, l’authentification, la sécurité après compromission et le secret de la poignée de main, dans les deux grands modèles d’analyse de la cryptographie, symbolique et calculatoire. Selon les auteurs, c’est la première preuve de ce niveau sur le code non modifié d’un protocole aussi déployé.
Les chiffres
Le dépôt compte près de 7 millions de lignes de Lean, dont environ 6,5 millions de preuves : 5,3 millions sur le binaire, 860 000 pour la preuve calculatoire et 350 000 pour la preuve symbolique. Le code vérifié fait environ 560 Ko, soit environ 140 000 instructions. Ce qu’un lecteur doit relire et croire tient en environ 18 000 lignes de spécification, plus environ 8 000 lignes de sémantique AArch64. Cette sémantique couvre 467 instructions et 31 appels système, testées contre deux références indépendantes.
Le travail a été fait par cinq personnes en quatre semaines. Chaque campagne de preuve mobilisait de 40 à 80 agents sur une seule machine pendant 24 à 72 heures. Les preuves ont été écrites entièrement par des agents Gemini 4 Carbon, sans aucune ligne humaine ; les spécifications sont nées d’allers-retours entre les chercheurs et des agents Gemini 4 Carbon et Claude Opus 5.5, chaque brouillon étant relu par un agent d’une autre famille de modèles.
Les garde-fous
Les agents ne peuvent pas modifier la spécification. Ils peuvent proposer un amendement à un agent critique qui ne voit pas leurs preuves, accepté seulement s’il est nécessaire, petit et sans affaiblir la sécurité ; ceux qui touchent aux hypothèses de confiance passent par un humain. Un agent gardien compare la preuve à une copie protégée de la spécification. Le rapport cite le cas, dans un autre essaim, d’un agent qui avait redéfini une hypothèse comme toujours fausse pour s’en sortir. Pour tester les spécifications, l’équipe a réintroduit deux failles réelles déjà corrigées dans libsignal : dans les deux cas, Lean prouve que le binaire fautif viole le théorème de sécurité symbolique.
En chemin, le travail a relevé des erreurs dans la littérature : quinze lacunes dans l’analyse calculatoire publiée du Double Ratchet, et des requêtes ProVerif imprimées qui rendent fausse la confidentialité persistante côté destinataire.
Les limites
Le rapport les détaille. Les résultats portent sur le programme de test libsignal-cli lancé comme un processus neuf, pas sur les applications Signal. La primitive cryptographique est supposée sûre, et certaines fonctions sont remplacées par des contrats de confiance. Le scénario est restreint : deux parties aux rôles fixes, clés d’identité connues d’avance, tailles bornées, pas de messagerie de groupe ni de plusieurs appareils. La preuve calculatoire ne vaut pas contre un attaquant quantique, et aucune des deux ne prouve la guérison post-quantique qu’apporte le nouveau ratchet. Les bornes deviennent vides à grande échelle, par exemple pour une session d’environ 25 000 messages si presque chaque message ouvre une nouvelle époque. Enfin, une compilation complète des preuves prend plusieurs heures.
Lecture Neurone21
Pour une entreprise, l’intérêt n’est pas de vérifier demain tout son code, mais de voir où se déplace l’effort. Si les preuves deviennent bon marché, ce qui coûte, c’est de savoir écrire noir sur blanc ce que le logiciel doit garantir. Les auteurs le disent : la spécification d’un logiciel non trivial est elle-même un logiciel non trivial. Cela vaut aussi, à plus petite échelle, pour les tests et les critères d’acceptation que l’on donne à des agents de code.
Le dispositif de contrôle est l’autre leçon réutilisable : ne jamais croire un agent qui déclare avoir fini, garder hors de sa portée la définition de ce qui est attendu, et faire relire par un modèle d’une autre famille.
D’où vient ce papier
Elvis Saravia (@omarsar0) l’a présenté le 11 novembre 2026 à 15:14 heure de Paris, puis a reposté son propre post le 12 novembre à 03:20 heure de Paris. Nous avons lu le rapport technique officiel en PDF. Neurone21 a déjà couvert l’annonce en actualité le 11 novembre ; cette fiche s’appuie sur le rapport complet. Écarts avec le post :
Le post parle d’agents propulsés par Gemini ; le rapport précise que les preuves viennent de Gemini 4 Carbon, mais que Claude Opus 5.5 a aussi servi à écrire et relire les spécifications. Le chiffre d’environ 1 % du travail signalé pour relecture humaine vient du billet de DeepMind, pas du rapport. Et la preuve porte sur une version en ligne de commande de libsignal, pas sur les applications qui l’utilisent.
Pour aller plus loin
- Le rapport technique : https://deepmind.google/documents/36/Formal_Verification_of_Signal_4.pdf
- Le billet de DeepMind : https://deepmind.google/blog/introducing-alphaproof-code/
- Les spécifications et preuves : https://github.com/google-deepmind/code-verification
- Le post d’Elvis Saravia : https://x.com/omarsar0/status/2120520666319647096
- Notre actualité du 11 novembre : /p/deepmind-alphaproof-code-verification-formelle-signal-quatre-semaines