ci(tbtc-signer): add formal verification workflow (moved from tbtc-v2)

Adds a focused workflow that runs the Rust signer's formal-invariant
test suite + TLA model checks. Moved from
threshold-network/tbtc-v2/.github/workflows/ci-formal-verification.yml
(jobs `signer-formal-invariants` + `tla-model-checks`) per extraction
plan v38 §3.1 — the signer code lives here at pkg/tbtc/signer/, not
in tbtc-v2, so the CI jobs that exercise it belong here too.

Jobs
- signer-formal-invariants: cargo test --manifest-path pkg/tbtc/signer/
  Cargo.toml formal_verification_ (filter to formal-only cases)
- tla-model-checks: pkg/tbtc/signer/scripts/formal/run_tla_models.sh
  (iterates over .cfg files in pkg/tbtc/signer/docs/formal/models/ and
  runs TLC against each; MODELS_PATH env var allows override per the
  path-normalization commit b84b574c on this branch)

Triggers
- pull_request on pkg/tbtc/signer/** changes + this workflow file
- schedule nightly at 05:23 UTC (mirrors monorepo's pattern of running
  formal invariants both on PRs and nightly)
- workflow_dispatch for manual runs

Related changes in companion PR threshold-network/tbtc-v2#971:
- Removed these jobs from canonical tbtc-v2's ci-formal-verification.yml
- Added a comment in that file pointing here

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: mswilkison

.github/workflows/tbtc-signer-formal.yml

@@ -0,0 +1,57 @@
+name: tBTC Signer Formal Verification
+
+on:
+  pull_request:
+    paths:
+      - pkg/tbtc/signer/**
+      - .github/workflows/tbtc-signer-formal.yml
+  schedule:
+    - cron: "23 5 * * *"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: tbtc-signer-formal-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  signer-formal-invariants:
+    name: Signer formal invariants
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Setup Rust
+        uses: dtolnay/rust-toolchain@stable
+
+      - name: Run signer formal invariant tests
+        # Filters cargo test by the formal_verification_ prefix so only
+        # the formal-invariant test cases run (faster + clearer signal
+        # than the full suite). Matches the convention used in the
+        # source monorepo's ci-formal-verification.yml.
+        run: cargo test --manifest-path pkg/tbtc/signer/Cargo.toml formal_verification_
+
+  tla-model-checks:
+    name: TLA model checks
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Setup Java
+        uses: actions/setup-java@v4
+        with:
+          distribution: temurin
+          java-version: "17"
+
+      - name: Run TLA model checks
+        # Iterates over every .cfg under pkg/tbtc/signer/docs/formal/models/
+        # and runs TLC against the matching .tla module. MODELS_PATH defaults
+        # to the canonical signer-relative path; override via env var for
+        # alternate environments (set in extraction/frost-signer-mirror PR).
+        run: pkg/tbtc/signer/scripts/formal/run_tla_models.sh