AlphaProof Code, da DeepMind, verificou o protocolo criptográfico do Signal em 4 semanas

Todo desenvolvedor conhece a sensação: os testes passaram, a revisão do código foi aprovada, a auditoria não encontrou nada e, mesmo assim, é difícil dormir tranquilo. Os testes verificam cenários específicos, e um bug pode estar escondido em um cenário que ninguém imaginou. Para uma aplicação web comum, isso pode ser tolerável. Para a criptografia que protege a privacidade de milhões de conversas, não.

O Google DeepMind propõe outro caminho e lançou o AlphaProof Code, um sistema multiagente que automatiza a verificação formal de código.

O que é verificação formal, sem entrar na matemática

Imagine uma função de ordenação. Os testes vão verificá-la com uma centena de arrays. A verificação formal segue outro caminho. Primeiro, você descreve as propriedades matematicamente: o array de saída está ordenado e contém os mesmos elementos da entrada. Depois, constrói-se uma prova de que o código atende a essas propriedades para qualquer array, e não apenas para cem exemplos.

Esse é o nível mais alto de garantia de segurança. Mas quase ninguém o utiliza: o método é caro e demorado, e há poucos especialistas. Muitas vezes, a prova acaba sendo mais longa que o próprio código e precisa ser escrita à mão.

O que exatamente foi feito com o Signal

A equipe aplicou o AlphaProof Code ao código do protocolo criptográfico do Signal, usado para criptografar conversas no Signal e no Google Messages. Agentes baseados no Gemini 4 Carbon escreveram mais de seis milhões de linhas em Lean, uma linguagem e um ambiente de verificação de provas formais. O resultado é uma prova matemática de que o código oferece as garantias de segurança declaradas.

Dois números se destacam:

• 4 semanas. Segundo os autores, uma tarefa dessa dimensão costuma levar anos para equipes de especialistas.
• ~1%. Essa foi a proporção de pontos que os próprios agentes sinalizaram como necessitando de revisão humana após auditar sua prova. O restante foi concluído sem intervenção manual.

O Google afirma que essa é a primeira vez que a IA foi usada para verificar formalmente um programa real. Essa é uma afirmação da própria empresa; ainda não houve verificação independente.

Onde está a pegadinha

Primeiro, os limites. Uma prova formal só é tão sólida quanto sua especificação. Se as propriedades estiverem incompletas ou forem inadequadas, o código será provado correto em relação ao objetivo errado. Por isso, «a segurança foi provada» deve ser entendido como «foi provado o cumprimento de garantias específicas definidas por escrito». Isso não significa «é impossível invadir».

Outra ressalva: uma prova desse tipo não abrange tudo o que cerca o código. O ambiente, o hardware, os erros de integração e o fator humano ficam de fora. A fonte também não revela o custo de execução, os recursos computacionais necessários nem se o sistema ficará disponível para todos. Por enquanto, é uma demonstração de pesquisa, não um produto que possa ser integrado amanhã.

A abordagem também tem um ponto forte. A prova é verificada automaticamente, sem que seja preciso confiar na palavra dos agentes ou dos autores. Se o Lean aceitou a prova, ela está correta. As alucinações do modelo não são um problema aqui: um passo inválido simplesmente não passará pela verificação.

O que fazer com isso

Para quem desenvolve código crítico (criptografia, pagamentos, kernels de sistemas operacionais, protocolos de consenso): acompanhe a redução do custo da verificação formal. Se outros projetos confirmarem que o trabalho pode levar um mês em vez de anos, a barreira de entrada cairá drasticamente.

Para gerentes de produto e fundadores no setor de segurança: em vez de dizer «passamos por uma auditoria», será possível apresentar uma prova matemática verificável. É um argumento forte para setores regulados e clientes corporativos.

Para todos os demais: já vale a pena se acostumar a formular requisitos de código como propriedades verificáveis. Quando os agentes aprenderem a escrever as provas, o gargalo será a capacidade de dizer com clareza o que exatamente precisa ser verdadeiro.

A principal conclusão é simples. Os agentes já sabem escrever código, e agora começa a surgir uma forma de provar sua correção em uma escala antes inacessível. Os autores acreditam que essa talvez seja a única maneira de enfrentar a velocidade e a escala dos ciberataques atuais. É uma afirmação discutível, mas a direção está clara.