Verification Loops are how Specy turns a requirement from a written obligation into a living contract. Three loops close the gap between intent and behavior: Build translates intent into code, Check re-reads code against intent, and Observe matches runtime behavior back to intent. The requirement layer is the shared handle — every loop reads the same .sysreq file and uses the same IDs.
The Three Loops
Specy’s three loops are deliberately asymmetric — each one takes a different artifact as input and a different artifact as reference.
- Build — input: intent (requirements). Reference: the domain metamodel. Output: a domain model.
- Check — input: domain model. Reference: requirements. Output: a verdict on coverage and orphans.
- Observe — input: runtime events. Reference: requirements. Output: a drift signal.
The requirement layer is the only artifact shared by all three loops. That is why its austerity matters — any ambiguity in a requirement propagates into three loops at once.
Example:
The single statement "When a customer submits an order, the system shall create the order in draft status and emit an OrderPlaced event." (REQ-ORD-002) feeds all three loops: Build synthesizes a placeOrder operation with a satisfies [REQ-ORD-002] marker; Check verifies the marker exists; Observe matches production OrderPlaced events against the event-driven pattern.
Role of Requirements per Loop
The metamodel summarizes the role of requirements in each loop. The table below reproduces it unchanged — it is the canonical contract between the requirement layer and the verification machinery.
| Loop | Role of Requirements |
|---|---|
| Build (intent → code) | Requirements are the input specification. The builder reads requirements and produces a domain model whose elements declare satisfies references back to the requirement IDs. Every must and should requirement should be traceable to at least one domain element. |
| Check (code → intent) | The checker traverses satisfies lists in the domain model and verifies that every referenced requirement ID is covered. A requirement ID that appears in no satisfies list is a checker failure — a gap between intent and model. |
| Observe (runtime → intent) | Requirements with event-driven or unwanted patterns are observable at runtime. The observer traces event flows and verifies that the behaviors declared in requirements actually occur. Missing events or unhandled error conditions signal drift between intent and behavior. |
Example:
REQ-ORD-002 is event-driven — it participates in all three loops. REQ-ORD-001 is ubiquitous — it participates in Build and Check but is not directly observed at runtime (it is a structural invariant checked at admission, not a behavior emitted by the system).
Build (intent → code)
In the Build loop, requirements are the input specification. A modeler — or an AI assistant driven by the modeler — reads the .sysreq file and produces a domain model: operations, entities, events, services, policies. Every generated element declares a satisfies [IDs] marker pointing back to the requirements it realizes. Every must and should requirement should be traceable to at least one domain element — a could requirement with no satisfier is legitimate (the feature is deferred); a must requirement with no satisfier is a Build-time warning.
Example:
The builder reads REQ-ORD-002, REQ-ORD-003, and REQ-ORD-004 and emits a single placeOrder operation on the Order aggregate with satisfies [REQ-ORD-002, REQ-ORD-003, REQ-ORD-004]. The builder reads REQ-ORD-005 (the complex credit-limit requirement) and emits a CreditCheckPolicy with the matching satisfies list.
Check (code → intent)
The Check loop runs whenever the domain model changes. It traverses every domain element’s satisfies list, aggregates the referenced requirement IDs, and computes the complement against the declared requirement set. The outcome is twofold: coverage (every requirement has at least one satisfier) and orphans (every domain element satisfies at least one requirement). A mismatch is a verdict, not a suggestion — the Check loop fails a build if coverage of must priorities is incomplete.
Check is also where conflict detection runs at the requirement level. conflicts-with pairs must carry a documented resolution strategy in their rationale; the absence of one is a Check-time error.
Example:
If REQ-ORD-004 (the unwanted stockout requirement, priority must) has no satisfies reference on any operation, policy, or service, the Check loop fails with a coverage gap. If a service recomputeLoyaltyPoints has satisfies [], the Check loop emits an orphan warning and prompts the modeler to either delete it or add a requirement.
Observe (runtime → intent)
The Observe loop is the only one that touches production. It consumes event streams — domain events, audit records, trace spans — and matches them against requirements. Two EARS patterns make Observe possible:
- Event-driven requirements declare
When <trigger>, the system shall <response>. The observer listens for the trigger and verifies the response occurred (typically by matching an emitted event or state transition within a deadline). - Unwanted requirements declare
If <condition>, then the system shall <response>. The observer listens for the condition and verifies the compensating response occurred.
Requirements that are ubiquitous, state-driven, or optional are less directly observable — they are structural invariants, lifecycle guards, or feature flags. They are checked by the Check loop instead.
Example:
For REQ-ORD-002 ("When a customer submits an order, the system shall create the order in draft status and emit an OrderPlaced event."), the observer watches SubmitOrder commands in the event log and verifies an OrderPlaced event follows within the configured deadline. A missing OrderPlaced event is a drift signal — intent declares it should fire; runtime shows it did not.
For REQ-ORD-004 ("If the ordered product is out of stock, then the system shall reject the order and notify the customer."), the observer watches StockCheckFailed records and verifies both an OrderRejected outcome and a CustomerNotified event. A StockCheckFailed with no follow-up rejection is a drift signal — unhandled error condition.
Cross-cutting NFRs are the primary targets of the Observe loop: availability SLAs are monitored via uptime dashboards, latency budgets are tracked via distributed tracing, and compliance obligations are verified via periodic audits. See Non-Functional Requirements for the cross-cutting loop table.
Governance, not Replacement
The requirement layer does not replace the domain model. It governs it. The domain model remains the structural and behavioral specification — aggregates, entities, events, operations, services, policies. Requirements declare why each element must exist and what obligation it fulfills. Take the requirement layer away and the domain model still runs — but you lose the ability to detect drift, the ability to answer why is this here?, and the ability to prove that a change has not broken an unstated assumption.
Example:
Deleting REQ-ORD-001 does not delete the quantity-floor validation in code. It deletes the stated reason for the validation. The next modeler, seeing a validation with no satisfies, may treat it as an orphan and remove it — silently re-introducing the regression the original requirement was written to prevent. The loops are how that story stops being told in hindsight.