Claude passa a gerar provas matemáticas de que um código está correto, e já achou bugs antigos

Em parceria com a startup Theorem, a Anthropic usou o Claude para gerar 180 milhões de linhas de provas matemáticas sobre 123 bibliotecas de código aberto. No caminho, o modelo encontrou bugs que anos de testes convencionais não pegaram.

Em parceria com a startup Theorem, a Anthropic usou o Claude para gerar 180 milhões de linhas de provas matemáticas sobre 123 bibliotecas de código aberto. No caminho, o modelo encontrou bugs que anos de testes convencionais não pegaram.

O problema que a prova matemática resolve

Garantir que um software nunca vai quebrar, em qualquer circunstância, sempre foi caro demais para a maioria dos projetos. A chamada verificação formal (a demonstração matemática, passo a passo, de que um código se comporta exatamente como deveria) existe há décadas, mas ficou reservada a casos extremos.

Um exemplo citado pela Anthropic: verificar formalmente o seL4, um kernel (o núcleo que controla hardware e processos num sistema operacional) pequeno e simples, levou uma equipe de especialistas 20 anos-pessoa de trabalho. Por isso o método só aparecia em software crítico, como o de aviônica da Airbus, segundo reportagem do The Decoder de 23 de outubro de 2026.

Como o Claude virou provador de código que já existe

O time de pesquisa da Anthropic, o Frontier Red Team, fez parceria com a Theorem para testar se um modelo de linguagem consegue assumir esse trabalho. A ideia não foi pedir ao Claude que escrevesse software novo, e sim que verificasse código já em produção.

O processo, segundo a Anthropic, segue três passos: Claude traduz testes de falha (crash tests, usados para forçar o programa a quebrar) em problemas matemáticos, analisa o código de máquina compilado e produz a prova completa. Um verificador independente chamado Rocq confere cada prova automaticamente, e segundo a Anthropic, o processo precisa de quase nenhuma revisão humana. A Anthropic chama o processo de totalmente autônomo, embora as ferramentas e os fundamentos formais tenham sido construídos por humanos na Theorem.

180 milhões de linhas de prova em poucas semanas

O experimento usou programas de teste de 123 bibliotecas de código aberto do OSS-Fuzz, projeto de segurança do Google que gera entradas aleatórias para forçar falhas em software. Em poucas semanas, o Claude produziu cerca de 180 milhões de linhas de código de prova, segundo o The Decoder.

É um volume que não tem precedente em verificação formal tradicional, onde cada prova costuma consumir meses de trabalho especializado. A diferença é justamente o que torna a tese da Anthropic interessante para quem desenvolve software: se a máquina consegue provar a própria correção, a verificação formal deixa de ser exceção e pode virar rotina, como já é o teste automatizado hoje.

Bugs que o teste convencional não enxergava

Ao tentar provar que o código estava correto, o Claude esbarrou em centenas de bugs reais e teve autorização para corrigi-los sozinho. Muitos desses erros só aparecem em condições muito específicas, como arquivos de entrada incomumente grandes ou uma sequência particular de acessos à memória, exatamente o tipo de cenário que testes manuais ou fuzzing aleatório raramente cobrem.

Dois casos chamam atenção na reportagem:

• Ao verificar um leitor de PDF amplamente usado, a equipe encontrou, numa única semana, tantas falhas de segurança quanto costumam ser reportadas num ano inteiro para esse software.
• Em outra aplicação, o Claude identificou um erro lógico que tinha passado despercebido por mais de dez anos.

A Anthropic destaca ainda que, mesmo quando a prova completa falha no fim, a tentativa já expõe bugs reais no processo. Ou seja, o valor prático aparece antes de a prova estar fechada.

O que a palavra verificado não garante

Aqui mora o ponto que qualquer time de engenharia precisa levar a sério antes de comemorar: verificado formalmente não é sinônimo de livre de erros. As provas só valem sob condições bem definidas, segundo a Anthropic:

• uma arquitetura de processador específica;
• programas de thread única (sem paralelismo);
• entradas de até 64 MB.

Na prática, essas mesmas bibliotecas rodam em hardware diferente e em configurações diferentes das testadas. Uma prova feita para uma arquitetura e um cenário de thread única não cobre automaticamente o comportamento do mesmo código rodando em paralelo ou noutro processador, o que limita bastante o alcance imediato do resultado para sistemas de produção multithread, caso comum em backends em Node.js, Go ou Java.

O custo em tokens e o ganho de eficiência entre versões

O processo não é barato. Cada prova individual consome centenas de milhões de tokens (a unidade que mede o quanto um modelo de linguagem processa e que define o custo de uso da API). A Anthropic não divulgou o custo total do projeto.

Um teste menor trouxe dois dados relevantes para quem acompanha a evolução dos modelos da empresa: as provas se mostraram reaproveitáveis, e o modelo mais novo é mais eficiente que o anterior. Segundo a reportagem, o Opus 5.5 resolve metade das provas usando cerca de 40% menos tokens do que o Opus 5 precisava para a mesma tarefa, sinal de que o custo por prova deve cair à medida que os modelos evoluem.

O que muda para quem desenvolve software no Brasil

Se a IA consegue escrever código e também provar que ele está correto sob condições definidas, a pergunta deixa de ser só se a IA programa e passa a ser se ela prova que o que escreveu é seguro. É essa mudança de pergunta que a Anthropic está apostando.

O roadmap da Theorem já mira infraestrutura crítica que roda por baixo de praticamente todo stack brasileiro: glibc (a biblioteca padrão do sistema em distribuições Linux), OpenSSL (usada em conexões criptografadas) e cURL (presente em boa parte das integrações de API). Se a verificação formal avançar para esses projetos, times de TI passam a contar com componentes de base com garantias matemáticas, não apenas testados, reduzindo parte do trabalho manual de revisão em código crítico de segurança.

Isso não substitui teste nem revisão de código hoje, especialmente em sistemas concorrentes ou com entradas grandes, onde as provas atuais ainda não se aplicam. Mas para quem decide onde investir tempo de verificação, vale acompanhar o roadmap da Theorem e entender, biblioteca por biblioteca, sob quais condições exatas uma prova formal se aplica antes de tratá-la como garantia absoluta de segurança.

Fonte: The Decoder