DeepMind provou formalmente com IA as garantias-chave do Signal em 4 semanas

Testes mostram que o código funciona nos casos que você pensou em verificar. A verificação formal responde a outra pergunta: é possível provar matematicamente que o código não violará uma propriedade dada com nenhum dado de entrada? Em segurança, esse é um sonho antigo, mas na prática esbarra no custo. Agora ele ganhou um argumento notável: a Google DeepMind, com agentes de IA, provou as garantias-chave do protocolo criptográfico do Signal.

O que exatamente foi feito

A equipe da DeepMind usou um novo framework chamado AlphaProof Code. O trabalho levou quatro semanas e foi concebido como prova de conceito. O protocolo Signal protege as conversas não apenas no próprio aplicativo de mensagens, mas também no Google Messages e no WhatsApp, de modo que é um dos protocolos criptográficos mais usados do mundo.

Em termos simples, a verificação tem três etapas. Primeiro, as pessoas descrevem quais propriedades o código deve ter. Depois, essa descrição é traduzida em fórmulas. Por fim, constrói-se a prova de que o código corresponde a essas fórmulas. Antes da era da IA, as três etapas consumiam meses de trabalho de especialistas. Segundo os pesquisadores, a IA agêntica reduz drasticamente justamente a última etapa, a mais trabalhosa.

O sistema não encontrou novas vulnerabilidades nas partes verificadas do protocolo. Mas também foi testado o inverso: em versões antigas do Signal com bugs corrigidos há muito tempo, o AlphaProof Code mostrou corretamente que a prova não podia ser construída. Para quem trabalha na área, é um sinal importante. A ferramenta não carimba "está tudo seguro"; ela de fato tropeça em defeitos reais.

Onde está a pegadinha

É preciso avaliar a escala com sobriedade. A análise não cobriu todo o aplicativo móvel do Signal, apenas partes específicas do protocolo. Além disso, a DeepMind não começou do zero: a Signal Foundation já havia realizado antes a verificação formal de trechos menores de código. Isso deu à equipe uma vantagem. O diretor técnico do Signal, Eren Kret, observa que a abordagem da DeepMind permite ampliar significativamente a cobertura.

A principal questão do setor é escala e custo. A DeepMind fez a análise gratuitamente, como projeto de pesquisa, e a Google se recusou a dizer quanto ela custou. À pergunta sobre se a empresa planeja um produto ou serviço comercial de verificação formal, também não houve resposta. O próprio pesquisador Swarat Chaudhuri admite que "ainda há um longo caminho" até escalar isso para todo o software do mundo.

O humano continua no circuito

O mais interessante é o processo que a equipe chama de "human-AI collaboration". Os agentes contribuem em quase todas as etapas e corrigem seus próprios erros, mas nos pontos de decisão importantes pedem a revisão de um humano. Chaudhuri diz abertamente que não quer um "mundo de vibe" em que a IA formula sozinha os objetivos, escreve sozinha as provas e, na prática, aplica as provas a si mesma. É preciso um meio-termo.

A lógica é clara. Se o modelo ao mesmo tempo decide o que precisa ser provado e o prova, um erro na formulação do objetivo passará despercebido. A prova será formalmente correta, mas verificará a coisa errada. Por isso, a especificação das propriedades deve ser aprovada de forma consciente por um humano.

O que fazer com isso

Desenvolvedores e fundadores cujo produto depende de lógica crítica (pagamentos, criptografia, protocolos de sincronização) devem começar a olhar a verificação formal como uma opção real, e não como uma exotismo acadêmico. Enquanto seu custo é desconhecido, ainda é cedo para incluí-la no orçamento. Mas há um benefício concreto: a DeepMind publica a especificação e a prova do Signal, que podem ser estudadas e usadas em outros trabalhos de verificação.

Segundo Pushmeet Kohli, do Google Cloud e da DeepMind, bancos e outras empresas que dependem de garantias de correção poderão dizer: "posso provar estas propriedades". Por ora, é mais uma promessa do que um produto pronto. Mas a verificação com IA passou em seu primeiro teste sério, em um protocolo real e de uso massivo.