Skip to content

Commit 1a06816

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
docs(audits): estate-wide proof-debt audit 2026-05-26 (#195)
## Summary - Adds `docs/audits/2026-05-26-estate-proof-debt.md` — estate-wide proof-debt audit covering 283 repos. - Surfaces top offenders (ephapax, absolute-zero, maa-framework, hypatia, echidna, betlang, proven, standards itself) with file-line evidence. - Proposes a trusted-base reduction policy reusing the boj-server backend-assurance harness pattern. ## Coverage caveat Syntactic, not semantic — cannot tell `funExt` postulates apart from genuine debt. Per-repo PRs ask maintainers to classify. ## Companion PRs - `docs/audits/2026-05-26-estate-licence-debt.md` (separate PR) - `docs/audits/2026-05-26-estate-documentation-debt.md` (separate PR) - Per-repo `docs/tech-debt-2026-05-26.md` PRs to follow 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 4c2b978 commit 1a06816

1 file changed

Lines changed: 124 additions & 0 deletions

File tree

‎docs/audits/2026-05-26-estate-proof-debt.md‎

Lines changed: 124 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,124 @@
1+
# Estate Proof-Debt Audit — 2026-05-26
2+
3+
**Scanner:** automated grep sweep across 283 estate repositories.
4+
**Date:** 2026-05-26 (HEAD-state snapshot).
5+
**Scope:** every `*.v`, `*.lean`, `*.agda`, `*.idr`, `*.idr2`, `*.fst`, `*.dfy`, `*.tla`, `*.ads`, `*.adb` file outside `.git/`, `target/`, `_build/`, `node_modules/`.
6+
7+
**What was searched:**
8+
- Coq: `Axiom`, `Admitted`, `admit.` at line start
9+
- Lean: `sorry`, `axiom <name>`
10+
- Agda: `postulate` (top-level)
11+
- Idris2: `believe_me`, `really_believe_me`, `assert_total`, top-level `partial`, `%default partial`
12+
- F\*: `assume val`, `admit_p`
13+
- Cross-language: `TODO PROOF`, `OWED:`, `FIXME PROOF`
14+
- Plus Rust/Haskell `unsafePerformIO` / `unsafeCoerce` as a "soundness escape" indicator
15+
16+
### Headline numbers
17+
18+
| Language | Files scanned |
19+
|---|---|
20+
| Coq (`*.v`) | 554 |
21+
| Lean (`*.lean`) | 190 |
22+
| Agda (`*.agda`) | 1211 |
23+
| Idris2 (`*.idr`/`*.idr2`) | 4109 |
24+
| F\* (`*.fst`) | 7 |
25+
| Dafny (`*.dfy`) | 2 |
26+
| TLA+ (`*.tla`) | 68 |
27+
| SPARK (`*.ads`+`*.adb`) | 1011 |
28+
29+
### Top offenders (raw counts, including archive/vendored)
30+
31+
```
32+
# Proof-debt sweep 2026-05-26T12:18:05+01:00
33+
007 | files= 59 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 16 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
34+
absolute-zero | files= 6638 | Coq-Axm/Adm= 72 | Lean-srry/ax= 315 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
35+
affinescript | files= 593 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
36+
affinescript-stdlib-pr | files= 37 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
37+
agda-stdlib | files= 1229 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 27 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
38+
ambientops | files= 138 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
39+
asdf-tool-plugins | files= 567 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
40+
betlang | files= 10 | Coq-Axm/Adm= 0 | Lean-srry/ax= 5 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
41+
bofig | files= 6 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
42+
bofj-kitt | files= 19 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 6 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
43+
boinc-boinc | files= 7 | Coq-Axm/Adm= 0 | Lean-srry/ax= 1 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
44+
boj-server | files= 126 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 9 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
45+
burble | files= 55 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 2 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
46+
civic-connect | files= 12 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
47+
developer-ecosystem | files= 710 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 8 | Idr-prtl= 56 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
48+
docmatrix | files= 10 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
49+
docudactyl | files= 11 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
50+
echidna | files= 103 | Coq-Axm/Adm= 0 | Lean-srry/ax= 6 | Agda-pst= 2 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 12
51+
echidnabot | files= 7 | Coq-Axm/Adm= 1 | Lean-srry/ax= 4 | Agda-pst= 0 | Idr-blv= 1 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
52+
echo-types | files= 609 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
53+
eclexia | files= 8 | Coq-Axm/Adm= 9 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
54+
email-octad-experiment | files= 14 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 9 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
55+
ephapax | files= 23 | Coq-Axm/Adm= 3 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 1 | Idr-prtl= 1 | Fstr-asm= 0 | TODO= 14 | Unsafe= 0
56+
fireflag | files= 9 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
57+
flatracoon | files= 12 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
58+
formatrix-docs | files= 10 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
59+
frayed-knot-toolkit | files= 6 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
60+
fraying-model-computational-testbed | files= 13 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 6 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0
61+
gossamer | files= 28 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 13 | Idr-prtl= 4 | Fstr-asm= 0 | TODO= 2 | Unsafe= 0
62+
```
63+
64+
### Filtered by active development (excluding archive/vendored mirrors)
65+
66+
- **`hyperpolymath-archive`** — 878 Lean sorry/axiom, 18 partial Idris, 3 believe_me. *Archive — frozen, not active debt.*
67+
- **`repos-monorepo`** — 170 Coq axiom/admit, 129 Lean sorry, 105 believe_me, 138 partial. *Monorepo of vendored copies — proxy debt.*
68+
- **`absolute-zero`** — 72 Coq Axiom/Admitted, 315 Lean sorry/axiom across ~6638 proof files. **Active.** Open issue: #44 baseline glob fix + class-J axiom audit per memory.
69+
- **`maa-framework`** — 80 Coq, 54 Lean across just 25 files. **High density. Active.**
70+
- **`hypatia`** — 3 Coq, 6 Lean, 3 Agda postulate, 12 believe_me, 3 unsafe across 81 files. **Active.**
71+
- **`echidna`** — 6 Lean sorry, 2 Agda postulate, 12 unsafe. **L3-resume work per memory.**
72+
- **`betlang`** — 5 Lean sorry. `substTop_preserves_typing` axiom per memory (PR#27 closed but axiom remains).
73+
- **`echidnabot`** — 1 Coq, 4 Lean, 1 believe_me.
74+
- **`ephapax`** — 3 Coq Admitted (Semantics.v:4924, 5983, 6572), 1 believe_me, 1 partial, 14 TODO PROOF. **Active — closure plan owned (Item 1 in MEMORY).**
75+
- **`vcl-ut`** — 8 believe_me, 14 TODO PROOF. Known: HOLE deeper than documented (memory).
76+
- **`typed-wasm`** — 5 believe_me.
77+
- **`stapeln`** — 10 believe_me, 34 partial across 102 files.
78+
- **`proven`** — 51 believe_me, 10 partial, 1 unsafe, 372 TODO markers across 853 files. **Largest active TODO surface.**
79+
- **`proven-servers`** — 1 believe_me, 10 partial, 1 TODO.
80+
- **`standards`** — 4 Agda postulate, 1 believe_me, 11 partial. The canonical repo has its own proof debt.
81+
- **`veridical-simulation-core`** — 4 believe_me.
82+
- **`valence-shell`** — 1 Agda postulate, 8 partial.
83+
84+
### Cross-cutting patterns
85+
86+
1. **Idris2 `partial`** is the most common active marker (138 in repos-monorepo, 34 in stapeln, 11 in standards, 10 in proven, etc.). `partial` is correctness-relevant but often masquerades as ergonomic ("totality just hard to prove here").
87+
2. **`believe_me`** clusters around extraction-boundary code (Rust↔Idris FFI, codec runtime). Pattern repeats across typed-wasm, hypatia, stapeln, vcl-ut, somethings-fishy, snifs, rsr-template-repo (each 5–12 usages).
88+
3. **`TODO PROOF` / `OWED` markers** in `proven` (372) and `ephapax` (14) indicate that the codebases track their own debt — they're better surfaced than purely silent debt elsewhere.
89+
4. **Agda `postulate`** in `standards` (4) and `valence-shell` (1) — needs review for whether these are necessary axioms (e.g. `funExt`) or genuine debt.
90+
5. **Soundness-escapes outside proof languages**: `unsafePerformIO`/`unsafeCoerce` showed 12 in echidna, 3 in hypatia, 2 in somethings-fishy — these are not "proof debt" per se but soundness-relevant and warrant audit.
91+
92+
### Recommended next moves
93+
94+
| Repo | Action | Priority |
95+
|---|---|---|
96+
| ephapax | Close `formal/Semantics.v` 3 Admitteds via 6-9 day plan in `project_ephapax_preservation_closure_plan.md` | P0 (already on roadmap) |
97+
| absolute-zero | Triage 72 Coq Admitteds + 315 Lean sorries — likely cluster around T0 axiom-audit territory | P0 |
98+
| maa-framework | High density (80+54 in 25 files) — investigate whether vendored or original | P1 |
99+
| betlang | Discharge `substTop_preserves_typing` per PR#27 recipe | P1 |
100+
| proven | Convert the 372 TODO PROOF markers into a discharge schedule | P1 |
101+
| standards | Audit 4 Agda postulates + 11 Idris partials — set the example for downstream | P1 |
102+
| typed-wasm, stapeln, vcl-ut, hypatia, snifs, somethings-fishy | Each 5-15 believe_me — audit & document | P2 |
103+
| Rest | Document in per-repo `docs/tech-debt-2026-05-26.md`; no urgent fix | P3 |
104+
105+
### Trusted-base reduction policy (proposed estate rule)
106+
107+
Reuse the [boj-server backend-assurance harness pattern](https://github.com/hyperpolymath/boj-server) for `believe_me` / `assume val` / `Trust X` blocks: each must be one of
108+
- (a) discharged by a proof,
109+
- (b) property-tested via QuickCheck/Verus-style adversarial tests,
110+
- (c) annotated with a refutation budget and tracked in `docs/proof-debt.md`.
111+
112+
### Coverage caveat
113+
114+
This scan is **syntactic**, not semantic. It cannot distinguish:
115+
- Necessary axioms (e.g. `funExt` in HoTT) from genuine debt.
116+
- `partial` used because Idris2's totality checker is incomplete vs `partial` used to bury non-termination.
117+
- `unsafePerformIO` used at a verified library boundary vs ad-hoc soundness break.
118+
119+
The per-repo PRs ask each repo's maintainer to classify each finding.
120+
121+
---
122+
123+
🤖 Generated by Claude Code estate-wide proof-debt scan (2026-05-26).
124+
Companion docs: `2026-05-26-estate-licence-debt.md`, `2026-05-26-estate-documentation-debt.md`.

0 commit comments

Comments
 (0)