proof(lean4): mechanize Capability Soundness + Ethical Verdict Consistency by hyperpolymath · Pull Request #44 · hyperpolymath/phronesis

hyperpolymath · 2026-06-14T12:56:24Z

Summary

Two mechanization steps in the proof-completion sequence (sandbox → wire & conformance → mechanise → ethics specifics), both machine-checked in academic/formal-verification/lean4/Phronesis.lean over the real AST/PhrPolicy, on Lean 4.12.0 core (no Mathlib).

1. Capability Soundness (`safety_proofs.md §2`, Theorem 2)

Turns the informal "by inspection of execution paths" argument into a proof.

capability_soundness — no leaf action executes without the required capability. The Executes relation is capability-gated by construction (every leaf rule carries the required-capability membership; there is no constructor that executes without an enforcement point), so soundness follows by inversion.
capability_soundness_ite — enforcement is preserved through conditional actions.
least_privilege (§2.5) — a fresh context holds only granted capabilities.
no_escalation (§2.5) — a step never enlarges the capability set: S → S' ⟹ S'.caps ⊆ S.caps.

2. Ethical Verdict Consistency (`safety_proofs.md §2.6`) — the ethics-specific soundness

Formalizes Phronesis's previously-informal priority-ordered first-match policy arbitration (lib/phronesis/state.ex policies_by_priority + spec/SPEC.core.scm) as bestMatch (highest-priority matching policy, ties to the earlier policy):

bestMatch_sound — a verdict comes only from a policy that genuinely matches and is in the set (no spurious verdicts).
bestMatch_none / bestMatch_decisive — no verdict ⇒ no policy matched; conversely a verdict is produced whenever some policy applies.
bestMatch_maximal — the deciding policy has maximal priority among all matching policies, so a higher-priority verdict is never overridden by a lower-priority one (e.g. a high-priority REJECT cannot be undercut by a lower-priority ACCEPT — the core ethical override).

matches abstracts condition evaluation, decoupling arbitration soundness from the Eval expression semantics.

Verification

lake build exit 0, no warnings.
sorry-free. #print axioms reports only Lean's standard propext (and Quot.sound for bestMatch_maximal) — same trusted base as the existing preservation/sandbox proofs; capability_soundness_ite is fully axiom-free.

Docs

safety_proofs.md §2.4 + new §2.6 gain "Mechanized (Lean 4)" notes; the §5 status table now records Sandbox Isolation, Capability Soundness, and Ethical Verdict Consistency = Mechanized (Lean 4), and BFT Safety = Model-checked (TLA+/TLC).

Observations (not in this PR)

Pre-existing, unrelated: lib/phronesis/compiler.ex uses :erlang.binary_to_term/1 without :safe (CWE-502). Out of scope; flagged for visibility.
There is no Lean CI gate anywhere in the estate, so these mechanized proofs aren't yet guarded against regressions. Recommend adding a leanprover/lean-action (SHA-pinned) gate building academic/formal-verification/lean4/ — deferred here only because the unauthenticated rate limit blocked fetching a clean pinned SHA this session.

https://claude.ai/code/session_01DQACj3RFmAPZaBPgR9SAaS

…m 2) Make the informal "by inspection of execution paths" argument for Theorem 2 machine-checked, reusing the real PhrAction AST. * Model: Resource / Operation / Capability / Context (capability list); requiredCap? maps the four leaf actions to their capability per §2.3 (ACCEPT/REJECT -> route_decision:write, REPORT -> consensus_log:append, EXECUTE f -> module f:exec). * The Executes relation is capability-gated BY CONSTRUCTION: every leaf rule carries the required-capability membership as a hypothesis, and there is deliberately no constructor that executes without an enforcement point. capability_soundness then follows by inversion -- this is exactly "all paths have enforcement points" made formal. * capability_soundness_ite extends enforcement through conditional actions (an executed iteAction reduces to a gated branch). * The two §2.5 side-properties are mechanized too: least_privilege (a fresh context holds only granted capabilities) and no_escalation (a step never enlarges the capability set, S -> S' => S'.caps subset of S.caps). All four are sorry-free; #print axioms reports only Lean's standard propext (capability_soundness_ite is axiom-free). Builds clean on Lean 4.12.0 core, no Mathlib. Docs: safety_proofs.md §2.4 gains a "Mechanized (Lean 4)" note and §5 status table now reads Sandbox Isolation + Capability Soundness = Mechanized (Lean 4), BFT Safety = Model-checked (TLA+/TLC). https://claude.ai/code/session_01DQACj3RFmAPZaBPgR9SAaS

github-actions · 2026-06-14T12:57:17Z

🔍 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

Formalize the previously-informal "priority-ordered first match" policy arbitration (lib/phronesis/state.ex policies_by_priority + the first-match evaluation in spec/SPEC.core.scm) as the ethics-specific soundness of the decision procedure, over the real PhrPolicy record. Model: bestMatch = the highest-priority MATCHING policy, ties broken in favour of the earlier policy (a fold equivalent to sort-by-priority then find-first). `matches` abstracts condition evaluation, decoupling arbitration soundness from the Eval expression semantics. Theorems (all sorry-free; #print axioms reports only Lean's standard propext / Quot.sound): * bestMatch_sound -- a verdict is produced only by a policy that really matches the situation and is in the policy set (no spurious verdicts); * bestMatch_none -- no verdict ⇒ no policy matched; hence * bestMatch_decisive -- a verdict is produced whenever some policy applies (the procedure never silently abstains on a live case); * bestMatch_maximal -- the deciding policy has MAXIMAL priority among all matching policies, so a higher-priority verdict is never overridden by a lower-priority one -- e.g. a high-priority REJECT cannot be undercut by a lower-priority ACCEPT (the core ethical override). Builds clean on Lean 4.12.0 core, no Mathlib, no warnings. Docs: safety_proofs.md gains §2.6 "Ethical Verdict Consistency" with the mechanization note, and the §5 status table adds the row "Ethical Verdict Consistency | Mechanized (Lean 4)". https://claude.ai/code/session_01DQACj3RFmAPZaBPgR9SAaS

github-actions · 2026-06-14T13:08:57Z

🔍 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

hyperpolymath changed the title ~~proof(lean4): mechanize Capability Soundness (safety_proofs.md Theorem 2)~~ proof(lean4): mechanize Capability Soundness + Ethical Verdict Consistency Jun 14, 2026

hyperpolymath marked this pull request as ready for review June 14, 2026 14:06

hyperpolymath merged commit a088b15 into main Jun 14, 2026
7 checks passed

hyperpolymath mentioned this pull request Jun 14, 2026

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

Merged

Navigation Menu

Uh oh!

proof(lean4): mechanize Capability Soundness + Ethical Verdict Consistency - #44

proof(lean4): mechanize Capability Soundness + Ethical Verdict Consistency#44
hyperpolymath merged 2 commits into
mainfrom
claude/gifted-fermat-EmVcv

hyperpolymath commented Jun 14, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Jun 14, 2026

Uh oh!

github-actions Bot commented Jun 14, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

hyperpolymath commented Jun 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

1. Capability Soundness (safety_proofs.md §2, Theorem 2)

2. Ethical Verdict Consistency (safety_proofs.md §2.6) — the ethics-specific soundness

Verification

Docs

Observations (not in this PR)

Uh oh!

github-actions Bot commented Jun 14, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 14, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

hyperpolymath commented Jun 14, 2026 •

edited

Loading

1. Capability Soundness (`safety_proofs.md §2`, Theorem 2)

2. Ethical Verdict Consistency (`safety_proofs.md §2.6`) — the ethics-specific soundness