backlog: file B-0179 + B-0180 + B-0181 — 3 broken TLA+ specs from #1397 verify-then-claim sweep

docs/backlog/P2/B-0179-fix-spineasyncprotocol-tla-counterexample-blocks-b1-ci-registration-2026-05-03.md

@@ -0,0 +1,48 @@
+---
+id: B-0179
+priority: P2
+status: open
+title: Fix SpineAsyncProtocol.tla counterexample (blocks B1 → A CI registration; depth-9 trace dump on TLC run)
+tier: formal-verification
+effort: M
+ask: Otto 2026-05-03 verify-then-claim sweep (#1397) — running TLC on the 4 deferred B1 specs from the math-proofs honest assessment (#1383) found SpineAsyncProtocol produces a TTrace dump at depth 9, indicating counterexample / invariant violation. The "deliberately skipped pending re-verification" framing in `docs/research/proof-tool-coverage.md` §2 was correct; this row tracks the actual fix.
+created: 2026-05-03
+last_updated: 2026-05-03
+depends_on: []
+composes_with: [docs/research/2026-05-03-math-proofs-honest-assessment.md, docs/research/proof-tool-coverage.md, B-0180, B-0181]
+tags: [tla-plus, formal-verification, spine-async, counterexample, b1, math-proofs-assessment, verify-then-claim]
+---
+
+# Fix SpineAsyncProtocol.tla counterexample
+
+## Symptom
+
+Running `java -cp tools/tla/tla2tools.jar tlc2.TLC -workers 4 -config tools/tla/specs/SpineAsyncProtocol.cfg tools/tla/specs/SpineAsyncProtocol.tla` produces a TTrace dump:
+
+```
+Trace exploration spec path: tools/tla/specs/SpineAsyncProtocol_TTrace_<ts>.tla
+The depth of the complete state graph search is 9.
+Finished in 00s
+```
+
+TLC dumps a trace file when it finds an invariant violation or a `run` that can't be satisfied. The depth-9 termination + 0-second run suggests TLC found a violation immediately (rather than exhausting state space).
+
+## Investigation needed
+
+1. Read the TTrace file to identify which invariant fails
+2. Determine whether the invariant or the spec needs the fix:
+   - If the spec models the protocol incorrectly, fix the spec
+   - If the invariant is over-strong (asks for a property the protocol doesn't actually guarantee), weaken the invariant
+3. Verify the fix locally — re-run TLC; expect clean "No error has been found"
+4. Add `[<Fact>] TLC validates SpineAsyncProtocol` to `tests/Tests.FSharp/Formal/Tlc.Runner.Tests.fs`
+5. Add registry row to `docs/research/verification-registry.md`
+
+## Why P2
+
+Pre-existing failure surfaced by verify-then-claim sweep, not a new regression. Blocks B1 → A in the assessment matrix but doesn't block any current functionality (the SpineAsync runtime works in practice; this is a formal-verification gap).
+
+## Composes with
+
+- B-0180 (CircuitRegistration config bug — sibling B1 issue)
+- B-0181 (SpineMergeInvariants counterexample — sibling B1 issue)
+- The closure of B1 → A in the math-proofs honest assessment requires all 3 sibling fixes to land

docs/backlog/P2/B-0180-fix-circuitregistration-tla-config-bug-safety-invariant-undefined-2026-05-03.md

@@ -0,0 +1,54 @@
+---
+id: B-0180
+priority: P2
+status: open
+title: Fix CircuitRegistration.tla config bug — `.cfg` references invariant `Safety` not defined in `.tla` (blocks B1 → A CI registration)
+tier: formal-verification
+effort: S
+ask: Otto 2026-05-03 verify-then-claim sweep (#1397) — running TLC on `CircuitRegistration` produces a clear configuration error rather than a counterexample; the `.cfg` references `INVARIANT Safety` but the `.tla` spec doesn't define a `Safety` predicate. Fixable in either direction (define `Safety` in spec OR remove `Safety` line from cfg).
+created: 2026-05-03
+last_updated: 2026-05-03
+depends_on: []
+composes_with: [docs/research/2026-05-03-math-proofs-honest-assessment.md, docs/research/proof-tool-coverage.md, B-0179, B-0181]
+tags: [tla-plus, formal-verification, circuit-registration, config-bug, b1, math-proofs-assessment, verify-then-claim, smallest-of-3-b1-fixes]
+---
+
+# Fix CircuitRegistration.tla config bug
+
+## Symptom
+
+Running `java -cp tools/tla/tla2tools.jar tlc2.TLC -workers 4 -config tools/tla/specs/CircuitRegistration.cfg tools/tla/specs/CircuitRegistration.tla` produces:
+
+```
+Error: The invariant Safety specified in the configuration file
+is not defined in the specification.
+Finished in 00s
+```
+
+The TLC error is unambiguous: `CircuitRegistration.cfg` has an `INVARIANT Safety` directive but `CircuitRegistration.tla` doesn't define a `Safety` operator.
+
+## Fix options
+
+Two directions, decision needed:
+
+1. **Define `Safety` in the spec.** Read the spec; identify which invariant the original author intended `Safety` to capture; add `Safety == ...` operator that captures it. Most likely the existing `FlagSound` post-condition or a similar property.
+
+2. **Remove `Safety` from the cfg.** Inspect what other invariants the cfg references; if those alone are sufficient validation, drop the missing `Safety` reference. Risk: may drop an intentional invariant the author meant to add but never finished writing.
+
+The verify-then-claim follow-up tick should pick (1) if the spec has a clear "what was Safety supposed to mean" thread, else (2) with a comment in the cfg documenting why.
+
+## Why this is the smallest of 3 B1 fixes
+
+This is a config-syntax error, not a semantic counterexample. The other two B1 broken specs (B-0179 SpineAsyncProtocol, B-0181 SpineMergeInvariants) require investigating actual counterexamples — substantially harder. This one is bounded to "find the missing operator definition or drop the line."
+
+## After the fix
+
+1. Re-run TLC locally; expect clean "No error has been found"
+2. Add `[<Fact>] TLC validates CircuitRegistration` to `tests/Tests.FSharp/Formal/Tlc.Runner.Tests.fs`
+3. Add registry row to `docs/research/verification-registry.md`
+
+## Composes with
+
+- B-0179 (SpineAsyncProtocol counterexample — sibling B1 issue)
+- B-0181 (SpineMergeInvariants counterexample — sibling B1 issue)
+- Closure of B1 → A in the math-proofs honest assessment requires all 3 sibling fixes

docs/backlog/P2/B-0181-fix-spinemergeinvariants-tla-counterexample-blocks-b1-ci-registration-2026-05-03.md

@@ -0,0 +1,64 @@
+---
+id: B-0181
+priority: P2
+status: open
+title: Fix SpineMergeInvariants.tla counterexample (blocks B1 → A CI registration; depth-17 trace dump on TLC run)
+tier: formal-verification
+effort: M
+ask: Otto 2026-05-03 verify-then-claim sweep (#1397) — running TLC on `SpineMergeInvariants` produces a TTrace dump at depth 17, indicating counterexample / invariant violation. Sibling failure to B-0179 SpineAsyncProtocol but at deeper depth, which may indicate the violation is more subtle (further from initial state).
+created: 2026-05-03
+last_updated: 2026-05-03
+depends_on: []
+composes_with: [docs/research/2026-05-03-math-proofs-honest-assessment.md, docs/research/proof-tool-coverage.md, B-0179, B-0180]
+tags: [tla-plus, formal-verification, spine-merge, balanced-spine, counterexample, b1, math-proofs-assessment, verify-then-claim]
+---
+
+# Fix SpineMergeInvariants.tla counterexample
+
+## Symptom
+
+Running `java -cp tools/tla/tla2tools.jar tlc2.TLC -workers 4 -config tools/tla/specs/SpineMergeInvariants.cfg tools/tla/specs/SpineMergeInvariants.tla` produces a TTrace dump:
+
+```
+Trace exploration spec path: tools/tla/specs/SpineMergeInvariants_TTrace_<ts>.tla
+The depth of the complete state graph search is 17.
+Finished in 00s
+```
+
+TLC dumps a trace file when it finds an invariant violation. The depth-17 termination suggests TLC explored 17 transitions before finding the violation — deeper than the SpineAsyncProtocol failure (depth 9), which may indicate the violation is more subtle (further from initial state, requires more interleaving to manifest).
+
+## Investigation needed
+
+1. Read the TTrace file to identify which invariant fails at the depth-17 state
+2. Determine the failure class:
+   - **Spec bug**: spec models the LSM-spine merge protocol incorrectly
+   - **Invariant over-specification**: invariant asks for a property the merge protocol doesn't actually guarantee
+   - **Real bug found**: the invariant is correct but the modeled protocol violates it; this would indicate a bug in `BalancedSpine.fs` itself
+3. The third class is the most interesting — TLA+ found a real concurrency bug. If that's the case, file as a P0/P1 in BUGS.md instead of treating it as a spec-fix.
+
+## Composes with
+
+- B-0179 (SpineAsyncProtocol counterexample — sibling B1 issue)
+- B-0180 (CircuitRegistration config bug — sibling B1 issue, smallest fix)
+- `src/Core/BalancedSpine.fs` — the production code this spec models
+- Closure of B1 → A in the math-proofs honest assessment requires all 3 sibling fixes
+
+## Why P2
+
+Pre-existing failure surfaced by verify-then-claim sweep, not a new regression. The actual blast radius depends on the failure class — if it's a "real bug found" case, escalate to BUGS.md P0 immediately. If it's spec-bug or over-specification, P2 is right.
+
+## After the fix (or escalation)
+
+If spec-bug or over-specification:
+
+1. Fix the spec / invariant
+2. Verify locally — TLC clean "No error has been found"
+3. Add `[<Fact>] TLC validates SpineMergeInvariants` to `tests/Tests.FSharp/Formal/Tlc.Runner.Tests.fs`
+4. Add registry row to `docs/research/verification-registry.md`
+
+If real bug found:
+
+1. File P0/P1 BUGS.md entry referencing this spec + the TTrace
+2. Land the production-code fix
+3. Verify spec passes after fix
+4. Then land the CI registration as above