Skip to content

docs: seed docs/proof-debt.md index per trusted-base policy#78

Open
hyperpolymath wants to merge 1 commit into
mainfrom
claude/seed-proof-debt-2026-05-26
Open

docs: seed docs/proof-debt.md index per trusted-base policy#78
hyperpolymath wants to merge 1 commit into
mainfrom
claude/seed-proof-debt-2026-05-26

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

What this PR does NOT do

Migrate the substantive content out of PROOF-NEEDS.md. That file remains canonical; this file just makes the schema-conformant filename exist for the check-trusted-base.sh CI gate.

🤖 Generated with Claude Code

Per the trusted-base reduction policy (hyperpolymath/standards#203),
adds a schema-conformant index at docs/proof-debt.md that references
PROOF-NEEDS.md as the source of truth.

This repo already has substantive proof-debt documentation in
PROOF-NEEDS.md — this PR doesn't duplicate that content, just adds the
schema bridge so the check-trusted-base CI gate (standards#211) finds
docs/proof-debt.md at the canonical filename and recognises this repo
as documented.

Marker count detected by check-trusted-base.sh: 134.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath hyperpolymath enabled auto-merge (squash) May 26, 2026 16:52
@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 34 issues detected

Severity Count
🔴 Critical 3
🟠 High 12
🟡 Medium 19

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Go file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/maa-framework/maa-framework/absolute-zero/examples/go/nop.go",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "Ada pragma Suppress disables runtime checks (1 occurrences, CWE-704)",
    "type": "ada_pragma_suppress",
    "file": "/home/runner/work/maa-framework/maa-framework/absolute-zero/examples/ada/balanced_ops.adb",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (3 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/maa-framework/maa-framework/absolute-zero/proofs/coq/quantum/QuantumMechanicsExact.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (33 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/maa-framework/maa-framework/absolute-zero/proofs/coq/quantum/QuantumCNO.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (3 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/maa-framework/maa-framework/absolute-zero/proofs/coq/lambda/LambdaCNO.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (1 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/maa-framework/maa-framework/absolute-zero/proofs/coq/category/CNOCategory.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (4 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/maa-framework/maa-framework/absolute-zero/proofs/coq/common/CNO.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (13 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/maa-framework/maa-framework/absolute-zero/proofs/coq/filesystem/FilesystemCNO.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "User-defined Coq axiom -- not verified by kernel (14 occurrences, CWE-704)",
    "type": "coq_axiom",
    "file": "/home/runner/work/maa-framework/maa-framework/absolute-zero/proofs/coq/physics/LandauerDerivation.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant