AlphaProof Code provou a correção do núcleo de criptografia do Signal em 4 semanas, em vez de anos

Testes mostram que o código funciona nos dados de entrada que você pensou em verificar. Para criptografia isso não basta: um bug que não foi encontrado em cinco anos continua sendo um bug. Por isso, nos pontos mais críticos usa-se a verificação formal, ou seja, a prova matemática de correção. Funciona, mas é cara: exige especialistas raros e anos de trabalho. A DeepMind afirma ter encontrado uma forma de reduzir bastante esse prazo.

O que a DeepMind mostrou

A equipe apresentou o AlphaProof Code, um sistema que prova que um programa atende à sua especificação de segurança sem erros. A demonstração foi feita no núcleo do protocolo de criptografia do Signal. Segundo os pesquisadores Pushmeet Kohli e Swarat Chaudhuri, no blog da DeepMind, esse tipo de trabalho costuma levar anos, e aqui bastaram quatro semanas.

Há uma segunda diferença. As tentativas anteriores de verificar o Signal paravam no nível do design teórico: provavam que o protocolo em si estava bem concebido. O AlphaProof Code verificou o código criptográfico real, que roda nos dispositivos dos usuários. Entre um esquema elegante e sua implementação costumam se esconder os erros mais desagradáveis, e foi essa lacuna que aqui se fechou.

Como funciona, com um exemplo simples

Imagine uma função que soma dois números. Um teste verifica algumas dezenas de combinações. A prova em Lean funciona de outro modo: mostra que o resultado está correto para quaisquer valores de entrada, e o Lean verifica mecanicamente cada passo. Se o raciocínio tiver furos, ele simplesmente não passa na verificação.

O processo é dividido em duas etapas:

• Primeiro, especialistas humanos formulam os requisitos formais de segurança: o que exatamente o código deve garantir.
• Depois, agentes de IA baseados no Gemini Carbon ajudam a elaborar as especificações e provam de forma independente que o programa as atende.

No total, os agentes escreveram mais de seis milhões de linhas em Lean. Cerca de 1% da base de código foi marcado pelo sistema para revisão manual por pessoas. Como controle, os pesquisadores inseriram dois erros no código, e ambos foram detectados de imediato. O diretor de tecnologia do Signal, Eren Kret, diz que essa abordagem aumenta a confiança na privacidade dos dados diante das crescentes ameaças ligadas à IA.

O que vale ter em mente

Primeiro: a prova é tão correta quanto a especificação. Se os especialistas erraram nos requisitos ou esqueceram uma classe de ataques, o sistema provará honestamente a conformidade com o objetivo errado. O gargalo se desloca da escrita de provas para a formulação de requisitos, e isso não elimina as pessoas.

Segundo: por enquanto é uma demonstração em um único projeto, e quem a divulgou foi o próprio desenvolvedor. O material não diz quanto custou a computação nem quão fácil é transferir o método para outra linguagem e outra arquitetura. Não vimos uma avaliação independente do resultado.

Terceiro: 1% do código em revisão humana parece pouco, mas falamos de criptografia, em que um único trecho não verificado pode invalidar o restante. Marcar esses trechos faz parte do método, não é uma fraqueza.

O que isso significa na prática

Para desenvolvedores, o principal sinal é este: começa-se a automatizar a parte mais cara da verificação, a escrita das provas. A habilidade de formular requisitos precisos para o código, por exemplo invariantes e limites do comportamento permitido, será mais valiosa do que saber escrever provas à mão. Se você trabalha com criptografia, pagamentos ou protocolos, vale olhar para o Lean e ferramentas semelhantes já.

Para product managers e fundadores, é um novo argumento de confiança. A frase "o código foi provado matematicamente" é mais forte do que "passamos por uma auditoria". Se o custo da verificação realmente cair de anos para semanas, esse argumento ficará acessível a mais empresas além do Signal.

A DeepMind planeja estender o método a redes elétricas e dispositivos médicos por meio de sistemas como o CodeMender. Lá o custo de um erro não é menor do que em um mensageiro, e os requisitos costumam ser mais rigorosos. Resta verificar se o resultado se repetirá em outros projetos e se especialistas independentes o confirmarão.