Skip to content
JacqOS
Get Started

Fixtures and Invariants

Overview

Section titled “Overview”

Fixtures and invariants are the two verification surfaces that let you trust AI-generated rules without reading them.

  • Golden fixtures are deterministic scenarios: “given these observations, produce these exact facts.”
  • Invariants are universal constraints: “no matter what observations arrive, this must hold.”

Together they answer both questions a developer needs answered: “does it do the right thing?” and “does it never do the wrong thing?”

This guide walks through defining both, running verification, and using counterexample shrinking to drive the AI feedback loop. All examples use the appointment-booking app.

Fixture Format

Section titled “Fixture Format”

Fixtures are JSONL files in your app’s fixtures/ directory. Each line is an observation that enters the system. The expected world state lives beside the fixture as <fixture-stem>.expected.json. See Golden Fixtures for the digest-backed evidence model.

{"kind":"slot.status","payload":{"slot_id":"slot-42","state":"listed"}}
{"kind":"booking.request","payload":{"request_id":"req-1","email":"pat@example.com","slot_id":"slot-42"}}
{"kind":"reservation.result","payload":{"result":"succeeded","request_id":"req-1","slot_id":"slot-42"}}
{"kind":"confirmation.result","payload":{"result":"sent","request_id":"req-1"}}

Each observation has:

FieldPurpose
kindObservation type — matches your mapper’s routing
payloadArbitrary JSON body — your mapper extracts atoms from this

Observations are replayed in order. The evaluator processes each one through your mapper (producing atoms), then re-evaluates the ontology to a fixed point before processing the next.

The matching expectation file uses the derived world-state shape:

{
  "facts": [
    {
      "relation": "booking_confirmed",
      "value": ["req-1", "slot-42"]
    }
  ],
  "intents": [
    {
      "relation": "intent.send_confirmation",
      "value": ["req-1", "pat@example.com", "slot-42"]
    }
  ],
  "contradictions": [],
  "invariant_violations": []
}

The expected file is exact. If the evaluator derives a fact or intent that is not listed, verification reports it as unexpected. If it fails to derive a listed tuple, verification reports it as missing and includes why-not provenance when the ontology can explain the missing rule path.

Fixture Authoring Loop

Section titled “Fixture Authoring Loop”

Start new scenarios from a template:

Terminal window
jacqos fixture template happy-path first-booking
jacqos fixture template contradiction-path double-booking
jacqos fixture template policy-bypass refund-threshold
jacqos fixture template human-review clinical-escalation
jacqos fixture template multi-agent incident-triage

Each command writes a fixture and a matching .expected.json skeleton. The observations are placeholders; replace them with domain observations your mapper understands. The skeleton gives your AI coding agent a concrete target: fill the exact expected facts, intents, contradictions, and invariant violations, then iterate until jacqos verify passes.

When verification fails, review the expected-world diff in the persona you need:

Terminal window
jacqos fixture review fixtures/refund-threshold.jsonl --persona developer
jacqos fixture review fixtures/refund-threshold.jsonl --persona risk-leader
jacqos fixture review fixtures/refund-threshold.jsonl --persona auditor

The developer report focuses on missing and unexpected tuples. The risk-leader report frames the same evidence as policy and contradiction-path coverage. The auditor report records the verification bundle, evaluator digest, and expected-world digest so the reviewed behavior can be reproduced later.

Defining Happy-Path Fixtures

Section titled “Defining Happy-Path Fixtures”

A happy-path fixture proves the system does the right thing when everything goes well. Start with the simplest successful scenario for your domain.

For appointment booking, the happy path is: a slot exists, a patient requests it, the reservation succeeds, and confirmation is sent.

Create fixtures/happy-path.jsonl:

{"kind":"slot.status","payload":{"slot_id":"slot-42","state":"listed"}}
{"kind":"booking.request","payload":{"request_id":"req-1","email":"pat@example.com","slot_id":"slot-42"}}
{"kind":"reservation.result","payload":{"result":"succeeded","request_id":"req-1","slot_id":"slot-42"}}
{"kind":"confirmation.result","payload":{"result":"sent","request_id":"req-1"}}

Then add fixtures/happy-path.expected.json — the facts and intents the evaluator must derive after replaying all observations:

{
  "facts": [
    {
      "relation": "booking_confirmed",
      "value": ["req-1", "slot-42"]
    },
    {
      "relation": "booking_status",
      "value": ["req-1", "confirmed"]
    },
    {
      "relation": "confirmation_sent",
      "value": ["req-1"]
    }
  ],
  "intents": [
    {
      "relation": "intent.reserve_slot",
      "value": ["req-1", "slot-42"]
    },
    {
      "relation": "intent.send_confirmation",
      "value": ["req-1", "pat@example.com", "slot-42"]
    }
  ],
  "contradictions": [],
  "invariant_violations": []
}

Expectations can assert:

  • facts — facts that must exist in the final world state
  • intents — intents that must have been derived
  • contradictions — contradictions that must remain visible
  • invariant_violations — invariant failures that are expected for a negative fixture

To assert that something must not exist, omit it from the expected file. jacqos verify compares the entire derived world and reports any extra tuple as unexpected.

Defining Contradiction-Path Fixtures

Section titled “Defining Contradiction-Path Fixtures”

Contradiction-path fixtures prove the system handles conflicts and failures correctly. These are not optional — every app should ship them.

Common contradiction scenarios:

  • Two requests for the same resource
  • A cancellation mid-flow
  • An LLM extraction that contradicts existing facts
  • An effect that fails after an intent fires

Double-Booking Attempt

Section titled “Double-Booking Attempt”

Create fixtures/double-booking-path.jsonl:

{"kind":"slot.status","payload":{"slot_id":"slot-42","state":"listed"}}
{"kind":"booking.request","payload":{"request_id":"req-1","email":"alice@example.com","slot_id":"slot-42"}}
{"kind":"booking.request","payload":{"request_id":"req-2","email":"bob@example.com","slot_id":"slot-42"}}
{"kind":"reservation.result","payload":{"result":"succeeded","request_id":"req-1","slot_id":"slot-42"}}
{"kind":"reservation.result","payload":{"result":"failed","request_id":"req-2","slot_id":"slot-42","reason":"slot already held"}}

Expected: only one booking succeeds, the other is rejected, and the no_double_booking invariant holds.

Mid-Flow Cancellation

Section titled “Mid-Flow Cancellation”

Create fixtures/contradiction-path.jsonl:

{"kind":"slot.status","payload":{"slot_id":"slot-42","state":"listed"}}
{"kind":"booking.request","payload":{"request_id":"req-2","email":"cancelled@example.com","slot_id":"slot-42"}}
{"kind":"reservation.result","payload":{"result":"succeeded","request_id":"req-2","slot_id":"slot-42"}}
{"kind":"booking.cancelled","payload":{"request_id":"req-2","slot_id":"slot-42"}}

Expected: the hold is retracted, the slot becomes available again, and no confirmation intent fires for the cancelled request.

Organizing Fixtures

Section titled “Organizing Fixtures”

A typical app has several fixture files covering distinct scenarios:

fixtures/
  happy-path.jsonl              # Normal successful flow
  contradiction-path.jsonl      # Conflicting or cancelled observations
  double-booking-path.jsonl     # Concurrent requests for same resource
  llm-extraction.jsonl          # LLM-assisted intake with candidate facts
  error-recovery.jsonl          # Effect failures and retries

Each fixture is self-contained — it replays from scratch on a clean database. Fixtures do not depend on each other.

Contradiction Coverage Checklist

Section titled “Contradiction Coverage Checklist”

For every invariant-backed trust claim, keep at least one fixture that tries to break it. A useful contradiction-path corpus usually covers:

  • Conflicting evidence — two observations assert incompatible states for the same entity.
  • Stale evidence — a later observation should retract or supersede an earlier fact.
  • Unsafe proposal — a proposal.* relation is present but no domain decision ratifies it.
  • Missing review — a sensitive proposal lacks the required reviewer role, quorum, expiry, or review digest binding.
  • Effect ambiguity — an effect attempt reaches a state that requires explicit reconciliation instead of silent retry.
  • Policy denial — the ontology can explain why the action did not fire, not only that it did not fire.

Use jacqos fixture template contradiction-path, policy-bypass, or human-review to start these scenarios, then replace the placeholder observations with domain evidence.

Declaring Invariants in .dh

Section titled “Declaring Invariants in .dh”

Invariants are integrity constraints declared in your ontology that must hold after every evaluation fixed point. They use the same syntax as derivation rules but express constraints rather than derivations.

The body of an invariant is a query over the parameter domain. The evaluator computes every binding of the invariant’s free variables that appears in the current state and checks that the body succeeds for each one. If the body fails for any binding in the domain, the invariant is violated and the transition that produced that state is rejected. Read every invariant body as “for every binding I declare, this query must always hold.” See Invariant Review for the deep dive on this semantics, including the common “must always hold” vs. “must never hold” framing trap.

Cardinality Constraints

Section titled “Cardinality Constraints”

Prevent impossible states by bounding how many times a relation can hold for a given key:

-- No slot should ever be double-booked
invariant no_double_booking(slot) :-
  count booking_confirmed(_, slot) <= 1.


-- No slot should have multiple active holds
invariant no_double_hold(slot) :-
  count slot_hold_active(_, slot) <= 1.


-- A request can only reach one terminal state
invariant one_terminal_outcome(req) :-
  count booking_terminal(req) <= 1.

Data Integrity Constraints

Section titled “Data Integrity Constraints”

Ensure derived facts satisfy expected relationships:

-- Every confirmed booking must have a valid email
invariant confirmed_has_email(req) :-
  booking_confirmed(req, _),
  booking_request(req, email, _),
  email != "".


-- No intent should fire for a cancelled request
invariant no_cancelled_intents(req) :-
  intent.reserve_slot(req, _),
  not booking_cancelled(req, _).

LLM-Derived Fact Constraints

Section titled “LLM-Derived Fact Constraints”

If your app uses LLM-assisted extraction, require that LLM-derived facts pass through candidate acceptance:

-- LLM-derived facts must be accepted through the candidate pipeline
invariant llm_facts_accepted(fact_id) :-
  derived_from_llm(fact_id),
  candidate.accepted(fact_id).

This is a mandatory pattern in JacqOS. The validator rejects, at load time, any rule that derives an accepted fact or executable intent directly from atoms produced by a mapper predicate marked requires_relay without going through the reserved candidate.* or proposal.* relay namespace. This is enforced by the relay-boundary check and is keyed on mapper predicate configuration, not on observation class strings.

Where to Put Invariants

Section titled “Where to Put Invariants”

Invariants go in your .dh ontology files alongside the rules they constrain. A common pattern is to declare them in the same file as the rules they relate to:

ontology/
  schema.dh       # Relation declarations
  rules.dh        # Derivation rules + structural invariants
  intents.dh      # Intent derivation rules + intent invariants

You can also create a dedicated ontology/invariants.dh if your invariant set grows large.

Running jacqos verify

Section titled “Running jacqos verify”

jacqos verify replays every fixture, checks expectations, and exercises all invariants:

Terminal window
$ jacqos verify
Replaying fixtures...
  happy-path.jsonl             PASS  (4 observations, 6 expectations matched)
  contradiction-path.jsonl     PASS  (4 observations, 3 expectations matched)
  double-booking-path.jsonl    PASS  (5 observations, 4 expectations matched)


Checking invariants...
  no_double_hold               PASS  (427 slots evaluated)
  no_double_booking            PASS  (427 slots evaluated)
  one_terminal_outcome         PASS  (89 requests evaluated)


All checks passed. Digest: sha256:a1b2c3d4e5f6...

Each replay is deterministic. The same observations, evaluator, and rules produce the same facts every time. The verification digest is a cryptographic hash covering:

  • Evaluator identity — hash of ontology rules, mapper semantics, and helper digests
  • Fixture corpus — hash of every .jsonl fixture file
  • Derived state — byte-identical facts, intents, and provenance for each fixture

This digest is portable and independently verifiable. It travels with your evaluation package.

Reading Verification Reports

Section titled “Reading Verification Reports”

Fixture Failures

Section titled “Fixture Failures”

When a fixture fails, the report shows exactly what diverged:

Terminal window
$ jacqos verify
Replaying fixtures...
  happy-path.jsonl             FAIL


  Expected: booking_confirmed("req-1", "slot-42")
  Got:      (not derived)


  Missing facts: 1
  Unexpected facts: 0


  Hint: rule rules.dh:23 did not fire.
  Provenance: no atom matched booking_request(_, "slot-42", _)

The report tells you:

  • Which expectation failed — the exact fact or intent that was expected but not derived (or derived but not expected)
  • Which rule didn’t fire — the specific rule and line number
  • Provenance hint — what atom or condition was missing

This is your first debugging surface. Most fixture failures are mapper issues (observations not producing the right atoms) or rule issues (conditions not matching).

Invariant Violations

Section titled “Invariant Violations”

When an invariant is violated during fixture replay:

Terminal window
Checking invariants...
  no_double_booking            FAIL


  Violation at fixture: double-booking-path.jsonl, after observation #4
  Counterexample: booking_confirmed("req-1", "slot-42")
                  booking_confirmed("req-2", "slot-42")


  Invariant no_double_booking requires:
    count booking_confirmed(_, "slot-42") <= 1
  Actual count: 2

The report identifies the exact fixture, the observation that triggered the violation, and the concrete values that broke the constraint.

Counterexample Shrinking

Section titled “Counterexample Shrinking”

Beyond replaying defined fixtures, jacqos verify also generates observation sequences to search for invariant violations you haven’t thought of. This is property testing applied to your ontology.

When a generated sequence breaks an invariant, the verifier shrinks it to the smallest reproduction:

Terminal window
$ jacqos verify
Property testing invariants...
  no_cancelled_intents         FAIL


  Counterexample found for no_cancelled_intents:
    Shrunk to 3 observations (from 47):
      1. booking.request  {email: "a@b.co", slot_id: "s1"}
      2. booking.cancel   {request_id: "req_1"}
      3. slot.released    {slot_id: "s1"}


    Violation: intent.reserve_slot("req_1", "s1") derived
      but request_cancelled("req_1") is true.


    Provenance: rule intents.dh:14 fired on atoms from obs #3,
      but did not check cancellation status.

A generated sequence might contain 47 observations. The shrunk counterexample is 3. The shrunk counterexample includes:

  • The invariant that was violated
  • The minimal observation sequence that triggers it
  • The provenance chain showing exactly which rule and observation caused it

The Shrinking Workflow

Section titled “The Shrinking Workflow”
  1. jacqos verify finds a counterexample — a generated sequence that breaks an invariant
  2. The verifier shrinks it — removes observations until the minimal reproduction remains
  3. You review the counterexample — understand why this sequence should not violate the invariant
  4. Promote it as a fixture — the shrunk counterexample becomes a checked-in regression fixture
  5. Tell the AI to fix it — the AI iterates on the rules until the new fixture passes and all invariants hold
Terminal window
# Shrink the failing generated fixture
$ jacqos shrink-fixture fixtures/generated-no_cancelled_intents.jsonl \
    --output generated/shrunk-fixtures/no_cancelled_intents.jsonl


# Promote the shrunk sequence into the checked-in fixture corpus
$ jacqos fixture promote-counterexample \
    generated/shrunk-fixtures/no_cancelled_intents.jsonl \
    counter-no-cancelled-intents \
    --output fixtures/counter-no_cancelled_intents-001.jsonl


# Replay to confirm the failure
$ jacqos replay fixtures/counter-no_cancelled_intents-001.jsonl


# Review the expected-world diff before editing the ontology
$ jacqos fixture review fixtures/counter-no_cancelled_intents-001.jsonl \
    --persona developer


# After AI fixes the rules, verify everything again
$ jacqos verify
All checks passed. Digest: sha256:f6e5d4c3b2a1...

Each shrunk counterexample is a new test case that your fixture corpus didn’t cover. Over time, your fixture directory grows to reflect every edge case the property tester has found.

Worked Example: Appointment Booking

Section titled “Worked Example: Appointment Booking”

Let’s walk through the full verification workflow for the appointment-booking app.

Step 1: Define the Schema

Section titled “Step 1: Define the Schema”

In ontology/schema.dh, declare the relations your app uses:

relation booking_request(request_id: text, patient_email: text, slot_id: text)
relation slot_listed(slot_id: text)
relation slot_available(slot_id: text)
relation slot_hold_active(request_id: text, slot_id: text)
relation booking_confirmed(request_id: text, slot_id: text)
relation booking_cancelled(request_id: text, slot_id: text)
relation booking_rejected(request_id: text, slot_id: text, reason: text)
relation booking_terminal(request_id: text)
relation booking_status(request_id: text, status: text)

Step 2: Declare Invariants

Section titled “Step 2: Declare Invariants”

In ontology/rules.dh, alongside your derivation rules, declare what must always be true:

-- No slot should have multiple active holds
invariant no_double_hold(slot) :-
  count slot_hold_active(_, slot) <= 1.


-- No slot should ever be double-booked
invariant no_double_booking(slot) :-
  count booking_confirmed(_, slot) <= 1.


-- A request can only reach one terminal state
invariant one_terminal_outcome(req) :-
  count booking_terminal(req) <= 1.

These are short, declarative, and express domain intent. A domain expert can read them and judge whether they capture the right business rules — without understanding the derivation rules.

Step 3: Write Fixtures

Section titled “Step 3: Write Fixtures”

Create the happy path (fixtures/happy-path.jsonl):

{"kind":"slot.status","payload":{"slot_id":"slot-42","state":"listed"}}
{"kind":"booking.request","payload":{"request_id":"req-1","email":"pat@example.com","slot_id":"slot-42"}}
{"kind":"reservation.result","payload":{"result":"succeeded","request_id":"req-1","slot_id":"slot-42"}}
{"kind":"confirmation.result","payload":{"result":"sent","request_id":"req-1"}}

Create the contradiction path (fixtures/contradiction-path.jsonl):

{"kind":"slot.status","payload":{"slot_id":"slot-42","state":"listed"}}
{"kind":"booking.request","payload":{"request_id":"req-2","email":"cancelled@example.com","slot_id":"slot-42"}}
{"kind":"reservation.result","payload":{"result":"succeeded","request_id":"req-2","slot_id":"slot-42"}}
{"kind":"booking.cancelled","payload":{"request_id":"req-2","slot_id":"slot-42"}}

Create the double-booking path (fixtures/double-booking-path.jsonl):

{"kind":"slot.status","payload":{"slot_id":"slot-42","state":"listed"}}
{"kind":"booking.request","payload":{"request_id":"req-1","email":"alice@example.com","slot_id":"slot-42"}}
{"kind":"booking.request","payload":{"request_id":"req-2","email":"bob@example.com","slot_id":"slot-42"}}
{"kind":"reservation.result","payload":{"result":"succeeded","request_id":"req-1","slot_id":"slot-42"}}
{"kind":"reservation.result","payload":{"result":"failed","request_id":"req-2","slot_id":"slot-42","reason":"slot already held"}}

Step 4: Run Verification

Section titled “Step 4: Run Verification”
Terminal window
$ jacqos verify
Replaying fixtures...
  happy-path.jsonl             PASS  (4 observations)
  contradiction-path.jsonl     PASS  (4 observations)
  double-booking-path.jsonl    PASS  (5 observations)


Checking invariants...
  no_double_hold               PASS
  no_double_booking            PASS
  one_terminal_outcome         PASS


Property testing invariants...
  no_double_hold               PASS  (2,500 generated sequences)
  no_double_booking            PASS  (2,500 generated sequences)
  one_terminal_outcome         PASS  (2,500 generated sequences)


All checks passed. Digest: sha256:a1b2c3d4e5f6...

Step 5: Iterate

Section titled “Step 5: Iterate”

If jacqos verify finds a counterexample, the workflow is:

  1. Review the shrunk counterexample — understand the scenario
  2. Decide if the invariant is correct (it usually is)
  3. Promote the counterexample with jacqos fixture promote-counterexample <shrunk-fixture> counter-<name> --output fixtures/counter-<name>.jsonl
  4. Review the expected-world diff with jacqos fixture review <fixture> --persona developer
  5. Have the AI regenerate the rules until all fixtures pass and all invariants hold
  6. Run jacqos verify again

You review invariants and counterexamples. The AI writes and rewrites the rules. The evaluator proves correctness. Nobody reads the generated Datalog.

Next Steps

Section titled “Next Steps”