AlphaProof Code a prouvé que la cryptographie de Signal est correcte — au niveau du binaire compilé

Six millions et demi de lignes de Lean, produites en quatre semaines, par des équipes d'agents à l'écriture desquelles aucun humain n'a contribué. C'est le chiffre phare que Google DeepMind a publié le 10 novembre 2026 pour AlphaProof Code, un cadre agentique de vérification formelle que le laboratoire a utilisé pour vérifier mécaniquement le cœur cryptographique du protocole Signal — et, fait inhabituel, pour le vérifier au niveau du binaire AArch64 compilé plutôt qu'à celui du document de conception situé au-dessus. Les modèles qui ont réalisé le travail sont une autre question. une clé API au prix catalogue du fournisseur, avec 0 % de majoration Le moteur des agents de preuve ne fait pas partie des services que nous proposons.

Le framework n’est pas un modèle que l’on peut appeler. C’est un harnais : des experts humains décident de ce qui doit être vrai, un mélange de modèles transforme ces objectifs en spécifications Lean, puis des équipes d’agents rédacteurs de preuves — le blog cite G​emini Carbon comme moteur — complètent les preuves jusqu’à ce que le noyau de Lean les accepte. Ce qui accompagne l’annonce, c’est l’ensemble d’artefacts, à github.com/google-deepmind/code-verification, et un article technique qui est bien plus franc sur les limites du résultat que ne l’est le billet de blog. L’essentiel de ce qui suit provient de cet article, car c’est là que se trouvent les chiffres intéressants.

Qu’a-t-on réellement prouvé, et contre quoi ?

La cible est libsignal v0.105.4 avec spqr v1.6.0, compilé par rustc 1.98.1 standard, lié statiquement à musl et produit sous la forme d’un unique exécutable Linux AArch64. Ce détail compte plus que n’importe quel benchmark : les preuves portent sur les octets qui s’exécuteraient sur un téléphone, et non sur une fonction Rust dont on fait confiance au compilateur pour la traduire fidèlement. L’équipe a vérifié environ 560 Ko de code source de libsignal, environ 140 000 instructions AArch64, et elle y est parvenue en écrivant un modèle Lean du jeu d’instructions — 467 instructions et 31 appels système, en 7 578 lignes — puis en prouvant que l’image ELF réelle, chargée et exécutée sous ce modèle, préserve les propriétés de sécurité.

Les propriétés sont celles qu’un ingénieur en protocoles demanderait. Dix théorèmes symboliques couvrent la confidentialité persistante, la sécurité après compromission, la confidentialité de l’initiateur et du répondeur, l’authentification, ainsi que cinq corollaires du théorème 1 de PQXDH. Le résultat principal est nommé signal_session_secure_placed. Il existe également un volet calculatoire avec une borne concrète, et les deux volets utilisent des modèles d’adversaire différents : le côté symbolique (Dolev–Yao, via le cadre DyLean) couvre même un attaquant quantique qui casse Diffie–Hellman après la poignée de main, tandis que le côté calculatoire ne couvre que les adversaires classiques.

Où vont les six millions de lignes

« Plus de six millions de lignes » est la formulation du blog, exacte mais grossière. La ventilation détaillée de l’article est celle qui est utile, et il vaut la peine de la lire comme un tableau des coûts plutôt que comme une vantardise :

• Preuves pour le binaire — 5,3 millions de lignes, l’essentiel du travail, couvrant la sémantique du code machine et le raffinement depuis le modèle symbolique jusqu’à l’exécutable.

• Preuves computationnelles — environ 860 000 lignes.

• Preuves symboliques — environ 350 000 lignes.

• Preuves de réfutation de bogues — environ 140 000 lignes, pour les deux vulnérabilités réintroduites délibérément décrites ci-dessous.

• Preuves de l’allocateur — environ 70 000 lignes.

Près de sept millions de lignes si l’on compte les commentaires et les lignes vides, ce que fait l’article et pas le billet de blog. Quoi qu’il en soit, le ratio qui compte est celui entre la preuve et ce qui est prouvé : 6,5 millions de lignes de Lean pour établir des propriétés d’un binaire de 560 Ko. Ce ratio est la mesure honnête de la distance qui sépare cette technique de la routine, et c’est le chiffre à citer quand quelqu’un demande si la vérification formelle est devenue bon marché.

La base de confiance est plus petite que la preuve, et c’est précisément là tout l’intérêt.

Une preuve ne vaut que ce que valent ses hypothèses. L’article est précis sur ce point, et cette précision est ce qui le distingue d’un communiqué de presse. Les spécifications de confiance font environ 18 000 lignes (28 000 avec la documentation), la sémantique AArch64 environ 8 000, et l’encodage Lean du code machine environ 95 000. Trente-sept routines sont remplacées par des contrats plutôt que vérifiées — la compression SHA-256 et SHA-512, AES-256-CBC, X25519, les opérations sur courbe d’Edwards, Kyber1024 et ML-KEM-768, et le HMAC de libcrux. Dix-huit points d’entrée de panique sont de même supposés plutôt que prouvés.

Ainsi, l'affirmation n'est pas « tout est prouvé ». L'affirmation est que la logique du protocole cryptographique, la machine à états de session et le raffinement de cette logique vers les instructions réellement exécutées sont prouvés, tandis que les primitives sous-jacentes sont supposées fiables de la même manière que tout projet de vérification fait confiance à ses primitives. Le compilateur Rust, notamment, n'est pas dans la base de confiance — l'équipe a évité de devoir lui faire confiance en raisonnant au niveau du code machine, ce qui est la même astuce qui leur permet de se passer entièrement d'un compilateur vérifié. Pour donner une idée de l'échelle, l'article cite seL4 à environ 20 années-personnes et CompCert à environ 6.

Deux bugs, réintroduits volontairement

Un système de vérification qui ne dit jamais que « correct » est impossible à tester. L’équipe a donc pris deux vulnérabilités qui avaient auparavant été trouvées et corrigées dans le code de Signal — un bug d’état faible et un bug de petit sous-groupe — les a réintroduites dans une copie isolée, puis a relancé le pipeline. Dans les deux cas, AlphaProof Code a produit une preuve vérifiée par machine que la version boguée échoue au théorème de sécurité : l’énoncé symbolique se réduit à ¬Sec(Asm_bug).

L'article ajoute une réserve qu'une page marketing aurait supprimée : réfuter le théorème calculatoire pour ces bugs est « bien plus difficile » et a été laissé en suspens. Autrement dit, le test négatif fonctionne proprement sur le volet symbolique et ne fonctionne pas encore sur le volet calculatoire. C'est exactement le type d'asymétrie qu'un lecteur devrait connaître avant de considérer ce cadre comme un détecteur de bugs.

Comment les agents ont été exécutés

Cinq chercheurs sur quatre semaines, chacun faisant tourner des agents sans interruption. La rédaction des preuves elle-même a été assurée par des équipes de 40 à 80 agents, fonctionnant entre 24 et 72 heures sur une seule machine par équipe, avec un agent superviseur au-dessus de l'orchestrateur d'équipe. Un agent gardien vérifie chaque soumission à l'aide d'un comparateur par rapport à une copie de la spécification tenue à l'écart et au noyau de Lean — une protection contre un agent qui démontrerait une version subtilement affaiblie de ce qui était demandé.

Le travail humain a été concentré en amont sur les spécifications. Chaque spécification a été examinée par un expert avant le début du travail de preuve, et la passe d’audit des agents eux-mêmes a signalé environ 1 % de la base de code comme nécessitant l’attention humaine. Aucun humain n’a écrit de code de preuve. L’article est également très franc sur l’ingénierie : une compilation propre peut prendre plusieurs heures, au début, une modification mineure du code source ou un binaire recompilé a entraîné d’importantes réparations de preuves, et il existe « un large champ d’optimisation » tant dans les preuves générées par l’IA que dans les techniques de preuve elles-mêmes.

Ce que les preuves ne couvrent pas

Les limites sont suffisamment longues pour constituer la section la plus importante de l’article, et elles sont énoncées clairement. Aucune garantie post-quantique n’est établie pour la propriété de guérison de SPQR — les théorèmes de ratchet supposent que l’attaquant choisit les clés SPQR. La confidentialité de la charge utile n’est pas prouvée. L’authentification du répondeur n’est pas prouvée pour le premier message d’une poignée de main qui n’est jamais promue. Le modèle autorise une seule session par promotion, des longueurs de message fixes, aucun état multi-appareil et des clés d’identité fondées sur la confiance au premier usage.

Il y a aussi une borne qui devient vide. Le terme de falsification MAC de 8 octets est d'au moins 2⁻⁶⁴ par tentative et croît quadratiquement avec le nombre de messages et d'époques, ce qui signifie que la borne ne dit plus rien pour une seule session d'environ 25 000 messages, ou pour 2²⁰ sessions de 2¹⁰ messages. Et le sujet de la preuve est la version de libsignal-cli compilée par l'équipe, exécutée comme un nouveau processus — et non l'application Signal sur votre téléphone. Plusieurs hypothèses sur l'environnement sont justifiées de manière informelle plutôt que prouvées.

Il n’y a ni API, ni prix, ni modèle à appeler.

C’est la partie qui risque de décevoir quiconque arrive depuis un classement de modèles. AlphaProof Code est un cadre de recherche et un ensemble d’artefacts publiés. Il n’y a ni point de terminaison, ni grille tarifaire par token, ni liste d’attente, ni poids : le dépôt contient le développement Lean, la sémantique AArch64, le binding libsignal et les spécifications, pas un checkpoint. Le billet de blog indique que les artefacts sont open source ; la page d’accueil ne mentionne aucune licence, ce qu’il vaut la peine de vérifier avant d’envisager de construire dessus.

Les modèles qui ont fait le travail constituent une autre question. L’article cite G​emini 4 Carbon pour les agents de preuve et indique que Claude Opus 5.5 a été utilisé aux côtés d’autres modèles pour rédiger et réviser des spécifications. Claude Opus 5.5 figure aujourd’hui au catalogue d’OrcaRouter à 4 $ par million de jetons d’entrée et 20 $ par million de jetons de sortie, avec le prix catalogue du fournisseur répercuté à 0 % de marge — donc si ce que vous voulez retenir concrètement est « lancer une boucle de rédaction de spécifications avec le modèle utilisé dans l’article », cette partie est un appel d’API ordinaire, et un changement de prix du fournisseur est répercuté de notre côté le jour même. Le moteur des agents de preuve n’est pas un service que nous proposons, et rien ici n’implique que nous hébergions AlphaProof Code lui-même.

Pourquoi c'est plus important que le résultat de Signal

La vérification de Signal est impressionnante en soi — la première vérification formelle, pour un protocole largement déployé, de l'implémentation par toute méthode, avec ou sans IA, selon DeepMind, et la première fois que l'IA a vérifié un protocole cryptographique déployé à ce niveau de profondeur. Mais l'argument transférable, c'est le flux de travail. Une équipe de cinq personnes, en quatre semaines, avec une étape de revue de spécification et un agent garde-fou, a produit un corpus de preuves qui aurait auparavant été un projet de plusieurs années. Si ce ratio tient, même approximativement, l'ensemble des systèmes qui peuvent se permettre une vérification change : le firmware des dispositifs médicaux, les logiciels des réseaux électriques, le genre de code qui, actuellement, a droit à une revue de code et à une prière.

La question de savoir si cela tient n’a pas été testée. La cryptographie de Signal est exceptionnellement bien spécifiée, l’équipe a fait réviser la méthodologie par les propres ingénieurs de Signal, et les primitives ont été sous-traitées plutôt que vérifiées. Le prochain système ne sera pas aussi accommodant. Le cadrage du document lui-même — associer la vérification formelle à des agents de défense automatisés comme CodeMender — est la forme honnête de l’argumentaire : la vérification dit ce qui est vrai, et autre chose doit corriger ce qui ne l’est pas.

Quoi regarder

Trois choses feraient passer cet article d’un article de référence à une technique industrielle. Une deuxième base de code indépendante, vérifiée par quelqu’un extérieur à G​oogle, idéalement une base où la spécification aurait dû être écrite de zéro plutôt qu’adaptée à partir d’une analyse existante. Un chiffre de coût — heures-agent, heures-accélérateur, dollars — car quatre semaines et des équipes de 40 à 80 agents ne constituent pas une unité sur laquelle un responsable d’ingénierie peut établir un budget. Et la réfutation de bogues sur le volet computationnel, que l’article laisse en suspens et qui fait la différence entre un système qui prouve des propriétés et un système qui peut aussi vous dire, par le calcul, qu’un binaire spécifique est défaillant.

D'ici là, lisez le dépôt d'artefacts plutôt que l'annonce. Les preuves y sont, Lean les vérifie, et l'article vous dit exactement ce qu'elles supposent.