Repair Coq + Agda formal verification so it actually checks (axiom-free)

[hyperpolymath]

What this is

A ground-truth audit of Phronesis's verification layer found that none of the three machine-checked proof files had ever compiled — the "120+ theorems / Mechanized: Coq, Lean4, Agda" claims in theorem-index.md and the "100% production-ready" in ANALYSIS-COMPLETE.md were not backed by anything a tool checks (academic/TODO.md is the honest doc). This PR makes the Coq and Agda formalizations genuinely check.

Coq — academic/formal-verification/coq/Phronesis.v (fully proved, axiom-free)

The file never compiled. Faults found & fixed:

• omega (removed in Coq 8.12+) → lia.
• value_eqb / phr_type_eqb used a mutual Fixpoint … with across phr_type and list, which Coq's guard checker rejects (they aren't mutually inductive) → rewritten with the nested-fix idiom.
• value_eqb_refl invoked a nonexistent phr_value_rect P0/P1 eliminator → two strong (nested) induction principles phr_type_ind' / phr_value_ind'.
• phr_type_eq_dec's decide equality couldn't dispatch the nested TRecord → now genuinely decidable (the same obligation that was unsound in Agda).
• preservation was missing the T_List case, elided the record-field case, and lost the empty context in EVar → reproved by induction on evaluation (keeps [] concrete); T_List via a list helper; field case closed by stating VT_Record over field_lookup.
• eval_deterministic had a variable-name clash + miscalibrated bullets → uniform IH-driven tactic.
• no_system_calls was unsound (ELit (VString "system") satisfied it) and ill-typed → honest by-construction sandbox_no_call_form.
• totality was malformed (Theorem … with Fixpoint) and false as stated (no typing hypothesis) → restated correctly and discharged as genuine progress-to-a-value.

Result: coqc Phronesis.v exits 0, no Admitted/Abort/sorry, and Print Assumptions on preservation, totality, eval_deterministic, type_safety, phr_type_eq_dec, subtype_trans, value_eqb_refl, sandbox_no_call_form = "Closed under the global context" (axiom-free).

Agda — academic/formal-verification/agda/Phronesis.agda (checks under --safe --without-K)

• Ctx's _,_ clashed with Data.Product._,_ → renamed to _,,_.
• Two Data.Integer imports listed names in both using and renaming (and re-imported _+_, clashing with Data.Nat) → kept only the renamings.
• _≟ᵗ_ was unsound: it omitted the TRecord case and used a single _ ≟ᵗ _ = no (λ ()) catch-all, which --safe rejects (TRecord fs ≡ TRecord gs is inhabited by refl) → rewritten as a mutual decision with _≟ᶠ_ over the field list, every same-head case handled and distinct-head pairs enumerated.
• _<ᵛ_ parsed as a ≤ᵇ (b ∧ …) (fixity) and used _≡ᵛ_ at an ambiguous index → parenthesised + indexed at TInt.
• Added {-# OPTIONS --safe --without-K #-}.

So the intrinsic-typing "type safety is automatic" and "eval is total" claims now genuinely hold.

Notes

• SPDX headers (Apache-2.0 OR MIT) left unchanged.
• Honest scope: Lean (Phronesis.lean — sorry, needs lake+Mathlib), TLA+ (never model-checked), the multi-surface semantics drift, and the AST representation drift remain open and are not addressed here.

How to verify

# Coq
cd academic/formal-verification/coq && coqc Phronesis.v   # exits 0; add `Print Assumptions preservation.` etc.
# Agda (needs agda-stdlib ≥ 2.x on the library path)
cd academic/formal-verification/agda && agda Phronesis.agda   # exits 0 under --safe --without-K

🤖 Generated with 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 -- 3 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 -- 3 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 -- 3 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 -- 3 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