feat(formal/tla): TLA+ model of Invoker — isolation + classification coverage

[hyperpolymath]

Summary

• Adds specs/elixir-harness/Invoker.tla — TLA+ model of BojRest.Invoker (Phase 2 fork-per-request Zig FFI dispatcher)
• Adds specs/elixir-harness/Invoker.cfg — TLC config: 3 requests, 8 possible result kinds
• Updates specs/elixir-harness/README.adoc — adds Invoker section, moves it out of "Not yet modelled"; updates sanity-control shell loop

What the model covers

Invoker is stateless and synchronous: System.cmd/3 blocks until boj-invoke exits; there is no pool, no GenServer, no shared mailbox. The interesting formal question is not a state machine but an isolation guarantee: N concurrent callers cannot interfere with each other's result.

State variables: status[r] (new/running/done), result[r] (one of 8 terminal kinds), doneCount[r] (double-resolution detector).

Actions:

• Invoke(r) — CLI found, subprocess spawned (new → running)
• CliMissing(r) — cli_path() returns nil, short-circuits immediately (new → done)
• RespondOk / RespondCliCrashed / RespondArgs / RespondOpen / RespondMissingSym / RespondInitFailed — subprocess exits (running → done)

Properties verified:

• DoneOnce — each invocation resolves at most once; no race can deliver two results for the same call (since System.cmd is blocking, the subprocess exits exactly once)
• Consistent — running ↔ no result yet; done ↔ exactly one result
• EventuallyDone [ASSUMED] — running ~> done, under the assumption that the subprocess exits on its own

Known gap documented: Phase 2 has no per-invocation timeout. System.cmd blocks indefinitely if boj-invoke hangs. ADR-0005 specifies 5 s for the future pool (not yet implemented). EventuallyDone rests on an [ASSUMED] liveness condition.

Non-vacuity: all 7 result kinds refuted by TLC with witness traces.

Formal coverage after this PR

Component	Model	Headline properties
JsWorker (single slot)	JsWorker.tla	ReplyOnce, EventuallyReplied
JsWorkerPool (N slots)	JsWorkerPool.tla	+ RouteConsistency, crash isolation
Invoker (Zig-FFI, Phase 2)	Invoker.tla	DoneOnce, classification coverage
Zig FFI ABI	abi_axioms.zig + abi_verify.zig	comptime proofs + 40 boundary tests
Idris2 ABI	SafetyLemmas.idr	4 class-J axioms + charEqSym discharged

Test plan

• java -cp tla2tools.jar tlc2.TLC Invoker.tla — no invariant violation, EventuallyDone holds
• All 7 sanity controls (ReachOk … ReachInitFailed) each refuted by TLC with a short witness trace
• JsWorker.tla and JsWorkerPool.tla still pass (no regression)

🤖 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