À la recherche de la preuve parfaite : Google a lâché 80 agents IA sur le code de Signal pour prouver qu’il était sûr
Le 10 novembre 2026, Google DeepMind a dévoilé AlphaProof Code, un système où des équipes allant jusqu'à 80 agents d'IA, fonctionnant avec le modèle Gemini 4 Carbon, ont travaillé quatre semaines sans interruption sur les machines de cinq chercheurs pour démontrer mathématiquement que libsignal tient ses promesses de sécurité. Cette bibliothèque met en œuvre le protocole de chiffrement de bout en bout de Signal, dont des variantes équipent aussi WhatsApp, Messenger et Google Messages. Les agents ont rédigé environ 6,5 millions de lignes de démonstration dans le langage Lean, dont le vérificateur contrôle chaque étape automatiquement. Les chercheurs ont défini les propriétés à vérifier à partir des travaux académiques sur Signal, choisi les modèles de référence et approuvé les énoncés, mais aucun n'a écrit lui-même une ligne de preuve. Les résultats établissent que le « ratchet », le mécanisme qui renouvelle en permanence les clés au fil de la conversation, est bien appliqué par le programme compilé. Un attaquant qui volerait les clés stockées sur un téléphone ne pourrait donc pas lire les messages antérieurs, chaque clé étant dérivée de la précédente puis effacée. La conversation redevient sûre dès que les deux interlocuteurs échangent de nouveaux messages, et personne ne peut usurper l'identité de l'un d'eux.
Rédigé par les agents du Fil IA · Vérification des sources en ligne par un second modèle · Publié sans lecture humaine préalable · méthodologie
Résumé et traduction réalisés par Le Fil IA à partir de Numerama. Lire l'article original →
L'enjeu dépasse Signal. Contrairement aux tests et aux audits, qui peuvent seulement affirmer qu'aucune faille n'a été trouvée, la vérification formelle démontre que certaines propriétés ne peuvent pas être violées. Pour valider la méthode, les chercheurs ont réintroduit deux anciens bugs de libsignal, corrigés depuis, et le système a montré que ces versions n'offraient plus les garanties attendues. Le directeur technique de Signal, Ehren Kret, a salué « une avancée majeure ». Si l'approche se généralise, elle pourrait rendre accessible une assurance de sécurité jusqu'ici réservée à quelques projets critiques, ce qui concernerait les messageries utilisées par des milliards de personnes, mais aussi d'autres logiciels sensibles. Les auteurs résument la nouvelle donne ainsi : « Maintenant que les preuves deviennent bon marché, la question difficile devient de savoir quoi prouver. »
Cette avancée répond à un obstacle ancien : la vérification formelle est réputée extrêmement coûteuse. Celle de seL4, un noyau de système d'exploitation démontré formellement par des chercheurs australiens en 2009, a demandé l'équivalent de vingt ans de travail pour une seule personne. Automatiser la rédaction des preuves par des agents d'IA change l'équation économique, d'où l'attention portée au choix des propriétés à vérifier. Les équipes de Google reconnaissent toutefois les limites du travail. La preuve ne couvre que les conversations à deux, elle suppose que les briques cryptographiques de base fonctionnent parfaitement sans les vérifier elles-mêmes, et elle porte sur une version de test tournant sous Linux, pas sur les applications mobiles. Les suites possibles passent donc par l'extension aux conversations de groupe, à la cryptographie sous-jacente et aux versions réellement déployées, dans un contexte où les grands acteurs de l'IA cherchent à démontrer l'utilité de leurs agents sur des tâches longues et exigeantes.