formal-verify.yml

name: Formal Verification

on:
  push:
    branches: [main, staging]
    paths:
      - 'src/machines/nf-workflow.machine.ts'
      - '.planning/formal/tla/**'
      - '.planning/formal/alloy/**'
      - '.planning/formal/prism/**'
      - 'bin/run-tlc.cjs'
      - 'bin/run-alloy.cjs'
      - 'bin/run-prism.cjs'
      - 'bin/generate-formal-specs.cjs'
      - 'bin/check-spec-sync.cjs'
      - 'bin/verify-quorum-health.cjs'
      - 'bin/xstate-to-tla.cjs'
      - 'bin/run-formal-verify.cjs'
      - 'bin/run-oauth-rotation-prism.cjs'
      - 'bin/run-account-pool-alloy.cjs'
      - 'bin/run-account-manager-tlc.cjs'
      - 'bin/write-check-result.cjs'
      - 'bin/check-results-exit.cjs'
      - 'bin/check-trace-redaction.cjs'
      - 'bin/check-trace-schema-drift.cjs'
      - '.planning/formal/trace/**'
  # Always trigger on PRs — this is a required check for branch protection.
  # Without this, PRs that don't touch formal files never get the check,
  # and branch protection blocks the merge.
  pull_request:
  workflow_dispatch:  # manual trigger

jobs:
  verify:
    name: TLC + Alloy + PRISM model checks
    runs-on: ubuntu-latest
    timeout-minutes: 25

    steps:
      - name: Checkout
        uses: actions/checkout@v4
        with:
          fetch-depth: 2  # needed by check-trace-schema-drift (git diff HEAD~1)

      - name: Set up Java 17
        uses: actions/setup-java@v4
        with:
          distribution: temurin
          java-version: '17'

      - name: Set up Node.js
        uses: actions/setup-node@v4
        with:
          node-version: '20'

      - name: Install dev dependencies
        run: npm ci || npm install

      - name: Build XState machine (needed by validate-traces)
        run: npm run build:machines

      - name: Create tool directories
        run: mkdir -p .planning/formal/tla .planning/formal/alloy

      - name: Cache TLA+ tools JAR
        id: cache-tla
        uses: actions/cache@v4
        with:
          path: .planning/formal/tla/tla2tools.jar
          key: tla2tools-v1.8.0
          restore-keys: tla2tools-

      - name: Download tla2tools.jar
        if: steps.cache-tla.outputs.cache-hit != 'true'
        run: |
          curl -fsSL --retry 3 --retry-delay 5 \
            https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar \
            -o .planning/formal/tla/tla2tools.jar

      # Formal-discrimination benchmark: proves the debug prove-bug/prove-fix loop
      # genuinely depends on the bug (bug spec → counterexample, fix spec → clean).
      # Guards against the "theater" failure mode where a checker passes regardless.
      - name: Formal-discrimination benchmark (prove-bug / prove-fix)
        run: node bin/check-formal-discrimination.cjs

      # Chain-enforcement: the full code→model→fix→model→code loop must be bound to
      # ONE bug per case (code bug ≡ model bug; both fixes proven on real artifacts).
      - name: Debug chain-enforcement (code↔model end-to-end)
        run: node bin/check-debug-chain.cjs

      - name: Cache Alloy JAR
        id: cache-alloy
        uses: actions/cache@v4
        with:
          path: .planning/formal/alloy/org.alloytools.alloy.dist.jar
          key: alloy-v6.2.0
          restore-keys: alloy-

      - name: Download Alloy 6.2.0 JAR
        if: steps.cache-alloy.outputs.cache-hit != 'true'
        run: |
          curl -fsSL --retry 3 --retry-delay 5 \
            https://github.com/AlloyTools/org.alloytools.alloy/releases/download/v6.2.0/org.alloytools.alloy.dist.jar \
            -o .planning/formal/alloy/org.alloytools.alloy.dist.jar

      - name: Generate all formal specs from XState machine (source of truth)
        run: node bin/generate-formal-specs.cjs

      - name: Verify generated specs are in sync with XState machine
        run: node bin/check-spec-sync.cjs

      - name: TLC — safety check (MCsafety, N=5, symmetry)
        run: node bin/run-tlc.cjs MCsafety

      - name: TLC — liveness check (MCliveness, N=3)
        run: node bin/run-tlc.cjs MCliveness

      - name: TLA+ QGSDMCPEnv — MCMCPEnv (MCPENV-02)
        env:
          NF_SKIP_STATE_SPACE_GUARD: '1'
        run: node bin/run-tlc.cjs MCMCPEnv

      - name: Alloy — majority threshold assertions (ThresholdPasses, BelowThresholdFails, ZeroApprovalsFail)
        run: node bin/run-alloy.cjs .planning/formal/alloy/quorum-votes.als

      - name: Cache PRISM binary
        id: cache-prism
        uses: actions/cache@v4
        with:
          path: /tmp/prism
          key: prism-v4.10-linux64-x86
          restore-keys: prism-

      - name: Download and extract PRISM 4.10 (Linux x86)
        if: steps.cache-prism.outputs.cache-hit != 'true'
        run: |
          mkdir -p /tmp/prism
          curl -fsSL --retry 3 --retry-delay 5 \
            https://github.com/prismmodelchecker/prism/releases/download/v4.10/prism-4.10-linux64-x86.tar.gz \
            -o /tmp/prism-4.10-linux64-x86.tar.gz
          tar -xzf /tmp/prism-4.10-linux64-x86.tar.gz -C /tmp/prism --strip-components=1
          chmod +x /tmp/prism/bin/prism
          # Fix hardcoded PRISM_DIR in launch script to point to actual install path
          sed -i 's|^PRISM_DIR=.*|PRISM_DIR="/tmp/prism"|' /tmp/prism/bin/prism

      - name: PRISM — quorum convergence P=?[F DECIDED]
        env:
          PRISM_BIN: /tmp/prism/bin/prism
        run: node bin/run-prism.cjs

      - name: PRISM mcp-availability — per-slot MCP availability rates (MCPENV-04)
        env:
          PRISM_BIN: /tmp/prism/bin/prism
        run: node bin/run-prism.cjs --model=mcp-availability

      - name: Quorum health check (requires scoreboard — advisory only in CI)
        run: node bin/verify-quorum-health.cjs || echo "[verify-quorum-health] No scoreboard in CI — skipped (run locally against live data)"
        continue-on-error: true

      - name: Run full FV pipeline via master runner (run-formal-verify.cjs)
        env:
          PRISM_BIN: /tmp/prism/bin/prism
          NF_SKIP_STATE_SPACE_GUARD: '1'
        run: node bin/run-formal-verify.cjs

      - name: Trace redaction enforcement (check-trace-redaction.cjs)
        run: node bin/check-trace-redaction.cjs

      - name: Trace schema drift guard (check-trace-schema-drift.cjs)
        run: node bin/check-trace-schema-drift.cjs

      - name: Check NDJSON exit code (fail if any result=fail in check-results.ndjson)
        env:
          PRISM_BIN: /tmp/prism/bin/prism
        run: node bin/check-results-exit.cjs