Google DeepMind usa agentes de IA para verificar o código de máquina central do Signal

O Google DeepMind apresentou o AlphaProof Code em 10 de novembro de 2026, usando equipes de agentes de IA para produzir provas em Lean, verificadas por máquina, de propriedades de segurança especificadas do código compilado do libsignal, do Signal. A equipe de pesquisa, composta por cinco pessoas, concluiu o trabalho de prova em quatro semanas e divulgou as especificações e os artefatos de verificação para análise externa.

O trabalho foi além de um modelo abstrato do projeto do protocolo do Signal e chegou à sua implementação compilada. Os pesquisadores envolveram os crates libsignal v0.105.4 e SPQR v1.6.0, sem modificações, em um pequeno programa de linha de comando e, em seguida, usaram o rustc padrão para criar um executável Linux AArch64 vinculado estaticamente. O artigo técnico descreve o resultado como as primeiras provas de segurança no nível do protocolo para o código sem modificações de uma implementação de protocolo criptográfico amplamente utilizada.

Como o AlphaProof Code dividiu o trabalho

Cinco pesquisadores dedicaram quatro semanas ao trabalho de prova, executando agentes continuamente em suas estações de trabalho enquanto desenvolviam, em paralelo, provas simbólicas e computacionais. O artigo informa que os agentes geraram cerca de 6,5 milhões de linhas de código de prova em Lean verificadas por máquina, apoiadas em aproximadamente 26 mil linhas de especificações confiáveis e semântica AArch64.

Os humanos selecionaram as propriedades, resolveram ambiguidades e avaliaram as compensações de segurança, revisaram as especificações e mantiveram a aprovação final. Agentes equipados com o Gemini 4 Carbon e o Claude Opus 5.5 redigiram e revisaram essas especificações, inclusive com uma revisão feita por uma família de modelos diferente. Em seguida, equipes de agentes do Gemini 4 Carbon geraram todo o código de prova; nenhum dos autores escreveu código de prova. As campanhas típicas usaram de 40 a 80 agentes em uma única máquina durante 24 a 72 horas. Um orquestrador e líderes de equipe coordenavam os agentes responsáveis pelas provas, enquanto as funções de arquiteto e integrador mantinham a base de provas compartilhada.

Um mecanismo de controle só aceitava uma prova depois que o núcleo do Lean a verificava e um comparador confirmava que ela correspondia à especificação reservada e aprovada por humanos, incluindo todas as definições transitivas, usando apenas os axiomas padrão do Lean. Os agentes podiam propor pequenas alterações quando as provas revelavam problemas nas especificações, mas mudanças nas premissas confiáveis exigiam aprovação humana ou uma política definida pelo usuário e eram registradas com justificativas. Esse controle aborda um risco documentado das provas geradas por agentes: uma especificação pode ser enfraquecida indiretamente por meio de uma de suas definições.

Cobertura de segurança e testes com bugs históricos

O alvo verificado foi o código de sessões individuais, que abrange o handshake PQXDH e as mensagens com o Triple Ratchet. Os pesquisadores relatam dois argumentos independentes: dez teoremas simbólicos sob premissas criptográficas idealizadas e uma prova computacional que limita a vantagem de um atacante por meio de premissas criptográficas e termos estatísticos. Entre as propriedades estão o sigilo futuro, que protege mensagens anteriores caso o estado atual seja roubado; a autenticação; a segurança pós-comprometimento, relacionada à recuperação após um comprometimento; e o sigilo do handshake. O argumento simbólico também abrange o sigilo do handshake após uma quebra posterior do Diffie–Hellman.

Para testar se essas especificações poderiam detectar erros reais, a equipe reverteu as correções de dois bugs do libsignal que já haviam sido corrigidos, conhecidos como estado fraco e subgrupo pequeno, e recompilou os binários alterados. Nos dois casos, produziu provas em Lean de que o teorema de segurança simbólico falhava. O repositório público de verificação separa os materiais computacionais, simbólicos, do binário compartilhado e da semântica AArch64, além de documentar como reconstruir e verificar as provas de forma independente.

Ehren Kret, diretor de tecnologia do Signal, afirmou que o trabalho “nos dá ainda mais confiança nas garantias de privacidade do nosso código”.

Limites e próximos passos

As garantias estão longe de certificar os aplicativos completos do Signal. Elas dizem respeito à compilação do libsignal-cli dos pesquisadores, executada como um processo novo; a geração de chaves não foi verificada, as mensagens em grupo ficaram para trabalhos futuros, e os canais laterais e o estado em vários dispositivos estão fora do escopo do cenário. Primitivas criptográficas de baixo nível e determinadas rotinas de saída e da biblioteca são representadas por contratos confiáveis. Portanto, o resultado também depende desses contratos, das especificações aprovadas, do núcleo do Lean, da semântica AArch64 e de premissas sobre as primitivas.

O artigo afirma que nenhum dos dois argumentos prova a recuperação pós-quântica que o SPQR foi projetado para acrescentar: o teorema computacional abrange atacantes clássicos, enquanto os teoremas simbólicos do ratchet permitem que o atacante escolha as chaves SPQR. O modelo computacional também restringe várias ações do atacante e torna-se vazio em escalas suficientemente grandes de mensagens e sessões. Esses limites definem o que um revisor externo precisa considerar confiável antes de tratar as provas verificadas por máquina como uma garantia de segurança para uma implantação específica.

Os próximos passos indicados pelos pesquisadores são fortalecer os teoremas, reduzir a base confiável verificando mais rotinas conectadas e vinculando contratos criptográficos a implementações verificadas, além de ampliar a cobertura para mensagens em grupo, remetente selado e protocolos do lado do servidor. O objetivo de verificar novas versões do libsignal antes de sua distribuição é uma meta de pesquisa, não uma implantação anunciada.

A importância imediata do resultado está na divisão de tarefas que ele demonstra: os agentes cuidaram da construção das demonstrações, enquanto a confiança continua dependendo de especificações revisadas por pessoas e de pressupostos explícitos. Disponibilizar as demonstrações e os procedimentos de verificação permite que revisores externos examinem essa base enquanto os pesquisadores trabalham para incorporar o fluxo de trabalho ao desenvolvimento contínuo do libsignal.