# Attractor formal models

This folder holds formal-verification artifacts for the Attractor
engine. They live alongside `SPEC.md` (top-level prose spec) and are
optional: the project ships and tests fine without them. They exist
for the same reason as the unit tests — to catch state-machine bugs
the code reviewer wouldn't — but at a layer prose can't reach.

## What's here

- **`Attractor.tla`** — TLA+ model of the run lifecycle (SPEC §6,
  §11). Models a small fixed workflow that exercises the
  verify/fixup loop and a human gate; checks four safety invariants
  and one liveness property. See the module header for the modeled
  workflow shape and what the model deliberately abstracts away.
- **`Attractor.cfg`** — TLC configuration: `MaxVerifyVisits = 3`,
  the four invariants, the `EventuallyTerminal` property, and
  `CHECK_DEADLOCK FALSE` (terminal states aren't deadlocks here,
  they're the goal).

## Running the model

You need Java (any recent JRE — TLC ships as a JAR) and the
`tla2tools.jar` from the [TLA+ release page](https://github.com/tlaplus/tlaplus/releases).
The jar is gitignored; download once into this directory:

```bash
curl -fL -o tla2tools.jar \
  https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
```

Then check the spec:

```bash
java -XX:+UseParallelGC -cp tla2tools.jar tlc2.TLC \
  -workers auto Attractor.tla
```

Expected output ends with:

```
Model checking completed. No error has been found.
```

A clean run explores 44 distinct states across a 12-deep state
graph in under a second.

## What's checked

| Property               | Kind       | Source rule          |
| ---------------------- | ---------- | -------------------- |
| `TypeInvariant`        | Safety     | well-typed variables |
| `GoalGatesHonored`     | Safety     | SPEC §6.2 / §16      |
| `MaxVisitsHonored`     | Safety     | SPEC §6.3            |
| `PauseConsistent`      | Safety     | SPEC §11             |
| `EventuallyTerminal`   | Liveness   | SPEC §16 / §6.4      |

## What's not modeled (and why)

- **Mid-node crash + resume (SPEC §6.4 case b).** The engine's
  recovery is "re-enter the same node without changing visit
  count," which from the model's perspective is observably
  identical to a slow dispatch. The interesting properties hold
  either way; modeling the crash separately would multiply the
  state space without proving more.
- **Concurrent runs (§6.5).** v0 executes one workflow per run; the
  model focuses on the single-run state machine.
- **Journal entries as a sequence.** We track the engine's loop
  invariants (current node, visit counts, latest outcomes, pause
  state). The journal is the durable record that lets these be
  reconstructed on resume; modeling it as a literal sequence
  inflates the state space without proving more about the engine
  semantics.
- **Agent-layer setup failures (`AgentError`).** From the
  engine's POV those collapse to a FAILURE outcome — the same
  edge-routing logic the model already exercises on a regular
  verify failure.

## Iterating on the spec

Sanity-check that TLC is actually checking, not silently passing,
by running with the deliberately-broken probe:

```bash
echo 'SPECIFICATION Spec
CONSTANTS MaxVerifyVisits = 3
INVARIANTS GoalGatesHonored_BUGGY
CHECK_DEADLOCK FALSE' > /tmp/Attractor_buggy.cfg

java -XX:+UseParallelGC -cp tla2tools.jar tlc2.TLC \
  -workers auto -config /tmp/Attractor_buggy.cfg Attractor.tla
```

You should see a counter-example trace ending in a state that
violates `GoalGatesHonored_BUGGY` (which asserts `latest[FIXUP] =
SUCCESS` at completion — false on the happy path that bypasses
fixup entirely).

## When to update the model

If you change anything in SPEC §6 (execution model), §11 (human
gates), §6.4 (resume), or any of the routing rules in §6.1, walk
through whether the abstraction in `Attractor.tla` still matches.
The model's job is to formalize what the prose says; if the prose
moves and the model doesn't, the model becomes a lie.

If you add a new node kind or a new outcome type, extend the
`Outcomes`, `Nodes`, and `NextHop` definitions accordingly. Keep
the modeled workflow small — TLC's state space grows fast.