Anthropic e Theorem Labs usam Claude para verificar segurança de software

LLMs are making formal software verification feasible at a much larger scale

Claude provou, no nível de assembly (RISC-V), propriedades de segurança em 123 bibliotecas open-source do OSS-Fuzz: 239 pontos de entrada provados sem crashes, erros de memória ou assertions falhas para qualquer entrada abaixo de 64 MB, em cerca de 180 milhões de linhas de Rocq (prova típica de ~600 mil linhas). Ao escrever as provas, Claude corrigiu os bugs que encontrou e revelou centenas de bugs. O texto ressalva que as garantias valem sob premissas (programa single-thread, binário estático, memória fixa, RISC-V com musl e Linux) e que 'formalmente verificado' não significa 'sem bugs': especificação, modelos de RISC-V e Linux, checker Rocq e hardware continuam na base confiável. Também cita zlib do kernel Linux provado no nível binário a partir de spec derivada da RFC 1950, e um interpretador de Python em Rust (Verus) com 99,95% de igualdade com CPython em 1,7 milhão de programas aleatórios. A Anthropic publica um subconjunto das provas e a semântica RISC-V/SO; a Theorem oferece o mesmo pipeline para outros projetos e publica uma skill do Claude para desenvolvedores. O artigo alerta para reward hacking (o modelo poderia reescrever o programa para tornar o teorema trivial), que o time penalizou e auditou.