Verificação formal com IA: pergunte qual propriedade foi provada, não quantas linhas saíram

Uma análise de Fabio Akita discute a pesquisa da Anthropic com a Theorem sobre provas de segurança em 123 bibliotecas abertas e 239 pontos de entrada de testes do OSS-Fuzz.[6] Segundo os números apresentados, o processo produziu aproximadamente 180 milhões de linhas de Rocq, mas a garantia está restrita a propriedades dos binários e testes modelados, com entradas de até 64 MB.[6]

O volume impressiona. Para uma decisão de engenharia, porém, a primeira pergunta deveria ser outra: qual comportamento deixou de ser possível dentro de quais hipóteses?

O que muda para quem desenvolve

O artigo destaca que uma prova relaciona uma propriedade a uma especificação e a um modelo; ela não decide sozinha se a especificação expressa a regra correta do produto.[6] Na pesquisa discutida, testes de fuzz existentes ajudam a fornecer as propriedades a verificar, incluindo relações de ida e volta em codecs.[6]

Minha leitura é que isso desloca parte do esforço: menos atenção ao tamanho da prova, mais atenção ao contrato que ela protege. Uma garantia estreita pode ser extremamente útil se cobre uma fronteira importante. Uma garantia ampla no anúncio e indefinida no contrato serve pouco para aceitar risco.

Em vez de começar tentando provar o produto inteiro, proponho escolher um componente pequeno, com entradas bem definidas e uma propriedade que a equipe consiga revisar. O retorno esperado deve justificar também o custo de manter a prova quando o código mudar.

Como aplicar

Considere uma função que autoriza uma reserva de orçamento. Antes de escolher a ferramenta, escreva a regra: uma reserva aceita não pode ultrapassar o saldo disponível, consideradas as condições explicitamente modeladas.

Monte um experimento em etapas:

1. Defina o domínio de valores, a política para entradas inválidas e a representação do estado.
2. Escreva testes de propriedade que gerem combinações dentro desse domínio.
3. Introduza deliberadamente um defeito em uma cópia isolada e confira se o teste o detecta.
4. Avalie uma prova para a mesma propriedade e compare o que cada abordagem efetivamente cobre.
5. Documente o que permanece fora, como persistência e coordenação entre requisições concorrentes, se esses comportamentos não fizerem parte do modelo.

Esse exercício não promete uma prova pronta. Ele produz uma especificação discutível e um limite de escopo antes de investir na automação.

Cuidados e limites

Os resultados da pesquisa descrita se referem a binários estáticos, de uma thread, para RISC-V e ligados à musl, não automaticamente às compilações x86 ou ARM de produção.[6] O artigo também alerta para auditar patches, pois um agente pode alterar o programa para facilitar a prova.[6]

Por isso, uma avaliação deveria registrar propriedade, versão, ambiente modelado e componentes excluídos. Proponho acrescentar a revisão das alterações e o procedimento para revalidar a garantia após mudanças.

Verificação formal não deveria virar selo decorativo nem substituir controles que estão fora de seu alcance. A utilidade está em tornar uma afirmação específica mais forte, não em transformar “provado sob estas condições” em “não tem bugs”.

Fonte

[6] Fonte: AkitaOnRails