DeepMind prouve formellement des pans de Signal en quatre semaines

Quatre semaines pour une démonstration

Selon un article de WIRED repris le 11 novembre 2026 par Ars Technica, des chercheurs de Google DeepMind ont utilisé des agents IA pour vérifier formellement, c’est-à-dire prouver mathématiquement, plusieurs des garanties cryptographiques clés du protocole Signal. Le projet, présenté comme une démonstration de faisabilité, a duré quatre semaines et s’appuie sur un nouveau cadre maison baptisé AlphaProof Code.

L’enjeu n’est pas mince : ce protocole protège les échanges de l’application Signal, mais aussi de Google Messages et de WhatsApp. Autrement dit, une part considérable des conversations de la planète, y compris celles où vous promettez de regarder ce ticket demain.

Ce que l’IA change vraiment

La vérification formelle est le vieux Graal de la sécurité logicielle : au lieu de tester un programme en espérant tomber sur le bug, on démontre par les mathématiques qu’il fait ce qu’il est censé faire. Le problème, jusqu’ici, tenait au temps humain : il fallait décrire les propriétés à prouver, les traduire en formules, puis construire la preuve. D’après l’article, c’est surtout cette dernière étape que les agents raccourcissent nettement.

Le résultat se lit en deux temps. Sur les portions examinées, l’analyse n’a révélé aucune nouvelle vulnérabilité. Et lorsque les chercheurs ont soumis à AlphaProof Code d’anciennes versions de Signal, porteuses de failles connues et corrigées depuis longtemps, l’outil les a correctement identifiées et a montré que le protocole ne pouvait pas y être vérifié formellement. Un outil de preuve qui sait aussi dire non, c’est rassurant. La spécification et la preuve sont publiées pour servir à d’autres travaux.

Côté Signal, le directeur technique Ehren Kret souligne dans une déclaration que les vérifications précédentes portaient sur des portions de code plus réduites et que cette approche permet de les étendre nettement.

Ce qui reste hors de portée

Les limites sont posées par les chercheurs eux-mêmes. Le périmètre d’abord : l’application mobile Signal n’a pas été vérifiée dans son ensemble, seulement des parties du protocole. La vitesse ensuite : DeepMind reconnaît avoir pris de l’avance grâce aux travaux de vérification formelle déjà menés par la Signal Foundation. Quatre semaines, donc, mais pas en partant d’une page blanche.

Reste la question que tout le secteur se pose : cela passe-t-il à l’échelle, et à quel prix ? L’analyse a été réalisée gratuitement, à titre de projet de recherche, et Google a refusé d’en communiquer le coût. L’entreprise n’a pas non plus souhaité dire si un produit ou un service commercial était prévu. Swarat Chaudhuri, chercheur chez DeepMind, se dit très enthousiaste mais reconnaît qu’il reste un long chemin avant d’appliquer la méthode à tous les logiciels du monde.

L’humain reste dans la boucle, et c’est voulu

Pushmeet Kohli, vice-président de la recherche de DeepMind, imagine déjà des banques et d’autres entreprises capables de prouver les propriétés de leur code plutôt que de les espérer. Le rêve est connu ; la facture, elle, ne l’est pas.

L’équipe insiste surtout sur sa méthode, que Swarat Chaudhuri décrit comme un « human-AI collaboration process » : les agents contribuent et se corrigent à presque chaque étape, mais sollicitent une relecture humaine aux moments clés. Le chercheur dit vouloir éviter un monde où l’IA fixerait les objectifs, rédigerait les preuves et passerait en somme des examens qu’elle a elle-même écrits.

N’importe quel développeur ayant écrit ses propres tests un vendredi soir sait exactement de quoi il parle. La preuve formelle, elle, ne se laisse pas attendrir par une coche verte.