Anthropic afirma que Claude comprovou propriedades de segurança em 123 bibliotecas

A Anthropic publicou uma pesquisa em 22 de outubro de 2026, relatando que Claude produziu provas formais verificadas por máquina de propriedades de segurança no nível do código assembly RISC-V para 239 pontos de entrada de testes de fuzzing em 123 bibliotecas de código aberto, em uma colaboração com a Theorem.

Segundo a Anthropic, Claude corrigiu os bugs encontrados e, em seguida, provou que os programas sempre serão encerrados normalmente, sem acionar erros de segurança de memória nem falhar em asserções, para todas as entradas com menos de 64 MB e todas as respostas modeladas do sistema operacional Linux e todos os layouts de memória. As provas pressupõem que o programa seja executado como um binário estático de thread única, com um orçamento fixo de memória, em uma CPU RISC-V com Linux. A Anthropic afirmou que as provas somam cerca de 180 milhões de linhas de Rocq, e que uma prova típica tem cerca de 600.000 linhas para cobrir binários com comprimento mediano de 18.000 instruções RISC-V. A empresa afirmou que, até onde sabe, este é o primeiro esforço em grande escala para usar IA na aplicação de verificação formal a software de produção no nível do código assembly.

Uma parte das provas, juntamente com a semântica RISC-V e do sistema operacional que lhes dá suporte, está sendo publicada no GitHub. A Anthropic afirmou que também está disponibilizando os componentes confiáveis desenvolvidos para o projeto que ainda não eram públicos, provas completas para testes de fuzzing que não exigiram correções e especificações para testes de fuzzing que não conseguiu provar, mas não divulgará provas que possam revelar um bug não corrigido.

Transformando testes de fuzzing em provas formais

A abordagem converte o teste de fuzzing compilável já existente de cada biblioteca em uma especificação formal que codifica uma regra: o teste nunca trava para nenhuma entrada com menos de 64 MB. A especificação é definida sobre instruções RISC-V compiladas, usando a semântica formal da Theorem para o conjunto de instruções RISC-V e os processos do Linux; o verificador de provas Rocq confere cada prova concluída em relação à especificação. Segundo a Anthropic, isso deixa apenas três componentes nos quais os desenvolvedores precisam confiar: os modelos formais de RISC-V e dos processos do Linux, os enunciados exatos dos teoremas e o próprio verificador Rocq.

A Anthropic afirmou que aplicou esse processo a centenas de projetos da iniciativa OSS-Fuzz do Google, que oferece testes contínuos de fuzzing para projetos de código aberto qualificados e instrumenta automaticamente programas em C e C++ com o AddressSanitizer, uma ferramenta que trava um programa sempre que ocorre um acesso inadequado à memória. Um apêndice datado de 22 de outubro de 2026 apresenta o teorema completo provado: para todas as entradas com menos de 64 MiB e todos os layouts de memória, nem o binário instrumentado com ASan nem o binário sem instrumentação apresenta falhas, é abortado ou exibe comportamento não modelado; além disso, ambos produzem rastros idênticos de leitura e gravação, comportamento de encerramento e estado final do sistema de arquivos.

O apêndice afirma que Claude escreveu cerca de um bilhão de linhas de Rocq durante o esforço, das quais aproximadamente 180 milhões passaram pelo verificador de provas; o ponto de entrada do analisador de 391 linhas do cJSON recebeu uma prova de 630.000 linhas, enquanto o fftw3, com 51.000 linhas vinculadas ao binário, recebeu uma prova de 480.000 linhas. Como Claude tinha permissão para corrigir o código antes de concluir uma prova, a Anthropic afirmou que penalizou as correções, ofereceu crédito extra por provar quais entradas uma correção alterava e registrou e auditou as correções para desestimular a manipulação da recompensa.

Bugs descobertos durante as tentativas de prova

A Anthropic relata que as tentativas de prova revelaram centenas de bugs, muitos dos quais dificilmente seriam encontrados por um fuzzer. Ao provar o ponto de entrada de uma biblioteca, Claude encontrou um underflow de contador em um descompressor que causava uma gravação fora dos limites, mas apenas com entradas de cerca de 20 MB e um layout específico e raro. Entre outras descobertas estavam uma leitura fora dos limites em um decodificador de imagens que exigia uma entrada de 64 MB e mais de 2 GB de memória; uma leitura fora dos limites que exigia uma sequência específica de chamadas usando dois identificadores para o mesmo arquivo; e a redescoberta da CVE-2026-56132 na libexpat, que exigia uma entrada profundamente aninhada.

Claude também encontrou bugs lógicos que nunca causam travamentos, incluindo uma restrição sobre quais arquivos um aplicativo pode carregar que nem sempre é aplicada. A Anthropic afirmou que as tentativas de verificação em vários aplicativos críticos amplamente utilizados revelaram um bug lógico até então desconhecido, que permanecia latente havia mais de uma década, e que, durante um esforço para verificar um leitor de PDF amplamente utilizado, encontrou em uma semana tantos bugs de segurança quanto os que normalmente são relatados em um ano.

Experimentos adicionais e conclusões sobre eficiência

Além do OSS-Fuzz, a Anthropic pediu a Claude que escrevesse uma especificação formal da RFC 1950, o documento técnico que define o formato de compactação zlib, e depois provasse que a implementação zlib do kernel do Linux a implementa corretamente. Claude provou diretamente o binário compilado para x86, usando a semântica formal do conjunto de instruções x86 gerada por Claude, e a Anthropic afirmou que repetiu o processo para meia dúzia de outras bibliotecas amplamente utilizadas, encontrando bugs menores e não exploráveis em casos extremos, que estão sendo reportados aos projetos responsáveis. A empresa também relatou que a geração da semântica x86 identificou centenas de erros na documentação oficial de referência e um número menor de bugs no próprio hardware, e que a execução passo a passo da semântica pode inicializar um ambiente de usuário do Ubuntu em um kernel do Linux.

Em outro experimento, Claude criou em Rust um interpretador para um grande subconjunto de Python e provou, usando a ferramenta de verificação Verus, que ele segue a semântica do CPython descrita em um artigo acadêmico. O apêndice técnico afirma que os 17 níveis do interpretador foram provados, com o teorema estabelecendo que «Sempre que o interpretador retorna um resultado, esse resultado é o que a semântica formal prescreve». A Anthropic afirmou que testes empíricos com 1,7 milhão de programas Python gerados aleatoriamente encontraram comportamento idêntico ao do CPython em 99,95% dos testes; dos sete bugs injetados deliberadamente, cinco resistiram aos testes aleatórios, enquanto todos os sete invalidaram a prova.

Para medir a eficiência, a Anthropic criou 36 pequenas tarefas de verificação reduzindo pontos de entrada reais do OSS-Fuzz, produzindo programas com 283–2.491 instruções, entradas limitadas a 64 bytes e o AddressSanitizer substituído por um ambiente de execução «mini-ASan» com cerca de 100 instruções. A Anthropic relata que Opus 5.5 prova metade das tarefas usando cerca de 40% menos tokens que Opus 5. A Anthropic também relata que agentes autorizados a copiar as provas uns dos outros em um espaço de trabalho compartilhado precisaram de 17% menos tokens do que agentes trabalhando sozinhos; alguns tiveram sucesso após falhar anteriormente quando trabalharam individualmente, e os agentes que trabalharam sozinhos não conseguiram concluir duas das provas. A empresa afirmou que o mesmo efeito de reutilização ocorreu em grande escala durante o trabalho com o OSS-Fuzz, no qual equipes de agentes copiaram provas concluídas e as adaptaram, pois boa parte de cada prova abrange código compartilhado de inicialização do ambiente de execução C e do AddressSanitizer.

Limitações declaradas e o programa OSS Verify

A Anthropic afirma que as provas não significam que as bibliotecas estejam livres de bugs: ainda pode haver bugs nos componentes confiáveis ou fora do escopo das provas. As provas abrangem binários RISC-V estáticos e de thread única, vinculados à musl libc, enquanto a maioria dos usuários executa essas bibliotecas em x86 ou ARM e faz a vinculação dinâmica com a glibc; além disso, o AddressSanitizer não detecta todos os bugs de segurança de memória. A empresa afirmou esperar que essas limitações se tornem administráveis à medida que os modelos melhorem.

A Theorem oferece gratuitamente o mesmo pipeline a projetos de código aberto que atendam aos requisitos, por meio do programa OSS Verify. A inscrição é feita por meio de uma solicitação de pull request que adiciona os arquivos project.yaml, Dockerfile e build.sh ao repositório do programa, e a Theorem afirma que avalia os projetos segundo critérios semelhantes aos do OSS-Fuzz, dando prioridade a infraestruturas críticas amplamente utilizadas. Segundo a Theorem, os mantenedores recebem uma prova em Rocq, verificada pelo kernel Rocq, de que cada alvo de fuzzing não falha com nenhuma entrada de até 64 MiB; os bugs encontrados durante o trabalho de prova são comunicados em privado aos mantenedores por e-mail, sem prazo para divulgação, e a produção das provas pode levar vários dias. O roteiro da Theorem prevê verificar todo o ecossistema Nix, incluindo infraestruturas críticas como glibc, OpenSSL e cURL.