Principais destaques
- Criptografia sob verificação: AlphaProof Code demonstrou matematicamente garantias importantes do protocolo de segurança do Signal.
- Teste de vulnerabilidades: a ferramenta identificou falhas conhecidas em versões antigas do protocolo, mas não encontrou novas vulnerabilidades nas partes analisadas.
- Impacto além do Signal: a tecnologia também interessa à segurança de serviços como WhatsApp e Google Messages, que utilizam o protocolo Signal.
A inteligência artificial está começando a assumir uma tarefa que, até pouco tempo atrás, exigia um trabalho matemático extremamente especializado: provar que sistemas de software realmente cumprem suas promessas de segurança.
Pesquisadores do Google DeepMind utilizaram uma nova estrutura de inteligência artificial, chamada AlphaProof Code, para verificar matematicamente algumas das principais garantias criptográficas do protocolo Signal. O experimento, realizado ao longo de quatro semanas, representa um avanço na aplicação de IA à verificação formal de software.
Segundo reportagem da WIRED publicada em 10 de novembro, o trabalho não identificou novas vulnerabilidades nas partes analisadas do protocolo.
E isso merece atenção. Afinal, estamos falando de uma tecnologia que protege conversas de bilhões de pessoas.
🔐 Não é apenas sobre proteger mensagens no Signal
O protocolo Signal é conhecido por implementar criptografia de ponta a ponta, mecanismo que impede que terceiros leiam o conteúdo das conversas durante sua transmissão.
Mas sua influência vai muito além do aplicativo que leva seu nome.
Outros serviços populares também utilizam tecnologias derivadas desse protocolo, incluindo o WhatsApp e o Google Messages.
O que muda com a pesquisa: em vez de depender exclusivamente de testes convencionais e auditorias de segurança, os pesquisadores utilizaram IA para construir provas matemáticas de que determinadas propriedades criptográficas são respeitadas.
A chamada verificação formal é uma abordagem particularmente importante para sistemas críticos. Ela permite demonstrar, por meio de métodos matemáticos, que um programa atende a determinadas especificações.
O problema é que esse processo costuma ser demorado, complexo e caro.
É justamente aí que a inteligência artificial pode fazer diferença.
🧪 A IA também precisou enfrentar falhas conhecidas
Antes de analisar as garantias de segurança, os pesquisadores colocaram o AlphaProof Code à prova com versões antigas do Signal que apresentavam vulnerabilidades já conhecidas.
O resultado foi importante: a ferramenta conseguiu identificar corretamente essas falhas e demonstrar que as versões comprometidas não poderiam passar pela verificação formal.
Esse teste ajudou a avaliar se o sistema realmente conseguia distinguir implementações seguras daquelas que apresentavam problemas.
Um detalhe importante: a pesquisa não representa uma auditoria completa do aplicativo Signal. O trabalho se concentrou em propriedades específicas do protocolo e não verificou todo o código dos aplicativos móveis.
Portanto, não significa que o Google tenha certificado a segurança absoluta do Signal, do WhatsApp ou do Google Messages.
🤝 Signal também vê vantagens na abordagem
O trabalho da DeepMind aproveitou pesquisas anteriores de verificação formal realizadas pelo próprio Signal.
Segundo Ehren Kret, diretor de tecnologia da organização, a nova abordagem permite ampliar significativamente o alcance de verificações que antes se concentravam em partes menores do código.
O executivo também afirmou que o resultado oferece ainda mais confiança diante do crescimento das ameaças de segurança impulsionadas por inteligência artificial.
💡 A questão não é apenas encontrar vulnerabilidades. É conseguir demonstrar matematicamente que determinadas garantias de segurança realmente são cumpridas.
A DeepMind pretende disponibilizar a especificação e as provas desenvolvidas durante o projeto, permitindo que outros pesquisadores aproveitem esse material em iniciativas semelhantes.
🏁 Uma corrida pela verificação automática de software
O Google não está sozinho nessa tentativa de aproximar inteligência artificial e demonstrações matemáticas.
Em abril de 2026, a Signal, a Beneficial AI Foundation e a Lean FRO lançaram o Signal Shot, uma iniciativa pública para verificar o protocolo Signal e sua implementação em Rust utilizando o assistente de provas Lean.
O objetivo é traduzir o código real do Signal para o Lean e demonstrar que sua implementação corresponde a um modelo matemático previamente verificado.
Embora compartilhem objetivos semelhantes, o trabalho da DeepMind é independente dessa iniciativa.
A diferença está na velocidade e na escala que a IA pode proporcionar. Se agentes inteligentes conseguirem produzir, revisar e corrigir provas matemáticas com supervisão humana, tarefas que antes exigiam longos períodos de trabalho especializado poderão se tornar mais acessíveis.
💰 Mas quanto custa verificar tudo isso?
Existe uma questão que ainda precisa ser respondida: a viabilidade econômica.
A DeepMind realizou o experimento gratuitamente como parte de uma iniciativa de pesquisa. O Google não revelou quanto custou o projeto nem confirmou se pretende transformar a tecnologia em um produto comercial.
Swarat Chaudhuri, cientista pesquisador da DeepMind, destacou que um dos avanços importantes foi permitir que agentes de IA contribuíssem para o desenvolvimento das provas e corrigissem seus próprios resultados, enquanto especialistas humanos faziam revisões em etapas fundamentais.
Ele também fez uma ressalva importante sobre os limites da automação:
Não queremos um mundo em que a IA gere os objetivos, produza as provas e depois aplique testes escritos por ela mesma.
A preocupação faz sentido. Em segurança digital, permitir que um sistema produza suas próprias regras e valide sozinho os resultados poderia criar uma falsa sensação de confiança.
🔎 O próximo desafio é verificar muito mais do que mensagens
O experimento com o Signal aponta para uma possibilidade maior: utilizar agentes de inteligência artificial para verificar matematicamente sistemas operacionais, softwares financeiros, infraestrutura digital e outros componentes críticos.
Mas ainda existe um longo caminho até chegar a esse cenário.
A própria DeepMind reconhece que ampliar a abordagem para praticamente todo o software existente será um desafio considerável.
Por enquanto, o resultado oferece uma demonstração concreta de como agentes de IA podem ajudar especialistas a enfrentar um dos problemas mais antigos da engenharia de software: provar que um programa faz exatamente aquilo que deveria fazer.
E, quando o assunto é criptografia, demonstrar segurança pode ser tão importante quanto encontrar uma falha.
