# TLA+ re-check of `KairosDistributed.tla` — 2026-09-06 (Claude)

**Input:** `~/propintel/kairos-signal-main/proofs/KairosDistributed.tla`, sha256 ffdc3ca8… (unmodified; see INPUTS.sha256).
**Checker:** TLC (tla2tools.jar 1.7.4 from github.com/tlaplus/tlaplus releases, sha in INPUTS.sha256), OpenJDK 11.0.32.
**Model (mine — the corpus retains no `.cfg`):** `MaxQueue=3, MaxInFlight=2, NumAssets=2`; `CONSTRAINT StateBound` from
`KairosModel.tla` (wrapper, `EXTENDS KairosDistributed`): `signal_ledger<=6 ∧ dag_version<=4 ∧ each queue<=8`.
Queues are bounded ABOVE `MaxQueue` deliberately so an overflow is observable. The spec's own comments intend
100/8/8, but `signal_ledger`, `dag_version` and `channel_ack` are unbounded in the spec, so any finite check needs a bound.

| # | Property | Kind | Verdict | Evidence |
|---|---|---|---|---|
| S1 | NoDeadlock (`ENABLED(Next)`) | safety | **HOLDS** | one_NoDeadlock.log, 437,472 states; TLC built-in deadlock check also clean (one_dl.log) |
| S2 | QueueBounds | safety | **VIOLATED** | one_QueueBounds.log: `CompleteForwardPass` sets `channel_ack = 4 > MaxQueue` at depth 23 (TypeOK fails the same way) |
| S3 | GPULimit | safety | **HOLDS** | one_GPULimit.log |
| S4 | DAGMonotonic | safety | **HOLDS** | one_DAGMonotonic.log |
| S5 | LedgerAppendOnly | safety | **HOLDS** | one_LedgerAppendOnly.log |
| S6 | SignalConservation | safety | **HOLDS** | one_SignalConservation.log |
| L1 | EventualSignal | liveness | **VIOLATED** | loop `N1Error→N1Recover` with tick_queue=3, ledger=0 |
| L2 | N1Recovery | liveness | **VIOLATED** | loop `N2Error→N2Recover` with n1_state="ERROR" forever |
| L3 | N2Recovery | liveness | **VIOLATED** | loop `N1Error→N1Recover` with n2_state="ERROR" forever |
| L4 | GPUEventuallyIdle | liveness | **VIOLATED** | loop through `ReceiveSignal→N1Error→N1Recover` with gpu_in_flight=1 |

**Are the liveness failures artefacts of the bound?** No. Each TLC counterexample is `Back to state N` over a cycle of real
actions whose states all satisfy the bound, so the cycle is a behaviour of the unconstrained spec. Root cause: `Spec ==
Init ∧ □[Next]_vars ∧ WF_vars(Next)` — weak fairness on the disjunction only guarantees *some* step, and the error/recover
pair supplies one forever. Fix would be per-action fairness (`WF_vars(N1Recover) ∧ WF_vars(N2Recover) ∧ WF_vars(ProcessTick)
∧ …`) plus a `channel_ack < MaxQueue` guard in `CompleteForwardPass` — as a v2 file, since manifests pin the current bytes.

**Note on S4/S5:** as written they assert `dag_version >= 1` and `signal_ledger >= 0`, i.e. non-negativity, not monotonicity;
they hold, but they do not say what their names say. Not counted against the corpus here; recorded for the v2 decision.

Re-run: `cd ~/research/tla_recheck_20260906 && java -cp <tla2tools.jar> tlc2.TLC -workers 4 -deadlock -config one_<Name>.cfg KairosModel.tla`
(copy `KairosDistributed.tla` alongside first).