Estate Proof-Debt Remediation — sequenced campaign
Master artifact: ~/dev/repos/PROOF-DEBT-AND-RUST-SPARK-AUDIT-2026-05-18.adoc (reconciled vs direct re-grep 2026-05-18; parallel survey agents systematically under-report — always re-grep before trusting any PROOF-NEEDS "zero believe_me" line).
This epic tracks discharge of verified proof debt across the estate in strict priority order. Each sub-issue reconciles the repo's PROOF-NEEDS against ground truth in the same pass. PRs use Refs hyperpolymath/standards#<this>; joint-close only on explicit agreement (major+requirements-target convention).
Verified ground truth (re-grep 2026-05-18)
| Repo |
believe_me |
other escapes |
tier |
| boj-server |
9 (3 files) |
— |
P0 |
| echidna |
21 (17 files) |
2 assert_total; E-series Lean DONE (#53 PR#71); 1 stray sorry ParetoMaximality.lean |
P0 |
| ambientops |
— |
19 SPARK_Mode, ~11 contract-less; no stance doc |
P0 |
| proof-of-work |
— |
seam+stance landed today; OWED ABI postulates |
P0-discharge |
| stapeln |
10 |
20 idris_crash, 45 partial, chainCommutative regression |
P1 |
| typed-wasm |
5 |
5 assert_total (trusted transitively) |
P1 |
| gossamer |
11 |
— (Rust frozen, proofs still owe) |
P1 |
| proven |
1 |
~30 Safe* modules w/o Proofs.idr |
P1 |
| absolute-zero |
— |
Lean CNO cons-case + Coq tier-0 |
P2 |
| ephapax |
— |
11 partial; also Rust/SPARK NON-COMPLIANT (no seam) |
P2 |
Leave alone (correct): standards 6 info-theory postulates; echo-types R-2026-05-18; stapeln crypto hardness axioms.
Withdraw not catch-up: Julia suite proof claims (redundant with JULIA-SUITE-ADVERSARIAL-AUDIT).
Execution order
P0 → P1 → P2, finishing each tier before the next (CAP ordering: corrective first). Sub-issues below.
Estate-level (parallel)
Add standards CI lint: fail safety-critical Rust without ABI/FFI seam + stance line; fail SPARK_Mode On with zero contracts (kills theatre). Do NOT blind-sweep proof markers across ~9,500 files — annotate at repo (PROOF-NEEDS) level only.
🤖 Generated with Claude Code
Estate Proof-Debt Remediation — sequenced campaign
Master artifact:
~/dev/repos/PROOF-DEBT-AND-RUST-SPARK-AUDIT-2026-05-18.adoc(reconciled vs direct re-grep 2026-05-18; parallel survey agents systematically under-report — always re-grep before trusting any PROOF-NEEDS "zero believe_me" line).This epic tracks discharge of verified proof debt across the estate in strict priority order. Each sub-issue reconciles the repo's
PROOF-NEEDSagainst ground truth in the same pass. PRs useRefs hyperpolymath/standards#<this>; joint-close only on explicit agreement (major+requirements-targetconvention).Verified ground truth (re-grep 2026-05-18)
sorryParetoMaximality.leanLeave alone (correct): standards 6 info-theory postulates; echo-types R-2026-05-18; stapeln crypto hardness axioms.
Withdraw not catch-up: Julia suite proof claims (redundant with JULIA-SUITE-ADVERSARIAL-AUDIT).
Execution order
P0 → P1 → P2, finishing each tier before the next (CAP ordering: corrective first). Sub-issues below.
Estate-level (parallel)
Add standards CI lint: fail safety-critical Rust without ABI/FFI seam + stance line; fail
SPARK_Mode Onwith zero contracts (kills theatre). Do NOT blind-sweep proof markers across ~9,500 files — annotate at repo (PROOF-NEEDS) level only.🤖 Generated with Claude Code