AlphaProof Code vérifie le protocole Signal en quatre semaines

Google DeepMind a vérifié formellement, en quatre semaines, le code du protocole Signal grâce à un nouveau cadre agentique, AlphaProof Code, qui a généré plus de six millions de lignes de preuves en Lean. Le laboratoire rappelle que la même tâche prendrait des années à des équipes expertes avec les méthodes traditionnelles.

Dans son billet de blog, DeepMind décrit AlphaProof Code comme "a multi-LLM agentic framework that splits the work of formal verification the way a research team would". Des agents alimentés par Gemini Carbon rédigent les preuves ; selon le billet, seuls "just one percent of the codebase, a massive time savings" ont nécessité un audit humain.

Pour éprouver le dispositif, l'équipe a réintroduit deux bugs réels déjà corrigés dans une version isolée du code Signal. Dans les deux cas, le système a produit "a machine-checked proof that the buggy version was insecure".

Ehren Kret, directeur technique de Signal, écrit dans le billet qu'"Using AI agents to translate live code into valid Lean theorems is a major breakthrough", en relevant que les vérifications formelles antérieures se limitaient à des portions plus restreintes du code. DeepMind affirme qu'il s'agit de la première vérification formelle, par quelque méthode que ce soit, de l'implémentation d'un protocole aussi largement déployé, utilisé notamment dans les apps Signal et Google Messages.

Le laboratoire élargit la perspective : "Cryptographic protocols underpin nearly all digital communication, from online banking to web browsing, and a single flaw can expose millions of people at once." Les artefacts de vérification sont publiés en open source. L'annonce prolonge un flux soutenu d'avancées agentiques suivies ces derniers mois sur AI Weekly.