Bertrand Meyer na CACM: combinar IA com verificação formal para sair do código “provável” para o “provado”

Resumo: O cientista da computação Bertrand Meyer publicou na Communications of the ACM de junho de 2026 um ensaio que vem agitando o debate sobre IA na programação. Para ele, copilotos como GPT, Claude e Gemini entregam código “provável” — funciona na maioria dos casos, falha nos que importam. A saída seria casar IA generativa com verificação formal, transformando o engenheiro em alguém que escreve especificações, não código. Esta matéria explica a proposta, o método em três passos e o que isso significa para quem usa IA para programar no Brasil.

Por que o “provável” não basta

Hoje qualquer time de desenvolvimento usa IA para escrever código. GitHub Copilot, Claude Code, Cursor, Gemini Code Assist — a lista é longa, e os ganhos de produtividade são reais. O problema começa quando esse código vai para produção em sistemas críticos: bancos, hospitais, infraestrutura, governo. Aí a pergunta deixa de ser “compila?” e passa a ser “tenho certeza de que não vai falhar em nenhuma das infinitas combinações possíveis de entrada?”.

O argumento de Meyer é direto: modelos estatísticos, por construção, entregam respostas prováveis. Eles aprendem padrões em bilhões de linhas de código e devolvem o que parece mais provável dado o contexto. Em 95% dos casos, isso é ótimo. Em 5%, o código compila, passa nos testes e ainda assim contém um bug sutil que vai aparecer no pior momento — o famoso bug de produção. Para software crítico, “provável” não é suficiente; é preciso “provável demonstrável”, ou seja, provado.

Os dois obstáculos da IA na engenharia de software

Meyer destaca dois entraves estruturais. O primeiro é a dificuldade de especificar o objetivo. Prompt engineering, ele observa, nada mais é do que engenharia de requisitos com outro nome — e engenharia de requisitos sempre foi a parte mais difícil da disciplina. Pedir “faça uma função que ordene a lista” parece simples, mas existem dezenas de decisões implícitas: ordenação estável? Em que critério? Tolerância a duplicatas? Performance esperada? Quando o desenvolvedor não explicita tudo isso, o modelo “preenche as lacunas” do jeito mais comum nos dados de treino, que pode não ser o que o sistema precisa.

O segundo obstáculo é a alucinação. Em texto, alucinação é chato. Em código, é catastrófico: o modelo inventa uma função que não existe, chama uma API com assinatura errada, ou — pior — produz uma lógica que parece correta mas viola uma propriedade silenciosa do sistema. Meyer chama isso de hallucination loop: o programador pede um conserto, a IA gera um patch que esconde o bug em outro lugar, e o ciclo continua.

A proposta: do provável ao provável (com prova)

A receita é simples de descrever e difícil de executar: combinar a criatividade da IA com o rigor da verificação formal. Em três passos:

• Especificação formal — o desenvolvedor descreve, em linguagem matemática (pré e pós-condições, invariantes), o que o código precisa garantir. Não como fazer, mas o que precisa ser verdadeiro antes e depois de cada operação.
• Geração assistida por IA — o modelo propõe uma implementação que tenta satisfazer a especificação. Aqui está a “criatividade”: o modelo explora caminhos que um humano talvez não enxergasse.
• Verificação automática — uma ferramenta de prova (SMT solver, model checker) tenta demonstrar matematicamente que o código atende à especificação. Se falhar, devolve um contraexemplo: uma entrada que faria o código quebrar. A IA usa esse contraexemplo para gerar uma nova tentativa. Iterando, chega-se a código que é, por construção, correto em relação ao spec.

O ponto sutil é que o trabalho do engenheiro muda de natureza: ele deixa de escrever código e passa a escrever especificações. Isso é mais difícil do que parece, mas é a única forma conhecida de obter garantias reais.

Por que importa — e o status no Brasil

Para times brasileiros, especialmente em fintechs, healthtechs, sistemas de governo e infraestrutura crítica, a discussão é prática. Bancos brasileiros já estão entre os maiores usuários corporativos de copilotos no mundo, e a regulação prudencial (Bacen, CVM) é cada vez mais exigente quanto a auditabilidade de software automatizado. Combinar IA com métodos formais é uma forma de continuar capturando o ganho de produtividade da IA sem abrir mão de rastreabilidade.

O ecossistema brasileiro tem grupos fortes em verificação formal — UFMG, USP, UFRN, UNICAMP — e ferramentas como o ESBMC, desenvolvido com participação de pesquisadores brasileiros, já são padrão internacional. Há uma janela real para que empresas locais combinem expertise em métodos formais com adoção massiva de IA, posicionando-se como fornecedores de software crítico verificado para mercados regulados.

Riscos e limitações

O caminho não é trivial. Primeiro, escrever especificações formais corretas é tão difícil quanto escrever código correto — e exige conhecimento que poucos times têm. Segundo, verificação formal escala mal: provar propriedades de sistemas grandes pode ser computacionalmente proibitivo. Terceiro, há propriedades importantes (usabilidade, comportamento sob carga, conformidade com leis em evolução) que não cabem em uma especificação formal. Por fim, métodos formais não eliminam o risco humano: se a especificação está errada, o código vai estar provavelmente errado de forma demonstrável — o que é pior do que parece.

Cenário e indicativo de futuro

A leitura mais provável é uma adoção em camadas. Para a maioria do código (CRUD, UIs, scripts internos), copilotos puros vão continuar dominando — o custo de formalizar não compensa. Para módulos críticos (criptografia, parsers de protocolos, motores de regras financeiras, código embarcado em saúde), o pipeline IA + verificação formal vai virar padrão nos próximos cinco anos. Já existem provas de conceito em compiladores, kernels e bibliotecas criptográficas que mostram que isso funciona; falta industrializar.

Conclusão prática

Se você é desenvolvedor brasileiro, vale começar a se familiarizar com pelo menos uma ferramenta de verificação formal (Dafny, Frama-C, Why3, ou Coq/Lean para quem quer ir fundo) e treinar o reflexo de pedir à IA não só o código, mas também o invariante que ele deve satisfazer. Se você é gestor de produto em setores regulados, vale auditar quais módulos do seu sistema justificariam o custo extra dessa abordagem. A ideia central de Meyer é mais importante do que qualquer ferramenta específica: o engenheiro do futuro será avaliado pela qualidade das especificações que escreve, não pela quantidade de linhas de código que produz.

Fonte original: Artificial Intelligence for Software Engineering: From Probable to Provable — Communications of the ACM, junho de 2026.