# Running TLA+ Specs — Hazmat

## Tooling

| Tool | Purpose | Install |
|------|---------|---------|
| `tla2tools.jar` | TLC model checker — finds invariant violations by exhaustive state exploration | `curl -L https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar -o ~/workspace/tla2tools.jar` |
| Java 17+ | Runtime for TLC | `brew install --cask temurin` (or download from adoptium.net) |

**Installed location:** `~/workspace/tla2tools.jar`

Verify:
```bash
cd tla/
./run_tlc.sh -help | head -3
```

`run_tlc.sh` resolves a real Java binary before invoking TLC. This matters on
macOS hosts where `java` or `/usr/bin/java` may be the Apple launcher stub
instead of an installed JDK.

If your shell exports `JAVA_HOME=/usr`, that is the same launcher stub, not a
usable JDK for TLC. `run_tlc.sh` ignores it and keeps searching.

If auto-detection misses your JDK, set one of:

```bash
JAVA_BIN=/path/to/java ./run_tlc.sh -help
JAVA_HOME=/path/to/jdk ./run_tlc.sh -help
TLA2TOOLS_JAR=/path/to/tla2tools.jar ./run_tlc.sh -help
```

---

## Spec File Structure

Each problem description maps to two files:

```
tla/
  MC_SetupRollback.tla    # the spec (variables, actions, properties)
  MC_SetupRollback.cfg    # model configuration (bounds, what to check)
```

---

## Running TLC

### Run the verified suite
```bash
cd tla/
bash check_suite.sh
```

To keep per-spec TLC logs for regression comparison:

```bash
cd tla/
TLC_LOG_DIR=/tmp/hazmat-tlc-logs bash check_suite.sh
```

### Audit proof inventory and metrics
```bash
cd tla/
bash proof_audit.sh
bash proof_audit.sh --fail-on-drift
bash proof_audit.sh --log-dir /tmp/hazmat-tlc-logs
```

The audit reports the promoted `MC_*` suite, checked invariants/properties from
each `.cfg`, source/gzip sizes, local ignored TLC trace artifacts, tool
versions, and generated/distinct/depth counters when TLC logs are available.
Use it before and after structural refactors so source cleanup is compared
against proof behavior, not just bytes. Use `--fail-on-drift` when the audit
should exit non-zero for canonical roster, promoted-suite, `.tla`, or `.cfg`
inventory drift, as CI does in the fast proof-hygiene tier.

`promoted_specs.tsv` is the checked-in canonical roster for the promoted suite.
It records the expected `MC_*` specs and whether each one needs liveness flags.
`proof_audit.sh --fail-on-drift` and `proof_ownership_check.sh` both compare
this roster against `check_suite.sh`; removing a spec from the live suite or
changing a liveness setting must be an explicit roster change.

### Check proof ownership
```bash
cd tla/
bash proof_ownership_check.sh
```

`proof_ownership.tsv` maps every checked invariant/property to its owning
`VERIFIED.md` section and companion design note. Update it whenever a `.cfg`
adds, removes, or renames an invariant/property.

### Check trace artifact policy
```bash
cd tla/
bash trace_artifact_check.sh
```

Raw TLC `_TTrace_` files and `tla/states/` are local generated output, not proof
source. See `TRACE_ARTIFACTS.md` for the retention policy.

### CI proof tiers

CI intentionally splits TLA+ proof work into a fast hygiene tier and a deep TLC
tier.

- `TLA+ proof hygiene` runs `proof_ownership_check.sh`,
  `trace_artifact_check.sh`, and `proof_audit.sh --fail-on-drift`. This tier
  fails quickly on canonical-roster, promoted-suite, `.cfg`, ownership-ledger,
  design-note, or generated-artifact drift before the expensive model-checking
  job starts.
- `TLA+ model checking` still runs `check_suite.sh` against every promoted
  `MC_*.tla` / `MC_*.cfg` pair and uploads per-spec TLC logs plus parsed audit
  metrics. Do not remove a promoted spec, invariant, property, or liveness flag
  from `check_suite.sh` to make the fast tier pass.

Decision record: the 2026-06-04 GitHub Actions baseline for run
`26942387327` completed the TLA+ job in about 24 minutes, with the verified TLC
suite step taking about 23m52s. The tier split is for earlier drift feedback and
clearer status ownership; it is not a reduction in mandatory promoted-spec TLC
coverage.

### Check one spec (safety)
```bash
cd tla/
./run_tlc.sh \
  -workers auto \
  -config MC_SetupRollback.cfg \
  MC_SetupRollback.tla
```

### Check one spec with liveness properties
```bash
cd tla/
./run_tlc.sh \
  -workers auto \
  -lncheck final \
  -config MC_SetupRollback.cfg \
  MC_SetupRollback.tla
```

### Key flags

| Flag | Meaning |
|------|---------|
| `-workers auto` | Use all CPU cores |
| `-deadlock` | Check for deadlock (no enabled actions) — on by default |
| `-lncheck final` | Check liveness at the end of each trace (faster) |
| `-config <file>` | Model configuration |
| `-metadir /tmp/tlc` | Write state files to a temp dir (keep working dir clean) |
| `-dump dot <file>` | Export state graph as Graphviz dot |
| `-terse` | Less verbose output |

---

## Reading TLC Output

### Success
```
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states ...
X states generated, Y distinct states found, Z states left on queue.
```

### Invariant violation (safety)
```
Error: Invariant AgentContained is violated.

The behavior up to this point is:
1: <Initial predicate>
   agentUser = FALSE, sudoers = FALSE, pfAnchor = FALSE ...

2: <BeginSetup line ...>
   phase = "setting_up", setupStep = 0 ...

3: ...
```

The numbered trace is the **counterexample**. Read bottom-up from the violation.

### Deadlock
```
Error: Deadlock reached.
```
All variables are in a state where no action in `Next` is enabled. Usually
means the spec is incomplete (forgot an action or exhausted attempt bounds).

---

## Problem-Specific Configs

### 01 — Setup/Rollback State Machine
```cfg
SPECIFICATION Spec
CONSTANTS
    MaxSetupAttempts    = 2
    MaxRollbackAttempts = 2
INVARIANTS
    TypeOK
    AgentContained
    NoOrphanedArtifacts
    SudoersRequiresHelper
    AgentDepsRequireUser
PROPERTIES
    CanAlwaysReachClean
```
Expected: No error has been found.

---

## Agentic Workflow

TLC exits `0` on success and non-zero on any error or violation.

```bash
if ./run_tlc.sh \
      -workers auto -terse \
      -config MC.cfg MC.tla 2>&1 | tee /tmp/tlc_out.txt; then
  echo "PASS: no violations found"
else
  echo "FAIL: see /tmp/tlc_out.txt for counterexample"
  grep -A 30 "Error:" /tmp/tlc_out.txt
fi
```

---

## State Space Sizes (Reference)

Reference values below come from GitHub Actions run `26945272162`, where the
TLA+ proof hygiene job completed in 7s and the deep model-checking job completed
in about 24m31s. The table is advisory; CI gates proof inventory and TLC
success, not exact byte or runtime values.

| Problem | Model Bounds | Observed Distinct States | Runtime |
|---------|-------------|--------------------------|---------|
| 01 Setup/Rollback | 2 setup attempts, 2 rollback attempts | 35,005 | 03s with `-lncheck final` |
| 02 Seatbelt Policy | Credential/read/temp/network policy choices | 12,672 | 02s |
| 03 Backup Safety | 3 snapshots, 2 sessions, 2 restores | 395 | 00s with `-lncheck final` |
| 04 Version Migration | 3 versions, rollback from any state | 72,442 | 04s with `-lncheck final` |
| 05 Tier 3 Launch Containment | Project/read planning, env, backend, approval, shell/version gates | 23,580 | 01s |
| 06 Tier 2 vs Tier 3 Policy Equivalence | Tier 2/Tier 3 project/read/write/network/resume choices | 327,680 | 19s |
| 07 Session Permission Repairs | Native/docker repair planning, preview/launch/rollback phases | 13,268 | 00s |
| 08 Harness Lifecycle | 7 harnesses, import/save/dry-run/rollback variants | 633,107 | 24s |
| 09 Launch FD Isolation | 2 inherited-fd classes, helper cleanup toggle, exec boundary phases | 112 | 00s |
| 10 Git-SSH Routing | 2 hosts, 2 keys, sockets, profiles, profile/inline identity variants | 1,990,656 | 09s |
| 11 Git Hook Approval | 3 hook types, 2 bundle hashes, wrapper/dispatcher/install/drift lifecycle | 2,179,200 | 59s |
| 12 Secret Store Recovery | 2 harnesses, 2 secret values, crash/restart recovery phases | 10,870 | 01s |
| 13 Credential Capability Lifecycle | 5 harnesses, 9 credentials, 2 values, registry delivery classes | 8,351,181 | 22min 11s |
| 14 Linux Native Launch | 1024 launch/capability input combinations and linear launch stages | 2,842 | 00s |

If TLC runs materially longer than the reference runtime for the spec you are
changing, run that spec in isolation and compare generated/distinct/depth counts
before widening the model.
