Anthropic prova segurança de 123 bibliotecas com IA em RISC-V

Verificação formal sai do laboratório e vai para produção

Antes, provar que código não tem bugs exigia anos de trabalho de especialistas. O sistema operacional seL4, por exemplo, levou dois anos para ser implementado e vinte para ser formalmente verificado. Agora, a Anthropic prova que binários estáticos RISC-V não vão travar nem violar segurança de memória, desde que rodem em Linux com entrada menor que 64 MB, como single-threaded com orçamento de memória fixo. O Claude gerou as provas automaticamente em semanas.

Durante a análise, a IA descobriu bugs que haviam passado por trilhões de testes automatizados ao longo de anos. Os erros não eram críticos em cenários normais, mas mostram como testes convencionais deixam lacunas. A equipe trabalhou em parceria com a Theorem, que agora oferece o mesmo pipeline para outras bibliotecas open-source.

O que falta e o que já está disponível

A Anthropic não afirma que eliminou todos os bugs. As provas valem apenas para as condições testadas: binários estáticos RISC-V em Linux, com entrada limitada a 64 MB e ambiente single-threaded. Modelos multi-threaded, ambientes sem Linux ou entradas maiores não foram cobertos. Mesmo assim, o custo da verificação formal caiu de dezenas de anos-homem para semanas de máquina.

A empresa publicou um subconjunto das provas e as semânticas de RISC-V e do sistema operacional usadas nos testes. A Theorem lançou uma skill do Claude para ajudar desenvolvedores a aplicar o método em seus próprios projetos. A antropic também explorou outros métodos de verificação formal, como analisar a segurança do zlib e provar equivalência comportamental de um interpretador Python escrito em Rust. Em todos os casos, a IA achou bugs antigos que haviam resistido a décadas de uso.

O anúncio marca um ponto de virada: verificação formal não é mais privilégio de especialistas em sistemas críticos. Com IA, a técnica começa a escalar para bibliotecas de uso geral. A Anthropic vê isso como passo rumo a desenvolvimento de software com garantias matemáticas de segurança, ainda que o escopo atual seja limitado.