Cerca de 560 kilobytes de código, um arquivo menor que uma foto comum de celular, guardam o segredo das conversas de bilhões de pessoas no Signal e no Google Mensagens. Em 10 de novembro de 2026, pesquisadores do Google DeepMind (abre em nova aba) anunciaram que usaram uma nova estrutura de agentes de inteligência artificial, chamada AlphaProof Code, para inspecionar esse núcleo criptográfico e escrever mais de 6 milhões de linhas de provas matemáticas sobre ele. Quatro semanas bastaram. O trabalho comprovou que o programa responsável por embaralhar as mensagens cumpre suas regras centrais de proteção até o nível das instruções que rodam direto no processador do telefone.
No desenvolvimento de programas tradicionais, a prática padrão é testar o sistema com vários exemplos de uso para ver se ele trava ou deixa passar algum erro. O limite dessa abordagem é que testes comuns só atestam o funcionamento para as situações simuladas. O método aplicado pelo AlphaProof Code é a chamada verificação formal: transformar o comportamento do software em fórmulas e provar, com o mesmo rigor de um teorema de matemática, que nenhuma combinação possível de ações viola as regras de segurança definidas. Segundo o Google DeepMind, é a primeira vez que a implementação de um protocolo criptográfico usado em larga escala passa por uma verificação formal nessa profundidade, com ou sem ajuda de inteligência artificial.
Para concluir em um mês uma tarefa que historicamente consumia anos de trabalho humano (projetos clássicos de verificação como o sistema operacional seL4 exigiram cerca de 20 pessoas-ano de dedicação), o AlphaProof Code dividiu o serviço como um departamento de engenharia. Especialistas humanos decidiram o que precisava ser provado e revisaram cerca de 26 mil linhas de especificações matemáticas traduzidas com a ajuda de diferentes modelos de IA. Em seguida, agentes autônomos impulsionados pelo modelo Gemini Carbon (abre em nova aba) assumiram a parte pesada e redigiram as milhões de linhas de demonstração em Lean.
O Lean é uma linguagem computacional que funciona como um auditor automático e inflexível: ele confere cada passo lógico da prova matemática e barra qualquer argumento incompleto. Como essa checagem é automatizada, os próprios agentes de IA revisaram o material produzido e separaram apenas os trechos que exigiam o olhar de um engenheiro de carne e osso. Os especialistas humanos precisaram inspecionar somente 1% da base de código.
Do projeto no papel ao chip do celular
Até agora, a verificação matemática de sistemas de mensagens ou de transações bancárias costumava parar na planta arquitetônica do protocolo. Faltava a tradução. Quando o código escrito por programadores na biblioteca libsignal (feita na linguagem Rust) é convertido por um programa tradutor (o compilador) para os bytes que o processador do celular executa, falhas graves podem surgir justamente nessa passagem.
A equipe do Google contornou esse risco verificando o código já compilado, composto por cerca de 140 mil instruções de máquina na arquitetura AArch64, padrão na maioria dos smartphones atuais. A prova matemática confirmou, por exemplo, que as mensagens enviadas antes e depois de um aparelho sofrer uma invasão temporária continuam protegidas.
Convém não confundir, contudo, a prova matemática desse motor criptográfico com uma blindagem total do aplicativo que a gente abre na tela do celular. O artigo técnico (abre em nova aba) divulgado pelos pesquisadores detalha o que entrou na checagem matemática e o que ficou como premissa ou fora da análise:
| Componente ou ameaça | Status na verificação do AlphaProof Code |
|---|---|
| Criptografia e descriptografia de mensagens (Triple Ratchet) | Provado matematicamente |
Código de máquina compilado do núcleo (libsignal, ~560 KB) | Verificado (cerca de 140 mil instruções) |
| Rotinas criptográficas de base (37 funções, como AES-256 e SHA-256) | Assumidas como corretas por contrato |
| Resistência a ataques de computadores quânticos | Parcial (cobre o sigilo da conexão inicial, sem garantia na outra prova) |
| Geração de chaves e vazamentos na memória do aparelho | Fora do escopo |
| Aplicativo móvel completo do Signal | Não verificado |
Para conferir se as regras escritas não estavam deixando passar falhas reais por engano, os cientistas pegaram dois bugs antigos do libsignal, que já haviam sido descobertos e consertados no passado, e os colocaram de volta em uma cópia isolada do sistema. Nos dois testes, o AlphaProof Code bloqueou a validação e gerou uma prova matemática demonstrando que a versão adulterada era insegura, abordagem que, segundo o diretor de tecnologia do Signal, Ehren Kret, amplia o alcance prático da verificação formal contra ameaças digitais.