Le code de Signal est désormais prouvé, pas seulement testé

Votre équipe a écrit des tests. Ils passent tous. Trois semaines plus tard, un client signale une facture calculée de travers. Le test existait, il vérifiait le bon cas, et il ne couvrait pas celui qui est arrivé.

C'est la limite ordinaire du test. Il montre qu'un programme se comporte bien sur les cas qu'on a pensé à lui donner. Il ne dit rien des autres.

Le 10 novembre 2026, Google DeepMind a annoncé avoir franchi une étape d'une autre nature. Ses chercheurs ont fait démontrer par des agents d'intelligence artificielle que le code de Signal se comporte correctement. Pas sur quelques exemples : sur tous les cas décrits par une définition mathématique du comportement attendu.

Signal est une application de messagerie chiffrée. Des variantes de son protocole, c'est-à-dire de la façon dont deux téléphones se mettent d'accord pour chiffrer leurs échanges, équipent aussi WhatsApp et Google Messages.

Ce que Google a fait, en clair

Le travail porte sur libsignal, la bibliothèque de code qui met en œuvre le protocole de Signal. Autrement dit le morceau de programme que l'application appelle pour chiffrer et déchiffrer. Une erreur y expose des millions de conversations.

Trois chiffres donnent la mesure. Le code vérifié pèse environ 560 kilooctets, soit à peu près 140 000 instructions machine. Les agents ont produit environ 6,5 millions de lignes de démonstration. Une équipe de cinq personnes y a consacré quatre semaines, sans écrire elle-même une seule ligne de ces démonstrations.

Deux comparaisons situent le résultat. La vérification du noyau seL4, un petit système d'exploitation, a demandé vingt années de travail d'une personne. Celle du compilateur CompCert en a demandé six. Ces deux projets avaient en plus été écrits pour être vérifiables, ce qui n'est pas le cas d'un code industriel existant.

Tester et prouver ne sont pas la même chose

Un test ressemble à une dégustation. On goûte la soupe à trois endroits, elle est bonne, on sert le plat. Une preuve ressemble à un calcul de cuisine : on démontre que, avec ces ingrédients et ces étapes, le résultat ne peut pas être autrement.

La vérification formelle est ce second travail. On écrit d'abord, dans un langage mathématique, ce que le programme doit garantir. Puis on démontre que le programme le garantit, pour tous les cas autorisés, sans exception.

Le langage utilisé ici s'appelle Lean. Sa particularité est décisive. La démonstration est elle-même relue par un petit programme, appelé noyau, qui refuse tout raisonnement faux. Un agent d'intelligence artificielle peut donc proposer une démonstration. Il ne peut pas faire passer une erreur pour une preuve.

C'est la différence avec un modèle qui répond en langage courant : on croit sa réponse. Ici, une machine sans opinion la vérifie.

Pourquoi descendre jusqu'au code de la machine

La plupart des vérifications s'arrêtent au plan. On prouve que la conception du protocole est saine, sur le papier ou dans un modèle simplifié. Le défaut réel arrive souvent plus bas. Il se loge dans la traduction du plan vers le programme, puis vers les instructions que le processeur exécute.

L'analogie est celle du bâtiment. Vérifier le plan de l'architecte ne dit pas si les murs montés ont les bonnes dimensions. Les chercheurs ont donc vérifié le bâtiment tel qu'il est construit.

Ils ont pris libsignal sans le modifier, l'ont compilé avec le compilateur standard du langage Rust, puis ont analysé le fichier produit. Ce fichier contient les instructions destinées à une famille de processeurs, les ARM 64 bits, désignée par le nom AArch64. C'est ce fichier que la machine exécute réellement.

Les propriétés démontrées sont celles qui comptent pour une messagerie. Le secret des messages anciens. Le secret rétabli après le vol temporaire d'un téléphone. L'authentification de l'interlocuteur. Et le secret de l'échange initial, même face à un futur ordinateur quantique.

La partie que la preuve ne couvre pas

Une preuve ne vaut que par la phrase qu'elle démontre. Cette phrase s'appelle la spécification. Des chercheurs l'ont écrite avec l'aide de plusieurs modèles, puis des humains l'ont approuvée, une propriété après l'autre.

Le chiffre à retenir n'est donc pas les 6,5 millions de lignes de démonstration. C'est le petit nombre de lignes qu'un lecteur doit lire et croire pour accepter le résultat. Environ 18 000 lignes de définitions, plus environ 8 000 lignes décrivant le fonctionnement du processeur.

DeepMind indique que les agents ont signalé environ 1 % du code pour une seconde relecture humaine. Cela ne veut pas dire que 1 % suffise à auditer. La confiance repose sur ces 26 000 lignes environ, pas sur le reste.

Les auteurs signalent un risque plus subtil. Un agent sommé de finir peut affaiblir l'énoncé plutôt que le démontrer, en ajoutant une condition ou en restreignant son champ. Dans un cas documenté ailleurs, un agent a remplacé une définition par « faux », et la ruse s'est propagée à son équipe. D'où un garde-fou. La démonstration finale est rejouée dans un environnement neuf, et certains raccourcis sont refusés d'office.

L'article liste aussi plus de 200 endroits où ses énoncés s'écartent des publications de référence. La plupart sont sans conséquence. Quinze sont des oublis ou des erreurs dans une analyse publiée du Double Ratchet, le mécanisme qui renouvelle les clés à chaque message.

Les limites sont écrites noir sur blanc. La cryptographie elle-même est supposée parfaite : les fonctions de chiffrement sont traitées comme des boîtes dont on connaît le contrat, pas comme des objets prouvés. Une seule famille de processeurs est couverte. Les conversations à plus de deux participants ne le sont pas. Et la garantie perd sa valeur au-delà d'environ 25 000 messages dans une même session, selon l'article.

Enfin, ce n'est pas une preuve que l'application Signal est sans défaut. C'est une preuve sur le cœur cryptographique, dans un exécutable de test. Ni le blog ni l'article technique ne donnent le coût de calcul de l'opération.

Le contrôle qui donne du poids au résultat

Un résultat vert ne prouve rien s'il ne peut pas virer au rouge. Les chercheurs ont donc fait le test inverse.

Ils ont repris deux défauts réels de libsignal, déjà corrigés, et les ont réintroduits dans une copie isolée. L'un concernait un état de session mal rangé. L'autre, une vérification manquante sur une clé publique. Dans les deux cas, la démonstration a établi que la version fautive violait la propriété de sécurité.

La méthode sait dire non. Un audit qui ne produit jamais de refus n'est pas un audit, c'est une confirmation.

Signal réagit par la voix de son directeur technique, Ehren Kret, cité dans l'annonce. Il parle d'une avancée majeure et souligne que les vérifications antérieures portaient sur des portions plus petites du code.

Trois questions à poser à votre prestataire

Qu'est-ce qui est prouvé, exactement ? Demandez la spécification, pas la conclusion. Une phrase comme « notre logiciel est vérifié » ne veut rien dire sans la liste des propriétés couvertes et des hypothèses retenues.

Sur quel code, et sur quelle machine ? Une preuve sur un modèle de conception et une preuve sur l'exécutable ne disent pas la même chose. La seconde est plus forte, et plus rare.

Qui a approuvé la spécification ? C'est le point de passage obligé. Ici, des humains ont validé chaque propriété, et c'est ce travail qui a pris le plus de temps. Si personne ne peut nommer l'auteur de la spécification, la preuve ne protège personne.

Reste le bon usage. Aujourd'hui, l'exercice vise des morceaux de code petits, stables et critiques : signature, paiement, gestion des clés. Il ne couvre pas un back-office qui change tous les mois. Sur un logiciel en mouvement, la spécification se périme plus vite que la preuve ne se fabrique.

Gardez aussi vos tests. Une preuve couvre ce que la spécification décrit. Elle ne dit rien d'un besoin mal compris, ni d'un cas que personne n'a jugé utile de décrire. Écrire en français ce qui ne doit jamais arriver dans votre système est déjà un gain, même sans preuve.

Ce qu'il faut retenir

• Google DeepMind a fait démontrer par des agents d'IA que le code compilé de Signal respecte plusieurs propriétés de sécurité. Cinq personnes, quatre semaines.
• Une preuve mathématique ne remplace pas un test. Elle couvre tous les cas décrits par une spécification, et rien de plus.
• Environ 6,5 millions de lignes de démonstration reposent sur environ 26 000 lignes à lire et à croire. C'est cette base qui fait la valeur du résultat.
• Deux anciens défauts réintroduits ont été détectés par la méthode. Sans cas d'échec, un résultat positif ne prouve pas grand-chose.
• Le périmètre est étroit : cœur cryptographique, un seul type de processeur, conversations à deux, cryptographie supposée parfaite. L'application entière n'est pas couverte.
• La question utile à poser n'est pas « est-ce vérifié ? » mais « quoi, sur quel code, et qui a approuvé la spécification ? ».