feat(formal/tla): TLA+ pool model — JsWorkerPool crash-isolation + route-consistency

[hyperpolymath]

Summary

• Adds specs/elixir-harness/JsWorkerPool.tla — pool-level TLA+ model composing with the existing JsWorker.tla (same status/reply/replyCount discipline, lifted to N workers)
• Adds specs/elixir-harness/JsWorkerPool.cfg — TLC config: 2 workers ({w0,w1}), 3 requests ({r1,r2,r3}), Route = [r1 |-> w0, r2 |-> w1, r3 |-> w0]
• Updates specs/elixir-harness/README.adoc — documents the pool model and removes JsWorkerPool from "Not yet modelled"

What the model covers

New state variables beyond JsWorker.tla:

• assigned[r] — which pool slot a request was dispatched to (or NoWorker for fallback/new)
• wup[w] — whether worker w's Deno process is alive

New actions:

• ArrivePool(r) — phash2-routed dispatch when slot is up (js_worker_pool.ex pick_worker/1 → JsWorker)
• ArriveFallback(r) — atomic dispatch via JsInvoker when slot is down (modelled as always-terminates)
• Crash(w) / Restart(w) — per-slot crash and :one_for_one restart (only affects slot w)

New properties:

• RouteConsistency — a pool-dispatched request is always at Route[r]; no request ever lands at the wrong slot. Enforces the phash2 invariant.
• NoPendingWhileDown — Crash(w) atomically clears all requests at w; no pending request outlives its worker.
• ReplyOnce and EventuallyReplied inherited from JsWorker.tla, now verified pool-wide.

CRASH-ISOLATION is enforced structurally: Crash(w) touches only assigned[r] = w. With Route = [r1 |-> w0, r2 |-> w1, r3 |-> w0], a Crash(w0) terminates r1 and r3 but not r2 — TLC exhaustively verifies no interleaving of concurrent crashes at w0 and w1 can violate ReplyOnce.

Non-vacuity: ReachOk / ReachTimeout / ReachCrashed / ReachFallback are sanity controls (not in .cfg) — all four are expected violations, proving every terminal outcome is reachable.

Test plan

• java -cp tla2tools.jar tlc2.TLC JsWorkerPool.tla — no invariant violation, EventuallyReplied holds
• All four sanity controls (ReachOk, ReachTimeout, ReachCrashed, ReachFallback) each refuted by TLC with a short witness trace (non-vacuity check)
• JsWorker.tla still passes (no regression): 341 states, depth 8, no error

🤖 Generated with Claude Code

https://claude.ai/code/session_01F8pqMfJViUaKabWKNQ9wUg

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 219 issues detected

Severity	Count
🔴 Critical	15
🟠 High	131
🟡 Medium	73

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action actions/checkout@v4 needs attention",
    "type": "unpinned_action",
    "file": "pages-deploy.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in pages-deploy.yml",
    "type": "missing_timeout_minutes",
    "file": "pages-deploy.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in push-email-notify.yml",
    "type": "missing_timeout_minutes",
    "file": "push-email-notify.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "missing_timeout_minutes",
    "file": "scorecard-enforcer.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "scorecard_publish_with_run_step",
    "file": "scorecard-enforcer.yml",
    "action": "split_scorecard_publish_job",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "secret_action_without_presence_gate",
    "file": "instant-sync.yml",
    "action": "peter-evans/repository-dispatch",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "codeql_missing_actions_language",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/academic-workflow-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/ephapax-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/boj-server/boj-server/cartridges/bofig-mcp/adapter/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence