Claude prova a segurança de 123 bibliotecas abertas e acha centenas de bugs

A Anthropic publicou nesta quinta-feira (22) uma pesquisa em que o Claude escreveu provas matemáticas de segurança para mais de 100 bibliotecas de código aberto usadas no mundo real. Segundo o texto da própria Anthropic, assinado pelo time de Frontier Red Team em parceria com a empresa Theorem, foram 239 pontos de entrada em 123 bibliotecas do projeto OSS-Fuzz, do Google, provados livres de travamentos para qualquer entrada de até 64 MB. Durante o trabalho, o modelo também encontrou centenas de bugs que tinham sobrevivido a anos de testes.

O que é verificação formal e por que quase ninguém usa

Verificação formal é a técnica de provar, com matemática, que um programa obedece a regras definidas. Em vez de testar milhares de casos e torcer para não faltar nenhum, a prova garante que a regra vale para todos os casos possíveis. O problema sempre foi o custo. A Anthropic lembra que o kernel seL4 levou cerca de dois anos-pessoa para ser implementado e cerca de 20 para ser verificado. Por isso a técnica ficou restrita a sistemas críticos, como o software de aviões da Airbus.

A tese do artigo é que modelos de linguagem estão baixando esse custo o suficiente para a técnica importar em segurança. O contexto é de alerta: a própria Anthropic cita que mais de mil vulnerabilidades do kernel do Linux foram divulgadas recentemente, mesmo em um software muito testado.

Como a Anthropic fez

O método tem quatro passos. Primeiro, testes de fuzzing já existentes no OSS-Fuzz viraram especificações: a regra passou a ser que o teste nunca trava, seja qual for a entrada abaixo de 64 MB. Segundo, cada biblioteca foi compilada para RISC-V e modelada com a semântica do Linux e do processador desenvolvida pela Theorem, de modo que a prova vale para o binário e não apenas para o código-fonte. Terceiro, o Claude escreveu as provas na linguagem Rocq, e o verificador de provas Rocq conferiu cada uma contra a especificação. Quarto, quando o modelo esbarrava em um travamento real, ele corrigia o código, regerava a especificação e seguia provando.

Esse último passo traz um risco que os autores admitem: o modelo poderia reescrever o código só para escapar do erro, o chamado reward hacking. Para reduzir isso, a equipe penalizou correções, deu pontos extras por documentar quais entradas cada correção altera e auditou os patches.

Os números do estudo

O esforço principal levou algumas semanas. As provas somam cerca de 180 milhões de linhas de Rocq, com provas típicas de 600 mil linhas para binários de mediana de 18 mil instruções. Algumas provas exigiram centenas de milhões de tokens. Em 36 tarefas pequenas de verificação, o Opus 5.5 resolveu metade usando cerca de 40% menos tokens que o Opus 5. Quando os agentes compartilharam provas prontas, gastaram 17% menos tokens que agentes isolados, e alguns tiveram sucesso onde a tentativa solo havia falhado.

Em outro experimento, um interpretador de Python escrito em Rust, verificado contra a semântica do CPython, bateu com o original em 99,95% de 1,7 milhão de programas aleatórios. O Claude também escreveu uma especificação formal da RFC 1950 e provou que a implementação de zlib do kernel do Linux a cumpre no nível do binário, repetindo o feito para cerca de outras seis bibliotecas. Em um leitor de PDF, uma tentativa de verificação revelou em uma semana tantos bugs de segurança quanto costumam ser reportados em um ano.

Que tipo de bug apareceu

Entre os exemplos, há um contador que estoura para baixo em um descompressor, ativado só por entradas de cerca de 20 MB com um layout raro, o que leva a uma escrita fora dos limites. Há uma leitura fora dos limites em um decodificador de imagens que exige uma entrada de 64 MB e mais de 2 GB de memória, e outra que só ocorre com uma sequência específica de chamadas em dois acessos ao mesmo arquivo. O Claude também redescobriu a CVE-2026-56132 na biblioteca libexpat e achou um erro de lógica em que um recurso de restrição de arquivos nem sempre era aplicado, sem nenhum travamento envolvido. Um dos bugs estava latente havia mais de uma década em um aplicativo muito usado. Fuzzers dificilmente acham esse tipo de falha porque costumam mutar entradas limitadas a cerca de 1 MB.

As limitações que a própria Anthropic aponta

O texto insiste que verificado formalmente não significa sem bugs. O verificador de provas não consegue confirmar que a especificação reflete a realidade, e a confiança recai sobre o verificador Rocq, os modelos formais de RISC-V e do sistema operacional, o compilador OCaml e o hardware. As provas cobrem binários RISC-V estáticos, de uma só thread, ligados à biblioteca musl, enquanto a maior parte dos servidores reais usa x86 ou ARM com glibc dinâmica. Elas também cobrem apenas erros de memória detectáveis pelo AddressSanitizer, só alguns pontos de entrada por biblioteca, e não tratam de corrupção causada por quem chama a biblioteca de forma errada. O custo em tokens segue alto, embora os autores esperem queda.

A Anthropic vai publicar um subconjunto das provas, a semântica de RISC-V e do sistema operacional e as especificações dos testes que não conseguiu provar. Reteve as provas que poderiam expor bugs ainda sem correção. A Theorem se ofereceu para rodar o processo em outros projetos de código aberto e publicou uma skill do Claude para quem quiser começar.

Por que isso importa para você

Mesmo que você nunca vá escrever uma prova em Rocq, o resultado afeta o que roda no seu computador e nos servidores que você usa. Bibliotecas como zlib, expat e decodificadores de imagem estão dentro de navegadores, aplicativos, plugins e ferramentas de automação. Se a IA ajuda a limpar essas peças básicas, a base sobre a qual você monta seu negócio com IA fica mais sólida. Para escolher ferramentas com critério, veja o checklist para escolher ferramenta de IA com segurança.

Há também uma lição de método. O estudo mostra que a IA rende mais quando recebe um verificador objetivo, no caso o checador de provas, que diz se o trabalho está certo ou errado. Quem usa agentes de código no dia a dia ganha o mesmo efeito ao exigir testes automáticos antes de aceitar uma mudança, tema que tocamos em IA vai substituir programadores? O que muda até 2030. A conta fica clara: o modelo propõe, uma checagem independente decide.

Para quem pensa em carreira, a demanda por gente que entende de segurança e de IA tende a crescer, como detalha o guia de carreira em cibersegurança com IA. E, como a IA também ajuda atacantes, a corrida entre quem acha e quem corrige falhas só acelera. Já cobrimos o caso em que a IA da Anthropic achou uma falha crítica e hackers a exploraram em 24 horas e o estudo em que as correções de segurança falham dez vezes mais em 2026. Para saber o que você entrega às ferramentas, leia também IA e privacidade.

O que observar daqui para frente

O ponto central é se outros grupos conseguem reproduzir o resultado e se o custo por prova cai a ponto de caber em projetos pequenos. Também vale acompanhar quais provas e especificações a Anthropic de fato liberará, e se mantenedores de bibliotecas adotarão a verificação como parte da rotina de lançamento. Enquanto isso, a recomendação prática continua a mesma: mantenha tudo atualizado e trate provas e testes como complemento, nunca como garantia absoluta.