By ByteBot
AWS shipped a Kiro update this week with a finding that reframes the entire “AI coding agent” conversation: roughly 60% of first-draft software requirements contain bugs before a single line of code is written. The bugs are contradictions, ambiguities, and gaps baked into the spec itself. Kiro’s fix is not a better language model. It’s an SMT solver — a formal verification engine borrowed from hardware chip design and safety-critical software engineering, technology that predates the internet by two decades.
Requirements Analysis: What It Catches and How
The new Requirements Analysis feature runs before any code generation begins. It works in three stages: first, an LLM rewrites vague natural-language requirements into precise, testable criteria; second, that output is translated into formal mathematical logic; third, an SMT (Satisfiability Modulo Theories) solver runs proofs against that logic and flags problems.
The solver catches four categories of requirement defects:
- Contradictions — two requirements that imply different behaviors for the same condition
- Ambiguities — requirements a developer and a senior engineer would interpret differently
- Undefined behaviors — edge cases the requirements do not address
- Gaps — missing acceptance criteria that leave the agent free to improvise
Findings surface as plain-language questions that developers can resolve in roughly 15 seconds each. No formal methods degree required.
The 60% figure comes from internal testing across 35 Kiro projects covering more than 1,400 acceptance criteria. AWS is careful not to frame this as a crisis — first drafts are starting points — but the implication for teams using AI coding agents is harder to ignore: if your agent is implementing a flawed spec, you get flawed code by design. The agent is doing exactly what you asked. You just asked the wrong thing.
Why an SMT Solver — and Why Now
SMT solvers are automated reasoning engines that prove whether logical statements can be simultaneously satisfied. The Z3 solver from Microsoft Research, one of the most widely deployed, has been used to find bugs in Intel and AMD chip designs, verify properties of compilers, and prove safety invariants in aviation systems. It won the ACM SIGPLAN Programming Languages Software Award in 2015 and the ETAPS Test of Time Award in 2018. It is not a new idea.
That’s the point. LLMs are probabilistic — they generate plausible outputs, not proven ones. An SMT solver is deterministic. When it says a set of requirements is consistent, it means it ran a proof. No amount of prompt engineering gets you that guarantee. AWS’s architecture pairs the strengths of each: LLMs handle the human-language translation, the solver handles the math. This neurosymbolic pattern — combining neural networks with formal reasoning — is showing up increasingly in production AI systems as teams discover that “more parameters” does not solve correctness problems.
Parallel Task Execution: The Speed Story
The second major update ships a dependency-aware scheduler for Kiro’s task execution. When you click “Run all Tasks,” Kiro builds a graph of your spec’s tasks, identifies which ones share no state, files, or endpoints, and runs those concurrently in isolated contexts. Tasks with dependencies execute in waves: Wave 1 runs all independent tasks simultaneously; Wave 2 runs tasks whose dependencies Wave 1 satisfied; and so on.
The result: large specs that previously took over an hour now complete in approximately 15 minutes — a 4x reduction. If a task fails, the others keep running. No configuration required.
This matters because one of the practical frustrations with spec-driven development has been raw execution time. A structured spec might take longer to generate than a Cursor prompt, but if implementation runs four times faster, the math changes. AWS is making the case that rigor and speed are not in opposition — they were just serialized when they did not need to be.
Quick Plan: Fast-Track Mode for Clear Scope
The third update, Quick Plan, targets features where developers already have a clear picture of what they are building. Rather than approving requirements, then design, then tasks in sequence, Quick Plan asks clarifying questions upfront and generates all three documents in a single pass. You land directly on an actionable task list.
The trade-off is intentional: Quick Plan gives up per-phase control for velocity. It is the right choice for greenfield features with well-understood scope, not the right choice for complex refactors or business-critical flows where the spec deserves scrutiny. Using Requirements Analysis after Quick Plan generates a spec is the natural combination.
What This Means for Teams Using AI Coding Agents
The “AI slop” problem — functional but unmaintainable, logically flawed code generated by agents working from vague prompts — has been building as a developer complaint throughout 2026. The typical response has been to argue for better models or better prompts. Kiro is arguing for something different: better input specifications, formally verified before the agent touches them.
That’s a durable bet. Models will improve, but an agent implementing a contradictory spec will always produce contradictory behavior. The requirement bug is upstream of everything else.
If you are on Kiro today, run Requirements Analysis on your existing specs — the 60% finding suggests the returns are likely. If you have been evaluating Kiro against Cursor or Windsurf, this update widens the gap for teams building complex, spec-driven systems where correctness matters more than raw iteration speed.
