Red to Green Proves Nothing: Formal Requirements Analysis in Kiro

In May I wrote a comparison of Kiro CLI and Claude Code and closed it with a prediction. Kiro’s Deep Spec Analysis, a neuro-symbolic requirements checker, had just launched in the Kiro integrated development environment (IDE), and I do most of my work in the command line interface (CLI). I said the analysis was “the kind of feature I expect to land in the CLI before long.”

It is August 3rd, 2026, and it has not landed yet. I went looking for it because I wanted to use it, and what I found was more interesting than a simple yes or no. So this post is the follow-up: what that capability actually does, where it lives today, and what to do if you cannot reach it from the surface you work in.

I checked primary documentation for every claim here. Where I am relying on a vendor’s own description of their product, I say so.

Why I went looking

#

My workflow already has real upfront rigor. I run background research with parallel agents before I write anything. I run a spec skill that produces requirements, a high-level design, a low-level design, and a task list. I have principal engineer and principal product manager agents that challenge the design before implementation starts. That pipeline catches problems I would otherwise ship, and I am not giving it up.

Then implementation starts, and this is the failure mode I keep hitting. If I am not reading every line of the spec and actively driving the work, the model implements one layer of the application correctly and that layer fails the moment the code deploys. The data layer is right on its own terms. The application programming interface (API) contract is right on its own terms. The two do not agree with each other, or neither agrees with what the product actually has to do. Every individual piece passes review. The assembled system does not work.

Test-driven development is supposed to be the guard here. An agent doing TDD writes a test, watches it fail, and makes it pass. Red to green. That loop proves the code does what the test says. It does not prove the test says what the product needs. When the test encodes the same misreading of intent as the implementation, it goes green and tells you nothing. You get a passing suite and a broken deploy.

The frontier models have made this better. They hold more context, follow specs more faithfully, and catch more of their own mistakes than they did a year ago. They have also raised the stakes. A model competent enough to build a large, internally consistent system quickly is equally capable of building a large, internally consistent, wrong system quickly. Garbage in, garbage out was always true. It matters more as throughput goes up, because the volume of code you have to review before catching the misunderstanding goes up with it.

So I want to shift that check left, to something that validates the requirements themselves are coherent before any code exists. A satisfiability modulo theories (SMT) solver over a formal model of your requirements does exactly that, which is why I went looking for this feature in the first place. An SMT solver is the same class of tool that formal verification engineers use to prove properties about hardware and protocols, and it either finds a case where your constraints hold or proves that none exists.

The problem this solves

#

Every requirement document contains bugs. Not code bugs, requirement bugs, and they fall into four categories that are hard to catch by reading.

A requirement can sit at the wrong level of detail. “The system shall support authentication” is a thesis statement, not a testable constraint. A requirement can be ambiguous, where the same sentence has two plausible readings and two developers implement it differently. Two requirements can be individually sensible and jointly impossible, which is inconsistency. And a requirement set can be incomplete, specifying behavior for some inputs and leaving whole regions of the input space undefined.

Kiro’s applied science team published a detailed writeup of why these are hard to detect. Level-of-detail and ambiguity problems are about what is not stated. Inconsistency requires reasoning over several requirements at once to find common triggers. Completeness requires reasoning over the whole set to find gaps. None of that is what a human does well on a first read.

That last problem has been measured, and the numbers are worse than I assumed. The Kiro team cites two papers. Larbi et al. (2025) mutated clear prompts into ambiguous, incomplete, and contradictory versions and measured Pass@1 drops of 20 to 40 percent, with 60 to 90 percent of syntactically valid code being semantically wrong. Yang et al. (2025) found that LLMs silently fill gaps in underspecified prompts, and that underspecified prompts are about twice as likely to regress across model changes. That second finding is the one that should worry anyone running an agentic pipeline, because it means the same spec can produce working code today and broken code after a model upgrade. I am citing both as the Kiro team presented them and linking the preprints so you can read them directly.

What Kiro’s requirements analysis actually does

#

This is where the marketing language and the engineering reality line up better than I expected.

Kiro’s spec workflow writes requirements in EARS notation, short for Easy Approach to Requirements Syntax, which is a structured format where each acceptance criterion follows a pattern like “WHEN [condition] THE SYSTEM SHALL [behavior].” That structure is what makes the next step possible.

The analysis runs in three stages. First, refinement uses a large language model (LLM) to rewrite thesis-level criteria into testable, solution-free ones, working backward from the user story to ask what could prevent success. Second, auto-formalization translates the natural language into SMT-LIB, the standard input language for SMT solvers. Each EARS clause maps to a logical implication: the WHEN or IF clause becomes the antecedent, the SHALL clause becomes the consequent. Third, logical analysis runs an SMT solver over that formal model to find contradictions and gaps.

The ambiguity detection is the part I found genuinely clever. LLM translation is non-deterministic, so asking for the formal version of the same criterion ten times can produce different answers. Kiro turns that into a detection mechanism by sampling multiple formalizations and clustering them by logical equivalence, then measuring the semantic entropy of the result. Low entropy means the model is confident and the translation is trusted. High entropy means the model cannot formalize the statement reliably and the criterion needs rewriting. Entropy in the middle means there are two dominant readings, which is exactly what ambiguity looks like, and Kiro computes a semantic diff between the top two candidates and turns it into a plain-English question.

You never see the formal logic. Every finding is surfaced as a two-option question where option A means keep the requirement as-is and option B means change it with a specific proposal. There are five finding types: ambiguity, conflict, completeness, accepted-scenario, and rejected-scenario.

Here is the worked example from Kiro’s post, because it makes the value concrete. Five acceptance criteria for an order system:

R1. WHEN an order is submitted AND inventory is available,
    THE Order System SHALL fulfill the order.
R2. WHEN an order is submitted AND inventory is not available,
    THE Order System SHALL place the order on backorder.
R3. THE Order System SHALL NOT place any order on backorder.
R4. WHEN an order is canceled,
    THE Order System SHALL refund all payments for the order.
R5. WHILE an order is in a canceled-and-refunded state,
    THE Order System SHALL NOT fulfill the order.

R2 and R3 contradict each other directly, and a careful reader catches that one. The solver also finds a conditional contradiction that requires case-splitting: if a canceled-and-refunded order is resubmitted, then either inventory is available and R1 conflicts with R5, or inventory is not available and R2 conflicts with R3. Either way no implementation satisfies all five. Then it finds a completeness gap, because when no order is submitted and none is canceled, none of the rules fire at all and the system has no defined behavior.

That third finding is the one I would never have caught by reading. It is also exactly the class of bug that produces the deploy failure I described earlier, where every layer is individually defensible and the system still has a state nobody specified.

Where it lives, and where it does not

#

This is the part that sent me through the documentation, and the answer is narrower than the marketing implies.

Kiro IDE has it. The Analyze Requirements page documents two invocation points: a chat option after requirements generate, and the Continue dropdown in the editor. Both are IDE surfaces.

Kiro CLI does not. I confirmed this three ways. The Specs in CLI page documents the full /spec command set, which is /spec new, /spec <name>, and /spec run <name>. It walks through Requirements, Design, Tasks, and Execution phases and never mentions an analysis step. The complete slash command reference lists more than thirty commands with no /spec analyze or equivalent. The CLI 3.0 feature comparison table, which is the authoritative tracker for what shipped to the CLI, lists spec-driven development as new but has no line item for requirements analysis.

Every row that says “not exposed” still reads and writes the same spec files. That shared format is what makes the workaround later in this post possible.

What this costs

#

One detail worth knowing before you plan around this feature. Kiro’s pricing announcement states that the Free tier includes 50 Vibe requests per month and 0 Spec requests. Requirements analysis consumes Spec-request quota. You need a paid tier to run it at all, not just to run it often.

It also costs tokens on the way in, and the direction runs opposite to what you might hope. The mechanism samples multiple formalizations of every criterion to measure semantic entropy, runs a refinement pass before that, and uses an LLM judge to filter generated scenarios afterward. The Analyze Requirements documentation notes the analysis takes minutes rather than seconds because cross-requirement reasoning is more computationally intensive than typical operations. Intake gets more expensive, not less. The bet is that catching a contradiction before implementation costs less than catching it after a deploy. I think that bet is right, and it is still a bet on downstream savings rather than a reduction in upfront cost.

The workaround I would actually use

#

Specs are portable. The CLI specs documentation is explicit that .kiro/specs/ is shared across IDE, CLI, and Web with an identical file format, and that you can start a spec in the CLI and continue it in the IDE.

So the practical path is to run /spec new in the CLI, open the same project folder in the Kiro IDE for the analysis step, resolve the two-option questions there, then go back to the CLI for design, tasks, and execution. That is not a hack. It is the portability model the documentation describes. It does mean you cannot stay in the terminal for that one step.

I also expect this to reach the CLI eventually, though the timeline so far argues for patience. Requirements analysis shipped in the Kiro IDE 0.12 release on May 6th. Kiro Web received the full Specs workflow about a month later, and its specs documentation covers requirements, design, and tasks, including a dedicated section on how Web differs from the IDE, without mentioning requirements analysis at all. Across all three surfaces, this capability currently lives in the IDE alone.

That timeline cuts against the assumption I made in May. The CLI 3.0 documentation says CLI 3.0 “is built on the same unified agent harness that powers the Kiro IDE and Kiro Web” and that “every improvement to the engine (new tools, better planning, smarter tool selection) now ships to all clients simultaneously.” I read that and concluded requirements analysis would follow quickly. Then a second client shipped the spec workflow a month later without it. I cannot tell from the outside whether the analysis pipeline is engine-side and simply unexposed, or IDE-side and not yet generalized, so I am not going to guess at it a second time.

LLM review and solver validation are not the same check

#

If you cannot get to the IDE, or you work in a different tool entirely, there is other tooling that claims to solve this problem. The line between it and what Kiro is doing is the reason I care about this feature at all.

There is good tooling that does requirements analysis with an LLM. GitHub Spec Kit is the most widely used, it works with more than thirty coding agents, and it ships /speckit.clarify for underspecified areas, /speckit.analyze for cross-artifact consistency and coverage, and /speckit.checklist, which its own documentation describes as “unit tests for English” for validating requirements completeness, clarity, and consistency. That is a serious answer to the same problem and worth running.

The difference is what happens when the checker is wrong. Extended thinking gives a model more tokens to deliberate. A reviewer agent is a model reading output from a model. A generated test is a model checking a model’s work against a target the same model set. LLM-based requirements analysis is a model auditing text a model wrote. All four are useful, and all four share one failure mode: the checker can be wrong in the same direction as the thing being checked. That is the red-to-green problem from the top of this post, and adding more LLM passes does not remove it.

An SMT solver does not have that failure mode. Kiro’s documentation draws the line explicitly in the Bedrock Automated Reasoning concepts guide: the translation step uses LLMs and may contain errors, while the validation step is mathematically sound. If the translation is right, the verdict is right. The solver cannot talk itself into accepting a contradiction, because it is not reasoning by analogy to text it has seen before. It is enumerating a logical space and returning a proof.

There is a practical consequence I am still testing. Two LLM agents reviewing each other have no grounded stopping point. Each round the reviewer generates plausible new concerns, because generating plausible critique is what it does, and plausible has no natural floor. I have watched my own principal-agent review loop run five or more rounds on a single spec. A solver terminates: the requirement set is either satisfiable or it is not, and the answer does not drift between rounds. Whether that actually reduces total review rounds in my workflow is a measurement I have not run yet, and I am not going to claim a result before I have one.

I treat Spec Kit’s analysis commands as a stopgap rather than a destination. Kiro has already shipped the solver-backed version of this check and continues to expand the spec workflow across surfaces. If it reaches the CLI, reaching for external tooling to approximate it stops making sense for anyone already working in Kiro. Reach for this if you need the capability today in a surface that does not have it.

The Bedrock path

#

My first instinct was that Amazon Web Services (AWS) must expose this capability directly, and it does, with a caveat that matters.

Amazon Bedrock Automated Reasoning checks is the same underlying technology. It translates natural language into SMT-LIB rules, uses an SMT solver for mathematically sound validation, and uses the same multi-model translation with confidence scoring that Kiro’s ambiguity detection relies on. AWS publishes a guide to driving it from Kiro CLI through natural language conversation.

The caveat is that it solves a differently shaped problem. Automated Reasoning checks validates a separate piece of text against a persistent policy, because it is built as a guardrail for LLM responses. Kiro’s requirements analysis validates one document for internal contradictions. To repurpose Bedrock for requirements work you would treat your own requirements.md as the policy, then feed each acceptance criterion back in as a claim to check against the others. Nothing in the AWS documentation describes that reverse use case.

Two pieces do map cleanly. The QUALITY_REPORT asset surfaces conflicting rules, which is the same concept Kiro reports as conflict findings. And GENERATE_POLICY_SCENARIOS produces accepted and rejected scenarios you can review for surprises, which is what Kiro’s accepted-scenario and rejected-scenario findings do with an LLM judge deciding what counts as surprising.

If you want scriptable, SMT-backed contradiction detection in a continuous integration (CI) pipeline, outside any particular agentic tool, this is a real option. You would rewrite your acceptance criteria as if-then rules, create a policy, run INGEST_CONTENT, and pull the quality report. AWS even publishes an LLM prompt template for converting prose into if-then rules as a preprocessing step.

I am not doing this for my blog. The setup overhead is significant, including a limit of two build workflows per policy with only one in progress at a time, and I would be reading raw SMT-LIB expressions and machine-readable quality reports instead of answering two-option questions. For a small static site the cost exceeds the benefit. For a regulated workload where requirement bugs are expensive, the math changes.

The same caveat from the previous section applies here, and more strongly. This is a workaround for wanting solver-backed validation today in a place that does not offer it natively. Kiro’s version already wraps the same class of technology in an interface designed for requirements work, which is most of the value. If requirements analysis reaches the CLI, the plumbing described above becomes unnecessary for spec work and I would drop it without hesitation. What I would keep it for is the case it was actually built for, which is validating model output against a policy at runtime.

What to do about it

#

The thing I keep coming back to is that this is the first capability I have seen in an agentic coding tool that is not another application of the same LLM. Every other guard in my pipeline shares a blind spot with the code it is guarding. The reviewer agent, the generated test, the extended thinking pass: each one can be wrong in the same direction as the thing it is checking. A solver cannot. That is the entire reason this matters.

It does not solve the whole problem. A requirement set can be perfectly coherent and still be the wrong requirement set, and only you can judge that. My principal product manager and principal engineer agents exist for exactly that judgment. What formal analysis removes is one full category of failure, and it removes it before implementation starts.

Here is what I would actually do, depending on where you work.

If you have the Kiro IDE on a paid tier, run Analyze Requirements on your next real spec before you approve the design. Not a toy spec. Pick the feature you are least certain about and find out what the solver says about requirements you already believed were finished.

If you live in the Kiro CLI, use the portable spec. Run /spec new in the terminal, open the same project folder in the IDE for the analysis pass, resolve the questions, then come back to the terminal for design, tasks, and execution.

If you work in another tool, run Spec Kit’s /speckit.analyze and /speckit.checklist. LLM-based analysis catches real problems and is worth having. Just know which failure mode you are still carrying.

If you need this scriptable or you build under regulatory pressure, wire the Bedrock Automated Reasoning path into your pipeline and check the quality report on every requirements change.

One action costs nothing regardless of tooling: write your acceptance criteria in EARS notation. WHEN this condition, THE SYSTEM SHALL that behavior. Naming the trigger and the observable outcome forces contradictions to the surface on its own, before any solver touches them. A meaningful share of the value here is the structure, and the structure is free.

Then count your review rounds. If your spec reviews are running five deep like mine, look at what those rounds are actually spending tokens on. Mechanical findings mean a solver would settle them in one pass. Judgment findings mean the loop is doing its job and your answer lies somewhere else. That measurement is the next thing I am running on my own workflow, and I will report what it says.

Keith