Proposal: CI for the formal models (Tamarin + TLC + NIP-PL mutation scripts)

[SeanGearin]

What's missing

The repo's formal artifacts are treated as load-bearing by the docs, but none
of them run in CI:

Artifact	Claim it backs	How it's run today
docs/spec/MultiTenantAuth.spthy	docs/multi-tenant-relay.md: S1–S8 "machine-verified green", all 32 lemmas on Tamarin 1.12.0 / Maude 3.5.1	by hand
crates/buzz-core/src/pairing/NIP-AB.spthy	NIP-AB.md: pairing protocol security lemmas	by hand (tamarin-prover --prove …)
docs/spec/MultiTenantRelay.tla + .cfg	docs/multi-tenant-relay.md: exhaustive TLC run, 16.2M distinct states, ~5m	by hand
docs/spec/GitOnObjectStore.tla + .cfg	docs/git-on-object-storage.md: 8 invariants, mutation-tested	by hand
docs/formal/nip-pl/*.py (6 scripts)	NOTE.md: lease acceptance, stateful gateway, fixed-payload noninterference + mutations	by hand

VISION.md's isolation bullet says "proven, not asserted". Right now that's true
at the commit where each proof was last hand-run, and silently decays after:
a PR can edit a .spthy/.tla/model .py with no re-check, and toolchain or
spec rot is invisible until someone re-runs manually.

Proposal

A formal.yml workflow — no Rust build involved — with three jobs:

1. Tamarin (matrix over the two .spthy models): install Tamarin 1.12.0 +
   Maude 3.5.1 (the exact versions docs/multi-tenant-relay.md records as
   verified-green), sha256-pinned against the digests the upstream GitHub
   releases publish; run --prove --quit-on-warning; gate on the summary
   (batch tamarin exits 0 even on falsified lemmas): no falsified/analysis incomplete, and verified-lemma count == lemma declarations in the file.
2. TLC (matrix over the two .tla specs): the documented invocations
   against the committed bounded .cfg harnesses, tla2tools.jar sha256-pinned.
   TLC's exit code is already a correct red/green.
3. NIP-PL scripts: run all six in NOTE.md order. Two need a tiny patch to
   exit non-zero on failure (acceptance.py prints violations but exits 0;
   mutation_test.py prints detection counts without asserting M1>0, M2>0,
   SPEC==0) — I'd fold that into the same PR.

Triggers: nightly schedule (drift watch) + workflow_dispatch +
pull_request path-filtered to docs/spec/**, docs/formal/**, the NIP-AB
.spthy, and the workflow itself — so it costs zero minutes on ordinary PRs.

Cost: one ~15m job (MultiTenantRelay TLC on standard runners; documented ~5m on
8 workers), everything else minutes or seconds, only nightly and on
spec-touching PRs.

Questions for maintainers

• Is nightly + path-filtered PR the right gating level, or would you rather
  start nightly-only and promote to a PR gate once it's proven stable?
• Any appetite for a just formal recipe mirroring the workflow for local
  runs? (Left out of the first PR to keep the diff minimal.)
• docs(spec): operator provisioning plane — Tamarin S9 model + TLA/conformance prose (stacked on #1657) #1664 adds a Tamarin S9 model and docs: add bounded exhaustive model for NIP-RS manual-unread encoding #1958 a bounded NIP-RS model — both would
  be picked up by the path filter once merged; the S9 .spthy under
  docs/spec/ gets proven automatically, and new Python models would just be
  added to the third job's list.

Status

The workflow is written, and the two script exit-code fixes are tested (including forced-failure runs). Per CONTRIBUTING's "for significant changes, open an issue first to discuss the approach," I'm holding the PR pending your nod rather than sending a new CI workflow unsolicited — happy to open it immediately if this direction sounds right.