feat(solve): add --no-coderlm flag (21× benchmark speedup) #186
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 | |
| - 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 |