Google DeepMind apresenta AlphaProof Code, que usou IA para verificar propriedades de segurança do protocolo do Signal

O AlphaProof Code é um framework multiagente com vários LLMs que divide a verificação formal como uma equipe de pesquisa faria. Humanos e modelos definem o que provar. Um grupo de agentes, movidos pelo Gemini Carbon, faz as provas. Primeiro, os objetivos de segurança do Signal viraram especificações matemáticas formais, e especialistas revisaram cada uma. Depois, os agentes geraram mais de seis milhões de linhas de Lean, linguagem em que o verificador checa as provas de forma automática.

O ponto técnico central é o nível da verificação. Segundo a DeepMind, boa parte do trabalho em protocolos para no desenho, e as falhas reais costumam se esconder na distância entre o design e a implementação. Aqui, as provas cobrem o código compilado que roda nos dispositivos, em propriedades como manter mensagens protegidas antes e depois de um comprometimento temporário do aparelho. A empresa diz que o processo levou quatro semanas, tarefa que historicamente tomaria anos de times especialistas. Os agentes também auditaram a prova e apontaram só 1% da base para revisão humana. Para testar se o sistema distingue código correto de código com bug, a equipe reintroduziu dois bugs reais já corrigidos numa versão isolada do código, e nos dois casos saiu uma prova verificada por máquina de que a versão era insegura. Os artefatos de verificação foram abertos para a comunidade. Tudo isso vem da própria DeepMind, que também afirma ser a primeira verificação da implementação de um protocolo desse porte, com ou sem IA.

A cobertura do CEVIU mostra a trajetória da DeepMind em verificação e segurança com IA. Em 13 de fevereiro de 2026, o CEVIU noticiou "DeepMind Apresenta Aletheia: Um Agente de IA para Pesquisa Matemática Avançada", agente que gera e verifica provas matemáticas complexas. Em 11 de agosto de 2026, veio "Google revoluciona correção de bugs com IA para segurança de memória", sobre a integração do OSS-Fuzz com o CodeMender. A diferença agora é o alvo: código criptográfico real em produção, com provas em Lean e não só pesquisa matemática ou correção de bugs. O AlphaProof Code foi anunciado em 10 de novembro de 2026, e esta matéria reflete o lançamento oficial.

Para quem trabalha com IA aplicada a segurança, o dado mais útil é o custo de revisão humana: 1% da base. Se isso se sustentar fora do caso Signal, a verificação formal deixa de ser luxo de projeto acadêmico. Ainda é um resultado reportado pela própria empresa, num código específico e com especificações escritas com ajuda humana. Vale esperar replicação da comunidade usando os artefatos abertos antes de tratar como método geral.