Invariants

Invariants are declared in YAML under invariants/, a path protected by CODEOWNERS. load_invariants("invariants") loads every *.yaml and *.yml file in the directory and rejects duplicate ids. Each invariant has an id, a version, a kind, params, and required_signals, which are event kinds that must be present for a verdict. When a required signal is absent, the result is UNKNOWN. For the model behind them, see Concepts: Invariants.

A scenario names the invariants it checks by default under invariants:. Adding a file doesn't change what an existing scenario evaluates. To change what an invariant means, bump its version. The kernel records invariant_version with every verdict it recomputes.

Generated

The tables below are generated by scripts/build_docs.py from invariants/*.yaml.

invariants/core.yaml

Id	Kind	Version	Required signals	What it checks
epistemic.no_future_knowledge	epistemic	1.0	none	Information-state separation. No role view holds an event received before its event_time_ns, and no decision cites a known_event_id that its actor's role had not received by at_ns. FAIL witness: offending view event ids, then each offending decision id followed by the ids it cited prematurely.
epistemic.label_isolation	epistemic	1.0	none	Role coast_guard never receives an event carrying policy label harbour_private. FAIL witness: the labelled event ids present in that role's view.
response.alert_ack	response	1.0	alert	G(alert -> F<=within_ns acknowledged) inside the harbour_ops view: every received alert is followed, within within_ns of its receipt, by an ack whose payload.acks is the alert id. FAIL witness: [alert id, latest event the role received before the deadline].
absence.no_corrupted_in_decision	absence	1.0	decision	No decision's known_event_ids includes a corrupted event (quality == 0.0 or provenance that cites the event itself, the marker set by interventions.corrupt). FAIL witness: [decision id, corrupted event id].
decision.consistent_with_truth	decision	1.0	decision	Each recorded decision equals the option its rule yields when evaluated over truth as of at_ns. A mismatch means stale or missing information caused a wrong decision. FAIL witness: truth events at or before at_ns that the actor's role had not received at at_ns, in canonical order. UNKNOWN (decision_rule_evaluator) when no scenario or evaluate_rule callable is supplied.
always.non_negative_capacity	always	1.0	none	State predicate over truth: no truth event reports payload.capacity below zero. UNKNOWN when no truth event carries payload.capacity. FAIL witness: the first offending truth event.

invariants/extended.yaml

Id	Kind	Version	Required signals	What it checks
latency.bound	latency	1.0	none	Every correction reaches harbour_ops within bound_ns of its event_time (received_time_ns - event_time_ns <= bound_ns). FAIL witness: every offending event id in canonical order. UNKNOWN when the role has no view or never received that kind.
ordering.causal	ordering	1.0	none	If event B references event A through a payload link field (corrects, acks, acknowledges, in_reply_to), every role receives A (or a copy of A) no later than B. Checked in every role view. FAIL witness: [A, B] for the first violation in receipt order. UNKNOWN when no view event carries a link field that resolves to a truth event.
duplicate.suppressed	duplicate	1.0	none	No decision's known_event_ids contains two copies of the same origin event (origin = id before '#dup', else the first provenance id, else the id). This is the duplicate-delivery mechanism random exploration found on port_alert. FAIL witness: [decision id, copy ids...] for the first duplicated origin. UNKNOWN when the trace has no decisions.
quorum.independent_sources	quorum	1.0	none	A duty_officer escalate rests on at least two distinct source_ids among the known, uncorrected sightings with confidence >= 0.6. FAIL witness: [decision id, supporting event ids...]; the explanation names the distinct sources counted. PASS when no decision chose the option. UNKNOWN when the trace has no matching decisions.
decision.fault_attributed	decision	1.0	decision	Same verdict as decision.consistent_with_truth. With a reference trace (check(..., reference=root_trace)) the FAIL witness is only the truth events missing at decision time in this trace but received in the reference: the information the fault took away. Without a reference the witness lists all missing information and the explanation says so. UNKNOWN (decision_rule_evaluator) when no evaluator is supplied.
epistemic.permitted_only	epistemic	1.0	none	Approximation of non-interference: no decision's known_event_ids includes an event whose policy_labels its actor's role may not see under the scenario's role visibility. FAIL witness: [decision id, offending event ids...]. UNKNOWN (scenario) without a scenario, (decision) without decisions, or (role:/event:) when a role or cited event cannot be resolved.

Parameters, witnesses and worked examples for each invariant are in the Invariant catalogue.

File shape

invariants:
  - id: response.alert_ack
    version: "1.0"
    kind: response
    description: >
      G(alert -> F<=within_ns acknowledged) inside the harbour_ops view ...
    params:
      role: harbour_ops
      trigger_kind: alert
      response_kind: ack
      within_ns: 300000000000
      link_field: acknowledges
    required_signals: [alert]

Verdict record

Each check returns a VerdictRecord with these fields: invariant_id, invariant_version, result (PASS, FAIL, or UNKNOWN), witness[], explanation, missing_data[], derived_at_ns (evaluator time, separate from event time), and trace_digest. The CLI writes them to verdicts/<trace>.json.