Vera verificação formal potencializa IA em engenharia de software

O problema: IA escala a escrita, não a revisão

Agentes de IA já conseguem escrever código a custo marginal quase zero, mas a revisão humana desse código se torna o novo gargalo. O autor argumenta que a IA está hoje aproximadamente no nível de um único desenvolvedor humano: um dev sozinho mantém qualidade, mas não escala; times humanos escalam distribuindo trabalho e usando code review. A IA escala a escrita sem escalar a revisão.

A solução: verificação formal + IA

O paradigma proposto combina duas coisas:

1. Humanos escrevem a especificação formal (em linguagens como Lean), definindo as propriedades que o software deve satisfazer.
2. A IA escreve o código E a prova formal de que ele satisfaz a especificação. A prova é verificável por máquina, eliminando a necessidade de revisão humana da implementação.

O framework geral tem três camadas:

• Restrições rígidas (hard constraints): propriedades formais que o código deve provar que satisfaz.
• Objetivos de otimização: benchmarks que medem performance, uso de recursos, etc.
• Agentes escrevem código e provas: cada mudança vem com prova formal + resultados de benchmark automáticos.

Analogias com machine learning

O autor, ex-engenheiro de ML, traça paralelos: os benchmarks funcionam como training set; overfitting é um risco real; instruções como "generalize em vez de adicionar um caso especial" funcionam como regularização; specification gaming já foi observado na prática (um agente explorou uma fraqueza na spec).

Caso real: powdr autoprecompiles

No projeto powdr (otimização de circuitos para zkVMs), a equipe aplicou o paradigma:

• ~500 linhas de Lean especificam a corretude do otimizador (2 dias para escrever + 1 dia de review).
• Agentes de IA escreveram 100% da implementação e das provas, com orientação mínima.
• A "revisão" de um PR gerado por IA consiste em checar um label no CI e ler um comentário com resultados de benchmark.
• Redução de tamanho de circuitos equivalente à implementação anterior em Rust.
• O caso de teste mais lento ficou 3x mais rápido em três dias.
• Integração via FFI: Lean compila para C, chamado do Rust.

Implicações para engenharia de software

O autor reconstruiu um componente central do produto principal em uma a duas semanas. Para o paradigma funcionar em escala, escrever e auditar a especificação precisa ser substancialmente mais barato que escrever e manter a implementação. Bibliotecas reutilizáveis de especificações (como já existem para código) ajudariam. Via FFI, é possível introduzir código verificado formalmente módulo a módulo, sem reescrever o codebase inteiro.

A visão de longo prazo: desenvolvimento de software pode deixar de ser sobre código e passar a ser sobre requisitos - propriedades críticas especificadas formalmente, o resto validado por testes automatizados. O desenvolvedor talvez nunca veja o código gerado.