Your Spec Has Bugs. Catch Them Before Your Agent Codes. - Rajath Mahendrappa Kotyal, AWS

A customer submits an order for an item that is out of stock. What should the store do? One rule in the e-commerce specification says to place the order on backorder. Elsewhere in the same file, another rule forbids placing any order on backorder. Each reads clearly on its own. Give them the same submitted, out-of-stock order and every implementation has to violate one of them.

Rajath Mahendrappa Kotyal, who worked on Kiro’s specification analyzer in the automated reasoning group at AWS, wants to catch that decision before it reaches a coding agent. He cites research reporting a 20–40% drop in generated-code accuracy with unclear prompts, 60–90% of valid code still being wrong, and twice as many regressions on deployment. He gives no task definitions or comparison baselines for those figures, so they motivate checking the input without quantifying what Kiro fixes.

The analyzer acts as a first reviewer. Within one sentence it can look for a word with two meanings or a requirement written at the wrong level of detail. Across sentences it has a different job. It needs to find situations where two rules demand incompatible outcomes, or where the author has left a case uncovered. Polishing the two backorder rules individually would leave the store with exactly the same problem.

Kiro first gives the LLM a chance to clean up the wording. If that leaves a question unresolved, the model translates the English into formulas in SMT-LIB, a language for expressing logical constraints. An SMT (satisfiability modulo theories) solver can then check whether any assignment of values satisfies the constraints under consideration. When the check exposes a problem, the analyzer sends the relevant sentence back to the LLM for another pass. A passing check needs no such revision.

What has to survive the translation of the inventory rule? In compact notation, its meaning is (submitted AND inventory_unavailable) ⇒ backordered. Both conditions belong on the left. Consider an order for which both are true. The implication now requires backordered to be true, while the blanket prohibition requires it to be false. Fixing the input case matters. With inventory available, the conditional rule makes no demand, so that case alone would never expose the conflict.

A single translation quietly commits to one reading of the English. To see where that choice matters, Kiro asks the LLM to translate the same requirement repeatedly. Kotyal gives seven or ten samples as examples. The analyzer groups the resulting formulas by logical equivalence. Two translations belong together if they agree for every assignment of values, even when their expressions look different. Separate groups mean there is at least one case in which the translations disagree.

That disagreement gives the reviewer something specific to investigate. The model may have supplied different assumptions on different attempts. A solver can establish that the resulting formulas differ in meaning, but the split alone cannot tell which assumption the author intended. Kiro can accept an interpretation, ask the user to clarify, or leave that part unimplemented.

Consider the instruction “remove the record.” What should remain afterward? Under one interpretation the system deletes the record. Under another it retains the record and hides it from users. A user looking at the list could see the same result either way, yet the two implementations leave different data behind. Kiro puts that concrete choice to the user.

Reviewing a set of rules produces two other kinds of question.

• Conflict. For the submitted, out-of-stock order, two rules apply and demand incompatible results. The author has to settle which behavior the store should implement.
• Gap. In the order example, no rule covers an idle order. There is no competing instruction to discard. The missing decision is what, if anything, the system should do in that state.

Even a consistent set of rules can describe the wrong product. A team may know what removal means in its domain and never have written that knowledge down. Reviewing the whole specification before handing it to the coding agent still falls to someone who knows the domain. Kotyal also describes the evidence for using this kind of formalization in agents as thin.

Kotyal sums up the division of work: “The LLM translates, the solver checks and the human decides.” Logical equivalence gives the solver a precise question it can settle about the translations. Choosing whether a record ought to survive deletion from the user’s view requires product judgment. If the user leaves that question unanswered, the workflow can fall back to an LLM judge or abstain from implementing that piece. Abstaining keeps an unresolved choice visible before it becomes code.