Existe uma crença confortável na engenharia de software: a de que o bug mora no código. Que ele aparece quando o programador esquece um caso de borda, troca um sinal ou erra a condição de um loop. É onde a gente procura, é onde o teste aponta, é onde o code review cava. Mas o primeiro bug de um sistema quase nunca está lá. Ele nasce muito antes — no requisito que a reunião inteira leu, aprovou e classificou como claro, sem perceber que a mesma frase aceitava três interpretações diferentes.
A novidade de 2026, no desenvolvimento assistido por IA, não é usar verificação formal pra provar que um código está correto — isso existe há décadas em nichos como aviônica e criptografia. A virada é aplicar rigor formal um passo antes: na especificação, quando o código ainda não existe. Ferramentas de spec-driven development começaram a estruturar o requisito com a notação EARS e a traduzir esse requisito em lógica formal, deixando um SMT solver caçar contradição, ambiguidade e fluxo incompleto antes de qualquer geração de código. O reposicionamento é a parte importante: não é verificar o código, é verificar o requisito.
Principais pontos
- O bug nasce no requisito, não no código — a ambiguidade aprovada na reunião é o defeito mais fácil de achar e o mais custoso de deixar passar, porque contamina tudo que vem depois.
- EARS troca a frase bonita por requisito estruturado — cinco padrões de sintaxe que forçam gatilho, estado e resposta explícitos, sem exigir que quem escreve domine métodos formais.
- A virada é neuro-simbólica — a LLM traduz o requisito em lógica formal e o SMT solver, um verificador determinístico, caça contradição entre regras e critério de aceite com múltiplas leituras.
- IA rápida sobre requisito ambíguo entrega o erro mais cedo — dados de 2026 sobre sobrevivência de problemas em código gerado por IA mostram por que verificar antes virou urgente.
- O limite é honesto — o solver verifica a coerência da especificação, nunca a intenção estratégica; ele não descobre se o negócio pediu a coisa errada com clareza perfeita.
Pra quem decide um projeto de software hoje, a pergunta deixou de ser só "a IA escreve bom código?". Passou a ser "o que garante que ela vai escrever a coisa certa?". É exatamente nesse ponto — na fronteira entre o requisito e a primeira linha de código — que um parceiro como a Vertis Tech concentra a parte do trabalho que mais evita retrabalho: estruturar o requisito, versionar o contexto e colocar revisão humana antes de a IA executar.
O defeito mais barato de corrigir é o que ninguém procura
Pense no fluxo típico. Alguém escreve "o sistema deve notificar o cliente quando o pedido for aprovado". A frase parece completa. Mas ela não diz por qual canal, não define o que acontece se o pedido for aprovado e depois cancelado em segundos, não esclarece se "aprovado" é o estado do pagamento ou o da análise antifraude, e não trata o caso de o cliente não ter canal de contato válido. Cada uma dessas lacunas é uma decisão que alguém vai tomar — o programador, o agente de IA, ou o cliente reclamando em produção. E cada decisão tomada no escuro é um bug em potencial que não existe no código ainda, mas já está codificado na ambiguidade do requisito.
O custo dessa lacuna cresce de forma desproporcional conforme ela avança. Corrigir uma frase ambígua numa reunião de refinamento custa alguns minutos. Corrigir a mesma ambiguidade depois que ela virou arquitetura, código, teste e três integrações custa sprints. Essa assimetria é velha na engenharia, mas a era da IA a tornou aguda: quando a geração de código deixa de ser o gargalo, o gargalo real fica exposto, e ele está na qualidade do que se pede.
Os dados de 2026 dão contorno a isso. Um relatório da Veracode, em sua atualização de 2026 sobre segurança de código gerado por IA, manteve a taxa de aprovação de segurança em torno de 55% — ou seja, em cerca de 45% dos casos o modelo introduz uma falha de segurança conhecida no código. Uma análise da CodeRabbit sobre aproximadamente 470 pull requests de projetos open source, publicada no fim de 2025, encontrou cerca de 1,7 vez mais problemas relevantes em PRs coautorados por IA em comparação com código escrito por humanos. E um estudo em larga escala de 2026, que examinou 304.362 commits de IA em 6.275 repositórios reais, apontou que problemas de segurança introduzidos por commits de IA têm taxa de sobrevivência de 41,1% — continuam presentes na revisão mais recente do repositório. O padrão é consistente: IA rápida em cima de instrução mal especificada não corrige o erro, só o entrega mais cedo e em maior volume.
EARS: trocar a frase que aceita três leituras por requisito estruturado
A notação EARS — Easy Approach to Requirements Syntax — nasceu na engenharia aeronáutica justamente pra atacar a imprecisão da linguagem natural sem obrigar o autor do requisito a virar um especialista em lógica formal. A ideia é simples e poderosa: em vez de escrever prosa livre, você encaixa cada requisito em um de poucos padrões que forçam explicitar gatilho, estado, condição e resposta. A frase deixa de ser bonita e passa a ser verificável.
São cinco padrões principais:
Ubíquo
Uma regra sempre ativa, sem gatilho. "O sistema deve registrar toda alteração de estado de um pedido." Não depende de evento nem de condição — vale o tempo todo. É o comportamento de fundo do sistema.
Dirigido por evento
A estrutura "Quando , o sistema deve ". "Quando o pagamento for confirmado pelo antifraude, o sistema deve notificar o cliente por WhatsApp." Repare como o padrão obriga a nomear o gatilho exato — "confirmado pelo antifraude", não o vago "aprovado" — e a resposta concreta.
Dirigido por estado
A estrutura "Enquanto , o sistema deve ". "Enquanto o pedido estiver em análise antifraude, o sistema deve exibir status pendente e bloquear cancelamento self-service." O padrão captura comportamento que vale durante uma condição contínua, não num instante.
Opcional
A estrutura "Onde , o sistema deve ". "Onde a integração com transportadora estiver ativa, o sistema deve exibir código de rastreio." Isola comportamento que só existe quando um recurso ou configuração está habilitado — o que evita confundir requisito universal com requisito condicional.
Comportamento indesejado
A estrutura "Se <condição>, então o sistema deve ". "Se o cliente não tiver canal de contato válido, então o sistema deve registrar a falha de notificação e escalar para atendimento humano." É o padrão que captura o caso de exceção que quase todo requisito em prosa esquece de tratar — e que costuma ser exatamente onde o bug aparece.
O ganho de encaixar o requisito nesses padrões não é estético. É que a estrutura torna a lacuna visível. Quando você é forçado a nomear o gatilho, fica óbvio quando dois requisitos disparam no mesmo gatilho com respostas conflitantes. Quando você separa estado de evento, fica evidente qual comportamento vale durante uma condição e qual vale num instante. A frase estruturada expõe o que a frase bonita escondia.
A virada neuro-simbólica: a LLM traduz, o solver caça a contradição
Estruturar com EARS já reduz ambiguidade, mas o salto de 2026 vem de combinar duas famílias de tecnologia que costumavam viver em mundos separados: a rede neural, boa em linguagem e ambiguidade, e o raciocínio simbólico, bom em lógica exata. É a abordagem neuro-simbólica.
O fluxo funciona assim. A LLM lê o conjunto de requisitos — de preferência já estruturados em EARS — e os traduz em fórmulas de lógica formal: predicados, condições, restrições. Essa é a parte em que o modelo de linguagem brilha, porque exige interpretar texto. Em seguida, entra o SMT solver. SMT quer dizer Satisfiability Modulo Theories: é um verificador determinístico, matemático, que responde a uma pergunta precisa — existe alguma atribuição de valores que satisfaça todas essas restrições ao mesmo tempo? Se não existe, há contradição. E o solver não chuta: ou encontra uma combinação que satisfaz as restrições, ou aponta que determinado conjunto de regras é impossível naquele modelo.
Na prática, isso caça uma classe de defeitos que revisão humana deixa passar por fadiga: duas regras de negócio que se contradizem em um caso de borda que ninguém imaginou; um critério de aceite escrito de forma que admite duas interpretações incompatíveis; um fluxo em que falta o tratamento de um estado; uma regra de exceção que nunca foi escrita porque todo mundo assumiu que "nunca acontece". O solver não se cansa e não assume nada — testa a combinatória de estados que a mente humana não consegue enumerar. Ferramentas de spec-driven development já começaram a embutir esse tipo de análise: a função de análise de requisitos do Kiro, por exemplo, usa lógica formal e SMT solver pra flagrar contradições antes de gerar código a partir de uma especificação escrita em EARS.
O efeito é mover a detecção do defeito pro ponto mais precoce do ciclo. Em vez de a contradição virar código, virar teste que passa por acaso e explodir em produção três meses depois, ela é apontada na especificação — quando corrigir custa reescrever uma frase, não refatorar um módulo.
O limite honesto: coerência não é intenção
Aqui entra a parte que separa análise séria de promessa de laboratório. O SMT solver verifica a coerência da especificação. Ele ajuda a responder se o conjunto de restrições formalizadas é internamente consistente e onde há lacunas ou combinações impossíveis. Ele não responde — e não tem como responder — "esse conjunto de requisitos é o que o negócio realmente precisa?".
São perguntas diferentes. Uma especificação pode ser perfeitamente coerente, sem uma única contradição, formalmente impecável, e ainda assim descrever o produto errado. Se o negócio pediu a coisa errada com clareza matemática, o solver vai aprovar com entusiasmo. Ele verifica a lógica interna, não a intenção estratégica. A ambiguidade que ele elimina é a de interpretação; a ambiguidade que ele não toca é a de propósito — se estamos construindo a coisa certa pro problema certo.
Por isso a verificação formal do requisito não substitui o discernimento humano; ela o libera. Ao remover a carga de caçar contradição lógica na mão, sobra atenção humana pra pergunta que só gente responde: isso resolve o problema real do cliente? Quem trata o solver como oráculo de correção cai numa armadilha nova — a de confiar que "passou na verificação" significa "está certo". Passou na verificação significa "é coerente". O resto continua sendo trabalho de decisão.
Como a Vertis Tech ajuda em verificação de requisito antes do código
A Vertis Tech desenvolve software sob medida com foco em CRM, automação e IA aplicada. Cada projeto é dimensionado conforme a criticidade do processo, a maturidade da especificação que chega, as integrações necessárias e o grau de autonomia que a IA vai ter na execução. A depender do escopo, a abordagem pode contemplar:
- Requisito estruturado antes da geração, com a especificação tratada como fonte de verdade que humanos e agentes seguem, em vez de prompt solto que aceita interpretação livre.
- Contexto versionado, mantendo requisitos, regras de negócio e histórico de decisão em base auditável — no mesmo espírito com que a operação interna versiona seu próprio Know-How e Playbook, editáveis e rastreáveis.
- Gate humano em pontos críticos, com agentes construídos sobre Claude Agent SDK e ferramentas MCP, onde a aprovação de uma pessoa precede a execução quando envolve dado sensível, dinheiro ou decisão crítica.
- Auditoria append-only, para que cada passo do agente e cada aprovação fiquem registrados de forma imutável, permitindo reconstruir por que o sistema fez o que fez.
- Revisão antes de a IA executar, desenhando o fluxo pra que ambiguidade e contradição sejam tratadas na especificação, e não descobertas em produção.
Os itens acima são dimensões de desenho, calibradas caso a caso — não uma promessa de que todo projeto embarca método formal de laboratório. Verificação formal com SMT solver é uma técnica poderosa e específica; o valor prático, na maioria dos projetos de negócio, está em capturar a disciplina que ela representa: estruturar o requisito, expor a lacuna cedo e colocar gente no lugar certo do fluxo.
Perguntas frequentes
EARS exige que meu time aprenda métodos formais?
Não. Esse é o ponto da notação. EARS foi desenhada pra que qualquer pessoa que escreve requisito consiga encaixar a frase em um de poucos padrões, sem dominar lógica matemática. O rigor formal, quando entra, acontece na camada seguinte — na tradução para o solver — e fica em geral por conta da ferramenta ou do time técnico, não de quem redige o requisito de negócio.
SMT solver é a mesma coisa que verificar o código formalmente?
Não, e a diferença é o ponto central. Verificação formal de código prova propriedades sobre um programa que já existe. A aplicação nova verifica a especificação antes de o código existir — caça contradição e ambiguidade no requisito, quando corrigir ainda custa pouco. São camadas diferentes do ciclo, com custos de correção muito diferentes.
Se o solver aprova a especificação, o software está correto?
Não. O solver garante que a especificação é internamente coerente — sem contradição, sem lacuna óbvia. Ele não garante que a especificação descreve o que o negócio precisa. Uma spec coerente pode descrever o produto errado com clareza perfeita. A pergunta sobre intenção estratégica continua sendo humana.
Isso serve pra projeto pequeno ou só pra sistema crítico?
O método formal completo faz mais sentido onde o custo do erro é alto. Mas a disciplina por trás dele — estruturar o requisito, nomear gatilho e exceção, expor a lacuna antes de codar — melhora qualquer projeto, inclusive os pequenos, e não exige ferramenta sofisticada. O ganho vem menos da tecnologia e mais do hábito de não deixar a ambiguidade passar.
A IA não deveria resolver a ambiguidade sozinha?
A IA resolve ambiguidade tomando uma decisão — nem sempre a que você queria. Um requisito com três leituras vira código com uma leitura, escolhida pelo modelo sem te consultar. Verificar o requisito antes força a decisão a ser explícita e humana, em vez de implícita e escondida no código gerado.
O deslocamento de fundo é este: quando escrever código deixou de ser o passo custoso, o passo custoso passou a ser saber exatamente o que se quer construir. Estruturar o requisito com EARS e submetê-lo a verificação neuro-simbólica é uma forma concreta de atacar isso — não porque elimina o julgamento humano, mas porque separa o que é lógica, que a máquina resolve, do que é intenção, que continua sendo sua. A jogada de qualidade da era da IA não é escrever código mais rápido. É verificar o requisito antes que a velocidade da IA transforme uma frase ambígua num passivo pesado.
