Google DeepMind afirma ter verificado formalmente o código de máquina do protocolo Signal com o AlphaProof Code

Pushmeet Kohli, da Google DeepMind, anunciou que sua equipe provou propriedades importantes de segurança do código de máquina que sustenta o protocolo de mensagens Signal. A DeepMind afirma que esta é a primeira vez que o código de produção de um protocolo amplamente utilizado foi verificado formalmente, por qualquer método, nesse nível de profundidade. Essas são afirmações da própria DeepMind.

O trabalho usou o AlphaProof Code, que a DeepMind descreve como uma nova estrutura agêntica para verificação formal executada em LLMs, incluindo o Gemini Carbon. A DeepMind afirma que a verificação chega ao código executado nos dispositivos e levou cerca de um mês, enquanto esforços semelhantes poderiam exigir décadas de trabalho combinado de equipes. A empresa reconhece a equipe do Signal como parceira.

A DeepMind está disponibilizando como código aberto suas especificações formais e os artefatos de verificação para que outras pessoas possam dar continuidade ao trabalho. Até a manhã de 10 de novembro, a publicação tinha 1.297 curtidas no X.