Anthropic diz que Claude escreveu provas formais de que 123 bibliotecas de código aberto não podem falhar

Em uma colaboração com a Theorem, a Anthropic diz que usou Claude para provar propriedades de segurança no nível de assembly (RISC-V) em mais de 100 bibliotecas de código aberto usadas no mundo real, o que, segundo a empresa, é o primeiro uso em larga escala de IA para verificar formalmente software de produção nesse nível.

Segundo a Anthropic:

• O que foi provado: para 239 pontos de entrada de testes de fuzzing distribuídos por 123 bibliotecas do OSS-Fuzz, os programas sempre terminam normalmente, sem erros de segurança de memória nem asserções que falham, para qualquer entrada de até 64 MB. Isso vale sob algumas premissas: um binário estático de thread única, com um limite fixo de memória, em uma CPU RISC-V com Linux. As provas somam cerca de 180 milhões de linhas de Rocq, verificadas pelo verificador de provas Rocq.
• Como: o teste de fuzzing existente de cada biblioteca foi transformado em uma especificação ("este teste nunca falha"), e Claude escreveu a prova, corrigindo os bugs encontrados ao longo do processo. A Anthropic diz que isso revelou centenas de bugs, inclusive alguns que um fuzzer dificilmente encontraria, como uma gravação fora dos limites que exige uma entrada rara de 20 MB, e a redescoberta da CVE-2026-56132 no libexpat.
• Outros experimentos: Claude provou que a implementação de zlib do kernel do Linux corresponde a uma especificação da RFC 1950 no nível do binário x86 e criou um interpretador de Python em Rust cujo comportamento correspondeu ao do CPython em 99,95% de 1,7 milhão de programas aleatórios. A Anthropic também diz que tentativas de verificação formal em um leitor de PDF amplamente usado encontraram, em uma semana, tantos bugs de segurança quanto normalmente são relatados em um ano.
• Custo: as provas podem exigir centenas de milhões de tokens. Em 36 pequenas tarefas de verificação, a Anthropic diz que Opus 5.5 prova metade delas com cerca de 40% menos tokens que Opus 5, e que agentes que compartilham provas precisaram de 17% menos tokens.

A Anthropic está publicando um subconjunto das provas e as semânticas de RISC-V e Linux. A Theorem se oferece para executar o mesmo pipeline em outros projetos de código aberto e está publicando uma skill de Claude para verificar seu próprio código. A Anthropic observa que isso não demonstra que as bibliotecas estejam livres de bugs: os bugs restantes estariam nos componentes confiáveis ou fora do escopo das provas.