A Frontier Red Team da Anthropic publicou em 22 de outubro uma pesquisa em que o Claude escreveu provas formais para 239 pontos de entrada de 123 bibliotecas de código aberto: enquanto a entrada for menor que 64 MB, esses programas não travam. As provas incidem diretamente sobre os executáveis RISC-V compilados, em parceria com a Theorem, empresa de ferramentas de verificação formal. Segundo a Anthropic, é a primeira vez que uma IA faz verificação formal em larga escala no nível de assembly de software de produção.
Todas as bibliotecas vêm do projeto OSS-Fuzz, do Google, ou seja, o conjunto de componentes básicos que fica há muito tempo na plataforma de fuzzing, incluindo compressão, decodificação de imagens e análise de HTTP. O trabalho todo levou algumas semanas.
Transformar fuzzing em teorema
O método tem três etapas. Na primeira, a equipe reescreveu a suíte de testes de fuzz já existente de cada biblioteca como uma especificação formal, que diz em essência: “este código de teste não trava para qualquer entrada”. A especificação se apoia nos modelos de semântica de instruções RISC-V e de semântica de processos Linux fornecidos pela Theorem.
Na segunda, o Claude escreve a prova, e o verificador de provas Rocq a confere passo a passo.
“Claude writes the proof; the Rocq kernel checks it against the specification.” (O Claude escreve a prova; o núcleo do Rocq a confere contra a especificação.)
A terceira etapa trata do caso em que a prova não avança. Quando uma prova trava, muitas vezes é sinal de que há de fato um defeito no código; nesse ponto o próprio Claude altera o código, a especificação é gerada de novo e a prova continua. A equipe admite que essa etapa favorece o “reward hacking”: o modelo pode alterar o programa de forma arbitrária só para fazer a prova passar. Por isso os patches receberam uma penalidade, exige-se provar a faixa de entradas afetada por cada patch, e tudo é registrado item a item e auditado por humanos.
Uma prova típica tem cerca de 600 mil linhas. No fim, o que resta a ser confiado são os modelos de semântica de RISC-V e Linux, o enunciado do teorema em si e o verificador Rocq.
Falhas descobertas durante as provas
Durante as provas, foram encontradas e corrigidas centenas de falhas, algumas delas difíceis de esbarrar com fuzzing. O texto cita alguns casos: um underflow de contador em um descompressor, que só dispara com certas entradas de cerca de 20 MB; uma leitura fora dos limites em um decodificador de imagens, que exige 64 MB de entrada e mais de 2 GB de memória; e outra leitura fora dos limites que requer duas handles operando o mesmo arquivo em determinada ordem. A CVE-2026-56132 da libexpat também foi redescoberta.
A prova do cpp-httplib teve um obstáculo extra: a recursão na destruição de um std::set pode causar estouro de pilha. Para descartar isso, a equipe provou, no nível do código de máquina, que o algoritmo de balanceamento da árvore rubro-negra da libc++ mantém a profundidade da árvore em escala logarítmica.
A mesma pesquisa traz ainda alguns experimentos paralelos. O Claude escreveu em Rust um subconjunto de Python e, com o Verus, provou que ele segue a semântica do CPython; em 1,7 milhão de programas aleatórios, o comportamento coincidiu com o do CPython em 99,95% dos casos. Ele também gerou por conta própria uma semântica de instruções x86 que, executando passo a passo, consegue iniciar o espaço de usuário do Ubuntu, e de quebra encontrou centenas de erros na documentação de referência oficial.
Comparando com o seL4
A verificação formal não é novidade na indústria; a dificuldade sempre foi a mão de obra. O exemplo comum no setor é o microkernel seL4: cerca de dez mil linhas de C, com um esforço de prova frequentemente citado na época como algo em torno de vinte pessoas-ano. O compilador CompCert segue uma linha parecida, lapidado durante anos por uma equipe pequena. O que esses projetos têm em comum é poucos objetos, ciclos longos e muitos especialistas.
Desta vez, a escala da Anthropic foi de 123 bibliotecas em algumas semanas; numa comparação grosseira, a estrutura de custo por unidade de trabalho mudou de formato, e as pessoas deixam de escrever provas para definir especificações e revisar patches. O custo passou a ser em tokens: o texto afirma que uma prova completa pode consumir centenas de milhões de tokens. Nas 36 tarefas pequenas, cada tarefa deu a um único agente três tentativas, com orçamento de 5 milhões de tokens cada; ao permitir que os agentes reutilizassem as provas uns dos outros, os tokens necessários caíram mais 17%.
A força da garantia também não é do mesmo nível. O seL4 prova correção funcional; aqui se prova apenas “não travar”, um escopo bem mais estreito.
Lacunas além da prova
As limitações que a própria Anthropic lista são bastante concretas. As provas se baseiam em binários RISC-V de thread única, ligados estaticamente e com musl libc, enquanto a maioria dos usuários roda versões em x86 ou ARM com glibc ligada dinamicamente. O AddressSanitizer não detecta todos os erros de segurança de memória, há pontos de entrada não cobertos, e a corrupção de memória causada por uso indevido da biblioteca por quem a chama também fica fora das provas.
“Formally verified” does not mean “bug-free.” (“Formalmente verificado” não significa “sem bugs”.)
O desvio entre a especificação e a máquina real é o ponto em que esse caminho mais facilmente dá problema. O Rocq e os modelos de semântica também precisam ser reforçados, algo que o texto descreve como “nada trivial”. A avaliação da equipe é que a verificação formal vai se tornar uma etapa rotineira do desenvolvimento de software seguro; quanto a quando essas provas alcançarão ambientes de implantação dominantes, como x86 e glibc, o texto não dá prazo.
Fontes: artigo de pesquisa da Frontier Red Team da Anthropic, CocoLoop; página de pesquisa da Anthropic, usada para conferir o número de bibliotecas, pontos de entrada, linhas de prova e o critério de comparação de tokens.