Google DeepMind affirme avoir vérifié formellement le code machine du protocole Signal avec AlphaProof Code

Pushmeet Kohli, de Google DeepMind, a annoncé que son équipe avait démontré des propriétés de sécurité essentielles du code machine qui sous-tend le protocole de messagerie Signal. DeepMind affirme que c’est la première fois que le code de production d’un protocole largement déployé est vérifié formellement, quelle que soit la méthode, à ce niveau de profondeur. Il s’agit des propres affirmations de DeepMind.

Le travail s’est appuyé sur AlphaProof Code, que DeepMind décrit comme un nouveau cadre agentique de vérification formelle reposant sur des LLM, dont Gemini Carbon. DeepMind affirme que la vérification va jusqu’au code exécuté sur les appareils et qu’elle a pris environ un mois, alors que des efforts similaires pourraient demander des décennies de travail cumulé à des équipes. L’entreprise remercie l’équipe de Signal pour sa collaboration.

DeepMind publie en open source ses spécifications formelles et ses artefacts de vérification afin que d’autres puissent s’en servir. Au matin du 10 novembre, la publication avait reçu 1 297 mentions J’aime sur X.