L’essentiel
- Google DeepMind a prouvé mathématiquement des propriétés de sécurité du code réel du protocole Signal, avec son cadre d’agents AlphaProof Code.
- Les agents, fondés sur Gemini Carbon, ont écrit plus de six millions de lignes de preuve en Lean ; environ 1 % est revenu aux experts humains pour relecture.
- Quatre semaines ont suffi pour une tâche qui mobilise d’ordinaire des équipes d’experts pendant des années ; deux anciens bugs de Signal, réinjectés, ont été identifiés comme des failles.
Prouver qu’un logiciel tient sa promesse de sécurité occupait jusqu’ici des équipes d’experts pendant des années. Google DeepMind affirme l’avoir fait en quatre semaines pour le code cryptographique de Signal, le protocole qui protège les conversations de milliards de personnes, dans Signal comme dans Google Messages. L’outil s’appelle AlphaProof Code. Ses chiffres impressionnent, mais ils ne mesurent pas tous la même chose.
Quatre semaines face à « des années » : une comparaison à moitié mesurée
Le gain annoncé repose sur deux grandeurs de nature différente. Les quatre semaines sont celles du projet, observées. Les « années » sont une estimation générale de DeepMind pour des équipes d’experts, sans projet de référence nommé. Si le mot signifie au moins un an, le facteur dépasse 13 ; au-delà, la publication ne permet pas de le calculer.
Ces quatre semaines ne se réduisent pas non plus à du temps machine. Les chercheurs ont traduit les objectifs de sécurité de Signal en spécifications formelles (des énoncés mathématiques de ce que le code doit garantir), et des experts humains ont relu chacune d’elles. Parmi ces objectifs figure la protection des messages avant et après la compromission temporaire d’un appareil. Le temps humain ne s’est pas évaporé : il a migré en amont, vers la définition de ce qu’il faut prouver.
DeepMind avance un autre point de comparaison : la plupart des vérifications de protocoles s’arrêtent au niveau de la conception. Ici, les agents ont démontré que le code compilé respecte les propriétés visées, jusqu’au code qui tourne sur les appareils. L’entreprise précise que c’est la première fois que l’implémentation d’un protocole aussi répandu est vérifiée formellement, avec ou sans IA.
Six millions de lignes de preuve, et soixante mille à relire ?
Les agents ont généré plus de six millions de lignes en Lean, un langage dans lequel chaque preuve est contrôlée automatiquement par la machine. Ils ont ensuite audité leur propre travail et signalé aux humains environ 1 % du code à examiner. Appliqué aux six millions de lignes de preuve, ce pourcentage représente quelque 60 000 lignes, soit la taille d’un projet logiciel conséquent. Mais DeepMind parle de « 1 % de la base de code » sans dire quelle base sert de dénominateur : la preuve ou le code de Signal. Selon la réponse, l’effort humain varie du tout au tout.
Le volume impressionne moins qu’il n’y paraît. Un agent peut écrire n’importe quoi dans une preuve : si elle est fausse, Lean la rejette. Personne n’a donc besoin de croire les agents, ni de lire les 99 % restants. Lean ne peut pas dire, en revanche, si l’énoncé prouvé correspond bien à ce que les ingénieurs voulaient garantir. Une spécification trop faible produit une preuve irréprochable d’une propriété qui ne protège de rien.
Deux bugs réinjectés : un test parlant, un échantillon minuscule
Pour vérifier que le système distingue un code correct d’un code fautif, l’équipe a replacé deux vrais bugs de Signal, déjà corrigés, dans une version isolée du code. Dans les deux cas, AlphaProof Code a produit une preuve, validée par la machine, que cette version n’était pas sûre. C’est un résultat utile : l’outil ne déclare pas tout conforme par défaut.
Deux cas, c’est peu. Il s’agit de défauts connus, déjà documentés, et rien n’indique comment le système réagirait face à une faille inédite, ou face à une propriété que personne n’a pensé à spécifier. Une preuve formelle garantit ce qu’on a écrit, pas ce qu’on a oublié d’écrire.
Où se loge la confiance quand les agents rédigent les preuves
Dans ce montage, la confiance repose sur trois points : les spécifications relues par des humains, le vérificateur de Lean, et le lien entre le code réel et son modèle formel. DeepMind affirme avoir prouvé le code compilé, sans détailler comment ce lien est établi. Les spécialistes examineront ce maillon en premier.
Pour les équipes qui maintiennent des logiciels critiques, le déplacement est concret. L’audit ne consiste plus à lire des milliers de lignes de code, mais à relire des énoncés : que garantit-on, dans quelles conditions, face à quel adversaire ? Cette compétence, rare aujourd’hui, devient la plus recherchée. Le directeur technique de Signal, Ehren Kret, y voit un renfort de la confiance dans la protection des données à l’heure où les menaces dopées à l’IA se multiplient. DeepMind envisage d’étendre la méthode aux réseaux électriques et aux dispositifs médicaux, notamment via son système CodeMender.
Si la preuve se fabrique en quatre semaines, la spécification devient le document à auditer, et celui-là, aucun agent ne peut le relire à notre place.
Mon avis
Les six millions de lignes de preuve comptent peu : Lean les relit en bloc, sans fatigue ni complaisance. Seules les spécifications décideront de la valeur de ce travail, et je trouverais normal que DeepMind les publie intégralement. Une preuve dont l’énoncé reste confidentiel ne rassure personne, surtout quand elle porte sur la messagerie de milliards d’utilisateurs.
Vous avez aimé celui-ci ?
La newsletter du vendredi réunit les articles de la semaine, avec leurs sources.
Offert à l'inscriptionMa configuration Claude Code, avec mes skills, mes sous-agents et mes hooks, prêts à copier.
Sources
- son système CodeMender
- Introducing AlphaProof Code: a breakthrough in verifying complex software at depth
Ils m’ont fait confiance
« Il ne se contente pas de corriger les symptômes, il cherche à comprendre l'origine des problèmes et à sécuriser les modifications effectuées. J'ai réellement le sentiment d'avoir trouvé un développeur qui comprend à la fois la technique et les enjeux globaux du projet. »
Évaluation client · projet WordPress · septembre 2026
5,0/5 sur 22 évaluations
Faire appel à mes services →
