Google DeepMind lança AlphaProof Code: agentes provam em Lean a segurança do código compilado do Signal
O Google DeepMind detalhou em 10 de novembro o AlphaProof Code, um sistema de agentes que produziu cerca de 6,5 milhões de linhas de provas em Lean sobre o código de máquina da libsignal, a biblioteca de referência do protocolo Signal. As provas cobrem o aperto de mão pós-quântico PQXDH e o Triple Ratchet, com premissas e limitações especificadas no artigo técnico.
A demonstração havia sido mencionada brevemente durante o lançamento do Gemini 4 Carbon; agora ela está documentada. O Google DeepMind publicou em 10 de novembro um post de blog e um artigo técnico sobre o AlphaProof Code, um sistema de agentes que provou matematicamente propriedades de segurança do código da libsignal, a biblioteca de referência do protocolo Signal. Esse protocolo também criptografa, em variantes, o WhatsApp, o Messenger e o Google Mensagens.
O que foi provado
A originalidade está no nível da prova. A maioria das verificações de protocolos se limita ao seu projeto conceitual. Desta vez, os pesquisadores compilaram a libsignal com o compilador padrão do Rust para processadores AArch64 (Arm de 64 bits) no Linux e depois provaram que esse código de máquina respeita as propriedades esperadas. Essas provas cobrem o aperto de mão pós-quântico PQXDH e o Triple Ratchet: sigilo para frente, autenticação, segurança após o comprometimento temporário de um dispositivo e segredo do aperto de mão.
Os números mostram a escala: cerca de 6,5 milhões de linhas de provas escritas em Lean, uma linguagem de prova cujo núcleo valida cada etapa. Elas se apoiam em cerca de 26.000 linhas de especificações e de descrição do processador que, por sua vez, precisam ser consideradas confiáveis. O trabalho levou quatro semanas para uma equipe de cinco pessoas. O artigo lembra que a verificação do micronúcleo seL4 exigiu vinte pessoas-ano, e a do compilador CompCert, seis.
Como os agentes trabalham
O AlphaProof Code divide as tarefas como uma equipe de pesquisa. Humanos decidem o que provar e revisam cada especificação, redigida com o auxílio de vários modelos. Agentes movidos pelo Gemini Carbon escrevem as provas de forma autônoma em seguida. Um agente “guardião” só aceita uma prova se o Lean a validar contra uma cópia da especificação aprovada: a confiabilidade do resultado final, portanto, não depende da confiabilidade dos agentes. De acordo com o Google DeepMind, os agentes auditaram seu próprio trabalho na sequência e sinalizaram apenas cerca de 1% do código de prova para revisão humana.
Para verificar se o sistema distingue código seguro de código com defeito, a equipe reintroduziu dois bugs reais, já corrigidos anteriormente, em uma cópia isolada da libsignal. Em ambos os casos, o sistema produziu uma prova verificada de que a versão com erros não era segura. O diretor de tecnologia do Signal, Ehren Kret, citado na publicação, considerou o feito um “avanço importante”. Os artefatos de verificação foram publicados em código aberto.
Os limites, explícitos no papel
O artigo técnico detalha com precisão o que ele não garante. As provas simbólicas pressupõem criptografia perfeita e nada dizem sobre o segredo computacional dos bytes. Os limites computacionais não são válidos contra um adversário quântico. A geração de chaves não é verificada. A descrição do processador abrange 467 instruções e 31 chamadas de sistema, mas não modela threads, sinais ou vinculação dinâmica. Por fim, o resultado confia no núcleo do Lean, nas primitivas criptográficas e nos contratos de determinadas rotinas chamadas pelo programa.
Nossa leitura
A verificação formal sempre teve um ponto fraco: custa caro demais para quase todos os softwares. O AlphaProof Code demonstra que agentes conseguem produzir a maior parte das provas, desde que humanos definam o que deve ser provado e o Lean valide todo o restante. Trata-se de uma mudança de método mais do que um feito isolado: a confiança deixa de recair sobre agentes falíveis e passa para um verificador mecânico. Mas o resultado diz respeito a um escopo bem delimitado — um pequeno programa de teste em linha de comando, uma arquitetura específica e premissas criptográficas assumidas. O pioneirismo alegado e o custo real de computação ainda precisam passar pela análise de outras equipes, até porque o Google DeepMind não esclareceu se a ferramenta em si será disponibilizada para terceiros. Para os desenvolvedores de softwares críticos, a pergunta torna-se prática: quem escreverá e revisará as especificações, que passam a ser a principal tarefa humana?
Fontes
- Google DeepMind — Introducing AlphaProof Code: a breakthrough in verifying complex software at depth (10 de novembro de 2026) Fonte primária
- Google DeepMind — AlphaProof Code: Verifying Signal's Security at the Machine-Code Level (artigo técnico e desenvolvimento em Lean) Fonte primária
- The Register — Google DeepMind melds humans and AI agents to vet Signal's secure messaging techniques Fonte secundária
Uma fonte primária vem diretamente da empresa, do laboratório ou da organização envolvida. Uma fonte secundária relata a informação sem ser a sua autora: nós a sinalizamos como tal. Encontrou um erro? Consulte nossa política de correções.
