Requirements and Contracts: The Two-Gate Model for AI

Requirements, specification and contract engineering turns a stakeholder's intent into an obligation a machine can be held to, then proves what was built honors it. Executives should care because an AI system can pass every test it was given and still do the wrong thing, since the tests were too narrow to catch the gap. Two 2026 studies show automated checking finds real defects, and neither shows a passing check means the system understood what you meant.

What it is

The discipline works across six layers of increasing precision, each trading nuance for enforceability: a narrative requirement in the stakeholder's own words, a structured requirement with an explicit actor, condition and response, an executable acceptance test proving one input behaves correctly and nothing about the rest, a formal contract quantifying over an entire modeled domain but only guaranteeing what that model contains, a temporal property adding ordering and deadlines, and a policy language governing who is allowed to see or move what. Choose the weakest representation that expresses the property you need: a mistaken interpretation shared across layers contaminates all of them at once.

Systems once checked against a specification can now write it, generate the tests, and propose changes to their own acceptance criteria. Hall and Eiers (arXiv, May 2026) ran 64 requirements through 85 typed variables, a Z3 solver and five stochastic formalizations, catching 249 of 256 seeded mutations, a 97.3 percent detection rate (confidence interval 94.5 to 98.7 percent). Counterexample-guided repair raised agreement with the generated formal model from 55.4 to 98.5 percent across 65 questions after five rounds, though it did not independently confirm the model captured true meaning, and its code and data were unavailable for review. Tufano and coauthors at Google (arXiv, August 2026) ran 90 internal bugs through five attempts of a fixed model: detection rose from 53.4 to 63.2 percent, a meaningful gain, while first-attempt detection rose only from 36.9 to 41.1 percent, not established as significant, at a cost of roughly 38 percent more tokens. Ignoring that distinction costs money twice, in defects reaching production and in paying for attempts that may not earn their keep.

The architecture

The named framework here is the two-gate model. Every specification must clear an adequacy gate, proving it captures what the business actually meant, and a separate conformance gate, proving the implementation obeys what was written. The two must never collapse into one: a specification can be self-consistent and still be wrong.

Each requirement enters as a record: an identifier, an owner, its scope, the risk it addresses, a testable predicate and a version number. Acceptance criteria freeze before an implementation is chosen, since a criterion that can still move tends to drift toward whatever code already exists.

The adequacy gate checks intent. An independent reviewer who did not write the specification or the code tests it against examples the implementer never saw, probes its edges with adversarial cases, and runs mutation tests that weaken a requirement to see whether the gate catches the sabotage. It also checks for vacuous guarantees: a rule that every request eventually gets a response is worthless if requests never occur in the model.

The conformance gate checks implementation against the frozen specification, by test, solver or human review. A parser failure, a solver timeout, an unresolved result and a genuine counterexample are four different findings, and a timeout must never count as a passing proof. A specification can also be correct and still miss the point: a banking transfer proof can hold for every case in its model while allowing a transfer from an account the caller does not own, because the model never included an ownership check. The proof was not false. It proved the wrong property.

Ownership sits with the business, not the tooling: it keeps requirement identifiers, versions and authorization, and models may propose candidate specifications, but a proposal is not authority. Formal checkers, test runners and model providers stay swappable adapters, never the source of truth, with their solver logic and policy assumptions recorded so a silent vendor change does not silently change your guarantees. Keep hidden acceptance tests access-separated from the system being optimized, or the loop being checked can see the answer key. Two decisions belong to an executive and cannot be delegated: classifying a change as compatible, behavior-changing or authority-changing, and approving anything authority-changing.

What it is worth

Money shows up twice: undetected defects reaching production, and the checking process itself, since token spend rises alongside detection gains. Risk shows up in authority-changing errors a proof can miss if its model never included the boundary, and in nonfunctional failures such as a correct answer arriving after its deadline. Time shows up in review cycles: freezing acceptance criteria trades a slower start for avoiding rework against a moving target.

Measure before adopting the two-gate model: baseline defect rate by obligation class, false-constraint rate, and review minutes per requirement, at a fixed budget. Measure after at that same budget, not your best run out of five, since the Google study's own detect-at-five gain was not shown to hold at equal cost against detect-at-one. The dossier supports contract-assisted test generation finding more defects across repeated attempts, and counterexample-guided repair sharply raising agreement with a generated formal model. It does not support fewer production incidents, or beating a well-designed template at equal cost.