A Property is a verifiable claim about the domain model. It says something must hold — about state, about a transition, about a contract between an operation’s input and output, or about a truth that spans aggregates. The metamodel collects these claims in one place because together they form the verifiable surface of the model: the precise things a property-based test can generate inputs for, simulate state through, and check assertions against.

This page covers state-predicate properties (invariants, agreements), behavior-constraining properties that live on operations (preconditions, postconditions), lifecycle properties that live on entities (state-machine constraints), and the cross-aggregate enforcement mechanisms that maintain agreements at runtime (reconciliation and its escalation chain).

Properties as the verifiable surface

Every property in this section is a candidate for property-based testing. The pattern is the same in every case:

1. The model declares the property — what must hold and over what scope.
2. A generator produces arbitrary valid inputs (commands, state, time progression).
3. The system runs.
4. The assertion checks the property after each operation, after each event, or at every observable point.

The metamodel makes that workflow tractable because every property has an explicit predicate and a scope. There is no buried business rule for the test generator to discover — the contract is declared on the operation, the entity, or the aggregate. A property-based test can enumerate the operations on an aggregate, generate valid argument values, and check the invariants after every call. It can drive an entity through every state machine transition and check the state-scoped invariants at every step. It can simulate two aggregates running concurrently and check that an agreement holds within its declared inconsistency window.

Properties are not just rules for humans to read. They are executable claims that can be checked continuously against the system as it evolves.

Invariant — synchronous state predicate

An Invariant is a safety property: a named boolean expression over state that must evaluate to true at every observable point. It is synchronous, checked at a specific point in time, and scoped to a single aggregate, entity, or state.

Every invariant declares one of three enforcement strategies:

• Rejection — the operation is refused and no state change occurs. The most common choice. The operation emits an error event tied to the violated invariant.
• Compensation — the state change is accepted and a corrective command is issued afterward. Used when rejecting would be worse than letting the change happen and fixing it.
• Alert — the violation is recorded for review. No rejection, no compensation — the system flags the anomaly and keeps going. Used for soft rules where human judgment decides the response.

Invariants split by scope:

• An entity-level invariant must hold across all states of the entity’s lifecycle.
• A state-scoped invariant must hold only while the entity occupies that specific state.

State-scoped invariants are implicitly conjoined with entity-level invariants — both must hold simultaneously while the entity is in that state.

Example:

invariant orderTotalMatchesLines {
  satisfies [REQ-ORD-003]
  scope: aggregate Order
  predicate: order.total == sum(order.lines.map(l => l.amount))
  enforcement: rejection
}

invariant creditLimitNotExceeded {
  satisfies [REQ-CRED-001]
  scope: aggregate Customer
  predicate: customer.outstanding <= customer.creditLimit
  enforcement: compensation
  compensatingCommand: SuspendCustomer
}

orderTotalMatchesLines rejects any addLine or removeLine that would break the sum. creditLimitNotExceeded uses compensation because rejecting the transaction might leave the customer mid-checkout; the system accepts the order and then issues a SuspendCustomer command.

As a verifiable property. A property-based test enumerates the operations on the aggregate, generates valid arguments, runs each operation in isolation and in sequences, and asserts the invariant predicate after every commit. A failing test produces the minimal command sequence that violates the invariant.

Agreement — cross-aggregate predicate

An Agreement is a property that spans multiple aggregates within the same bounded context, or across bounded contexts. Unlike an invariant — guaranteed atomically within one aggregate — an agreement expresses a truth that no single transaction can verify alone. The system commits to maintaining the agreement through coordination rather than synchronous enforcement.

An agreement has:

• Name — anchored in the ubiquitous language.
• Predicate — an expression over the combined observable state of the participants.
• Participants — the list of aggregates whose states are involved.

Agreements are either bilateral (exactly two aggregates) or multilateral (N aggregates must collectively satisfy the predicate). Multilateral agreements are substantially harder to reconcile because a violation is caused by the collective — no individual state change is “the” cause.

Every agreement accepts an inconsistency window: the predicate may be temporarily violated between a participant’s state change and the moment reconciliation detects and resolves it. The window must be explicit and acceptable to domain experts. Hiding it is how distributed systems lie about consistency.

Every agreement is maintained by exactly one reconciliation.

Example:

agreement weeklyPayoutBalancesCaptures {
  satisfies [REQ-PAY-010]

  participants: [RideCaptures, DriverPayouts]
  predicate: sum(captures.forWeek(w)) == sum(payouts.forWeek(w))
  inconsistencyWindow: up to 6 hours after Sunday 23:59 UTC
  maintained by: weeklyPayoutReconciliation
}

The total amount captured from riders for a week must equal the total paid out to drivers for that week. No single transaction can check it — the agreement is maintained by a weekly reconciliation, with an acceptable six-hour window.

As a verifiable property. A property-based test simulates concurrent participant transactions, lets time advance up to the inconsistency window, and asserts the predicate. A failing test reveals either a missing reconciliation trigger or a window that is too short for real workloads.

Preconditions & Postconditions — operation contracts

Every operation declares preconditions (what must be true before it runs) and postconditions (what must be true about the state transition it performs). They are part of the operation’s contract — not separate concepts, but properties of operations. Their canonical definitions live with operations on Interfaces & Operations.

This page treats them as the behavior-constraining properties of the model — the things every operation guarantees to its caller and the things every caller can rely on without inspecting the operation’s body.

• A precondition is a predicate over the operation’s arguments and (for entity operations) the entity state, evaluated before the operation runs. If it fails, the operation is rejected; the named violation reason becomes the error event the operation emits.
• A postcondition is a predicate over state_before, state_after, and the arguments, evaluated after the operation runs. It is the operation’s promise: if the precondition held, the postcondition will hold.

As verifiable properties. Pre/post pairs are the canonical target of property-based testing. The test generator produces valid arguments that satisfy the precondition, runs the operation, and asserts the postcondition. It also produces arguments that violate the precondition and asserts that the operation rejects with the declared reason. Together these two checks cover the full operation contract.

State-machine constraints — lifecycle properties

A State Machine declares what shape an entity’s lifecycle can legally take. Its canonical definition lives with entities on Structures.

Treated as a property, a state machine is a bundle of related verifiable claims:

• Reachability — the entity always occupies exactly one declared state; every state must be reachable from the start state through some sequence of transitions.
• Transition guards — each transition declares a guard that must hold for the transition to fire; firing a transition whose guard is false is a violation.
• Transition postconditions — each transition declares what must be true about state_before and state_after; the entity always lands in the target state if the transition succeeds.
• State-scoped invariants — every invariant scoped to a state must hold for the entire time the entity occupies that state.
• Termination — once the entity reaches a final state, no further transitions fire.

As verifiable properties. A property-based test drives the entity through random sequences of valid transitions, asserts the state-scoped invariant after every step, and asserts that no transition fires when its guard is false. Random walks across the state graph are particularly effective at finding combinations of transitions the modeler did not anticipate.

Reconciliation — maintaining agreements

A Reconciliation is the mechanism that detects violations of an agreement and drives the system back toward consistency. It is the enforcement counterpart to an agreement, just as rejection/compensation/alert are the counterparts to an invariant predicate.

A reconciliation has:

• Name — e.g., “budget reconciliation”, “capacity reconciliation”, “weekly payout reconciliation”.
• Trigger — what initiates the check. Either an event (reactive — the reconciliation runs each time a relevant participant emits a relevant event) or a schedule (periodic — the reconciliation runs at fixed intervals).
• Detection strategy — how the violation is discovered. Either query-based (evaluate the agreement’s predicate against current participant state) or event-sourced (accumulate events and detect that the sequence has produced a violating state).
• Compensation — one or more commands issued to restore the agreement. Compensation may target any participant.

A reconciliation may be choreographed (each participant reacts to events from the others in a chain, with no central coordinator) or orchestrated (a dedicated process — often called a saga — coordinates the sequence of commands and compensations). The choice is driven by the number of participants and the complexity of compensation: bilateral agreements often work well with choreography; multilateral agreements typically need orchestration.

A reconciliation triggered by events and using choreography is structurally close to a set of cooperating reactions. The distinction is intent: reactions express independent reactive rules; a reconciliation is a coordinated mechanism serving a single agreement. If several reactions exist solely to maintain one cross-aggregate truth, name the agreement and reconciliation explicitly rather than leaving the coordination implicit.

Example:

reconciliation weeklyPayoutReconciliation {
  satisfies [REQ-PAY-010]

  maintains: agreement weeklyPayoutBalancesCaptures

  trigger: schedule "every Monday at 00:00 UTC"   // recurring temporal event
  detection: query-based
  style: orchestrated

  compensation: [
    command IssueMissingPayout(driverId, delta)    // if payouts < captures
    command ClawbackOverpayment(driverId, delta)   // if payouts > captures
  ]

  onFailure: weeklyPayoutEscalation
}

Escalation chain — when reconciliation fails

An Escalation Chain is an ordered sequence of steps that the reconciliation follows when compensation fails. Each step defines a condition under which it activates and an action to take. Steps are evaluated in order — the first step whose condition is met is executed; if that step also fails, the next step is evaluated.

An escalation step has:

• Trigger condition — what determines this step activates: the previous action failed, a timeout elapsed, a maximum retry count was reached.
• Action — one of five choices:
  • Retry — re-execute the original compensation, with a maximum attempt count and backoff.
  • Alternative compensation — issue a different set of commands targeting any participant.
  • Alert — notify a defined role or monitoring system without halting.
  • Suspend — freeze further state changes on the agreement’s participants until resolved.
  • Manual intervention — create a structured work item for human resolution, carrying the full failure context.
• Max attempts — for retry actions only.

An escalation chain must terminate. The final step must be alert, suspend, or manual intervention — never retry or alternative compensation, which could themselves fail indefinitely. This guarantees every reconciliation failure eventually reaches a defined end state rather than looping.

Example:

escalationChain weeklyPayoutEscalation {
  belongs to: reconciliation weeklyPayoutReconciliation

  step 1 retry {
    when: compensation failed
    maxAttempts: 3
    backoff: exponential 5min
  }

  step 2 alternative compensation {
    when: step 1 exhausted
    action: command IssueReserveFundTransfer(delta)
  }

  step 3 suspend {
    when: step 2 failed
    action: freeze driverPayouts for the week
  }

  step 4 manual intervention {
    when: step 3 activated
    action: create work item "weekly payout reconciliation blocked"
    carries: { week, captures, payouts, delta, stepHistory }
  }
}

Four steps, escalating. The chain terminates on manual intervention — a human must resolve what the system could not. That final step is always present in a well-formed chain.