Como o AlphaProof Code provou a criptografia do Signal em Lean

Cinco pesquisadores da Google DeepMind (abre em nova aba) comprovaram matematicamente, em quatro semanas, propriedades centrais de segurança da libsignal, a biblioteca de código aberto que implementa o protocolo criptográfico do Signal (abre em nova aba), do WhatsApp e do Google Messages. Apresentado em 10 de novembro de 2026, o framework AlphaProof Code combinou especialistas humanos, agentes baseados nos modelos Gemini 4 Carbon e Claude Opus 5.5 e a linguagem de verificação Lean (abre em nova aba) para produzir cerca de 6,5 milhões de linhas de provas formais. A auditoria validou o código de máquina compilado, sem encontrar vulnerabilidades novas nos trechos analisados e sem cobrir o aplicativo móvel inteiro.⁠​‌​​‌​​‌​‌​​​​​‌​​‌​‌‌‌​​‌‌​​​‌‌​‌‌​‌‌‌‌​‌‌​‌‌​‌​​‌​‌‌‌​​‌‌​​​‌​​‌‌‌​​‌​​‌‌‌‌‌​​​​‌‌​‌‌‌​‌‌​​​‌​​​‌‌​‌​‌​​‌‌​​​‌​​‌‌​‌​‌​‌‌​​‌​​​‌‌​​​‌​​‌‌​​​​‌​​‌​‌‌​‌​​‌‌‌​​‌​​‌‌​‌​​​‌‌​​​​‌​‌‌​​‌‌​​​‌​‌‌​‌​​‌‌​‌​​​‌‌​​​‌‌​​‌‌​‌‌​​​‌‌‌​​‌​​‌​‌‌​‌​​‌‌‌​​‌​​‌‌​​‌​​‌‌​​‌‌​​​‌‌​​​‌​​‌​‌‌​‌​‌‌​​​​‌​‌‌​​‌​‌​​‌‌​‌‌​​​‌‌‌​​​​​‌‌​‌​‌​​‌‌​​‌‌​​‌‌​​‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​​‌‌​‌​‌​​‌‌‌​​​⁠

Testes de software convencionais, como testes unitários ou fuzzing (técnica que injeta entradas aleatórias ou malformadas em busca de falhas), mostram apenas a presença de erros em cenários específicos. A verificação formal resolve outro problema: ela traduz o código e os requisitos do sistema para a lógica matemática e demonstra que determinadas propriedades se mantêm válidas para qualquer estado ou entrada possível.

Na criptografia aplicada, a maioria das verificações formais históricas limitava-se ao desenho abstrato do protocolo. Se o modelo teórico estivesse correto no papel, mas o compilador ou o desenvolvedor introduzisse um erro sutil na implementação, a falha passava despercebida. O trabalho conduzido por Pushmeet Kohli e Swarat Chaudhuri na DeepMind desceu até o código de máquina compilado mesmo, aquele que roda direto no dispositivo do usuário, marcando a primeira vez que a implementação de um protocolo criptográfico com essa escala de implantação passou por verificação formal em tal profundidade.

O que foi provado na libsignal e onde estão os limites

A equipe não tentou provar que o aplicativo Signal é invulnerável. Uma prova matemática em criptografia avalia garantias específicas dentro de um modelo de ameaça delimitado. Na libsignal, o trabalho partiu de provas preliminares já desenvolvidas pela Signal Foundation e concentrou-se em três garantias clássicas:

• Forward secrecy (sigilo futuro): propriedade que impede que o vazamento de chaves privadas atuais comprometa o conteúdo de mensagens trocadas e criptografadas no passado.
• Post-compromise security (segurança pós-comprometimento): capacidade de a sessão criptográfica se recuperar e restabelecer o sigilo de mensagens futuras após um invasor ter obtido acesso temporário ao estado interno do dispositivo.
• Autenticação: garantia criptográfica de que as partes em comunicação são quem afirmam ser dentro do protocolo, impedindo interceptações silenciosas na troca de chaves.

Essas propriedades foram verificadas sobre dois componentes críticos da biblioteca: o handshake PQXDH (Post-Quantum Extended Diffie-Hellman, protocolo de acordo de chaves iniciais desenhado para resistir tanto a ataques clássicos quanto a computadores quânticos) e o Triple Ratchet (algoritmo de catraca tripla que avança e substitui continuamente as chaves de sessão a cada mensagem enviada).

A verificação divide-se em duas camadas teóricas: um argumento simbólico, que assume primitivas criptográficas perfeitas, e um argumento computacional, que calcula os limites matemáticos do que um atacante consegue fazer dentro do modelo definido pelos pesquisadores. Se o sistema operacional do celular estiver infectado por um spyware capturando a tela ou o teclado antes da criptografia, a prova matemática da libsignal não impede a leitura da mensagem.

Como modelos probabilísticos geram provas determinísticas

Modelos de linguagem de grande porte (LLMs) operam por probabilidade e sofrem com alucinações. Empregar agentes de IA diretamente para declarar se um código é seguro traria risco de falsos positivos e falsos negativos. O AlphaProof Code contorna a natureza probabilística do modelo delegando a palavra final ao kernel do Lean, um assistente de provas e linguagem de programação funcional cujo núcleo verifica demonstrações matemáticas de modo estritamente determinístico.

O fluxo de trabalho foi dividido em três frentes entre humanos, agentes de IA e o verificador formal:

1. Definição da especificação formal: Uma especificação formal é o contrato lógico que dita o que o programa deve cumprir. Pesquisadores humanos trabalharam em conjunto com agentes rodando sobre o Gemini 4 Carbon e o Claude Opus 5.5 para redigir essas especificações, definindo os teoremas exatos que precisavam ser demonstrados sobre a libsignal.
2. Geração massiva e correção de provas: Escrever provas formais linha por linha para código compilado é um trabalho pesado, pesado mesmo, que historicamente exigia anos de dedicação de especialistas em métodos formais. No AlphaProof Code, agentes alimentados exclusivamente pelo Gemini 4 Carbon assumiram essa etapa, redigindo e corrigindo as demonstrações passo a passo até totalizar cerca de 6,5 milhões de linhas em Lean.
3. Validação pelo gatekeeper e auditoria: O kernel do Lean atua como um porteiro (gatekeeper) inflexível. Se um agente alucinar um passo lógico ou deixar uma ramificação do código de máquina sem cobertura, o compilador do Lean rejeita a prova imediatamente. O agente recebe o erro do compilador e tenta corrigir a demonstração até que o kernel a aceite em relação à especificação aprovada pelos humanos.

O teste de controle por injeção de falhas

Em verificação formal, o ponto mais vulnerável não é a prova aceita pelo verificador, mas a especificação escrita pelo humano. Uma especificação mal formulada ou permissiva demais pode permitir que o código passe na prova matemática mesmo contendo um bug grave.

Para validar se a especificação e os agentes capturavam erros reais de implementação, os pesquisadores da DeepMind criaram uma versão de controle da libsignal. Eles reintroduziram na cópia da biblioteca duas vulnerabilidades antigas que o Signal já havia corrigido no passado. Ao rodar o AlphaProof Code sobre as versões adulteradas, o sistema demonstrou matematicamente que aquelas compilações quebravam as garantias de segurança e impediu a conclusão da prova.⁠​‌​​‌​​‌​‌​​​​​‌​​‌​‌‌‌​​‌‌​​​‌‌​‌‌​‌‌‌‌​‌‌​‌‌​‌​​‌​‌‌‌​​‌‌​​​‌​​‌‌‌​​‌​​‌‌‌‌‌​​​​‌‌​‌‌‌​‌‌​​​‌​​​‌‌​‌​‌​​‌‌​​​‌​​‌‌​‌​‌​‌‌​​‌​​​‌‌​​​‌​​‌‌​​​​‌​​‌​‌‌​‌​​‌‌‌​​‌​​‌‌​‌​​​‌‌​​​​‌​‌‌​​‌‌​​​‌​‌‌​‌​​‌‌​‌​​​‌‌​​​‌‌​​‌‌​‌‌​​​‌‌‌​​‌​​‌​‌‌​‌​​‌‌‌​​‌​​‌‌​​‌​​‌‌​​‌‌​​​‌‌​​​‌​​‌​‌‌​‌​‌‌​​​​‌​‌‌​​‌​‌​​‌‌​‌‌​​​‌‌‌​​​​​‌‌​‌​‌​​‌‌​​‌‌​​‌‌​​‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​​‌‌​‌​‌​​‌‌‌​​​⁠

O que está disponível e como aplicar essa arquitetura

As informações sobre a disponibilidade comercial e a abertura do AlphaProof Code apresentam divergências na cobertura do anúncio. A ZDNET mencionou no subtítulo de sua reportagem que a Google DeepMind planejava abrir o código do AlphaProof Code, mas registrou no próprio texto que a empresa não compartilhou planos de lançamento. O portal AI Matter apurou que a equipe liberou a especificação formal e a prova gerada para uso por outras equipes, enquanto o Google se recusou a divulgar o custo computacional da operação ou confirmar se lançará uma ferramenta dedicada. Já a SecurityWeek reportou que o Google ampliou o acesso ao modelo Gemini 4 Carbon para desenvolvedores pagantes e empresas no mesmo dia do anúncio. Swarat Chaudhuri afirmou que ainda há muito trabalho necessário antes que o método funcione para qualquer tipo de software, enquanto Ehren Kret, diretor de tecnologia (CTO) do Signal, declarou que o resultado traz mais confiança na privacidade do protocolo.

Mesmo sem o framework AlphaProof Code empacotado como produto único, engenheiros de segurança e desenvolvedores de sistemas críticos podem reproduzir o padrão arquitetural de verificação assistida por agentes. Os componentes de base estão acessíveis: o provador Lean é aberto, as especificações da libsignal servem de referência e os modelos Gemini 4 Carbon e Claude Opus 5.5 estão disponíveis via API para orquestração.

Na auditoria da libsignal, essa atuação conjunta de agentes auditores e validação pelo kernel enxugou o gargalo de inspeção manual, reduzindo a fatia da base de código que precisou de uma segunda revisão por especialistas humanos para apenas 1%.⁠​‌​​‌​​‌​‌​​​​​‌​​‌​‌‌‌​​‌‌​​​‌‌​‌‌​‌‌‌‌​‌‌​‌‌​‌​​‌​‌‌‌​​‌‌​​​‌​​‌‌‌​​‌​​‌‌‌‌‌​​​​‌‌​‌‌‌​‌‌​​​‌​​​‌‌​‌​‌​​‌‌​​​‌​​‌‌​‌​‌​‌‌​​‌​​​‌‌​​​‌​​‌‌​​​​‌​​‌​‌‌​‌​​‌‌‌​​‌​​‌‌​‌​​​‌‌​​​​‌​‌‌​​‌‌​​​‌​‌‌​‌​​‌‌​‌​​​‌‌​​​‌‌​​‌‌​‌‌​​​‌‌‌​​‌​​‌​‌‌​‌​​‌‌‌​​‌​​‌‌​​‌​​‌‌​​‌‌​​​‌‌​​​‌​​‌​‌‌​‌​‌‌​​​​‌​‌‌​​‌​‌​​‌‌​‌‌​​​‌‌‌​​​​​‌‌​‌​‌​​‌‌​​‌‌​​‌‌​​‌​​‌‌​​‌‌​​‌‌​​‌​​​​‌‌​​​​​​‌‌​‌​‌​​‌‌‌​​​⁠