Why AWS Combines 50-Year-Old Logic with LLMs to Root Out Critical Software Bugs
AWS's Kiro platform uses LLMs and 50-year-old SMT solvers to prove requirement bugs—contradictions, ambiguities—before coding begins, reducing late-stage fixes.
Most expensive software bugs aren't born in code—they originate in the requirements that guide development. AWS has discovered that up to 60% of software flaws stem from contradictory, ambiguous, or incomplete requirements. To tackle this, the company is augmenting its generative AI agent, Kiro, with a decades-old mathematical technique: automated reasoning powered by SMT (Satisfiability Modulo Theories) solvers. The result is a new Requirements Analysis feature that mathematically proves requirement inconsistencies before a single line of code is written.
The Hidden Cost of Requirement Bugs
When a requirement like "the system must respond within 2 seconds" coexists with "the system must validate all data against a remote database," developers may interpret them differently. Mike Miller, director of AI product management at AWS, explains: "A bug in a requirement could be contradicting requirements that imply two different things, ambiguities or gaps where a requirement might mean one thing to one developer but something slightly different to another." By the time such conflicts surface in production, tracing them back to a misread requirement can consume weeks of debugging.
Traditional testing catches coding errors, but rarely validates the intent behind the code. Many teams rely on peer reviews or manual inspections, which are error-prone and time-consuming. AWS claims its new approach catches these issues up front, reducing rework and deployment delays.
How AWS's Requirements Analysis Works
The feature operates in three phases:
- LLM rewrites requirements: A large language model takes vague, natural-language specifications and restates them as precise, testable criteria. For example, "the system should be fast" becomes "response time must not exceed 500 ms under 1,000 concurrent users."
- Translation to formal logic: That precise output is converted into a formal mathematical representation—what AWS calls a "formal representation." This step transforms human language into a machine-verifiable set of constraints.
- SMT solver proves consistency: An SMT solver, a type of automated reasoning engine that has existed for about 50 years, runs proofs against that formal logic. It identifies contradictions, ambiguities, undefined behaviors, and gaps—provably demonstrating that no implementation can simultaneously satisfy conflicting rules.
Results are presented to developers as plain-language, two-option questions. Miller says these can be resolved in 10 to 15 seconds each, making the process practical for real-world workflows.
The Role of Automated Reasoning and SMT Solvers
AWS emphasizes the word prove. This is not a statistical probability from an LLM; it is a formal guarantee. "Automated reasoning allows us to take those requirements, look at them, identify gaps and ambiguities, and kind of address them up front," Miller says. "The LLM side does what it does best, and automated reasoning does what it does best."
This isn't AWS's first experience with automated reasoning. The company has used it for years in access control products like IAM, where it mathematically verifies that security policies are not contradictory. Jason Andersen, an analyst with Moor Insights & Strategy, notes: "AWS has been a pioneer in the idea that LLM model correctness can be evaluated using diverse algorithmic models to improve accuracy. That success has started to spread into other AWS product lines."
Why Not More AI? The NeuroSymbolic Approach
The approach exemplifies neuroSymbolic AI, which combines neural networks (the LLM) with symbolic reasoning (the SMT solver). Pure LLMs can hallucinate or miss subtle logical conflicts—they are pattern matchers, not proof engines. By adding formal logic, AWS ensures that the output is not just plausible but mathematically sound.
Andersen notes that the more typical method for evaluating LLM outputs is to use additional LLMs to inspect results. But that merely adds another statistical layer. AWS's method offers rigorous guarantees, aligning with the company's broader strategy of integrating automated reasoning into its core services.
Conclusion
Requirement bugs are the silent cost of software development—often discovered late and expensive to fix. AWS's new Requirements Analysis in Kiro brings the clarity of formal logic to the messiness of human language. By pairing LLMs' natural language understanding with SMT solvers' proof capabilities, AWS provides developers with a tool to catch contradictions before they become costly mistakes. It's a reminder that sometimes the best way to solve new problems is to combine modern AI with timeless mathematical rigor.