A Anthropic apresenta um resultado ambicioso numa das áreas mais exigentes da informática. Num trabalho de investigação divulgado a 22 de outubro, a empresa relata que o Claude, apoiado por ferramentas da startup Theorem, produziu provas formais de que um grande conjunto de código aberto real não falha nas condições que os próprios programadores testam. Até agora, a verificação formal ficava reservada à aviónica, a núcleos de sistemas operativos e a software em que se justificam anos de trabalho especializado. A Anthropic defende que os modelos de linguagem a tornam acessível para bibliotecas comuns.
O ponto de partida foram os testes de fuzzing do programa OSS-Fuzz, da Google. Um fuzzer dispara enormes quantidades de entradas alteradas contra um ponto de entrada e assinala qualquer uma que provoque uma falha, incluindo erros de memória detetados pelo AddressSanitizer. Essa procura nunca é completa. A equipa transformou cada teste numa afirmação matemática: o programa compilado nunca falha para qualquer entrada inferior a 64 MB. Coube ao Claude demonstrá-la no assistente de provas Rocq, com os modelos formais da Theorem para as instruções RISC-V e o comportamento dos processos Linux.
Segundo a publicação, o Claude concluiu provas para 239 pontos de entrada em 123 bibliotecas no espaço de algumas semanas. O conjunto soma cerca de 180 milhões de linhas de Rocq, e uma prova típica ronda as 600 mil linhas para um binário com perto de 18 mil instruções. Ninguém precisa de as ler, afirma a empresa, porque o núcleo do Rocq valida cada passo de forma mecânica. A confiança fica limitada aos modelos de RISC-V e de Linux, aos enunciados exatos dos teoremas e ao próprio verificador. As garantias assentam também em pressupostos, como um binário estático com um único fio de execução e memória fixa.
As tentativas de prova funcionaram ainda como caça a erros. Sempre que encontrava uma falha alcançável, o Claude corrigia o código e prosseguia, e a Anthropic diz que o processo revelou centenas de problemas. Entre os exemplos estão uma escrita fora dos limites num descompressor incluído numa biblioteca, que só surgia com entradas de cerca de 20 MB, uma leitura indevida num descodificador de imagens que exigia um ficheiro de 64 MB e mais de 2 GB de memória, e a redescoberta de uma vulnerabilidade conhecida da libexpat. Os fuzzers, que costumam limitar as entradas a cerca de 1 MB, dificilmente chegariam a estes casos.
Houve experiências paralelas ainda mais longe. O Claude escreveu uma especificação formal do formato zlib definido no RFC 1950 e provou que o código zlib do núcleo Linux a cumpre, desta vez sobre binários x86. Construiu também em Rust um interpretador para uma grande parte da linguagem Python, demonstrou com a ferramenta Verus a sua conformidade com um modelo académico do CPython e obteve comportamento idêntico em 99,95% de 1,7 milhões de programas aleatórios. Num leitor de PDF muito usado, encontrou numa semana tantas falhas de segurança como as que costumam ser comunicadas num ano, segundo a empresa.
O custo continua a ser o grande travão, já que algumas provas consomem centenas de milhões de tokens. A Anthropic indica que o Claude Opus 5.5 resolveu metade de um conjunto de 36 tarefas de verificação com cerca de 40% menos tokens do que o Opus 5, e que agentes a partilhar um espaço com provas reutilizáveis pouparam mais 17%. A Theorem tenciona oferecer o processo a outros projetos de código aberto e publicou um plano que aponta ao ecossistema Nix, incluindo glibc, OpenSSL e cURL.
A Anthropic vai disponibilizar os novos modelos de confiança, as provas completas dos testes que não precisaram de correções e as especificações dos que ficaram por provar, retendo tudo o que possa expor falhas ainda por corrigir. A empresa sublinha que uma prova vale o que vale a especificação: se o modelo da máquina estiver errado, código verificado pode falhar na mesma. Investigadores independentes ainda não tiveram tempo para auditar o material, pelo que os números continuam a ser, por agora, a versão da própria empresa.