A Anthropic e a Theorem disseram em 2026-10-22 que Claude ajudou a produzir provas de ausência de falhas verificadas por máquina para 239 pontos de entrada do OSS-Fuzz em 123 bibliotecas de código aberto, segundo a publicação de pesquisa da Anthropic.
O trabalho foi realizado no nível de assembly RISC-V compilado, com as provas verificadas pelo Rocq em vez de revisadas manualmente. A Anthropic também afirma que Claude encontrou e corrigiu bugs durante as tentativas de prova, incluindo problemas que o fuzzing não detectou apesar dos testes anteriores.
A garantia é mais restrita do que o título sugere. A principal alegação da Anthropic de ausência de falhas se aplica a entradas com menos de 64 MB e depende de premissas declaradas, incluindo binários Linux RISC-V estáticos e de thread única executados dentro de um orçamento fixo de memória. Isso significa que o resultado não se aplica automaticamente a outras arquiteturas ou caminhos de código não modelados.
A Anthropic afirma que está publicando publicamente um subconjunto das provas e da semântica, enquanto a Theorem oferece o pipeline para outros projetos de código aberto.