AlphaProof Code de DeepMind a vérifié formellement le protocole cryptographique de Signal en 4 semaines

Tout développeur connaît ce sentiment : les tests sont au vert, la revue de code est passée, l'audit n'a rien trouvé, et pourtant on dort mal. Les tests vérifient des scénarios précis, et un bug peut se cacher dans celui que personne n'a imaginé. Pour une application web ordinaire, c'est tolérable. Pour la cryptographie, sur laquelle repose la confidentialité de millions de conversations, ça ne l'est pas.

Google DeepMind propose une autre voie avec AlphaProof Code. Il s'agit d'un système multi-agents qui automatise la vérification formelle du code.

Qu'est-ce que la vérification formelle, sans les maths

Imaginez une fonction de tri. Les tests la vérifieront sur une centaine de tableaux. La vérification formelle procède autrement. On commence par écrire les propriétés de façon mathématique : en sortie, le tableau est ordonné et contient les mêmes éléments qu'en entrée. Ensuite, on construit une preuve que le code respecte ces propriétés pour n'importe quel tableau, et pas seulement pour une centaine d'exemples.

C'est le plus haut niveau de garantie en sécurité. Mais presque personne ne l'utilise : la méthode est coûteuse et longue, et les spécialistes sont rares. La preuve est souvent plus longue que le code lui-même, et il faut l'écrire à la main.

Ce qui a été fait avec Signal

L'équipe a appliqué AlphaProof Code au code du protocole cryptographique de Signal, qui chiffre les conversations dans Signal et Google Messages. Les agents, basés sur Gemini 4 Carbon, ont écrit plus de six millions de lignes en Lean, un langage et un environnement vérifiable pour les preuves formelles. Résultat : il est mathématiquement prouvé que le code assure les garanties de sécurité annoncées.

Deux chiffres comptent plus que les autres :

• 4 semaines. Selon les auteurs, une tâche de cette ampleur prend généralement des années à des équipes d'experts.
• ~1 %. C'est la part des endroits que les agents ont eux-mêmes signalés, après l'audit de leur propre preuve, comme nécessitant un regard humain. Le reste est passé sans intervention manuelle.

Google présente cela comme la première utilisation de l'IA pour la vérification formelle d'un programme réel. C'est une déclaration de l'entreprise elle-même ; il n'existe pas encore de vérification indépendante.

Où est le piège

D'abord, les limites. Une preuve formelle n'est fiable que dans la mesure où la spécification l'est. Si les propriétés sont écrites de façon incomplète ou sont les mauvaises, le code sera prouvé correct par rapport à un mauvais objectif. Il faut donc lire « sécurité prouvée » comme « conformité prouvée à des garanties précises et écrites ». Cela ne veut pas dire « impossible à pirater ».

Autre réserve : une telle preuve ne couvre pas tout ce qui entoure le code. L'environnement, le matériel, les erreurs d'intégration et le facteur humain restent hors du périmètre. La source ne précise pas non plus le coût d'exécution, les besoins en calcul, ni si le système sera accessible à tous. Pour l'instant, il s'agit d'une démonstration de recherche, pas d'un produit que l'on pourrait brancher demain.

L'approche a aussi un atout majeur. La preuve est vérifiée automatiquement, et il n'est pas nécessaire de croire sur parole ni les agents ni les auteurs. Si Lean a accepté la preuve, elle est correcte. Les hallucinations du modèle ne posent pas problème ici : une étape erronée ne passera tout simplement pas la vérification.

Que faire de tout cela

Pour les développeurs de code critique (cryptographie, paiements, noyaux d'OS, protocoles de consensus) : suivez la baisse du coût de la vérification formelle. Si un mois au lieu de plusieurs années se confirme sur d'autres projets, le ticket d'entrée chutera brutalement.

Pour les product managers et fondateurs dans la sécurité : au lieu de « nous avons passé un audit », on pourra présenter une preuve mathématique vérifiable. C'est un argument fort pour les secteurs régulés et les clients grands comptes.

Pour tous les autres : dès maintenant, il vaut la peine de s'habituer à formuler les exigences sur le code comme des propriétés vérifiables. Quand les agents sauront écrire les preuves, le goulot d'étranglement sera la capacité à dire clairement ce qui doit être vrai.

La conclusion principale est simple. Les agents savent déjà écrire du code, et il existe désormais un moyen de prouver sa correction à une échelle jusque-là inaccessible. Les auteurs estiment que c'est peut-être le seul moyen de résister à la vitesse et à l'ampleur des cyberattaques modernes. L'affirmation est discutable, mais la direction est claire.