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

## 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.)
- #1664 adds a Tamarin S9 model and #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.

Start with the proposed formal.yml workflow, the documented Tamarin and TLC invocations, and docs/formal/nip-pl/NOTE.md. Run the six NIP-PL scripts and inspect acceptance.py and mutation_test.py forced-failure tests, then verify the workflow covers the listed .spthy, .tla/.cfg, and Python artifacts. Done means pinned toolchains run on the stated triggers and failures cannot pass silently.

Written by the indexing model from the issue text.