Google DeepMind usa agentes de IA para provar matematicamente a segurança do código do Signal

A Google DeepMind anunciou em 10 de novembro de 2026 o AlphaProof Code, um sistema de agentes de IA que conseguiu provar matematicamente que o código do protocolo do Signal, a criptografia que protege conversas no Signal e no Google Messages, cumpre suas garantias de segurança. Segundo o post oficial da DeepMind, é a primeira vez que a implementação real de um protocolo criptográfico amplamente usado é verificada formalmente nesse nível de profundidade, com ou sem IA.

O trabalho foi assinado por Pushmeet Kohli e Swarat Chaudhuri e contou com feedback da equipe do Signal, incluindo Rolfe Schmidt, Michael Rosenberg e o CTO Ehren Kret. Para quem constrói e audita software crítico, o caso interessa menos pelo Signal em si e mais pelo método: uma forma de dividir o trabalho de prova formal entre especialistas humanos e agentes de IA que pode, em tese, baratear um tipo de verificação que até hoje era caro demais para a maioria dos times.

O que é verificação formal e por que ela quase nunca acontece

Verificação formal é o padrão mais alto de garantia de segurança que existe: em vez de testar o software com casos de uso e torcer para que ele se comporte bem nos cenários que ninguém previu, você prova matematicamente que o código faz exatamente o que deveria fazer, sem exceção. O problema é que essa prova é trabalhosa. A DeepMind descreve o processo tradicional como "difícil e frequentemente intensivo em mão de obra", e por isso a maioria das verificações formais historicamente para no nível do desenho do protocolo, não no código que efetivamente roda no dispositivo do usuário.

Essa distância entre design e implementação importa porque é exatamente onde vivem as vulnerabilidades do mundo real: um protocolo pode estar correto no papel e ainda assim ter um bug na forma como foi compilado ou integrado. Fechar essa lacuna é o que torna a prova mais complexa, e é também o que o AlphaProof Code se propôs a fazer: provar que o código compilado do Signal, e não só o desenho da sua criptografia, mantém propriedades como proteger mensagens antes e depois de um dispositivo ser temporariamente comprometido.

Como o trabalho foi dividido entre humanos e agentes

O AlphaProof Code é descrito como um framework agente multi-LLM (vários modelos de linguagem trabalhando em conjunto) que organiza o trabalho como uma equipe de pesquisa faria:

1. Pesquisadores da DeepMind, com apoio de uma combinação de modelos, traduziram os objetivos de segurança do Signal em especificações matemáticas formais, com especialistas humanos revisando cada uma delas.
2. Agentes rodando sobre o Gemini Carbon, o modelo de que a DeepMind falou em outubro de 2026, geraram as provas propriamente ditas: mais de 6 milhões de linhas escritas em Lean, uma linguagem usada para demonstrar matematicamente que um trecho de código está correto.
3. Os próprios agentes auditaram o resultado e sinalizaram as partes que precisavam de uma segunda olhada humana: apenas 1% da base de código.

Como o Lean verifica automaticamente o resto da prova, os especialistas puderam concentrar a revisão humana exatamente onde o julgamento de uma pessoa ainda é insubstituível. O processo inteiro levou quatro semanas, numa tarefa que a DeepMind diz levar historicamente anos para equipes de especialistas.

O teste que separa prova de maquiagem

Um risco óbvio de qualquer sistema automatizado de prova é ele simplesmente aprovar tudo. Para checar isso, a equipe reintroduziu dois bugs reais, já corrigidos anteriormente, numa versão isolada do código do Signal. Nos dois casos, o AlphaProof Code gerou uma prova verificada por máquina de que aquela versão com bug era insegura.

É esse resultado, mais do que o volume de linhas geradas, que sustenta a alegação central do anúncio: o sistema não está só produzindo prosa matemática complexa, ele está de fato distinguindo código correto de código com falha, e fazendo isso no nível da implementação real, não de um modelo simplificado do protocolo.

O que muda para quem precisa validar software crítico

Para times de TI no Brasil que lidam com sistemas sensíveis, bancos, fintechs, saúde, infraestrutura de governo sob LGPD, a verificação formal tradicional nunca foi uma opção realista fora de nichos muito específicos, como microkernels pequenos ou bibliotecas de criptografia isoladas. O custo de montar uma equipe de especialistas em Lean ou Coq para provar um sistema inteiro simplesmente inviabiliza o projeto na maioria das empresas.

O que o caso do Signal sugere é um caminho intermediário: humanos definem o que precisa ser provado (as propriedades de segurança), agentes fazem o trabalho mecânico e volumoso de escrever a prova, e a revisão humana se concentra numa fração pequena do problema. Isso não elimina a necessidade de expertise em verificação formal, alguém ainda precisa saber traduzir um requisito de segurança numa especificação Lean correta, mas reduz drasticamente o esforço braçal que hoje faz esse tipo de auditoria ser reservada a protocolos de altíssimo risco.

Em resumo: quem audita software crítico ganha, pelo menos no papel, um método para escalar verificação formal além do punhado de sistemas que historicamente justificavam o investimento.

Embora a verificação formal anterior sempre tenha se concentrado em partes menores do código, a abordagem da Google DeepMind permite uma expansão significativa. Usar agentes de IA para traduzir código real em teoremas Lean válidos é um grande avanço. Com o crescimento das ameaças cibernéticas impulsionadas por IA, verificar rigorosamente a implementação do protocolo Signal nos dá ainda mais confiança de que nosso código cumpre suas garantias de privacidade.

While prior formal verification focused on smaller portions of the code, Google DeepMind's approach enables significant expansion. Using AI agents to translate live code into valid Lean theorems is a major breakthrough. As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code's privacy guarantees.Ehren Kret, CTO do Signal

O que ainda fica em aberto

A DeepMind diz estar abrindo o código dos artefatos de verificação formal para uso da comunidade, o que permite a outros times estudar a metodologia usada no Signal. Mas o anúncio não detalha custo computacional do processo, nem se o acesso ao Gemini Carbon necessário para rodar os agentes de prova está disponível fora da própria DeepMind.

A empresa também sinaliza para onde pretende levar a técnica: firmware de dispositivos médicos e software de redes elétricas são citados como próximos alvos possíveis, e o plano é combinar essa verificação formal com agentes de defesa automatizada como o CodeMender, anunciado em outubro de 2025. Para quem avalia adotar algo parecido hoje, o caso do Signal ainda é prova de conceito feita por uma equipe de pesquisa de ponta, não um produto pronto para rodar no pipeline de CI de uma empresa comum.

Fonte: Google DeepMind Blog