A Anthropic diz que Claude comprovou propriedades de segurança em bibliotecas open-source 123

A Anthropic afirmou que seus modelos Claude foram capazes de produzir provas formais para propriedades de segurança em código compilado em 123 bibliotecas de código aberto, resultado que a empresa descreveu como um passo para tornar a verificação formal de software prática em escala muito maior. No post de pesquisa publicado em 22 de outubro de 2026, a Anthropic afirmou que o trabalho também revelou bugs que passaram despercebidos por anos.

Evidências e contexto

Segundo a Anthropic, Claude provou que 239 pontos de entrada nessas bibliotecas 123 não travariam em nenhuma entrada abaixo de 64 MB sob as condições modeladas do projeto. A empresa afirmou que as provas foram aplicadas no nível de código assembly em binários RISC-V e usaram a semântica formal da Theorem para o comportamento dos processos RISC-V e Linux. A Anthropic afirmou que o esforço abrangeu software open-source do mundo real, incluindo bibliotecas da iniciativa OSS-Fuzz do Google, e que representa, até onde sabe, o primeiro uso em larga escala de IA para aplicar verificação formal a softwares de produção no nível de código assembly.

A empresa afirmou que as provas foram geradas ao longo de várias semanas e que o Claude também corrigiu bugs encontrados durante o processo. Entre os exemplos listados estavam uma escrita fora de limites acionada por um raro layout de entrada de 20 MB, uma leitura fora de limites em um decodificador de imagem que exigia 64 MB de entrada e mais de 2 GB de memória, um travamento vinculado a uma sequência de chamadas específica entre dois handles de arquivo, e uma redescoberta de CVE-2026-56132 no libexpat. A Anthropic também afirmou que o esforço revelou bugs de lógica que não travaram o software, incluindo um caso em que uma restrição de acesso a arquivos nem sempre foi aplicada.

A empresa afirmou que as provas são condicionais e não implicam que o software seja livre de bugs. Sua própria seção de limitações afirma que as garantias dependem de pressupostos modelados, incluindo binários estáticos single-threaded com orçamento de memória fixo rodando no Linux RISC-V, e que o trabalho não cobre todos os pontos de entrada ou todas as formas como o software pode ser usado em produção. A Anthropic disse que a incerteza restante está concentrada nos componentes confiáveis: a semântica RISC-V e Linux, as declarações do teorema e o verificador de provas Rocq.

Por que isso importa

A Anthropic enquadrou o trabalho como evidência de que LLMs podem reduzir o custo da verificação formal, que historicamente exigiu esforço altamente especializado e geralmente se limitou a sistemas críticos para a missão. A postagem diz que modelos maiores precisavam de menos tokens para algumas tarefas de verificação, enquanto componentes compartilhados de provas reduziram a duplicação entre projetos relacionados. A empresa também afirmou que planeja publicar um subconjunto das provas e que o Theorem oferecerá o mesmo pipeline para outros projetos open-source (código aberto).

A pesquisa é consistente com trabalhos mais amplos da indústria que mostram que a verificação formal pode complementar os testes, e não substituí-los. Mas, como a própria Anthropic observa, o valor de uma prova ainda depende de a especificação e o modelo de máquina corresponderem à realidade, e muitas suposições de implantação permanecem fora do escopo das alegações verificadas.