Verificação de Programas na Era da IA: Por Que Alucinações Tornam a Verificação de Código Mais Importante

A IA generativa reviveu um antigo sonho dos programadores: simplesmente formule uma tarefa — e a máquina escreverá o código por si. Um novo estudo acadêmico esfria esse otimismo, sem negar o progresso real: programação representa apenas uma pequena parte da engenharia de software, e suas partes mais difíceis — requisitos, arquitetura e verificação — ainda permanecem com os engenheiros.

Por Que a IA Não Resolve o Problema Principal

Engenharia de software não é apenas escrever código. Pesquisas da indústria mostram: desenvolvedores gastam 20 a 30% de seu tempo de trabalho em programação direta. O resto é dedicado à coleta de requisitos, design de arquitetura, revisão, testes e correção de erros. Assistentes de IA conseguem gerar funções e explicar código desconhecido, mas não conseguem provar a correção do sistema como um todo — essa é uma tarefa fundamentalmente diferente.

O principal problema são alucinações. A IA oferece com confiança código que parece plausível, compila e passa em testes básicos, mas contém erros lógicos sutis. Componentes "quase corretos" empilhados juntos formam um sistema não confiável. Os autores coletaram incidentes documentados com código gerado por IA em produção: de citações legais incorretas em chatbots a erros em algoritmos de recomendação médica. O padrão é o mesmo: o sistema funcionava corretamente na maioria dos casos — até encontrar um caso limite.

Experimento com AutoProof e Eiffel

Os pesquisadores não se limitaram à teoria e conduziram um experimento concreto. Um sistema de gerenciamento de conferências foi criado com a ajuda de um assistente de IA em conjunto com AutoProof — um verificador formal para a linguagem Eiffel. A diferença fundamental em relação aos testes: verificação formal prova correção para todas as entradas possíveis, não apenas para um conjunto de exemplos selecionados.

O processo exigiu disciplina iterativa rigorosa:

• Formular um pequeno fragmento de requisitos como pré e pós-condições formais
• Pedir ao assistente de IA para implementar o código correspondente
• Executar AutoProof e obter um erro de verificação ou confirmação de correção
• Corrigir a especificação ou implementação — e repetir o ciclo

Observação chave: o assistente de IA não verificou o código independentemente. Ajudou a formular especificações e a escrever a implementação, enquanto um verificador formal independente verificava a correção. Essa divisão de papéis é fundamental — e, segundo os autores, é assim que as cadeias de ferramentas da próxima geração serão organizadas.

Federação de Agentes como Novo Paradigma

Os autores propõem uma nova perspectiva sobre desenvolvimento: não um único auxiliar de IA, mas uma federação de agentes que interagem com áreas claras de responsabilidade. Um gera código, um segundo escreve testes, um terceiro executa verificação formal, um quarto analisa incidentes de produção. Nenhum agente sozinho é responsável pela correção — essa é uma propriedade do sistema como um todo.

"Alucinação como um tipo de falha torna as garantias de correção mais,

não menos importantes", argumentam os autores.

Essa abordagem exige que os desenvolvedores entendam engenharia de software clássica: especificações formais, invariantes, contratos. A IA não elimina esse conhecimento — torna sua aplicação prática mais acessível. Um desenvolvedor que consegue formular requisitos com precisão e ler resultados de verificação está em uma posição fundamentalmente vantajosa.

O Que Isso Significa

A conclusão dos autores é cautelosamente otimista. Para desenvolvimento cotidiano, IA é uma tecnologia equalizadora: um desenvolvedor sem experiência se aproxima de um experiente, código rotineiro é escrito mais rapidamente, erros óbvios são encontrados mais cedo. Para sistemas críticos e empresariais, IA se torna uma tecnologia amplificadora: um engenheiro experiente obtém uma ferramenta poderosa, mas as lições clássicas da engenharia de software se aplicam mais do que nunca. Verificação se torna não menos, mas mais importante — precisamente porque a IA pode cometer erros com confiança e invisibilidade.