Em 22 de outubro de 2026, a Anthropic publicou que Claude e a Theorem produziram provas formais, verificadas pelo Rocq, para 239 pontos de entrada em 123 bibliotecas do Google OSS-Fuzz. O resultado relatado é específico: os pontos selecionados não apresentariam falhas para entradas abaixo de 64 MB dentro de um modelo definido de execução em RISC-V e Linux. Ele não abrange todas as funções das bibliotecas.
Como Claude e Rocq participam da verificação
Fuzzing é uma técnica que executa um programa com muitas entradas, frequentemente geradas de forma automática, para tentar encontrar falhas. A Anthropic relata que transformou testes fuzz existentes em especificações formais para binários compilados em RISC-V. Uma especificação formal descreve matematicamente a propriedade que se quer provar.
Claude gerou o código das provas; o núcleo do Rocq verificou se elas decorriam das especificações. A Theorem forneceu as semânticas de instruções RISC-V e de processos Linux usadas para modelar a execução. Assim, o Rocq checou as provas em relação às propriedades formuladas, não se essas propriedades descreviam todo comportamento possível do software no mundo real.
O que o resultado abrange
A Anthropic relata provas para 239 pontos de entrada distribuídos por 123 bibliotecas. Um ponto de entrada é uma função ou rotina por onde o programa começa a executar determinado teste. A propriedade principal era não ocorrer uma falha para qualquer entrada abaixo de 64 MB, incluindo erros de segurança de memória modelados e asserções que falhassem.
A prova se refere a binários estáticos, de execução em uma única thread, com orçamento fixo de memória, sob o modelo de Linux e a arquitetura RISC-V. A Anthropic afirma que não verificou todos os pontos de entrada das bibliotecas; os pontos escolhidos também não cobrem necessariamente todo o comportamento de cada biblioteca.
Durante as tentativas de prova, Claude também corrigiu bugs encontrados e a especificação foi gerada novamente para o código corrigido. A Anthropic diz que penalizou alterações no código, pediu evidências sobre as entradas afetadas e registrou e auditou as correções para reduzir o risco de mudanças feitas apenas para facilitar a aprovação das provas.
Bugs encontrados durante as tentativas
Entre os exemplos relatados pela Anthropic estão um contador que sofria underflow em um descompressor, levando a uma gravação fora dos limites da memória com uma entrada rara de cerca de 20 MB, e uma leitura fora dos limites em um decodificador de imagens. Esse segundo caso exigia uma entrada de 64 MB e mais de 2 GB de memória.
A Anthropic também relata uma leitura fora dos limites que dependia de uma sequência específica de chamadas usando dois identificadores para o mesmo arquivo, além da redescoberta da vulnerabilidade CVE-2026-56132 no libexpat, provocada por uma entrada profundamente aninhada. Esses casos são exemplos dos bugs relatados no projeto, não uma contagem de todas as falhas que podem existir nas bibliotecas.
Por que uma prova formal tem limites
Uma prova verificada estabelece que um programa satisfaz uma propriedade dentro da especificação e do modelo formal usados. Se a especificação não representar uma condição relevante, ou se o modelo da máquina não corresponder à execução real, o resultado não cobre essa diferença. A arquitetura, a configuração do binário e o ponto de entrada fazem parte do escopo.
A análise dinâmica AddressSanitizer, conhecida como ASan, instrumenta programas em C e C++ para detectar certos erros de memória durante a execução. A Anthropic observa que o ASan não detecta todos esses erros. Da mesma forma, verificar pontos de entrada selecionados não cobre automaticamente funções não alcançadas por eles, e uma aplicação que chama uma biblioteca ainda pode usá-la de maneira incorreta.
O que os números do apêndice dizem sobre as provas
O apêndice da Anthropic distingue cerca de 1 bilhão de linhas Rocq geradas durante as tentativas de aproximadamente 180 milhões de linhas incluídas nas provas que passaram pela verificação. Uma prova típica tinha cerca de 600 mil linhas, distribuídas por aproximadamente 1.400 arquivos. A checagem consumia de 30 minutos a várias horas de tempo de CPU.
Os totais medem etapas diferentes: linhas produzidas ao longo das tentativas e linhas que compõem provas aprovadas pelo verificador. O volume ajuda a dimensionar o trabalho, mas não amplia o que cada prova cobre.
O caso do interpretador Python combina prova e teste empírico
Em um estudo separado, a Anthropic relata que o Verus verificou os 17 níveis de um interpretador de Python escrito em Rust em relação à semântica formal definida pelo projeto. A comparação desse interpretador com o CPython foi feita por testes: em mais de 1,7 milhão de programas gerados, a Anthropic relata correspondência de comportamento em 99,95% dos casos.
A prova formal cobre a semântica especificada para o interpretador; a taxa de 99,95% vem da comparação empírica com o CPython nesses programas. São resultados diferentes, e a comparação não constitui uma prova de equivalência para todo programa Python.
