DeepMind a vérifié formellement en quatre semaines les garanties clés du protocole Signal

Les tests montrent que le code fonctionne sur les données d'entrée que vous avez pensé à vérifier. La vérification formelle répond à une autre question : peut-on prouver mathématiquement que le code se comporte correctement quelles que soient les données ? Les ingénieurs y voient depuis longtemps le Saint Graal de la sécurité, mais en pratique les preuves étaient écrites à la main, ce qui prenait des mois, voire des années. DeepMind vient de montrer qu'une part importante de ce travail peut être confiée à un agent.

Ce qui a été fait exactement

Les chercheurs de Google DeepMind ont, à l'aide du nouveau framework AlphaProof Code, vérifié formellement plusieurs garanties cryptographiques clés du protocole Signal. Ce protocole sous-tend le chiffrement dans l'application Signal, Google Messages et WhatsApp. Le projet était une preuve de concept et n'a duré que quatre semaines.

Pour mesurer cette vitesse, il faut comprendre en quoi consiste le travail. D'abord, des humains décrivent les propriétés que le code doit avoir. Ensuite, cette description est transformée en formules. Et seulement après, on écrit la preuve elle-même. L'IA agentique réduit fortement le temps passé sur cette dernière étape, la plus laborieuse.

Il y a aussi un test en conditions réelles. Le système n'a découvert aucune nouvelle vulnérabilité dans les parties étudiées du protocole. En revanche, sur d'anciennes versions de Signal contenant des bogues corrigés depuis longtemps, AlphaProof Code a trouvé ces problèmes et montré qu'un tel code ne peut pas être vérifié formellement. Pour un outil de vérification, c'est un test important : il ne se contente pas de confirmer que « tout va bien », il échoue réellement là où le code est erroné.

Les chercheurs ne partaient pas de zéro. La Signal Foundation avait déjà réalisé la vérification formelle de fragments de code plus petits, ce qui a donné une longueur d'avance à DeepMind. Le directeur technique de Signal, Eren Kret, explique que l'approche de DeepMind permet d'élargir nettement la couverture de la vérification, ce qui renforce la confiance dans la confidentialité de l'implémentation.

Pourquoi c'est important pour les praticiens

Le principal changement concerne le coût. La vérification formelle était hors de portée de la plupart des équipes non pas parce que personne n'en comprenait l'intérêt, mais parce que les preuves coûtaient trop cher en temps humain. Si les agents prennent en charge le travail de routine, le périmètre du code qu'il est pertinent de prouver s'élargit. Pushmeet Kohli, de Google Cloud et DeepMind, évoque directement les banques et d'autres entreprises qui pourront affirmer : « je peux prouver ces propriétés ».

L'élément le plus sensé du projet est l'organisation du travail. Les agents contribuent et s'autocorrigent presque à chaque étape, mais sollicitent une vérification humaine aux points clés. Swarat Chaudhuri, chercheur chez DeepMind, explique pourquoi : il ne faut pas un « monde vibe » où l'IA génère elle-même les objectifs, écrit elle-même les preuves et, en somme, passe des tests qu'elle a elle-même rédigés. Il faut un juste milieu.

Pour le développeur, la conclusion est simple. Une preuve vaut exactement ce que vaut la spécification, c'est-à-dire la description de ce qui est considéré comme un comportement correct. Si le modèle écrit à la fois la spécification et la preuve, on obtient un joli document sans aucune garantie. La responsabilité de la formulation des exigences reste à l'humain.

Limites et marche à suivre

Il faut garder la mesure quant à l'échelle. L'application mobile Signal dans son ensemble n'a pas été vérifiée, seulement certaines parties du protocole. Chaudhuri reconnaît lui-même que la vérification de tous les logiciels du monde est encore très lointaine. Le système n'a trouvé aucun nouveau bogue ; pour l'instant, il s'agit donc plutôt de la confirmation du travail d'autrui que d'une découverte.

La grande question de l'industrie est l'économie. DeepMind a réalisé cette analyse gratuitement, comme projet de recherche, et Google n'a pas dévoilé le coût. L'entreprise a aussi refusé de commenter l'éventualité d'un produit commercial ou d'un service de vérification formelle. Autrement dit, il n'existe pas encore de bouton « vérifier mon code » prêt à l'emploi.

Ce que l'on peut faire dès maintenant. Les chercheurs publient la spécification et la preuve pour Signal, ce qui constitue un bon support d'apprentissage pour ceux qui écrivent du code critique : paiements, cryptographie, infrastructures de confiance. Si vous travaillez dans ces domaines, il est judicieux de suivre la transformation d'outils comme AlphaProof Code, de démonstration en produit, et d'apprendre dès maintenant à formuler les propriétés du code de façon à pouvoir les prouver. Selon toute vraisemblance, c'est cette compétence, et non l'écriture manuelle de preuves, qui prendra de la valeur.