Claude prova a segurança de 123 bibliotecas no nível do código RISC-V

A Anthropic e a Theorem publicaram os resultados de um projeto em que o Claude escreveu, de forma autônoma, provas formais de correção para código open source real. O modelo provou a ausência de crashes em 239 pontos de entrada de 123 bibliotecas do Google OSS-Fuzz. As provas não trabalham com o código-fonte, e sim com as instruções RISC-V compiladas, e somam cerca de 180 milhões de linhas em Rocq. Antes, esse tipo de trabalho exigia anos de esforço de especialistas muito raros, por isso só era usado onde um erro custa caro demais, como na aviônica da Airbus.

Fuzz test como especificação pronta

O principal problema da verificação formal é que, primeiro, é preciso explicar o que significa "correto". Para um decodificador de PNG existe a RFC 2083, mas para um editor de texto ou um navegador não há uma especificação clara. Os pesquisadores contornaram isso da seguinte forma: pegaram os fuzz tests que os próprios desenvolvedores já tinham e transformaram a condição "o teste nunca falha" em especificação formal. Ela foi descrita sobre um modelo de como qualquer binário RISC-V é executado no Linux.

O fuzzer testa um número enorme de entradas semialeatórias, mas não garante cobertura completa. A prova, sim, oferece uma garantia: se o Claude provou que o teste não falhará com nenhuma entrada menor que 64 MB, o fuzzing desse ponto de entrada em RISC-V não vai encontrar mais nada. O OSS-Fuzz compila programas em C e C++ com AddressSanitizer, então qualquer acesso incorreto à memória conta como crash. Por isso, a propriedade provada inclui automaticamente memory safety, a principal fonte de vulnerabilidades.

O que exatamente foi alcançado

O projeto levou algumas semanas. O critério de sucesso: o Claude escreve a prova, o kernel do Rocq a verifica, e uma pessoa não precisa ler centenas de milhares de linhas. É preciso confiar em três coisas: nos modelos formais de RISC-V e de processos Linux, na formulação exata dos teoremas e no próprio Rocq.

• 123 bibliotecas do OSS-Fuzz, 239 pontos de entrada
• cerca de 180 milhões de linhas em Rocq; a prova típica tem cerca de 600 mil linhas
• binário mediano: 18 000 instruções RISC-V
• garantia: saída correta, sem erros de memória nem falhas de assertions, para qualquer entrada de até 64 MB
• premissas: binário estático e single-thread, orçamento de memória fixo, RISC-V e Linux

Os próprios autores ressaltam que isso não significa que as bibliotecas estejam livres de bugs. Os erros restantes podem estar nos componentes confiáveis ou fora da propriedade provada. Em compensação, a superfície de verificação diminui: para cobrir novos projetos, não é preciso aumentar a base confiável.

Bugs que o fuzzer não encontraria

Quando uma prova não fechava, o Claude corrigia o código, a especificação era gerada de novo e o modelo passava a provar a nova versão. Assim surgiram centenas de erros. O fuzzer quase certamente não pegaria muitos deles, porque ele muta entradas pequenas, em geral de até 1 MB. Exemplos:

• underflow de contador em uma cópia de um descompressor, levando a escrita fora dos limites do buffer, apenas com entradas de cerca de 20 MB e estrutura rara
• leitura fora dos limites em um decodificador de imagens, que exige entrada de 64 MB ou mais e mais de 2 GB de memória
• leitura fora dos limites em outra biblioteca, após uma sequência específica de chamadas por dois descritores do mesmo arquivo
• redescoberta da CVE-2026-56132 no libexpat, que exige aninhamento profundo
• erro lógico sem crash: a função de limitação de arquivos carregados nem sempre funcionava

Há também um efeito colateral importante: mesmo uma tentativa de prova malsucedida revela defeitos reais. Além disso, os fuzz tests costumam verificar propriedades de alto nível, como codificação e decodificação sem perdas. No algoritmo de compressão LZO, o teste afirma que a descompressão dos dados comprimidos devolve o original. Se a propriedade é violada, o programa falha, e provar a ausência de crashes equivale a provar a própria propriedade. No cpp-httplib, o Claude precisou excluir separadamente o estouro de pilha causado por recursão profunda no destrutor de std::set.

Lições práticas para as equipes

O contexto do trabalho é duro: no kernel do Linux, mais de 1000 vulnerabilidades foram divulgadas recentemente, e os modelos estão cada vez melhores em montar cadeias de exploits a partir de bugs pequenos. Para comparação, a implementação do kernel seL4 levou dois anos-pessoa, e a verificação, vinte. Se o custo das provas cai conforme os modelos evoluem, e se provas prontas podem ser reaproveitadas entre bases de código, a economia muda.

A Anthropic publica parte das provas, os modelos de RISC-V e do SO, além das especificações dos testes que não foi possível provar. A Theorem se oferece para rodar o mesmo pipeline em outros projetos open source e lança uma Claude skill para verificação independente. Desenvolvedores que já testaram métodos formais com modelos mais fracos e desistiram deveriam rever a questão. Um bom ponto de partida é um projeto que já tenha fuzz tests de qualidade: a especificação, nesse caso, está quase pronta. Em paralelo, os autores testam os mesmos métodos no zlib e na verificação de equivalência comportamental de um interpretador de Python escrito em Rust.