LLMs ampliam a escala da verificação formal de software
Aprofundamento CEVIU
Aprofundamento
A Anthropic, em parceria com a Theorem, usou o Claude para provar propriedades de segurança no nível do código assembly (RISC-V) em 123 bibliotecas open-source do OSS-Fuzz. Foram 239 pontos de entrada provados, com cerca de 180 milhões de linhas de Rocq. Uma prova típica tem uns 600.000 linhas e cobre binários com mediana de 18.000 instruções RISC-V. A garantia: o programa sai normalmente, sem erro de memória nem falha de assertiva, para qualquer entrada abaixo de 64 MB.
O truque está na especificação. Em vez de escrever specs do zero, a equipe transformou testes de fuzzing já existentes em uma regra formal: "este teste sempre passa". Se o Claude prova isso, o fuzzing daquele ponto de entrada não acharia mais bugs. As provas valem sob premissas: binário estático, single-thread, orçamento fixo de memória, RISC-V com Linux. O que o desenvolvedor precisa confiar se reduz aos modelos formais de RISC-V e de processos Linux, aos enunciados dos teoremas e ao verificador Rocq. No caminho, o Claude corrigiu bugs que apareceram, alguns que um fuzzer dificilmente acharia, como um underflow de contador em um descompressor que só disparava com entradas de cerca de 20 MB.
O que mudou
A cobertura anterior do CEVIU já apontava a tendência. Em 15 de junho de 2026, o CEVIU noticiou que a Jane Street reverteu uma postura de 25 anos contra métodos formais, com fluxos agentic mudando a conta de custo e benefício. Em 1 de julho de 2026 e 11 de julho de 2026, as matérias "A evolução e a nova acessibilidade da verificação formal no desenvolvimento de software" e "Verificação Formal e o Papel da IA: Avanços e Desafios para a Segurança do Software" tratavam do custo de escrever provas caindo com IA. A novidade agora é a demonstração em escala: mais de 100 bibliotecas reais, com provas publicadas para verificação independente.
Por que isso importa
Para quem opera código crítico ou mantém bibliotecas em C e C++, a leitura é que fuzzing contínuo pode ganhar um degrau acima: provar a ausência de crashes em vez de só procurar por eles. Ainda é um escopo restrito pelas premissas, mas o custo de provas deixou de ser o argumento padrão para ignorar verificação formal.
Linha do tempo
Jane Street reverte postura contra métodos formais, e o CEVIU cobre a ascensão dos métodos formais com agentes.
CEVIU noticia a nova acessibilidade da verificação formal com ferramentas de IA.
CEVIU noticia avanços e desafios da IA na verificação formal.
Anthropic e Theorem mostram provas formais em escala sobre mais de 100 bibliotecas open-source.
Perguntas frequentes
O que a Anthropic provou exatamente?
O Claude provou que programas compilados para RISC-V saem normalmente, sem erros de segurança de memória nem falhas de assertiva, para toda entrada abaixo de 64 MB. Isso vale para 239 pontos de entrada em 123 bibliotecas do OSS-Fuzz. As provas assumem binário estático, single-thread e memória fixa em Linux.
Isso significa que essas bibliotecas não têm mais bugs?
Não. Bugs restantes podem estar nos componentes confiáveis (modelos de RISC-V e Linux, verificador Rocq) ou fora do escopo da prova. Ainda assim, endurecer esses componentes é mais viável do que depurar todo o código coberto.
Como os testes de fuzzing viraram especificações?
A equipe converteu cada teste de fuzz na regra de que ele nunca quebra para entradas até 64 MB, definida sobre as instruções RISC-V compiladas. Se a prova fecha, o fuzzing daquele ponto não encontraria mais nada. Muitos fuzz tests já checam propriedades como encode-decode, então provar que não quebram equivale a provar a propriedade.
Dá para verificar ou reaproveitar as provas?
Sim. A Anthropic publicou um subconjunto das provas, com as semânticas de RISC-V e do SO. A Theorem também oferece rodar o mesmo pipeline em outros projetos open-source e publica uma skill do Claude para quem quiser começar.
Fontes
- anthropic.comfonte original
- Categoria
- CEVIU
- Publicado
- 23 de outubro de 2026
- Editoria
- CEVIU