Skip to content

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

Merged
hyperpolymath merged 2 commits into
mainfrom
claude/seed-proof-debt-2026-05-26
May 27, 2026
Merged

docs: seed docs/proof-debt.md index per trusted-base policy#24
hyperpolymath merged 2 commits 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: 2.

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

Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 67 issues detected

Severity Count
🔴 Critical 14
🟠 High 34
🟡 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": "Action actions/upload-artifact@v4 needs attention",
    "type": "unpinned_action",
    "file": "release.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/download-artifact@v4 needs attention",
    "type": "unpinned_action",
    "file": "release.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Ada Unchecked_Conversion bypasses type safety (3 occurrences, CWE-704)",
    "type": "ada_unchecked_conversion",
    "file": "/home/runner/work/somethings-fishy/somethings-fishy/safety_kernel/src/robofishy_c_api.adb",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
    "type": "agda_postulate",
    "file": "/home/runner/work/somethings-fishy/somethings-fishy/verification/proofs/agda/Properties.agda",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "Admitted leaves proof hole (1 occurrences, CWE-704)",
    "type": "admitted",
    "file": "/home/runner/work/somethings-fishy/somethings-fishy/verification/proofs/coq/TypeSafety.v",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/somethings-fishy/somethings-fishy/verification/proofs/idris2/Types.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "assert_total bypasses totality checker (1 occurrences, CWE-704)",
    "type": "assert_total",
    "file": "/home/runner/work/somethings-fishy/somethings-fishy/verification/proofs/idris2/Types.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/somethings-fishy/somethings-fishy/verification/proofs/idris2/ABI/Pointers.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "assert_total bypasses totality checker (1 occurrences, CWE-704)",
    "type": "assert_total",
    "file": "/home/runner/work/somethings-fishy/somethings-fishy/verification/proofs/idris2/ABI/Pointers.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

The original CI for this PR resolved governance-reusable.yml@main to
SHA 7c2b815 (2026-05-26 pre-#219). `gh run rerun` re-runs with the
same workflow resolution and doesn't re-resolve @main. This empty
push forces a fresh run that will pick up current standards/main
(post-#219 workflow_sha fix).

No content changes.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath
hyperpolymath merged commit 758ff3e into main May 27, 2026
24 of 25 checks passed
@hyperpolymath
hyperpolymath deleted the claude/seed-proof-debt-2026-05-26 branch May 27, 2026 11:12
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