Anthropic usa o Claude para provar matematicamente que códigos de programas existentes estão corretos

O que aconteceu

A Anthropic usou o Claude para provar, com matemática, que programas já existentes funcionam corretamente. Segundo o site The Decoder, o trabalho foi feito pelo time Frontier Red Team da empresa, em parceria com a Theorem. Em poucas semanas, o modelo produziu cerca de 180 milhões de linhas de código de prova. Elas cobrem 123 bibliotecas de código aberto, escolhidas a partir de testes do projeto de segurança OSS-Fuzz, do Google.

O Claude não escreveu software novo. Ele pegou testes que provocam falhas e os transformou em problemas matemáticos. Depois analisou o código já compilado, aquele que o computador executa, e montou as provas. Um programa independente, o Rocq, confere essas provas automaticamente. De acordo com a Anthropic, quase não foram necessários revisores humanos. Os pesquisadores chamam o processo de "totalmente autônomo", mas as ferramentas e as bases formais foram criadas por humanos na Theorem.

Bugs que testes não pegaram

Ao produzir as provas, o Claude encontrou centenas de bugs e pôde corrigi-los. Muitos escapariam de testes comuns, porque só aparecem em condições muito específicas, como arquivos de entrada enormes. Em um leitor de PDF muito usado, a equipe achou numa semana tantas falhas de segurança quanto costumam ser reportadas em um ano inteiro. Em outro programa, a IA encontrou um erro de lógica que passava despercebido havia mais de dez anos.

Por que importa

A verificação formal, que é a prova matemática de que um código se comporta como deveria, sempre foi caríssima. Para verificar o kernel seL4, um sistema operacional pequeno, foram necessários 20 anos-pessoa de especialistas. Por isso o método ficava restrito a casos extremos, como o software de aviônicos da Airbus. Se a IA fizer esse trabalho, a técnica pode chegar a muito mais projetos.

Há limites claros. A própria Anthropic reconhece que "formalmente verificado" não significa "sem erros". As provas valem apenas sob condições estritas: uma arquitetura de processador específica, programas de uma única linha de execução e entradas menores que 64 MB. Na prática, essas bibliotecas rodam em outros equipamentos e configurações. O custo de computação também é alto: provas individuais chegam a centenas de milhões de tokens (as unidades de texto que a IA processa). A Anthropic não informou o custo total do projeto.

O que muda para quem usa IA

Para quem usa assistentes de programação, a ideia é que o código gerado por IA possa vir acompanhado de uma garantia, e não só de testes. Isso tende a reduzir o tempo gasto revisando o que a IA escreveu. Segundo o The Decoder, a pergunta deixa de ser se a IA sabe programar e passa a ser se ela consegue provar que o que escreveu é seguro.

Os modelos também estão ficando mais eficientes. Num teste menor, o Opus 5.5 resolveu metade das provas usando cerca de 40% menos tokens que o Opus 5. Além disso, as provas se mostraram reaproveitáveis. A Anthropic espera que a verificação formal com IA se torne tão rotineira quanto os testes comuns. O plano da Theorem já mira softwares críticos como glibc, OpenSSL e cURL.

Por enquanto, é uma pesquisa, e não um produto que o usuário comum possa ligar. Mas indica um caminho para programas mais confiáveis.