Quando a IA Escreve o Software, Quem Define o que É Correto?

Leonardo de Moura publicou um ensaio em fevereiro de 2026 com uma tese provocativa: à medida que a IA escreve uma parcela crescente do software mundial, precisamos de verificação formal para garantir que esse software funciona.

A tese é atraente. Também é incompleta. E a parte que falta é exatamente a que importa para quem lidera tecnologia.

O Argumento da Prova Matemática

O raciocínio de De Moura segue uma lógica direta. Testes verificam amostras: você executa o código com inputs selecionados e confere se os outputs estão certos. Provas formais verificam propriedades: você demonstra matematicamente que o código funciona para todos os inputs possíveis, sem exceção.

Num mundo onde a IA gera entre 25% e 30% do código novo (números que Google e Microsoft já reportam), a diferença entre verificar amostras e verificar propriedades deixa de ser acadêmica. A Veracode analisou mais de 100 LLMs em 2025 e encontrou vulnerabilidades de segurança em 45% do código gerado. A CISQ estima que software de baixa qualidade custa US$ 2,41 trilhões por ano nos Estados Unidos.

De Moura propõe um roteiro para resolver isso: começar pela criptografia, avançar para bibliotecas core, depois engines de armazenamento, parsers e compiladores. Um “stack verificado” construído camada por camada.

Existem exemplos reais. O Microsoft SymCrypt usa verificação formal via Lean (a ferramenta criada por De Moura). O Veil, da Universidade Nacional de Singapura, verifica protocolos distribuídos. O AWS Cedar verifica políticas de autorização.

Até aqui, a narrativa é convincente. Mas faltam peças essenciais.

O Que o Argumento Esconde

De Moura não é um observador neutro. Ele criou o Lean, o provador de teoremas no centro de sua proposta. Lidera o Lean Focused Research Organization, financiado para expandir adoção da ferramenta. Quando alguém propõe que sua própria criação é a resposta para um problema da indústria, a leitura precisa ser crítica.

Três omissões merecem atenção.

Primeira: o ensaio não menciona nenhuma ferramenta concorrente. Coq, Isabelle, TLA+, Dafny, F*. Todas existem, todas têm resultados em produção, todas resolvem classes de problemas diferentes. Apresentar verificação formal como sinônimo de Lean é marketing, não análise técnica.

Segunda: a dicotomia testes versus provas é falsa. Entre “executar alguns casos de teste” e “provar matematicamente para todos os inputs” existe um espectro inteiro de técnicas. Análise estática detecta classes de bugs sem executar o código. Fuzzing gera milhares de inputs aleatórios para encontrar falhas. Testes baseados em propriedades verificam invariantes sobre conjuntos amplos de dados. Nenhuma dessas técnicas aparece no argumento de De Moura. A realidade da verificação é um continuum, não uma escolha binária.

Terceira: o próprio compilador Lean, um dos exemplos centrais do ensaio, foi validado por testes, não por prova formal. Isso não invalida a verificação formal como objetivo. Mas revela que, mesmo dentro do projeto que mais teria a ganhar com provas formais, a prática ainda depende de testes.

Há uma ironia adicional. O AWS Cedar, citado como caso de sucesso, usa Dafny para suas provas, não Lean. A ferramenta de verificação preferida pela AWS contradiz a narrativa do próprio funcionário da AWS.

Onde a Verificação Formal Funciona (e Onde Não Funciona)

Os exemplos de sucesso compartilham uma característica: são domínios com especificações claras e comportamento determinístico.

Criptografia tem especificações matemáticas precisas. Compiladores têm semânticas formais definidas. Parsers operam sobre gramáticas exatas. Protocolos de rede seguem RFCs detalhadas.

Agora considere o restante do software que a IA gera. Lógica de negócio depende de regras que mudam conforme o mercado. Interfaces de usuário dependem de percepção humana. Modelos de machine learning otimizam funções objetivo que podem estar erradas. Sistemas distribuídos interagem com ambientes imprevisíveis.

Para esses domínios, o problema não é “como provar que o código está correto”. É anterior: “como definir o que correto significa”.

E é aqui que a discussão sobre verificação formal se transforma em discussão sobre governança.

Especificações Codificam Valores

De Moura inclui uma frase que merece mais atenção do que o restante do ensaio: “Especificações codificam valores.”

Quando uma equipe escreve uma especificação formal para um sistema, está fazendo algo além de documentação técnica. Está declarando, de forma verificável, o que o sistema deve e o que não deve fazer. Está definindo os limites do comportamento aceitável.

Isso é governança.

Como exploramos em A Dívida de Verificação, o problema da verificação de código de IA não é disciplina individual. É infraestrutura organizacional. A verificação formal oferece uma camada adicional nessa infraestrutura, mas só para os casos em que alguém conseguiu primeiro articular o que “correto” significa.

E articular o que “correto” significa para um dispositivo médico, um sistema de votação ou um monitor de segurança de IA são decisões que nenhum provador de teoremas pode tomar. São decisões humanas, políticas, éticas. A ferramenta pode verificar a conformidade com a especificação. Não pode gerar a especificação.

O Problema da Especificação É o Problema

O grupo de pesquisa do Veil, na Universidade Nacional de Singapura, descobriu algo revelador: IA consegue gerar especificações formais. Mas parte dessas especificações são “vacuamente corretas”. Provam que o sistema funciona ao definir “funcionar” de forma trivial. Como provar que uma porta é segura ao especificar que “segura” significa “existir”.

Esse resultado ilumina o risco real. A IA vai escrever o código. A IA pode até escrever as provas. Mas se a IA também escreve as especificações, quem garante que as especificações capturam o que realmente importa?

Como argumentamos em Código Barato, Qualidade Cara, o custo de gerar código caiu para quase zero. O custo de garantir que o código faz a coisa certa permanece alto. Verificação formal não elimina esse custo. Desloca a questão: ao invés de perguntar “o código tem bugs?”, passamos a perguntar “a especificação captura a intenção?”. Pergunta mais precisa, sim. Mais fácil de responder, não.

Da Verificação de Código à Governança de Intenção

A contribuição real da verificação formal para organizações que usam IA não é provar que o código está certo. É forçar a articulação do que “certo” significa.

Organizações que passam pelo exercício de escrever especificações formais (mesmo que nunca executem uma prova) descobrem falhas de comunicação entre equipes, requisitos contraditórios e premissas não documentadas. O ato de especificar funciona como auditoria de intenção.

Para quem lidera tecnologia, três implicações práticas.

Verificação formal não substitui o que já funciona. Testes, análise estática, code review, fuzzing. Cada técnica captura classes de erros diferentes. Prova formal é poderosa para código determinístico com especificações claras: criptografia, compiladores, protocolos. Para lógica de negócio e interfaces, as técnicas existentes continuam sendo o alicerce.

O investimento em especificação vale mais que o investimento em prova. A maioria das organizações não falha porque não consegue provar propriedades do código. Falha porque não consegue articular o que o código deveria fazer. Investir em clareza de requisitos, em contratos formais entre componentes e em documentação verificável de comportamento esperado produz resultado mesmo sem um provador de teoremas.

Quem define “correto” precisa ser uma decisão explícita. Quando a IA gera código e potencialmente gera especificações, a cadeia de verificação precisa ter um ponto de ancoragem humano. Alguém precisa decidir que “o sistema de dosagem médica nunca administra mais que X” é a propriedade certa a verificar. Essa decisão não é técnica. É de governança.

Martin Kleppmann, pesquisador em sistemas distribuídos, argumenta que a IA vai tornar verificação formal algo comum, não por mérito acadêmico, mas por necessidade prática. Se isso se confirmar, a pergunta que separa organizações preparadas das demais não será “vocês usam verificação formal?”. Será “vocês sabem o que estão verificando?”.

A IA vai escrever código cada vez melhor. Vai gerar provas cada vez mais sofisticadas. A única coisa que continua dependendo de decisão humana é definir o que o software deve fazer. E essa definição é, por natureza, um ato de governança.

Verificação formal é uma ferramenta. Poderosa, sim. Limitada, também. O que determina se ela protege ou apenas automatiza conformidade é a qualidade da especificação. E especificações de qualidade começam com perguntas que nenhum algoritmo sabe fazer: para quem esse sistema trabalha? Quais danos ele não pode causar? Quem responde quando a definição de “correto” muda?

Essas perguntas não têm prova formal. Têm deliberação.

Fontes

De Moura, Leonardo. “When AI Writes the World’s Software, Who Verifies It?” Fevereiro 2026.
Veracode. “2025 GenAI Code Security Report.” 2025.
CISQ. “The Cost of Poor Software Quality in the US: A 2022 Report.” 2022.
Kleppmann, Martin. “AI Will Make Formal Verification Go Mainstream.” Dezembro 2025.

Victorino Group ajuda organizações a construir infraestrutura de verificação que acompanha suas ambições com IA: contato@victorino.com.br | www.victorino.com.br