DeepMind verificou formalmente em quatro semanas as garantias-chave do protocolo Signal

Os testes mostram que o código funciona com os dados de entrada que você pensou em verificar. A verificação formal responde a outra pergunta: é possível provar matematicamente que o código se comporta corretamente com quaisquer dados? Os engenheiros há muito a chamam de santo graal da segurança, mas na prática as provas eram escritas à mão, e isso levava meses ou anos. Agora a DeepMind mostrou que uma parte significativa desse trabalho pode ser entregue a um agente.

O que exatamente foi feito

Pesquisadores do Google DeepMind verificaram formalmente, com o novo framework AlphaProof Code, uma série de garantias criptográficas-chave do protocolo Signal. Esse protocolo sustenta a criptografia no aplicativo Signal, no Google Messages e no WhatsApp. O projeto foi uma prova de conceito e levou apenas quatro semanas.

Para avaliar a velocidade, é preciso entender em que consiste o trabalho. Primeiro, as pessoas descrevem quais propriedades o código deve ter. Depois, essa descrição é transformada em fórmulas. E só então se escreve a prova em si. A IA agêntica reduz muito o tempo justamente nessa última etapa, a mais trabalhosa.

Houve também uma verificação na prática. O sistema não encontrou novas vulnerabilidades nas partes do protocolo estudadas. Em compensação, em versões antigas do Signal com bugs corrigidos há muito tempo, o AlphaProof Code encontrou esses problemas e mostrou que tal código não pode ser verificado formalmente. Para uma ferramenta de verificação, esse é um teste importante: ela não se limita a confirmar que "está tudo bem", mas realmente falha onde o código está errado.

Os pesquisadores não partiram do zero. A Signal Foundation já havia feito antes a verificação formal de trechos menores de código, e isso deu uma vantagem à DeepMind. O diretor técnico do Signal, Eren Kret, diz que a abordagem da DeepMind permite ampliar de forma notável a cobertura da verificação, o que aumenta a confiança na privacidade da implementação.

Por que isso importa para os profissionais

A principal mudança está no custo. A verificação formal era inacessível para a maioria das equipes não porque ninguém entendesse sua utilidade, mas porque as provas saíam caras demais em tempo humano. Se os agentes assumem a rotina, amplia-se o conjunto de código que vale a pena provar. Pushmeet Kohli, do Google Cloud e da DeepMind, fala abertamente de bancos e outras empresas que poderão dizer: "posso provar essas propriedades".

O mais sensato no projeto é a organização do trabalho. Os agentes contribuem e se autocorrigem quase a cada passo, mas em pontos-chave solicitam a verificação de uma pessoa. O pesquisador da DeepMind Swarat Chaudhuri explica o motivo: não é preciso um "mundo vibe", em que a IA gera os objetivos por conta própria, escreve as provas por conta própria e, na prática, passa em testes que ela mesma escreveu. É preciso um meio-termo.

Para o desenvolvedor, disso decorre algo simples. Uma prova vale exatamente o quanto a especificação for correta, isto é, a descrição do que se considera comportamento correto. Se tanto a especificação quanto a prova são escritas por um modelo, você obtém um papel bonito sem garantias. A responsabilidade pela formulação dos requisitos continua com o ser humano.

Limitações e o que fazer

Convém olhar para a escala com sobriedade. O aplicativo móvel inteiro do Signal não foi verificado, apenas partes isoladas do protocolo. O próprio Chaudhuri admite que ainda falta muito para verificar todo o software do mundo. O sistema não encontrou bugs novos, então por ora isso é mais uma confirmação do trabalho alheio do que uma descoberta.

A principal questão da indústria é a economia. A DeepMind fez a análise de graça, como projeto de pesquisa, e o Google não revelou o custo. A empresa também se recusou a comentar sobre um produto comercial ou um serviço de verificação formal. Ou seja, ainda não há um botão pronto de "verificar meu código".

O que já pode ser feito. Os pesquisadores estão publicando a especificação e a prova do Signal, um bom material de aprendizado para quem escreve código crítico: pagamentos, criptografia, infraestrutura de confiança. Se você trabalha nessas áreas, vale acompanhar como ferramentas como o AlphaProof Code deixam de ser demonstração e viram produto, e aprender desde já a formular propriedades do código de modo que possam ser provadas. É essa habilidade, e não a de escrever provas à mão, que tudo indica será valiosa.