Google DeepMind, la division d'intelligence artificielle de Google, a annoncé le 10 novembre 2026 avoir vérifié formellement des propriétés de sécurité du code réel du protocole Signal, grâce à un nouveau cadre d'agents IA baptisé AlphaProof Code. Cette vérification formelle du protocole Signal porte sur les protections cryptographiques de base, jusqu'aux instructions machine, selon le billet officiel de l'entreprise signé par Pushmeet Kohli et Swarat Chaudhuri.

Le sujet intéresse directement le débat sur les messageries chiffrées, comme le montre l'actualité récente sur les messageries chiffrées et l'abandon des portes dérobées de l'article 16 bis en France. Il s'agit ici d'un projet de recherche et non d'un produit : la vérification concerne le code sous-jacent au protocole, pas l'application Signal dans son ensemble.

Comment AlphaProof Code vérifie-t-il le protocole Signal ?

AlphaProof Code repose sur une répartition du travail entre humains et agents IA. Selon DeepMind, des experts humains valident d'abord les spécifications, c'est-à-dire ce que le code doit garantir. Des agents propulsés par Gemini Carbon produisent ensuite les preuves correspondantes.

Ces preuves sont écrites en Lean, un langage dont le vérificateur contrôle automatiquement chaque étape. Seule une petite fraction du code, environ 1 %, est signalée pour une relecture humaine, le reste étant validé par Lean. DeepMind parle de millions de lignes de preuve vérifiées par machine pour couvrir les protections cryptographiques essentielles de Signal.

Quatre semaines de travail et un test avec deux bugs réintroduits

Le projet de vérification du code de Signal a pris quatre semaines, d'après DeepMind, qui le présente comme une démonstration de faisabilité. Pour contrôler la méthode, l'entreprise a réintroduit deux bugs réels, déjà corrigés, dans une version isolée de Signal. Le système a produit une preuve établissant que cette version défectueuse n'était pas sécurisée.

Sur le code actuel, l'analyse n'a relevé aucune nouvelle vulnérabilité dans les parties couvertes. Cette formulation compte : la vérification porte sur des propriétés précises et sur des portions définies du code, ce qui ne revient pas à démontrer que l'ensemble d'un système de messagerie est sûr.

Ce que dit Signal de cette vérification formelle

Le directeur technique de Signal, Ehren Kret, a réagi dans le billet de Google DeepMind. Il souligne la différence d'échelle avec les travaux précédents :

Alors que les vérifications formelles antérieures se concentraient sur des portions plus petites du code, l'approche de Google DeepMind permet une extension significative.

Des travaux de vérification formelle avaient déjà été menés par la Signal Foundation, qui constituent un point de départ pour cette analyse. Un autre projet, Signal Shot, mené avec la Lean FRO et la Beneficial AI Foundation, cofondée par Max Tegmark, vise lui aussi à vérifier le protocole et son implémentation en Rust.

AlphaProof Code : ressources publiées et disponibilité

DeepMind publie en open source ses artefacts de vérification, ainsi qu'un document technique détaillant la méthode. Aucun produit ni service grand public n'est annoncé, et aucune date ni aucun pays de disponibilité n'est mentionné : les utilisateurs de Signal ne voient aucune fonctionnalité modifiée à ce stade.

Le billet cite Signal et Google Messages parmi les messageries concernées par le protocole. Le coût du projet n'a pas été communiqué, et Google n'a pas indiqué s'il compte proposer l'outil commercialement. La question de son usage sur des bases de code de plus grande taille reste ouverte.