# DeepMind usa IA para verificar partes do protocolo do Signal

> O AlphaProof Code, do Google DeepMind, comprovou garantias importantes de segurança do Signal em um projeto experimental de quatro semanas.

Oossa · 2026-11-10 · https://oossa.com/pt/deepmind-uses-ai-to-formally-verify-parts-of-signal-protocol

Pesquisadores do Google DeepMind mostraram que um sistema de IA pode comprovar matematicamente propriedades importantes de segurança do protocolo de mensagens do Signal. A equipe usou uma nova estrutura, chamada AlphaProof Code, para verificar formalmente várias garantias criptográficas. O trabalho levou cerca de quatro semanas e foi realizado como projeto de pesquisa, não como produto comercial. Nenhum bug novo foi encontrado nos trechos analisados, e a IA identificou corretamente falhas antigas, já corrigidas, ao ser aplicada a versões anteriores do protocolo.

Verificação formal é o uso da matemática para checar se um software se comporta exatamente como deveria, sem deixar margem para vulnerabilidades ocultas. Historicamente, esse processo exigia que especialistas escrevessem especificações detalhadas, as traduzissem em fórmulas e, então, construíssem a prova — uma tarefa trabalhosa que podia levar meses. Ao permitir que uma IA agêntica (capaz de definir e perseguir subobjetivos próprios) assumisse boa parte do trabalho, o DeepMind reduziu o prazo para algumas semanas. Os pesquisadores dizem que a IA ainda precisou de supervisão humana em etapas importantes, mas foi capaz de sugerir provas e corrigir os próprios erros.

Ehren Kret, diretor de tecnologia do Signal, observou que trabalhos anteriores de verificação abrangiam apenas pequenos trechos de código. A abordagem do DeepMind, disse ele, permite uma “expansão significativa” do que pode ser verificado. A equipe está disponibilizando a especificação e a prova que desenvolveu para que outros grupos possam dar continuidade ao trabalho. Embora o resultado seja promissor, o DeepMind alerta que ampliar o método para aplicativos inteiros ou cadeias completas de suprimentos de software continua sendo um desafio, e o custo dessa verificação baseada em IA não foi divulgado.

## Por que isso importa

Se a IA puder comprovar de forma confiável a segurança de protocolos criptográficos, usuários do Signal, Google Messages, WhatsApp e aplicativos semelhantes poderão ter mais confiança de que suas mensagens permanecem privadas. Para empresas que dependem de comunicações criptografadas — bancos, prestadores de serviços de saúde e jornalistas —, a tecnologia poderá, no futuro, oferecer garantias verificáveis juridicamente de que seus softwares não têm falhas críticas.

## Os fatos

- O projeto do DeepMind durou cerca de quatro semanas, segundo os pesquisadores.
- O AlphaProof Code identificou corretamente vulnerabilidades conhecidas e já corrigidas em versões antigas do Signal.
- O diretor de tecnologia do Signal, Ehren Kret, disse que a nova abordagem de IA permite uma “expansão significativa” em relação aos trabalhos de verificação anteriores.
- Os pesquisadores disponibilizaram ao público a especificação e a prova que desenvolveram.
- O Google não divulgou o custo da análise nem anunciou um produto comercial.

## Por que importa

Para as pessoas em geral, a notícia significa que a criptografia que protege suas conversas conta agora com uma verificação matemática adicional, o que reduz a possibilidade de bugs ocultos. Para empresas que precisam comprovar conformidade com normas de privacidade, a verificação assistida por IA pode se tornar uma nova forma de demonstrar segurança sem auditorias manuais demoradas.

## Fontes e referências

1. [A New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure](https://www.wired.com/story/a-new-ai-tool-from-google-deepmind-formally-verified-the-signal-protocol/) – Wired, 2026-11-10

Última atualização: 2026-11-10