A Google DeepMind publicou a 10 de novembro de 2026 um texto de investigação que descreve o AlphaProof Code, uma estrutura agente que, segundo os autores, ajudou a demonstrar matematicamente propriedades essenciais de segurança do código real por detrás do protocolo Signal. O texto é assinado por Pushmeet Kohli e Swarat Chaudhuri. Chamaram à verificação formal de um protocolo criptográfico amplamente usado, nesta profundidade, um desafio antigo, e disseram que era a primeira vez que a inteligência artificial era usada para o fazer. Afirmaram também que era a primeira vez que a implementação de um protocolo tão difundido era formalmente verificada por qualquer método, com ou sem inteligência artificial.
O protocolo Signal protege conversas privadas em aplicações como o Signal e o Google Messages, escreveram os autores. A maior parte do trabalho anterior de verificação, disseram, parava no desenho do protocolo e não no código compilado que corre nos aparelhos. O AlphaProof Code é descrito como uma divisão do trabalho à maneira de uma equipa de investigação: especialistas humanos trabalham com modelos para decidir o que deve ser demonstrado e, depois, um grupo de agentes executa as provas.
A DeepMind disse que os seus investigadores colaboraram com vários modelos para traduzir os objetivos de segurança do Signal em especificações matemáticas formais, com revisão humana de cada especificação. Agentes alimentados pelo Gemini Carbon geraram depois mais de seis milhões de linhas de Lean, uma linguagem usada para escrever provas matemáticas verificadas por máquina. Os agentes também auditaram a prova e assinalaram cerca de um por cento do código para uma segunda leitura humana. Como o Lean verifica automaticamente o restante, escreveram os autores, os especialistas puderam concentrar a revisão onde o juízo humano ainda importa.
Os agentes foram usados para demonstrar que o código compilado cumpre propriedades especificadas, incluindo manter as mensagens protegidas antes e depois de um aparelho ser temporariamente comprometido. Os autores disseram que o processo levou quatro semanas, face a um trabalho que historicamente ocupa equipas especializadas durante anos. Para testar se o sistema distingue código correto de código com falhas, reintroduziram dois erros reais já corrigidos numa versão isolada do código do Signal. Nos dois casos, afirmaram, o sistema produziu uma prova verificada por máquina de que a versão com erros era insegura.
Ehren Kret, diretor de tecnologia do Signal, é citado a dizer que a verificação formal anterior se tinha concentrado em porções mais pequenas do código e que usar agentes de inteligência artificial para traduzir código em execução em teoremas Lean válidos é um avanço importante. Disse que, à medida que aumentam as ameaças de segurança impulsionadas pela inteligência artificial, verificar com rigor a implementação do protocolo dá ao Signal maior confiança nas suas garantias de privacidade. A DeepMind incluiu outros membros da equipa do Signal, entre os quais Rolfe Schmidt e Michael Rosenberg, entre quem comentou a metodologia.
Os autores apresentaram o resultado como um passo para levar este tipo de garantia a outro software crítico, do firmware de dispositivos médicos aos sistemas das redes elétricas, e disseram que estão a disponibilizar em aberto artefactos de verificação formal para uso da comunidade. Também apontaram os leitores para um artigo técnico na mesma página. O trabalho surge ao lado do lançamento, no mesmo dia, do Gemini 4 Carbon, que o anúncio do Carbon cita como o modelo usado com outros sistemas dentro do AlphaProof Code. Os dois textos estão relacionados, mas descrevem acontecimentos diferentes: um é um resultado de investigação sobre o código do Signal, o outro é uma mudança de disponibilidade de um produto.
As afirmações sobre a novidade, o prazo de quatro semanas, os seis milhões de linhas de Lean e os dois erros reintroduzidos vêm da DeepMind, apoiadas pelo endosso citado do Signal à abordagem. Esta reportagem não voltou a executar as provas nem auditou os artefactos disponibilizados. Convém tratar estes números e a comparação com esforços humanos de vários anos como o relato dos autores, e notar que a verificação cobre propriedades-chave especificadas da implementação do protocolo, e não uma promessa sem limites de que todas as falhas possíveis foram excluídas.