A verificação formal, provar matematicamente que um código se comporta como especificado, é há muito o padrão ouro da segurança e cara demais para quase todo mundo. A Anthropic dá uma referência clara: o kernel seL4 levou dois anos-pessoa para ser escrito e 20 para ser verificado. Em parceria com a empresa de verificação Theorem, a Anthropic agora relata que o Claude produziu provas assim numa escala impensável poucos anos atrás.
O truque foi não escrever especificações à mão. A equipe pegou testes de fuzzing do programa OSS-Fuzz do Google, pequenos pontos de entrada em que qualquer travamento conta como bug, e transformou cada um numa afirmação formal: o binário RISC-V compilado nunca trava, inclusive em erros de segurança de memória detectados pelo AddressSanitizer, para qualquer entrada menor que 64 MB. Em poucas semanas, o Claude provou isso para 239 pontos de entrada em 123 bibliotecas, corrigindo no caminho os bugs que encontrou. As provas, a maioria no assistente de provas Rocq, somam cerca de 180 milhões de linhas, com uma prova típica de umas 600.000 linhas para um binário com mediana de 18.000 instruções. Ninguém precisa lê-las; o verificador do Rocq as confirma.
Os bugs são o ganho imediato. Vários eram do tipo que um fuzzer raramente acha, como uma escrita fora dos limites num descompressor que só aparecia com entradas de cerca de 20 MB com um formato específico. Outros experimentos provaram o zlib do kernel Linux contra uma versão formal da RFC 1950 e checaram um interpretador em Rust para um subconjunto de Python, que coincidiu com o CPython em 99,95% de 1,7 milhão de programas aleatórios. O custo também cai: em 36 tarefas pequenas, o Claude Opus 5.5 provou metade com cerca de 40% menos tokens que o Opus 5, e compartilhar provas entre agentes economizou 17%.
Para mantenedores, é a evidência mais forte até agora de que garantias verificadas por máquina podem virar rotina para bibliotecas comuns, como aconteceu com o fuzzing. A Theorem se oferece para rodar o processo em outros projetos de código aberto e publicou uma skill do Claude.
Os autores são cuidadosos com os limites, e os leitores também devem ser. Verificado não é o mesmo que livre de bugs. As provas cobrem builds RISC-V de uma única thread, ligados estaticamente à musl, enquanto a maioria dos usuários roda essas bibliotecas em x86 ou ARM com glibc. O AddressSanitizer não pega todos os erros de memória, nem todos os pontos de entrada foram cobertos, e quem chama uma biblioteca ainda pode usá-la mal. As provas também podem custar centenas de milhões de tokens, e essa é a verdadeira barreira para fazer isso com todo o ecossistema.