A AWS trouxe para o Kiro um recurso chamado Requirements Analysis que combina LLMs com lógica formal e solvers SMT para encontrar contradições, ambiguidades e lacunas nas especificações antes que cheguem à produção, uma abordagem motivada pelo fato de que a empresa detectou problemas em cerca de 60% dos requisitos analisados.
A AWS identificou bugs em aproximadamente 60% das especificações que examinou, e a resposta não foi apenas mais IA generativa, mas a combinação dela com raciocínio formal.
O recurso Requirements Analysis do Kiro foi desenhado para capturar contradições e comportamentos indefinidos nas specs antes que se tornem código em produção.
O funcionamento é dividido em três etapas complementares.
Primeiro, um LLM reescreve requisitos vagos em critérios mais precisos e testáveis.
Segundo, esse texto refinado é traduzido para uma representação formal, ou seja, lógica matemática que descreve os requisitos de forma inequívoca.
Terceiro, um solver SMT (satisfiability modulo theories) executa provas sobre essa lógica para identificar contradições, ambiguidades e lacunas que não seriam aparentes apenas lendo o documento.
Os achados são apresentados ao desenvolvedor em perguntas de duas opções, em linguagem natural, que a AWS diz poder ser resolvidas em cerca de 10 a 15 segundos cada.
A empresa enfatiza o termo “prove” para diferenciar isso de um alerta probabilístico do LLM: trata-se de um motor de raciocínio formal demonstrando que duas regras não podem ser satisfeitas ao mesmo tempo.
“Automated reasoning allows us to take those requirements, look at them, identify gaps and ambiguities, and kind of address them up front,” Miller says.
Setores como saúde e finanças, onde correção é fundamental, têm mostrado interesse por essa capacidade porque precisam de IA que não tenha comportamento errático ou que “hallucine” em contextos sensíveis.
O mesmo movimento aparece com ferramentas de codificação agentes, e a AWS vê a garantia sobre o que é gerado como um diferencial competitivo além da mera velocidade de escrita de código.
Além do Requirements Analysis, o Kiro ganhou outras funções, como Parallel Task Execution, que executa tarefas independentes de forma concorrente e reduz o tempo de implementação de grandes especificações em cerca de 75%.
Outra novidade é o Quick Plan, que gera um conjunto completo de requisitos, especificações de design e divisão de tarefas em uma única passada, após fazer perguntas de esclarecimento iniciais.
O Kiro concorre com ferramentas como Cursor, Codex, Claude Code, GitHub Copilot e Windsurf, entre outras, mas a AWS afirma que a ferramenta já tem ampla adoção na indústria.
Casos práticos citados incluem a Socure, que completou uma migração de Scala para Go em dois dias num projeto inicialmente estimado em três semanas, e a Nymbus, que gera 80% do seu código Terraform, testes unitários e modelos Playwright com o Kiro, reduzindo o tempo de testes de 32 para 7 semanas em um projeto.
A Delta Air Lines atingiu metas de um programa piloto dois trimestres antes do previsto, a Nielsen viu aumento de 25% na cobertura de testes e queda de 40% no tempo gasto com documentação, e a Hughes destacou que as specs do Kiro eliminam a necessidade de reestabelecer contexto repetidamente no fluxo de trabalho.
Clientes corporativos citados incluem Siemens, Rackspace Technology, Mondelez International, Appian e Ericsson, além de equipes internas da Amazon como Alexa+, Prime Video, Amazon Stores e Fire TV.
Em paralelo ao lançamento, Shawn Bice foi anunciado como vice-presidente de AI Services dentro de Agentic AI na AWS e ficará à frente do Automated Reasoning Group.
Em um comunicado interno, Swaminathan Sivasubramanian escreveu: “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.”
Uma reflexão que surge é sobre o papel do humano no loop: mesmo que a AWS fique melhor em localizar problemas, continua sendo responsabilidade do desenvolvedor decidir como resolver esses pontos, e qualquer ganho nessa etapa pode ser valioso à medida que partes maiores do fluxo forem automatizadas.
