Google DeepMind apresenta AlphaProof Code e verifica formalmente o código do protocolo Signal

O Google DeepMind afirma que agentes de IA provaram propriedades de segurança centrais do código real do protocolo Signal, e não só do design. O trabalho usou o AlphaProof Code, um framework multi-LLM em que especialistas humanos e modelos definem o que provar, e um grupo de agentes faz as provas. Os objetivos de segurança do Signal viraram especificações matemáticas formais, todas revisadas por humanos. Depois, agentes baseados no Gemini Carbon geraram mais de seis milhões de linhas de Lean.

Os agentes também auditaram as provas e sinalizaram cerca de 1% da base de código para nova revisão humana, já que o Lean checa o restante automaticamente. As provas cobrem o código compilado e propriedades como manter mensagens protegidas antes e depois de um dispositivo ser temporariamente comprometido. Segundo o Google DeepMind, a verificação levou quatro semanas, tarefa que historicamente leva anos para equipes de especialistas. Para testar o sistema, a equipe reintroduziu dois bugs reais já corrigidos em uma versão isolada do código, e nos dois casos ele gerou prova verificada por máquina de que a versão com bug era insegura. Os artefatos de verificação serão abertos para a comunidade. Quanto ao ineditismo, a afirmação é do próprio Google DeepMind.

A cobertura anterior do CEVIU mostra que a ideia vinha ganhando tração. Em 11 de julho de 2026, o CEVIU noticiou "Verificação Formal e o Papel da IA: Avanços e Desafios para a Segurança do Software", sobre como LLMs tornam viável uma técnica antes inviável em esforço. Em 19 de outubro de 2026, em "IA Acelera a Verificação Formal do Ethereum, Reforçando Segurança e Inovação", agentes validaram em Lean a Regra de Confirmação Rápida do Ethereum em 4 a 5 dias. Em 23 de outubro de 2026, "LLMs ampliam a escala da verificação formal de software" tratou do mesmo problema dos anos de trabalho de especialistas.

Agora o caso é um protocolo criptográfico amplamente implantado, com provas sobre o código compilado e quatro semanas de trabalho. Em 11 de agosto de 2026, o CEVIU também cobriu a integração do CodeMender com o OSS-Fuzz, e o Google DeepMind agora cita o CodeMender como complemento da verificação formal.

Para quem trabalha com IA aplicada a segurança, a leitura é que o gargalo da verificação formal pode estar se deslocando da escrita das provas para a revisão das especificações. Se os agentes produzem milhões de linhas de Lean e humanos revisam só 1%, a qualidade da especificação passa a ser o ponto crítico. Vale acompanhar os artefatos abertos para checar o que as provas cobrem de fato.