AlphaProof Code : Google DeepMind fait prouver par des agents le code de chiffrement de Signal

Google DeepMind a présenté le 10 novembre 2026 AlphaProof Code, un système qui associe des experts humains et des agents IA pour prouver mathématiquement qu'un logiciel fait ce qu'il doit faire. Première cible : le code du protocole de chiffrement de Signal, utilisé par la messagerie du même nom et par Google Messages.

Tester n'est pas prouver

Un test vérifie qu'un programme se comporte bien dans les cas qu'on a pensé à essayer. La vérification formelle va plus loin : elle démontre, comme un théorème, qu'une propriété est vraie dans tous les cas. La méthode existe depuis longtemps, mais elle est si coûteuse en temps d'experts qu'elle reste réservée à de petits périmètres.

AlphaProof Code s'appuie sur Lean, un langage dans lequel on écrit des preuves qu'un programme vérifie ensuite automatiquement. Une preuve fausse est rejetée par la machine : c'est ce qui rend l'exercice compatible avec des modèles de langage, dont on connaît les erreurs.

Comment le travail est réparti

1. Les humains décident quoi prouver. Un ensemble de modèles traduit les objectifs de sécurité de Signal en énoncés mathématiques. Des experts relisent chaque énoncé.
2. Les agents écrivent les preuves. Des agents fondés sur le modèle Gemini Carbon ont généré plus de six millions de lignes de Lean.
3. Les agents signalent ce qui doit être relu. Environ un pour cent du code est renvoyé vers une relecture humaine ; Lean contrôle le reste.

Les résultats annoncés

Selon DeepMind, l'ensemble a pris quatre semaines, pour un travail que l'entreprise estime habituellement à plusieurs années d'équipes spécialisées. Le laboratoire affirme qu'aucun protocole de chiffrement aussi répandu n'avait vu son code réel, et pas seulement sa conception, vérifié à ce niveau.

Un essai donne du poids à la démonstration : les chercheurs ont réintroduit dans une copie isolée du code deux anciens bogues réels, déjà corrigés. Dans les deux cas, le système a produit une preuve, validée par la machine, que la version fautive n'était pas sûre.

Les éléments de vérification sont en cours de publication en accès libre, accompagnés d'un article technique.

Les réserves

• Une preuve vaut ce que vaut son énoncé. Si une propriété de sécurité est mal formulée ou oubliée, la preuve ne la couvre pas. D'où la relecture humaine de chaque énoncé, qui reste le maillon sensible.
• Ce sont les chiffres de DeepMind. Le billet cite le directeur technique de Signal, mais aucune équipe extérieure n'a encore reproduit le résultat. La mise à disposition des preuves doit justement le permettre.