Claude escreveu a prova. A especificação ainda é sua.

O binário é RISC-V estático, compilado com clang, musl libc e lld. O fuzz target existe desde antes da prova — o que Claude fez foi transformar o teste em um enunciado matemático: para todo input abaixo de 64 MiB, o programa termina sem erro de memória e sem falha de asserção. A prova foi escrita em Rocq, checada pelo kernel do assistente, e cobre 239 pontos de entrada em 123 bibliotecas do OSS-Fuzz. São cerca de 180 milhões de linhas de prova. Uma prova típica passa de 600 mil linhas para um binário mediano de 18 mil instruções.

A Anthropic publicou o resultado em 22 de outubro de 2026, em colaboração com a Theorem. O pipeline parte do fuzz target que o projeto já tinha. Esse target vira especificação formal sob o modelo de processo Linux e de CPU RISC-V da Theorem. Claude escreve a prova; o Rocq confere se ela bate com o enunciado. No caminho, o modelo encontrou e corrigiu bugs — incluindo a redescoberta de uma CVE em libexpat e falhas que anos de fuzzing não pegaram, como um underflow de contador acionado por um input de aproximadamente 20 MB com um arranjo raro de dados e um decoder de imagem que precisava de 64 MB de entrada e mais de 2 GB de memória para expor a falha.

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 ou 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". A incerteza remanescente se concentra nos componentes em que se precisa confiar: as semânticas de RISC-V e de processo Linux, os enunciados dos teoremas e o próprio kernel do Rocq.

O que significa "virar especificação formal"

O repositório público da Theorem deixa o mecanismo visível. Cada prova é sobre um binário compilado, não sobre código-fonte. O enunciado afirma que, em todo input dentro dos limites, a build com sanitizer se comporta como a build sem sanitizer e que o sanitizer nunca detecta erro. A checagem é feita com Rocq 9.2.0, e os enunciados são escritos em LPS, um modelo formal de processo Linux executando um binário RISC-V — um modelo declaradamente best effort e incompleto, que descreve parte do Linux e faz suposições que não verifica. A prova é tão boa quanto o LPS.

Um exemplo concreto ajuda a materializar o que "virar especificação formal" significa. No repositório oss-verify-proofs, a biblioteca boost-beast tem o entry point http_request provado para as builds ASan, UBSan e ASan+UBSan. O fuzz target original recebe bytes e chama o parser HTTP. A especificação formal não descreve o parser em português: ela enuncia, no vocabulário do LPS, que para qualquer sequência de bytes abaixo do limite, a execução daquele binário específico a partir do entry point do ELF não alcança o estado de erro que o sanitizer detectaria. O "erro" deixa de ser um crash observado e passa a ser um estado formal no modelo. O que se prova é a ausência desse estado, não a ausência de qualquer comportamento indesejado que a especificação não nomeou.

O custo oculto e o novo papel da engenharia

Há um custo operacional que a conversa sobre "prova gerada por IA" costuma deixar de fora. O kernel do Rocq não aceita a prova porque Claude disse que está certa. Ele verifica passo a passo, segundo regras lógicas, e uma única prova leva de 30 minutos a várias horas de tempo de CPU. O tempo de geração é uma coisa; o tempo de checagem é outra, e é ele que transforma 180 milhões de linhas em um artefato auditável. A escala do resultado — 239 entry points em poucas semanas — não elimina esse custo. Ela o desloca para a infraestrutura de checagem e para a fila de provas que precisam ser revalidadas quando o código ou o modelo semântico mudam.

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 sistema operacional, 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. Um selo de "verificado" sobre um contrato incompleto não é uma garantia a mais. É uma garantia com letras miúdas que ninguém leu.

Aprofunde-se no tema de forma estruturada — do contexto à governança de agentes — consultando a série Engenharia de Software Assistida por IA, disponível na Amazon e no Kindle Unlimited.

https://livro-engenharia-de-software-assistida-por-ia.aspepper.workers.dev/?utm_source=hashnode&utm_medium=article&utm_campaign=serie_ia

• Cupom de 30% OFF: LEIA30

Fontes de pesquisa consultadas:

• Anthropic + Theorem — LLMs are making formal software verification feasible at a much larger scale (22 out. 2026)
• Theorem — repositório theorem-labs/oss-verify-proofs, enunciados e provas Rocq sobre binários RISC-V do OSS-Fuzz
• Interesting Engineering — Claude finds bugs that survived trillions of software test runs (22 out. 2026)
• Blockchain.News — Anthropic says Claude proved security properties in 123 open-source libraries (22 out. 2026)
• 36Kr — Claude Generates 180 Million Lines of Formal Proof (23 out. 2026), com dados sobre tempo de checagem por prova
• DevOps.com — Claude Writes 180 Million Lines of Proofs to Verify 123 Open Source Libraries (23 out. 2026)
• Mallory — Anthropic Uses Claude to Prove Bounded Crash Safety Across 123 Open-Source Libraries (23 out. 2026)
• ExplainX — Claude Formal Verification: 123 Libraries Proven Crash-Free (22 out. 2026), com detalhes sobre o tamanho típico das provas
• WebProNews — Why Claude's No-Crash Proofs for 239 Open-Source Fuzz Targets Come With Fine Print (23 out. 2026)
• Documentação de semântica do LPS em theorem-labs/oss-verify-proofs/docs/semantics.md

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