Anthropic e Theorem relatam provas escritas por IA para alvos de fuzzing de código aberto

A Anthropic publicou em 22 de outubro uma pesquisa com a Theorem relatando que o Claude produziu provas formais de segurança para 239 pontos de entrada de testes de fuzzing em 123 bibliotecas de código aberto. O trabalho transforma testes existentes em enunciados matemáticos sobre programas compilados e usa um verificador independente para validar os argumentos gerados. Durante o processo, o modelo também encontrou e corrigiu bugs que impediam esses enunciados de se sustentarem.

As garantias se aplicam em um ambiente de execução definido: binários RISC-V estáticos e de uma única thread, vinculados à musl, executados em um modelo de processos Linux com orçamentos fixos de memória. O apêndice técnico especifica entradas menores que 64 MiB, e a documentação do driver da Theorem informa que arquivos desse tamanho ou maiores são recusados. As premissas do teorema também determinam quais respostas do sistema operacional, disposições de memória e condições de recursos são cobertas.

O processo utiliza a estrutura de fuzzing já existente na biblioteca, cujas asserções podem expressar propriedades como compressão e descompressão bem-sucedidas. Ele compara binários comuns com versões que contêm verificações de sanitizadores e raciocina sobre seu comportamento observável. No apêndice, falhas incluem erros de execução, abortos e comportamentos ausentes do modelo de processo. O Claude constrói os argumentos em Rocq, enquanto o núcleo de Rocq verifica se eles estabelecem os enunciados exigidos.

A fronteira de confiança continua concentrada nos modelos formais de máquina e processo, nos enunciados exatos dos teoremas e no próprio verificador, incluindo as ferramentas de apoio e o ambiente necessários para verificar cada binário. A cobertura acompanha o código alcançado pelo ponto de entrada escolhido e as verificações presentes no binário. Propriedades fora dessas verificações e diferenças entre o modelo e o hardware ou os sistemas operacionais implantados continuam relevantes quando um resultado é aplicado a software de produção.

A aplicação de patches trouxe outro desafio: um agente poderia tornar fácil provar a ausência de falhas removendo comportamento significativo do programa. A Anthropic afirma que o experimento penalizava cada patch e concedia crédito adicional pela prova de quais entradas uma mudança afetava e de quão pequeno era esse conjunto. Os pesquisadores também registraram e auditaram os patches para identificar esses atalhos. Após uma alteração, a especificação era gerada novamente e o modelo tentava provar o enunciado sobre o programa revisado.

O material público é um subconjunto dos resultados. No momento da análise, o repositório da Theorem listava 60 pontos de entrada em 25 bibliotecas, com provas verificadas usando Rocq 9.2.0. Ele fixa os binários compilados e registra os enunciados e premissas correspondentes. A versão publicada contém provas de concordância, que comparam comportamentos e excluem erros especificados; essas provas ainda podem permitir uma execução que nunca termina. A terminação exige um teorema separado.

A discussão de especialistas no apêndice da Anthropic descreve provas muito mais verbosas do que um especialista humano normalmente escreveria. Os agentes detalhavam repetidamente conteúdo de registradores, endereços de memória e ramificações de execução, enquanto também desenvolviam algumas abstrações conhecidas. A análise trata a melhoria da estrutura modular como uma questão em aberto para estender a abordagem a programas mais complexos. Ela separa a validade matemática de uma prova da eficiência e da organização para produzi-la.

A Theorem também oferece seu processo OSS Verify gratuitamente a projetos de código aberto qualificados. A elegibilidade é analisada individualmente, considerando manutenção, uso, licenciamento e a posição do projeto em fronteiras de segurança ou sob outros softwares. O programa prioriza infraestrutura amplamente usada e informa os bugs encontrados de forma privada aos mantenedores. A documentação diz que produzir provas pode levar dias e que elas podem ser atualizadas depois de concluídas, vinculando cada resultado a compilações específicas do programa.