proof(lean4): mechanize BFT quorum-intersection safety (Theorem 3)

[hyperpolymath]

Summary

Mechanizes BFT Safety (Theorem 3) in Lean 4 as a real-proof companion to the existing TLA+ model-check. Where formal/PhronesisConsensus.tla exhaustively checks Agreement for the instance N = 4, F = 1, this proves the underlying quorum-intersection invariant for all N, F — and every cardinality fact is proved, not assumed.

What's proved (academic/formal-verification/lean4/Phronesis.lean)

Model: agents = a universe List, votes / Byzantine = Bool predicates, cardinalities = countP.

Cardinality lemmas (core-Lean inductions + omega):

• countP_incl_excl — countP(p‖q) + countP(p&q) = countP p + countP q
• countP_or_le_length — union bound
• countP_mono — monotonicity under pointwise implication

Headlines:

• bft_no_two_quorums — with n ≤ 3f+1 and threshold 2f+1, two distinct values cannot both reach a quorum. The contradiction is f+1 ≤ |overlap| ≤ f: inclusion–exclusion forces overlap ≥ f+1, while honest-vote-once forces it ≤ f.
• bft_agreement — any two committed values are equal (a value is committed when its vote set reaches 2f+1; honest agents vote for at most one value; Byzantine may equivocate). This is exactly the TLA+ Agreement invariant, proved for all N, F.

Verification

• lake build exit 0, no warnings, on Lean 4.12.0 core (no Mathlib).
• sorry-free. #print axioms reports only Lean's standard propext / Quot.sound (and Classical.choice for bft_agreement, via Classical.em — by_contra isn't a core tactic, so I used Classical.em + cases).

Docs

safety_proofs.md §3.4 gains a "Verified two ways" note (TLA+ model-check + Lean proof); the §5 status table marks BFT Safety = Model-checked (TLA+/TLC) + Mechanized (Lean 4).

Status of the proof estate after this PR

Property	Status
Type safety (progress/preservation/determinism)	Mechanized (Lean)
Sandbox Isolation (Thm 1)	Mechanized (Lean)
Capability Soundness (Thm 2)	Mechanized (Lean) — #44
Ethical Verdict Consistency	Mechanized (Lean) — #44
BFT Safety (Thm 3)	Model-checked (TLA+) + Mechanized (Lean) — this PR

Still recommended (deferred, noted on #44): a SHA-pinned Lean CI gate so these proofs are guarded against regression (blocked this session only by the GitHub API rate limit).

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