Signal prouvé par des agents Gemini : ce que la vérification de DeepMind couvre, et ce qu'elle suppose

Ce qu'il faut retenir

Google DeepMind a démontré, avec une preuve que n'importe qui peut revérifier, que le code compilé de libsignal respecte les grandes garanties de sécurité du protocole Signal. C'est une première : jusqu'ici, les analyses formelles de Signal portaient sur des modèles du protocole, pas sur le programme qui tourne. Mais la preuve repose sur des hypothèses explicites, que l'annonce grand public ne détaille pas : les algorithmes de chiffrement sont supposés sûrs, le scénario couvert est restreint, et le résultat ne s'étend ni à l'application Signal, ni à WhatsApp.

L'annonce est datée du 10 novembre 2026, sur le blog de DeepMind, avec un article technique de neuf auteurs de Google et Google DeepMind et le dépôt des preuves. Elle s'inscrit dans le défi « Signal Shot », lancé en avril 2026 à Paris par la Beneficial AI Foundation, Signal et la Lean FRO pour vérifier en Lean le protocole puis l'application, d'après la page du projet.

Ce qui a été prouvé, et sur quel code

La cible est libsignal, la bibliothèque en Rust qui fait le chiffrement de Signal, dans sa version 0.105.4, limitée aux conversations à deux. Les chercheurs l'ont enveloppée dans un petit programme en ligne de commande, compilé avec le compilateur Rust standard en code machine AArch64, le jeu d'instructions 64 bits d'ARM qu'utilisent presque tous les smartphones. Les théorèmes portent sur ce binaire, instruction par instruction, depuis le démarrage jusqu'à la sortie du programme, selon l'article technique. Conséquence notable : le compilateur Rust n'a pas à être cru sur parole, puisqu'une erreur de compilation ferait échouer la preuve.

Deux parties du protocole sont couvertes : PQXDH, la poignée de main qui établit le secret partagé et résiste à un futur ordinateur quantique, et le Triple Ratchet, qui dérive une nouvelle clé pour chaque message. Les propriétés démontrées sont celles que la littérature attend de Signal : un attaquant qui vole l'état d'un téléphone ne peut pas relire les messages passés (confidentialité persistante), et perd l'accès dès que les deux parties échangent de nouveau (sécurité après compromission) ; les messages restent confidentiels et authentifiés.

Elles sont prouvées dans les deux cadres classiques de la cryptographie. Le modèle « symbolique » traite le chiffrement comme une boîte noire parfaite et donne dix théorèmes, dont la résistance à l'attaque « stocker maintenant, déchiffrer plus tard » d'un futur ordinateur quantique. Le modèle « calculatoire » borne la probabilité de succès d'un attaquant classique par la difficulté des problèmes mathématiques sous-jacents. Pour tester la solidité des énoncés, l'équipe a réintroduit deux failles réelles de libsignal, corrigées depuis, et prouvé en Lean que les binaires fautifs violaient bien le théorème, d'après DeepMind.

Qui a fait quoi : les humains écrivent l'énoncé, les agents la preuve

AlphaProof Code découpe le travail en deux. D'abord, la spécification : un agent rédige les énoncés en Lean avec un chercheur, en partant des modèles publiés de Signal, des agents relecteurs les critiquent, et l'humain approuve. Ces énoncés ont été écrits avec des agents Gemini 4 Carbon et Claude Opus 5.5, un modèle d'Anthropic, chaque brouillon étant relu par un modèle d'une autre famille, précise l'article technique. Ensuite, la preuve : des équipes de 40 à 80 agents Gemini 4 Carbon, le modèle de Google présenté le 28 octobre 2026 et réservé pour l'instant à des défenseurs en cybersécurité, tournaient 24 à 72 heures sur une seule machine, avec un orchestrateur, des chefs d'équipe et un intégrateur seul autorisé à modifier le dépôt.

« Aucun des auteurs n'a écrit de code de preuve », écrivent les chercheurs dans l'article technique (traduction Le Latent). Le travail a pris quatre semaines à une équipe de cinq personnes. Pour donner l'échelle, la vérification du micronoyau seL4, référence du domaine, avait demandé vingt années-personnes, et celle du compilateur C CompCert six, rappellent les auteurs.

Le point le plus intéressant pour qui fait travailler des agents est le garde-fou. Des agents pressés de finir ont tendance à affaiblir l'énoncé qu'on leur demande de prouver, en ajoutant une hypothèse ou en redéfinissant un terme. Ici, un agent « portier » n'accepte une preuve que si le noyau de Lean la valide et si l'outil comparator confirme qu'elle démontre exactement une copie de la spécification que les agents ne peuvent pas modifier. Les agents peuvent proposer de petits amendements, examinés par un critique qui ne voit pas leurs tentatives, puis par un humain quand ils touchent aux hypothèses, selon le même document.

Les chiffres, et ce qu'il faut vraiment relire

Une preuve formelle ne dispense pas de lire quelque chose : il faut lire et croire la spécification. C'est la vraie mesure du résultat, plus que le volume de preuve.

Un écart à signaler : Axios parle de « plus de 3 millions de lignes » de preuves, et le billet de DeepMind de plus de six millions. Le chiffre de l'article technique, 6,5 millions, est celui à retenir. Le billet affirme aussi que les agents n'ont signalé qu'« un pour cent » du code pour relecture humaine, une proportion que l'article technique ne détaille pas.

La spécification a aussi servi de test aux publications existantes. En confrontant les analyses de Signal au code réel, l'équipe dit avoir relevé quinze lacunes ou erreurs dans l'analyse calculatoire de référence du Double Ratchet, et des requêtes mal écrites dans une analyse automatisée publiée, qui rendaient une propriété fausse telle qu'imprimée, d'après l'article technique. Ces erreurs portaient sur les papiers, pas sur libsignal : Wired rapporte que l'analyse n'a trouvé aucune nouvelle faille dans le code examiné.

Ce que la preuve ne couvre pas

Les auteurs listent eux-mêmes les limites, et elles sont nombreuses. Les principales :

• La cryptographie elle-même. SHA-256, AES, X25519, Kyber et ML-KEM ne sont pas vérifiés : ce sont des contrats. Le modèle symbolique suppose un chiffrement parfait ; The Register le souligne aussi.
• Le quantique, en partie. La preuve calculatoire ne vaut que contre un attaquant classique, et la « guérison » post-quantique qu'apporte la nouvelle couche SPQR du Triple Ratchet n'est pas démontrée, selon l'article technique.
• Le scénario. Deux parties, un seul appareil chacune, messages de taille fixe, génération des clés non vérifiée, pas de groupes ni d'expéditeur scellé. La borne calculatoire devient vide pour une session d'environ 25 000 messages si presque chacun ouvre une nouvelle époque, d'après le même document.
• Les attaques physiques. Canaux auxiliaires et autres secrets en mémoire sont hors périmètre.
• L'application. Le binaire prouvé est un outil de test construit par les chercheurs, pas l'appli Signal. Les applis Android et iOS exécutent le même code Rust, mais avec d'autres options de compilation et un autre système, et la transposition reste une hypothèse. Wired rappelle que l'application mobile n'a pas été vérifiée.

WhatsApp, Messenger et Google Messages utilisent des variantes du protocole, mais pas ce code : la preuve ne dit rien de leur implémentation.

Ce qui reste à vérifier de l'extérieur

Contrairement à beaucoup d'annonces d'agents, celle-ci est vérifiable. Le dépôt GitHub est public, avec spécifications et preuves ; créé le 26 octobre 2026, il a reçu sa dernière modification le 10 novembre 2026 à 9 h 34, heure de Paris, d'après l'API GitHub consultée le même jour. Sa licence n'est pas reconnue automatiquement par GitHub, qui l'affiche comme « autre ». Signal a relu la méthode : son directeur technique, Ehren Kret, salue dans le billet de DeepMind une « avancée majeure » (traduction Le Latent), et trois membres de Signal, dont lui, sont remerciés pour leurs retours sur les spécifications.

Ce qui manque encore, c'est une relecture indépendante des 26 000 lignes à croire. Les auteurs l'écrivent : des spécifications de cette complexité demanderont « de nombreux cycles de relecture ouverte ». Au 10 novembre 2026, aucune analyse extérieure n'a été publiée, et Google refuse de dire combien la vérification a coûté en calcul, d'après Wired.

Ce que ça change

Pour les utilisateurs de Signal, rien à faire : aucune faille n'a été trouvée. Pour la sécurité logicielle, le signal est plus fort que celui des agents qui cherchent des bugs, comme ceux d'OpenAI sur le noyau Linux : trouver des failles ne prouve jamais qu'il n'en reste pas, une preuve formelle si, dans les limites de son énoncé. Les auteurs veulent maintenant vérifier les nouvelles versions de libsignal avant leur sortie.

La leçon rejoint celle de la formalisation de Fermat par 1 000 agents Claude, publiée sur Le Latent le 10 novembre 2026 : Lean rend la preuve fiable, mais toute la valeur se joue dans l'énoncé. « Une fois que les preuves deviennent bon marché, la question difficile est de savoir quoi prouver », résument les chercheurs dans l'article technique (traduction Le Latent). Le 11 novembre 2026, DeepMind a aussi ouvert un modèle de génomique, dont les chiffres se lisent avec la même prudence : ce que valent les 30 % d'AlphaGenome 2. Sur la même équipe de DeepMind et la cryptographie, voir aussi l'attaque RSA-1024 refaite par des agents. Les autres analyses de résultats publiés sont dans les Comparatifs du Labo.