proof(consensus): fix + model-check the BFT spec (TLC) + wire CI

[hyperpolymath]

What

Next items in the phronesis proof scope: fix + model-check the BFT consensus spec, and wire TLC into CI. (Conformance wiring follows on this branch.)

The spec had never been model-checked — and was invalid

Running TLC for the first time exposed three real defects:

• TypeOK violated — Commit logs a vote snapshot including "NONE" (commits fire once the approval threshold is met, before all agents vote), but the log type only allowed APPROVE/REJECT.
• Agreement mis-stated — asserted all committed actions are globally distinct (violated by a legitimate re-commit), not the consensus property.
• ByzantineSafety vacuous — a constant-level formula (no state variables), so TLC asserted nothing about the protocol.

Rewritten as a genuine Byzantine quorum model (per agreed design)

Per-agent commit views, an equivocating proposer (honest agents may receive different values) + Byzantine voters. Safety now rests on quorum intersection:

• Agreement — no two honest agents commit different values for a round;
• Validity — an honest commit is backed by a Threshold-quorum;
• ByzantineSafety — a committed value cannot be forged by the Byzantine minority alone (≥ Threshold − |Byzantine| honest senders; Threshold > F).

Verification (N=4, F=1, Threshold=2F+1=3)

• Positive: TLC — no error (all invariants hold).
• Negative: at Threshold=2 (< 2F+1) TLC violates Agreement — proving the quorum bound is load-bearing, so the invariants are not vacuous.

.github/workflows/tla-consensus.yml runs both: positive gate + asserts the negative test fails. tla2tools v1.8.0 is sha256-pinned.

Remaining on this branch

Wire the conformance suite into CI (needs a small fix — the runner's default command calls a non-existent Phronesis.CLI.parse).

🤖 Draft opened by Claude Code.

https://claude.ai/code/session_01DQACj3RFmAPZaBPgR9SAaS

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 30 issues detected

Severity	Count
🔴 Critical	0
🟠 High	7
🟡 Medium	23

View findings

[
  {
    "reason": "Action trufflesecurity/trufflehog@main needs attention",
    "type": "unpinned_action",
    "file": "secret-scanner.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_timeout_minutes",
    "file": "secret-scanner.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": "binary_to_term without :safe option -- deserialization attack (1 occurrences, CWE-502)",
    "type": "elixir_send_unsanitised",
    "file": "/home/runner/work/phronesis/phronesis/lib/phronesis/compiler.ex",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Nominal-only SAST in phronesis: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
    "type": "StaticAnalysis",
    "file": "/home/runner/work/phronesis/phronesis",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Add CodeQL or equivalent SAST workflow.",
    "scorecard_check": "SAST"
  },
  {
    "reason": "Repository has 3 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Hypatia): hypatia/structural_drift/SD007 -- Hypatia structural_drift: SD007 -- 2 day(s) old",
    "type": "CSA001",
    "file": ".claude/CLAUDE.md",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Hypatia): hypatia/structural_drift/SD007 -- Hypatia structural_drift: SD007 -- 2 day(s) old",
    "type": "CSA001",
    "file": ".claude/CLAUDE.md",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Hypatia): hypatia/structural_drift/SD007 -- Hypatia structural_drift: SD007 -- 2 day(s) old",
    "type": "CSA001",
    "file": ".claude/CLAUDE.md",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Hypatia): hypatia/structural_drift/SD007 -- Hypatia structural_drift: SD007 -- 2 day(s) old",
    "type": "CSA001",
    "file": ".claude/CLAUDE.md",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence