# 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