Google DeepMind présente AlphaProof Code, un système d’IA capable de prouver mathématiquement qu’un logiciel fait bien ce qu’il promet. Premier test grandeur nature : le protocole de chiffrement de Signal, la messagerie réputée la plus sûre. En quatre semaines, l’IA a démontré plusieurs garanties de sécurité clés du vrai code de Signal. Aucune nouvelle faille n’a été trouvée.
Dernière mise à jour : 10 novembre 2026.
Ce qu’il faut retenir
- AlphaProof Code associe des experts humains, qui décident quoi prouver, et des agents IA, qui rédigent les preuves.
- Le travail porte sur le code réel de Signal, jusqu’aux instructions exécutées par les appareils, et pas seulement sur sa théorie.
- Durée : quatre semaines, contre plusieurs années pour ce type de travail selon DeepMind.
- Aucune nouvelle faille découverte dans Signal.
- Les preuves et la spécification sont publiées en open source.
Qu’est-ce que la vérification formelle ?
Habituellement, on teste un logiciel en cherchant des bugs. Mais un test ne prouve jamais qu’il n’en reste aucun. La vérification formelle va plus loin : elle démontre mathématiquement qu’un programme respecte certaines règles, dans tous les cas possibles.
C’est très fiable, mais extrêmement long et coûteux. Il faut des spécialistes rares et parfois des années de travail. C’est ce frein que DeepMind veut lever avec l’IA.
Comment DeepMind a procédé
- Des experts humains ont traduit les objectifs de sécurité de Signal en énoncés mathématiques précis, puis les ont relus un par un.
- Des agents IA, basés sur Gemini, ont rédigé les preuves dans Lean, un langage qui permet à un ordinateur de vérifier chaque étape.
- Lean a contrôlé automatiquement les preuves. Les agents ont signalé environ 1 % du code pour une relecture humaine.
Parmi les garanties démontrées : la protection des messages avant et après qu’un appareil a été temporairement compromis. C’est l’une des promesses fortes de Signal.
Un test avec d’anciennes failles
Pour vérifier que le système ne valide pas n’importe quoi, les chercheurs ont réintroduit deux failles déjà corrigées dans une copie isolée du code. Dans les deux cas, AlphaProof Code a produit une preuve, vérifiée par la machine, que cette version était vulnérable.
Ehren Kret, directeur technique de Signal, salue « une avancée majeure » dans le fait d’utiliser des agents IA pour traduire du code réel en théorèmes valides.
Ce que ça ne prouve pas
- Le travail porte sur certaines garanties du protocole choisies par les experts, pas sur toute l’application Signal.
- Une preuve ne vaut que pour ce qui a été spécifié : un défaut en dehors de ce périmètre resterait possible.
- Elle ne protège pas contre un téléphone piraté par un logiciel espion ou contre une erreur humaine.
Notre avis
C’est une bonne nouvelle pour la cybersécurité. Après une IA d’OpenAI qui a découvert 948 failles dans le noyau Linux, DeepMind montre l’autre face de la médaille : l’IA peut aussi aider à prouver qu’un code est sûr. Si cette méthode se généralise, les logiciels critiques pourraient être vérifiés bien plus souvent qu’aujourd’hui.
FAQ
Signal est-il plus sûr après cette annonce ?
Le code n’a pas changé, mais plusieurs de ses garanties de sécurité sont désormais prouvées mathématiquement. Aucune nouvelle faille n’a été trouvée.
AlphaProof Code est-il disponible ?
DeepMind publie les preuves et les outils de vérification liés à Signal. Il n’annonce pas de produit commercial pour le moment.
Qu’est-ce que Lean ?
Un langage informatique qui permet d’écrire des preuves mathématiques et de les faire vérifier automatiquement par un ordinateur.
