Claude gera provas verificadas por máquina para 239 pontos de entrada de fuzz tests em 123 bibliotecas open-source

A Anthropic, em colaboração com a Theorem, usou o Claude para provar propriedades de segurança diretamente sobre código de montagem RISC-V em mais de 100 bibliotecas open-source. O ponto de partida foram fuzz tests do OSS-Fuzz do Google. Cada teste virou uma especificação do tipo "este teste nunca quebra para nenhuma entrada menor que 64 MB", escrita sobre as instruções RISC-V compiladas. Se o Claude prova a especificação, o fuzzing daquele ponto de entrada nunca vai achar bug.

Os números: 239 pontos de entrada em 123 bibliotecas, em poucas semanas, com cerca de 180 milhões de linhas de Rocq. Uma prova típica tem uns 600.000 linhas e cobre binários com mediana de 18.000 instruções RISC-V. As garantias valem sob premissas claras: binário estático, single-threaded, orçamento fixo de memória, CPU RISC-V e Linux. Quem precisa confiar em três coisas: os modelos formais de RISC-V e de processos Linux, os enunciados exatos dos teoremas e o verificador de provas Rocq. Isso não significa que as bibliotecas não tenham bugs, e sim que eventuais falhas estão nesses componentes ou fora do escopo da prova.

Em 11 de julho de 2026, o CEVIU noticiou "Verificação Formal e o Papel da IA: Avanços e Desafios para a Segurança do Software", que já apontava o custo historicamente inviável da verificação formal e o papel dos LLMs. Agora o assunto saiu do argumento geral e virou entrega medida: provas em escala sobre bibliotecas reais, com número de pontos de entrada, volume de proof code e publicação de parte dos artefatos.

Para quem mantém uma biblioteca em C ou C++ com fuzz tests, a leitura é que o teste que você já escreveu pode virar a especificação de uma prova. O custo de entrada, historicamente de anos de especialistas, parece cair. Mas as premissas (64 MB, single-threaded, memória fixa) mostram que é garantia de propriedades específicas, não de correção total. E o simples ato de tentar a prova já rendeu bugs que fuzzers dificilmente achariam.