A Anthropic divulgou na quinta-feira, 22 de outubro de 2026, um estudo realizado com a empresa Theorem no qual o modelo Claude produziu provas matemáticas de propriedades de segurança de programas de código aberto. Segundo a pesquisa, o sistema conseguiu demonstrar, sob condições técnicas delimitadas, a ausência de determinadas falhas capazes de provocar travamentos em 239 pontos de entrada de testes, distribuídos por 123 bibliotecas.
O trabalho é um avanço na automação da chamada verificação formal, mas não significa que as 123 bibliotecas estejam inteiramente livres de bugs ou seguras em qualquer computador. As provas se referem a versões compiladas e a cenários específicos, detalhados pelos próprios pesquisadores.
O que a Anthropic afirma ter demonstrado
De acordo com o relatório técnico publicado pela Anthropic, a equipe partiu de testes existentes no OSS-Fuzz, iniciativa de testes contínuos de projetos de código aberto. Esses testes normalmente tentam provocar falhas com muitas entradas diferentes; no experimento, foram transformados em especificações matemáticas.
O Claude escreveu demonstrações na linguagem do assistente de provas Rocq. Um verificador independente do modelo de IA, o núcleo do Rocq, conferiu se cada demonstração satisfazia a especificação proposta. Isso reduz a necessidade de confiar apenas na resposta textual do chatbot.
A Anthropic informa que, ao longo de algumas semanas, o projeto alcançou:
- 123 bibliotecas de software de código aberto com propriedades verificadas em parte de seus testes;
- 239 pontos de entrada de testes com provas de ausência de travamento dentro das condições modeladas;
- Cerca de 180 milhões de linhas de demonstrações escritas em Rocq;
- Identificação e correção, durante as tentativas de prova, de centenas de bugs, conforme relato da própria empresa.
Esses números são resultados declarados pelos autores do estudo. A publicação informa que um subconjunto das provas e dos componentes de verificação está sendo disponibilizado para inspeção e reutilização; isso não equivale a uma auditoria independente de todo o conjunto.
O que significa verificar um programa formalmente
Um teste tradicional executa um programa com muitas entradas e observa se ocorre algum erro. Por mais extenso que seja, esse processo não percorre necessariamente todas as possibilidades.
Na verificação formal, pesquisadores definem uma propriedade — por exemplo, que uma determinada rotina não deve travar com entradas de certo tamanho — e constroem uma demonstração matemática de que ela vale para todos os casos abrangidos pelo modelo.
A IA, nesse experimento, atuou como autora das provas e também propôs correções para falhas encontradas. O resultado foi conferido pelo Rocq, e não aceito apenas porque o Claude declarou ter resolvido o problema.
Limites importantes: RISC-V, Linux e entradas abaixo de 64 MB
As provas centrais foram realizadas sobre programas compilados para a arquitetura RISC-V, com pressupostos de execução em Linux, como binários estáticos, de uma única thread e com orçamento de memória fixo. O objetivo era demonstrar que determinados pontos de entrada não travariam com entradas menores que 64 MB, considerando as respostas do sistema operacional previstas no modelo.
Essas condições importam porque boa parte dos computadores e servidores utiliza arquiteturas x86 ou ARM, além de configurações de sistema diferentes das examinadas. Também não foram verificados todos os caminhos de execução de todas as bibliotecas, nem todos os tipos possíveis de vulnerabilidade.
A própria Anthropic ressalta que "formalmente verificado" não quer dizer "livre de bugs". Uma prova pode estar correta em relação à especificação e ainda deixar de fora comportamentos reais não modelados.
Falhas descobertas durante as provas
Segundo os pesquisadores, a tentativa de demonstrar ausência de travamentos revelou problemas que testes convencionais não haviam identificado. Um exemplo descrito envolve uma falha de escrita fora dos limites de memória em um descompressor, acionada apenas por uma combinação rara de dados de aproximadamente 20 MB.
A equipe também relata a redescoberta de uma vulnerabilidade já identificada no libexpat e problemas lógicos que não necessariamente causam travamentos. O estudo não afirma que todos os projetos analisados já distribuíram atualizações aos usuários para cada falha encontrada.
Por que a pesquisa importa para o futuro da programação
Se a geração automática de provas puder ser reproduzida com custo menor e aplicada a mais arquiteturas, desenvolvedores poderão complementar testes e revisões humanas com garantias matemáticas para partes específicas do software.
Ainda existem obstáculos: o próprio relatório menciona alto consumo de tokens para produzir as provas, dependência da precisão das especificações e necessidade de expandir os modelos para sistemas reais mais variados. A Theorem afirma que pretende oferecer a abordagem a outros projetos de código aberto.
A notícia, portanto, é sobre uma técnica promissora de segurança assistida por IA, e não sobre a eliminação definitiva de vulnerabilidades em programas.
Fontes e metodologia: pesquisa original da Anthropic, publicada em 22/10/2026. As métricas e descobertas descritas são atribuídas aos autores. Imagem de capa: placa RISC-V fotografada por Popolon, Wikimedia Commons, licença CC BY-SA 4.0; imagem ilustrativa de arquitetura, sem vínculo com os equipamentos do estudo.
Fontes
Anthropic Research (estudo primário, 22/10/2026) ↗
https://www.anthropic.com/research/formal-verification | https://commons.wikimedia.org/wiki/File:RISC-V_Bluetrum_AB32VG1_UG7200_2118_devboard.jpg