Google DeepMind a publié le 10 novembre 2026 un texte de recherche décrivant AlphaProof Code, un cadre agent qui, selon les auteurs, a aidé à démontrer mathématiquement des propriétés essentielles de sécurité du code réel derrière le protocole Signal. Le texte est signé Pushmeet Kohli et Swarat Chaudhuri. Ils ont présenté la vérification formelle d'un protocole cryptographique largement déployé, à cette profondeur, comme un défi de longue date, et indiqué que c'était la première fois que l'intelligence artificielle était utilisée à cette fin. Ils ont aussi indiqué que c'était la première fois que l'implémentation d'un protocole aussi répandu était formellement vérifiée par quelque méthode que ce soit, avec ou sans intelligence artificielle.
Le protocole Signal protège des conversations privées dans des applications comme Signal et Google Messages, ont écrit les auteurs. La plupart des travaux antérieurs de vérification, ont-ils indiqué, s'arrêtaient à la conception du protocole plutôt qu'au code compilé qui s'exécute sur les appareils. AlphaProof Code est décrit comme un partage du travail à la manière d'une équipe de recherche: des spécialistes humains travaillent avec des modèles pour décider ce qui doit être démontré, puis un groupe d'agents réalise les preuves.
DeepMind a indiqué que ses chercheurs avaient collaboré avec plusieurs modèles pour traduire les objectifs de sécurité de Signal en spécifications mathématiques formelles, chaque spécification étant relue par des experts humains. Des agents s'appuyant sur Gemini Carbon ont ensuite généré plus de six millions de lignes de Lean, un langage servant à écrire des preuves mathématiques vérifiées par machine. Les agents ont aussi audité la preuve et signalé environ un pour cent du code pour un second examen humain. Parce que Lean vérifie automatiquement le reste, ont écrit les auteurs, les experts ont pu concentrer leur relecture là où le jugement humain compte encore.
Les agents ont servi à démontrer que le code compilé satisfait des propriétés spécifiées, y compris le fait de garder les messages protégés avant et après qu'un appareil ait été temporairement compromis. Les auteurs ont indiqué que le processus avait pris quatre semaines, contre un travail qui occupe historiquement des équipes spécialisées pendant des années. Pour vérifier si le système distingue un code correct d'un code défaillant, ils ont réintroduit deux vraies failles déjà corrigées dans une version isolée du code de Signal. Dans les deux cas, ont-ils indiqué, le système a produit une preuve vérifiée par machine selon laquelle la version fautive était peu sûre.
Ehren Kret, directeur technique de Signal, est cité disant que la vérification formelle antérieure s'était concentrée sur de plus petites portions du code et que l'usage d'agents pour traduire du code vivant en théorèmes Lean valides constitue une avancée majeure. Il a indiqué qu'à mesure que grandissent les menaces de sécurité alimentées par l'intelligence artificielle, vérifier rigoureusement l'implémentation du protocole donne à Signal une plus grande confiance dans ses garanties de confidentialité. DeepMind a aussi cité d'autres membres de l'équipe de Signal, dont Rolfe Schmidt et Michael Rosenberg, parmi ceux qui ont commenté la méthode.
Les auteurs ont présenté le résultat comme une étape vers l'extension de ce type d'assurance à d'autres logiciels critiques, du micrologiciel de dispositifs médicaux aux systèmes des réseaux électriques, et indiqué qu'ils mettent en libre accès des artefacts de vérification formelle pour la communauté. Ils ont aussi renvoyé les lecteurs vers un article technique sur la même page. Ce travail paraît le même jour que le lancement de Gemini 4 Carbon, que l'annonce de Carbon cite comme le modèle utilisé avec d'autres systèmes à l'intérieur d'AlphaProof Code. Les deux textes sont liés mais décrivent des événements différents: l'un est un résultat de recherche sur le code de Signal, l'autre un changement de disponibilité d'un produit.
Les affirmations sur le caractère inédit du travail, le délai de quatre semaines, les six millions de lignes de Lean et les deux failles réintroduites viennent de DeepMind, étayées par l'appui cité de Signal à l'approche. Cette enquête n'a pas réexécuté les preuves ni audité les artefacts publiés. Il convient de traiter ces chiffres et la comparaison avec des efforts humains de plusieurs années comme le récit des auteurs, et de noter que la vérification porte sur des propriétés clés spécifiées de l'implémentation du protocole, et non sur une promesse sans limite que tous les défauts possibles ont été exclus.