Como o Kiro da AWS usa lógica formal para encontrar problemas nas especificações antes do código

O Kiro agora inclui Análise de Requisitos, que transforma requisitos vagos em lógica formal e usa solvers SMT para provar contradições e lacunas antes de chegar à produção, reduzindo o risco de bugs caros originados em especificações mal definidas.

A AWS apresentou uma novidade no Kiro: Análise de Requisitos para identificar problemas nas especificações antes que o código seja gerado.

O objetivo não é apontar apenas potenciais falhas no código, mas interceptar contradições, ambiguidades e omissões já na fase de requisitos.

Para isso a ferramenta combina o que os modelos de linguagem fazem bem com raciocínio automatizado clássico, convertendo texto natural em representações formais verificáveis.

O fluxo passa por três etapas: o LLM refina requisitos em critérios testáveis, esses critérios viram uma representação formal, e um solver SMT verifica provas de inconsistência, comportamentos indefinidos e lacunas.





Os resultados aparecem para o desenvolvedor como perguntas objetivas de duas opções, que a empresa diz ser possível resolver em cerca de 10 a 15 segundos cada.

A proposta é demonstrar formalmente que duas regras não podem ser satisfeitas ao mesmo tempo, ou seja, provar uma incompatibilidade e não apenas sinalizar uma suspeita.

Em testes internos com dezenas de projetos e mais de mil critérios de aceitação, aproximadamente 60% dos primeiros rascunhos exigiram ajustes antes de serem implementados com segurança.

Áreas como saúde e finanças, onde a correção é crítica, têm se mostrado especialmente atraídas por esse tipo de verificação para evitar “alucinações” em cenários sensíveis.

Além da Análise de Requisitos, o Kiro recebeu recursos como execução paralela de tarefas para acelerar implementações e o Quick Plan, que gera requisitos, especificações e tarefas em uma única passagem.

Clientes relatam ganhos práticos, como migrações bem mais rápidas, maior cobertura de testes e diminuição do tempo gasto em documentação e validação.

“We are at an inflection point with Agentic AI, and I can’t stress enough how critical AI and Automated Reasoning need to come together to build reliable and trustworthy agents.”

“To me, whether it’s a better or more precise method is not the question. My question is: what’s the impact on the human-in-the-loop?”

A companhia também reforçou a equipe com a contratação de Shawn Bice para liderar o grupo de Raciocínio Automatizado no âmbito de Agentic AI.

A aposta da empresa é que o diferencial competitivo em ferramentas de desenvolvimento assistido por IA será cada vez mais a confiança no que é gerado, e não apenas a velocidade de geração de código.

A Análise de Requisitos surge como peça central dessa estratégia, fazendo com que o rastreio entre código e requisito seja não só documentado, mas logicamente verificável.

Artigo anterior

NGINX CVE-2026-42945: exploração ativa causa crashes nos workers e risco de RCE

Próximo artigo

Anthropic adquire Stainless e deixa concorrentes sem um fornecedor chave de SDKs



Artigos relacionados