DeepMind a prouvé formellement en 4 semaines les garanties clés de Signal grâce à l'IA

Les tests montrent que le code fonctionne sur les cas que l'on a pensé à vérifier. La vérification formelle répond à une autre question : peut-on prouver mathématiquement que le code ne violera jamais une propriété donnée, quelles que soient les données d'entrée ? Pour la sécurité, c'est un vieux rêve, mais en pratique il se heurte au coût. Il dispose désormais d'un argument de poids : Google DeepMind a prouvé, à l'aide d'agents IA, les garanties clés du protocole cryptographique de Signal.

Ce qui a été fait exactement

L'équipe de DeepMind a utilisé un nouveau framework, AlphaProof Code. Le travail a duré quatre semaines et a été conçu comme une preuve de concept. Le protocole Signal protège les conversations non seulement dans la messagerie Signal elle-même, mais aussi dans Google Messages et WhatsApp : c'est l'un des protocoles cryptographiques les plus utilisés au monde.

En termes simples, la vérification comporte trois étapes. D'abord, des humains décrivent les propriétés que le code doit posséder. Ensuite, cette description est traduite en formules. Enfin, on construit la preuve que le code correspond à ces formules. Avant l'ère de l'IA, ces trois étapes demandaient des mois de travail à des spécialistes. Selon les chercheurs, l'IA agentique réduit fortement la dernière étape, la plus laborieuse.

Le système n'a découvert aucune nouvelle vulnérabilité dans les parties vérifiées du protocole. En revanche, l'inverse a aussi été testé : sur d'anciennes versions de Signal contenant des bugs corrigés de longue date, AlphaProof Code a correctement indiqué qu'il était impossible de construire une preuve. Pour un praticien, c'est un signal important : l'outil ne se contente pas de tamponner « tout est sûr », il bute réellement sur de vrais défauts.

Où est le piège

Il faut garder la mesure de l'ampleur. L'analyse n'a pas couvert toute l'application mobile Signal, seulement certaines parties du protocole. De plus, DeepMind ne partait pas de zéro : Signal Foundation avait déjà mené une vérification formelle de fragments de code plus petits. Cela a donné une longueur d'avance à l'équipe. Le directeur technique de Signal, Eren Kret, souligne que l'approche de DeepMind permet d'élargir considérablement la couverture.

La grande question pour l'industrie est celle de l'échelle et du coût. DeepMind a réalisé l'analyse gratuitement, comme projet de recherche, et Google a refusé de dire combien elle avait coûté. Interrogée sur un éventuel produit ou service commercial de vérification formelle, la société n'a pas répondu non plus. Le chercheur Swarat Chaudhuri reconnaît lui-même qu'il reste « un long chemin » avant de passer à l'échelle de tous les logiciels du monde.

L'humain reste dans la boucle

Le plus intéressant est le processus que l'équipe appelle « human-AI collaboration ». Les agents contribuent à presque toutes les étapes et corrigent eux-mêmes leurs erreurs, mais aux carrefours clés, ils demandent une validation humaine. Chaudhuri dit clairement qu'il ne veut pas d'un « monde de vibe coding » où l'IA formule elle-même les objectifs, écrit elle-même les preuves et, en somme, se fait passer ses propres examens. Il faut un juste milieu.

La logique est claire. Si un modèle imagine à la fois ce qu'il faut prouver et le prouve, une erreur dans la formulation de l'objectif passera inaperçue. La preuve sera formellement correcte, mais elle vérifiera autre chose que ce qui était nécessaire. C'est pourquoi la spécification des propriétés doit être validée de manière réfléchie par un humain.

Que faire de tout cela

Les développeurs et fondateurs dont le produit repose sur une logique critique (paiements, cryptographie, protocoles de synchronisation) devraient désormais considérer la vérification formelle comme une option réelle, et non comme une curiosité académique. Tant que son coût est inconnu, il est trop tôt de la budgéter. Mais il y a un bénéfice concret : DeepMind publie la spécification et la preuve pour Signal, qui peuvent être étudiées et réutilisées dans d'autres travaux de vérification.

Selon Pushmeet Kohli, de Google Cloud et DeepMind, les banques et autres entreprises dépendant de garanties de correction pourront dire « je peux prouver ces propriétés ». Pour l'instant, c'est plus une promesse qu'un produit fini. Mais la vérification par IA a passé son premier test sérieux, sur un protocole réel et massivement utilisé.