O Google DeepMind anunciou que agentes de IA conseguiram provar matematicamente propriedades de segurança do código real do protocolo Signal. A ferramenta se chama AlphaProof Code e, segundo a empresa, fez em quatro semanas um trabalho que costumava levar anos.
O protocolo Signal protege conversas no próprio app Signal e no Google Messages. Por isso, o anúncio interessa a qualquer pessoa que troca mensagens pelo celular, e não só a especialistas em segurança.
Neste artigo, você entende o que é verificação formal, como o AlphaProof Code funciona, o que foi comprovado e por que isso pode mudar a forma como softwares críticos são auditados.
O que o Google DeepMind anunciou
O anúncio foi publicado em 10 de novembro de 2026 no blog do Google DeepMind, assinado por Pushmeet Kohli e Swarat Chaudhuri. A empresa descreve o resultado como um desafio de segurança considerado muito difícil há décadas.
Segundo o texto, é a primeira vez que a IA é usada para verificar formalmente um protocolo criptográfico amplamente usado nesse nível de profundidade. Também é a primeira vez que a implementação de um protocolo desse porte é verificada formalmente por qualquer método, com ou sem IA.
O Google diz ainda que vai abrir os artefatos da verificação para a comunidade e publicou um artigo técnico com os detalhes.
O que é verificação formal, em palavras simples
A maioria dos softwares é testada com exemplos: você roda o programa em vários casos e confere se o resultado está certo. O problema é que nenhum conjunto de testes cobre todas as situações possíveis.
A verificação formal faz outra coisa: prova matematicamente que o código sempre se comporta como deveria. O Google chama isso de padrão mais alto de garantia de segurança. A desvantagem é que o processo é difícil e costuma exigir muito trabalho manual.
Pense na diferença entre testar uma ponte com alguns caminhões e calcular, com engenharia, que ela aguenta qualquer carga dentro do limite. O teste mostra que funcionou naquele dia; a prova mostra que sempre vai funcionar dentro das regras definidas.
Como o AlphaProof Code trabalha
O AlphaProof Code é um sistema com vários modelos de linguagem que divide o trabalho como uma equipe de pesquisa. Especialistas humanos decidem, junto com a IA, o que precisa ser provado. Depois, um grupo de agentes faz as provas.
Primeiro, os pesquisadores traduziram os objetivos de segurança do Signal em especificações matemáticas, com revisão humana de cada uma. Em seguida, agentes baseados no Gemini Carbon geraram mais de seis milhões de linhas em Lean, uma linguagem que verifica provas matemáticas automaticamente.
Por fim, os próprios agentes auditaram a prova e apontaram os trechos que mereciam um segundo olhar humano: só 1% da base de código. Como o Lean confere o resto automaticamente, os especialistas focaram onde o julgamento humano mais importa.
| Etapa | Quem faz | Resultado |
|---|---|---|
| Definir o que provar | Especialistas humanos com apoio de modelos | Especificações matemáticas revisadas |
| Escrever as provas | Agentes baseados no Gemini Carbon | Mais de 6 milhões de linhas em Lean |
| Conferir as provas | O verificador do Lean | Checagem automática de cada prova |
| Auditoria final | Agentes apontam e humanos revisam | Só 1% do código para revisão humana |
O que exatamente foi provado no Signal
Segundo o Google, a maior parte das verificações de protocolos para no nível do projeto, isto é, no desenho teórico. Os agentes foram além e provaram que o código compilado cumpre as propriedades de segurança, até o código que roda nos aparelhos.
Uma das propriedades citadas é manter as mensagens protegidas antes e depois de um aparelho ser comprometido temporariamente. É nesse espaço entre o projeto e a implementação que muitas falhas reais costumam se esconder.
Para testar se o sistema distingue código certo de código com defeito, a equipe reintroduziu dois bugs reais, já corrigidos, em uma cópia isolada do código do Signal. Nos dois casos, o AlphaProof Code gerou uma prova verificada de que a versão com bug era insegura.
Ehren Kret, diretor de tecnologia do Signal, afirmou no anúncio que usar agentes de IA para traduzir código real em teoremas válidos em Lean é um grande avanço e que a verificação dá ainda mais confiança nas garantias de privacidade do protocolo.
O que isso muda para empresas e usuários
Para o Google, o resultado abre caminho para verificar outros sistemas críticos, como firmware de equipamentos médicos e software de redes elétricas. A empresa também cita o uso combinado com agentes de defesa automatizada, como o CodeMender.
A própria DeepMind reconhece que escalar essas técnicas ainda exige pesquisa. Ou seja, não espere que todo aplicativo do seu celular seja verificado formalmente amanhã.
Para o usuário comum, a mensagem prática é que a base criptográfica do Signal ganhou uma camada extra de confiança. Para quem desenvolve software, o recado é outro: a IA começa a tornar viável um tipo de auditoria que antes só cabia em projetos com muito tempo e dinheiro.
Perguntas frequentes
Isso significa que o Signal é 100% seguro?
Não. A prova cobre as propriedades de segurança que os especialistas especificaram, no código analisado. Outros riscos, como um celular infectado ou um golpe que engana o usuário, ficam fora desse escopo.
O WhatsApp também foi verificado?
O anúncio fala do código do protocolo Signal e cita o app Signal e o Google Messages como usuários dessa tecnologia. O WhatsApp não é mencionado no texto do Google.
O que é Lean?
É uma linguagem de computador usada para escrever provas matemáticas que o próprio sistema confere automaticamente. Se uma prova tem erro, o Lean não a aceita.
O AlphaProof Code está disponível para outras empresas?
O anúncio não fala em produto comercial. O Google diz que vai abrir os artefatos da verificação do Signal e publicou o artigo técnico.
Conclusão
O AlphaProof Code mostra a IA saindo da geração de código para a prova de que o código está certo. No caso do Signal, isso levou quatro semanas e deixou só 1% do trabalho para revisão humana.
Quer ver outro lado da IA na segurança digital? Leia nosso artigo sobre 5 falhas de segurança que a IA deixa no seu código.