Claude prova código seguro: 180M linhas em semanas

Verificação formal sempre foi o sonho caro de quem opera software crítico

Verificação formal com Claude acaba de sair do laboratório e virar operação em escala industrial. A Anthropic, junto com a parceira Theorem, colocou o modelo para provar matematicamente que código open source existente está correto, e o volume assusta: cerca de 180 milhões de linhas de código de prova geradas em poucas semanas para 123 bibliotecas. Para quem vive de pipeline quebrado, rollback de madrugada e CVE que aparece na sexta à noite, a promessa é tentadora. E se o modelo que escreve o código também provar que ele não vai falhar nas condições que importam.

Eu testo essa ideia com um pé atrás. Já vi muita demo de AI coding que gera código rápido e deixa um rastro de bugs sutis para o time limpar depois. Aqui a proposta é diferente. Não é só gerar mais código, é gerar a prova junto. Mas prova do quê, em que máquina, com que limite de entrada e a que custo de tokens. É isso que precisamos destrinchar antes de comemorar o fim dos bugs.

O fato: Claude provou 123 bibliotecas e achou centenas de bugs

O projeto foi conduzido pelo Frontier Red Team da Anthropic com a Theorem. Em vez de pedir para o Claude escrever software do zero, o time mandou ele verificar software que já existe, usando como base testes do projeto OSS-Fuzz do Google, que reúne testes de crash para bibliotecas open source muito usadas. O Claude traduziu esses testes em problemas matemáticos, analisou o código de máquina compilado e produziu provas extensas de correção.

A checagem dessas provas não depende de acreditar no modelo. Um programa verificador independente chamado Rocq confere automaticamente cada prova. Segundo a Anthropic, o processo exige quase nenhuma revisão humana. Eles chamam de geração de prova 'totalmente autônoma', embora as ferramentas e as fundações formais tenham sido construídas por humanos na Theorem. É um detalhe importante, porque autonomia aqui significa autonomia na escrita da prova, não no desenho do sistema.

No caminho, o Claude esbarrou em centenas de bugs e recebeu permissão para corrigi-los. Muitos desses bugs tinham passado por anos de testes convencionais porque só aparecem em condições muito específicas, como arquivos de entrada anormalmente grandes ou uma sequência particular de acessos. Em um leitor de PDF muito usado, o time encontrou em uma semana tantos bugs de segurança quanto costumam ser reportados em um ano inteiro. Em outro caso, o modelo pegou um erro lógico que estava escondido há mais de uma década. Mesmo quando a prova completa falha, a tentativa ainda expõe falhas reais.

Como funciona na visão de quem opera

Pensa no fluxo como um pipeline de três estágios. Primeiro, você tem um alvo compilado e um conjunto de testes de crash. O Claude usa esses testes para definir o que significa estar correto naquele escopo, algo como não travar, não corromper memória e não desviar do comportamento esperado para entradas dentro de um limite. Depois, ele olha para o código de máquina, não só para o fonte em C ou C++, e tenta construir uma prova formal passo a passo de que aquelas propriedades valem.

Essa prova é escrita em uma linguagem que o Rocq entende. O Rocq funciona como um auditor frio e literal, ele não avalia intenção, só verifica se cada passo lógico fecha. Se fechar, você tem uma garantia matemática condicionada. Se não fechar, você tem pelo menos um contraexemplo ou um ponto de travamento que geralmente indica bug. Na prática, é fuzzing turbinado com matemática, porque o esforço de provar força o modelo a explorar caminhos que teste aleatório dificilmente cobre.

O custo, a latência e a arquitetura que ninguém pode ignorar

Aqui vem a parte que separa demo de produção. Provar software assim sempre foi caro. Para ter uma ordem de grandeza, a verificação formal do microkernel seL4, que é um programa pequeno, tomou cerca de 20 pessoas-ano de especialistas. O que a Anthropic fez foi trocar hora de PhD por tokens. Só que a conta continua pesada. Provas individuais chegaram a consumir centenas de milhões de tokens. A empresa não divulgou o custo total do projeto, e dá para imaginar o porquê.

O sinal positivo é a curva de eficiência. Um teste menor mostrou que as provas são reutilizáveis e que modelos novos gastam menos para o mesmo resultado. O Opus 5.5 resolve metade das provas com cerca de 40 por cento menos tokens que o Opus 5. Isso sugere que estamos vendo o início de uma curva, não o ponto final. Ainda assim, hoje você não vai rodar isso a cada commit como roda um pytest. Latência alta, custo alto e necessidade de ambiente controlado colocam essa técnica mais perto de um release gate para componentes críticos do que de um teste unitário do dia a dia.

O que isso muda na prática para quem constrói

Quem ganha primeiro são times que mantêm bibliotecas críticas e empresas que pagam caro por incidente de segurança. Se você mantém parser de PDF, imagem, vídeo, fonte, compressão ou protocolo de rede, esse tipo de verificação ataca exatamente onde dói, corrupção de memória e crashes exploráveis. Quem perde, pelo menos no curto prazo, é o fluxo que depende só de cobertura de teste como sinal de qualidade. Cobertura alta não significa ausência de bug raro, e esse projeto deixou isso bem claro.

Para times de produto que usam muito código gerado por IA, a mudança é de mentalidade. A pergunta deixa de ser apenas se a IA programa bem e passa a ser se a IA consegue provar que o que ela escreveu é seguro dentro de limites definidos. Isso reduz tempo de revisão manual e aumenta a confiança para automatizar mais, desde que você aceite operar dentro da cerca da prova. E a cerca atual é estreita, arquitetura de processador específica, programas single-thread e entradas abaixo de 64 MB. Na vida real, essas bibliotecas rodam em hardware variado e em configurações diferentes.

Se você quer agir agora sem se afogar em teoria, comece pequeno e mensurável. Minha recomendação prática é esta, escolha uma biblioteca crítica e isolável do seu sistema e rode o seguinte roteiro:

• Liste seus parsers e dependências C e C++ que tocam input externo e ordene por risco de segurança
• Congele uma versão, defina limites claros de entrada e arquitetura alvo, e rode fuzzing pesado antes de qualquer prova
• Separe provas reutilizáveis para funções puras e estáveis, porque são elas que vão pagar o custo de tokens no longo prazo

Esse recorte evita tentar provar o monolito inteiro. Você prova o que pode te derrubar, mantém o resto no teste tradicional e cria um artefato que pode ser revalidado a cada atualização com custo menor.

A tensão real: isso escala ou só move o gargalo

Minha dúvida central é simples, isso escala como teste ou vai continuar sendo um projeto especial para poucos. A Anthropic diz que espera que verificação formal com IA fique tão prática quanto teste padrão, e a Theorem já mira infraestrutura crítica como glibc, OpenSSL e cURL. Faz sentido como roadmap, porque são alvos com alto retorno sobre cada bug encontrado. Mas escalar para milhares de repositórios com código multithread, concorrência real e comportamento dependente de hardware é outra história.

Formalmente verificado também não quer dizer livre de erros. Quer dizer correto sob premissas. Se sua premissa ignora threads, ignora outra CPU ou ignora entrada maior que 64 MB, o bug pode continuar vivo fora da prova. Isso não invalida a técnica, só muda onde está o risco. O gargalo sai da escrita da prova, que o Claude acelerou brutalmente, e vai para a definição do modelo de ameaça, para a manutenção das premissas e para o custo de revalidar tudo quando o ambiente muda. Resolver prova sem resolver operação é trocar um problema difícil por outro.

Tem ainda o ponto econômico. Centenas de milhões de tokens por prova podem valer a pena para evitar um CVE crítico em OpenSSL, mas não fazem sentido para um CRUD interno. O jogo aqui é seletividade. Usar IA para provar tudo é queimar orçamento. Usar IA para provar o núcleo que processa bytes não confiáveis pode ser o melhor custo benefício em segurança que vimos em anos. A eficiência do Opus 5.5 ajuda, mas ainda estamos longe do custo de um CI comum.

Conclusão

O Claude provar 123 bibliotecas com 180 milhões de linhas de prova mostra que verificação formal automatizada deixou de ser curiosidade acadêmica. O uso inteligente agora é provar pouco, provar o crítico e reaproveitar provas. Será que seu time sabe exatamente qual biblioteca, se quebrar, derruba tudo.