O que foi realmente provado
A Frontier Red Team da Anthropic, em conjunto com a Theorem, publicou a 22 de outubro os resultados de uma tentativa de usar o Claude para verificação formal em larga escala. A equipa pegou em testes de fuzzing já existentes do OSS-Fuzz, da Google, tratou cada teste como uma propriedade que o código tem de satisfazer, compilou-o para assembly RISC-V e pediu ao Claude provas verificáveis por máquina de que o binário resultante nunca falha.
A propriedade é estreita e precisa: para qualquer entrada inferior a 64 MB, o programa não falhará com um erro de segurança de memória nem com uma asserção falhada. As provas pressupõem um binário estático de um só fio de execução com orçamento de memória fixo, numa CPU RISC-V sob Linux, e confiam no verificador Rocq, nas semânticas de RISC-V e de processos Linux da Theorem e no hardware e compilador de OCaml por baixo.
Os números
Em 123 bibliotecas de código aberto, o Claude provou que 239 pontos de entrada estão livres de falhas segundo aquela especificação. As provas somam cerca de 180 milhões de linhas de Rocq. Uma típica tem cerca de 600 mil linhas, contra um comprimento mediano de binário de cerca de 18 mil instruções RISC-V. O trabalho levou algumas semanas.
A Anthropic não diz quantos pontos de entrada foram tentados no total, pelo que os números não suportam qualquer taxa de sucesso. A empresa afirma que publica as provas dos testes que não precisaram de correção, e as especificações daqueles que não conseguiu provar.
Centenas de erros apareceram pelo caminho, e o Claude corrigiu-os, o que regenerava as especificações. Entre os exemplos dados estão um subfluxo de contador num descompressor que provoca uma escrita fora dos limites apenas numa disposição rara de cerca de 20 MB de entrada, uma leitura fora dos limites num descodificador de imagem que exige entrada de 64 MB e mais de 2 GB de memória, e uma redescoberta do CVE-2026-56132 na libexpat. Um deles era uma função de restrição de ficheiros nem sempre aplicada: um erro lógico que nunca falha e estava latente há mais de uma década.
O atalho óbvio, e o que fizeram quanto a ele
O arranjo tem um buraco que a própria equipa identifica. O Claude podia tornar um teorema demonstrável reescrevendo o programa para que nunca falhasse. A Anthropic diz que penalizou correções que mudavam o comportamento, deu crédito extra por provar que entradas uma correção altera, e registou e auditou cada correção.
O problema em aberto é o custo
Num conjunto de 36 pequenas tarefas de verificação construídas a partir de código real do OSS-Fuzz, com três tentativas independentes e um orçamento de cinco milhões de fichas cada, o Opus 5.5 provou metade usando cerca de 40% menos fichas do que o Opus 5. Os agentes autorizados a copiar as provas uns dos outros a partir de um espaço partilhado usaram menos 17% de fichas e completaram 34 das 36, contra 32 dos agentes que trabalharam sozinhos.
A Anthropic é explícita quanto aos limites. «Formalmente verificado» não quer dizer sem erros: um verificador não pode confirmar que a especificação corresponde à realidade, e podem persistir erros na especificação, no modelo de máquina ou na base de confiança. As provas cobrem binários RISC-V ligados à musl, ao passo que a maioria das instalações corre x86 ou ARM com glibc ligada dinamicamente. E uma única prova pode custar centenas de milhões de fichas, o que a empresa classifica como um problema em aberto central.
À parte, o Claude escreveu uma especificação a partir do RFC 1950 e provou que a implementação de zlib do núcleo Linux a cumpre ao nível do binário x86. A Anthropic afirma tê-lo repetido para cerca de seis outras bibliotecas muito usadas. Saber se esse trabalho em x86 se generaliza é o que convém acompanhar.
