DeepMind usa IA para provar matematicamente a segurança do núcleo do Signal

A Google DeepMind anunciou, em post de blog publicado em 11 de novembro de 2026 pelos pesquisadores Pushmeet Kohli e Swarat Chaudhuri, o AlphaProof Code: um sistema de IA que prova matematicamente que um software cumpre suas especificações de segurança, sem margem de erro. Como demonstração, a equipe aplicou a ferramenta ao núcleo criptográfico do Signal, o aplicativo de mensagens conhecido pela criptografia ponta a ponta. O trabalho, que normalmente levaria anos de verificação manual, foi concluído em quatro semanas (The Decoder, 11 nov. 2026).

O que muda em relação a tentativas anteriores

Segundo o post da DeepMind, esforços anteriores de verificação formal de sistemas criptográficos paravam no estágio do design teórico do protocolo, sem chegar a confirmar que o código que roda de fato no dispositivo do usuário respeita aquele design. O AlphaProof Code foi direto ao ponto sensível: verificou o código do núcleo criptográfico que efetivamente executa no aparelho de quem usa o Signal, não uma versão simplificada ou um modelo matemático do protocolo isolado do software real.

Para chegar lá, especialistas humanos primeiro definiram os requisitos formais de segurança que o código precisava cumprir. A partir dessa especificação, agentes de IA construídos sobre o modelo Gemini Carbon, da própria Google, escreveram as provas correspondentes na linguagem Lean. Ao todo, os agentes produziram mais de seis milhões de linhas de prova, das quais cerca de 1% foi sinalizado para revisão humana.

Por que a linguagem Lean importa aqui

Lean é uma linguagem de prova formal: um ambiente em que cada afirmação matemática precisa ser verificada passo a passo por um programa checador, sem espaço para intuição ou aproximação. Neste caso, a diferença está no alvo da prova: em vez de problemas matemáticos abstratos, o sistema prova que um trecho de código de produção, linha por linha, satisfaz uma especificação de segurança escrita formalmente.

Para quem desenvolve software, isso é categoricamente diferente de um teste automatizado ou de uma suíte de cobertura de código. Teste mostra que o programa se comportou corretamente nos casos que alguém pensou em testar. Prova formal mostra que não existe nenhuma entrada, nenhum caminho de execução, em que a propriedade provada deixe de valer. É o padrão usado historicamente em sistemas de altíssimo risco, como alguns microkernels certificados, mas que sempre exigiu equipes especializadas e anos de trabalho manual.

O teste com bugs plantados de propósito

A equipe da DeepMind plantou deliberadamente dois bugs no código para checar se o AlphaProof Code conseguia pegá-los. Os dois foram identificados imediatamente pelo sistema, segundo o relato da empresa. É o tipo de validação que interessa diretamente a quem trabalha com segurança: não basta o sistema provar que um código correto é correto, ele precisa também falhar a prova quando o código tem uma falha real, inclusive uma falha sutil inserida de propósito para enganar o processo.

Ehren Kret, CTO do Signal, afirmou que a abordagem reforça a confiança na privacidade dos dados num momento em que as ameaças de segurança também passam a usar IA. A declaração situa o anúncio num contexto mais amplo: a mesma tecnologia que ajuda a encontrar vulnerabilidades em escala também ajuda a fechá-las, e organizações que lidam com dados sensíveis estão sob pressão dos dois lados.

O que isso muda para quem constrói sistemas críticos no Brasil

A notícia ainda é um estudo de caso de um laboratório de pesquisa, não um produto disponível para qualquer equipe de engenharia contratar amanhã. Mas o recorte interessa a quem trabalha com sistemas de pagamento, saúde ou infraestrutura crítica no país, áreas em que o Brasil tem obrigações regulatórias crescentes (como as exigências de segurança em torno do Pix e de sistemas de saúde conectados).

Alguns pontos valem atenção de quem acompanha esse tipo de ferramenta:

• A especificação formal ainda é escrita por humanos: o salto de produtividade está na prova, não na definição do que precisa ser provado. Isso significa que equipes que já documentam requisitos de segurança de forma rigorosa têm mais chance de aproveitar esse tipo de verificação quando ela ficar acessível.
• O 1% de código sinalizado para revisão humana mostra que a ferramenta não elimina o especialista: ela concentra o trabalho dele nos pontos mais difíceis, em vez de espalhá-lo por toda a base de código.
• Verificação formal historicamente exige linguagens e arquiteturas pensadas para isso. Não está claro, pelo material divulgado, o quanto desse processo se generaliza para bases de código legadas, escritas em linguagens sem esse tipo de suporte, que são a maioria dos sistemas em produção no Brasil hoje.

O que a DeepMind planeja e o que ainda está em aberto

A empresa afirma que pretende estender o método para redes elétricas e dispositivos médicos, usando sistemas como o CodeMender, ferramenta da própria DeepMind voltada à identificação e correção automática de vulnerabilidades em software. O anúncio não detalha prazos, nem diz se o AlphaProof Code será aberto para uso externo ou permanecerá como pesquisa interna aplicada a parceiros selecionados, como parece ter sido o caso do Signal.

Também não há, no material divulgado até agora, benchmarks comparando o custo computacional desse processo com o de uma verificação manual equivalente, nem detalhes sobre quanto de supervisão especializada foi necessária para revisar aquele 1% da prova. São as perguntas que decidem se essa abordagem chega a equipes menores ou fica restrita a organizações com o orçamento e o acesso de um Signal.

Fonte

The Decoder, 11 nov. 2026: Google Deepmind's AlphaProof Code verified Signal's cryptographic core in four weeks instead of years

Fonte: The Decoder