A Anthropic e a Theorem usaram o Claude para gerar provas formais em 123 bibliotecas do OSS-Fuzz.

Claude produziu provas verificáveis para propriedades de segurança em 123 bibliotecas. O avanço é real, mas desloca o gargalo: o software atende estritamente à especificação formal, mas a especificação pode ignorar vetores reais de falha.

A Anthropic publicou, em 22 de outubro de 2026, o resultado de uma colaboração com a Theorem: Claude gerou provas formais de que 239 pontos de entrada de fuzz test, em 123 bibliotecas do OSS-Fuzz, não crasham para qualquer input abaixo de 64 MB. As provas foram escritas em Rocq, checadas pelo kernel do assistente de prova, e operam no binário compilado para RISC-V — não no código-fonte. São cerca de 180 milhões de linhas de prova no total; uma prova típica passa de 600 mil linhas para um binário mediano de 18 mil instruções.

O pipeline parte do fuzz test que o projeto já tinha. Esse teste vira enunciado formal: sob o modelo de processo Linux e de CPU RISC-V da Theorem, o programa termina sem erro de memória e sem falha de asserção, para todo input no limite. Claude escreve a prova; o Rocq confere se ela bate com a especificação. No caminho, o modelo encontrou e corrigiu bugs — incluindo rediscovery de CVE em libexpat e falhas que anos de fuzzing não tinham pegado.

A prova, porém, demonstra exatamente a propriedade que foi formulada. Single-thread. Binário estático. Orçamento de memória fixo. RISC-V e Linux modelados. Input até 64 MB. Fora desse recorte — multi-thread, glibc em x86/ARM, cenários que a especificação não nomeou — a garantia não se estende. A própria Anthropic deixa isso explícito: "formally verified" não é sinônimo de "sem bug em qualquer uso real".

Isso muda a conversa sobre verificação assistida por IA. Passar no teste deixa de ser o teto quando dá para provar ausência de crash num envelope definido. O trabalho caro e humano migra para outro lugar: escrever a especificação certa, escolher o que entra no teorema e o que fica de fora, e decidir se as hipóteses (modelo de SO, arquitetura, limites de input) cobrem o risco que o time de fato aceita. A ferramenta verifica o artefato. Quem define o que precisa ser verdadeiro continua sendo engenharia.

Para quem opera agentes de código e pipelines de segurança, o recorte prático é direto. Quando o time adotar prova formal gerada por modelo, o checklist deixa de ser só "o kernel aceitou?" e passa a incluir: quais propriedades foram enunciadas, sob quais premissas, e o que o negócio ainda precisa tratar fora do envelope formal. Sem isso, a prova vira um selo sobre um contrato incompleto.

Leia o artigo completo clicando na imagem abaixo:

Referências

• Anthropic + Theorem, LLMs are making formal software verification feasible at a much larger scale (22 out 2026) 239 entry points, 123 bibliotecas OSS-Fuzz, ~180M linhas Rocq, RISC-V assembly.
• Theorem oss-verify-proofs (subset público).

Autor da série de livros "Engenharia de Software Assistida por IA" (disponível na Amazon). Aprofunde-se no tema de forma estruturada do contexto à governança de agentes consultando a série clicando na imagem abaixo:

• Cupom de 30% OFF: LEIA30
• Disponível também no Kindle Unlimited

Tags

#EngenhariaDeSoftware #IA #VerificacaoFormal #Claude #Anthropic #Seguranca #OSSFuzz #Rocq #ProvasFormais #SoftwareEngineering #AI #FormalVerification #DevSecOps #Backend #RISC-V #Teorema #Especificacao