<!--
SPDX-License-Identifier: CC-BY-SA-4.0
SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
-->

# Tech-Debt Audit — developer-ecosystem — 2026-05-26

**Source:** estate-wide automated scan 2026-05-26.
**Companion:** [`hyperpolymath/standards` 2026-05-26-estate-*-debt audits](https://github.com/hyperpolymath/standards/tree/main/docs/audits).
**Combined severity:** `HIGH`.

This file records the *raw findings* — it does not by itself fix the debt. Each section ends with a 'Recommended next move' line; closing the debt is follow-up work.

## 1. Proof debt

Scanner counted the following markers in proof-bearing files of this repo:

```
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
```

**Total markers:** 64. **Severity:** `>064`.

**Marker types** (any non-zero counts above):
- Coq `Axiom`/`Admitted` — unconditional proof escapes.
- Lean `sorry`/`axiom` — Lean's equivalent.
- Agda `postulate` — accepted axiomatically.
- Idris2 `believe_me`/`assert_total` — runtime-safe coercion / totality assumption.
- Idris2 top-level `partial` — totality-check waived.
- F\* `assume val`/`admit_p` — F\* admit.
- `TODO PROOF` / `OWED:` — self-documented debt markers.
- `unsafePerformIO`/`unsafeCoerce` — soundness-relevant escape hatches in Haskell/Rust source.

**Recommended next move:** triage each finding into one of: (a) discharge by proof, (b) cover with property-tests + a documented refutation budget, or (c) annotate as a known/necessary axiom (e.g. `funExt`) in `docs/proof-debt.md`.

## 2. Licence debt

| Field | Value |
|---|---|
| LICENSE file | `LICENSE` |
| SPDX header | `MPL-2.0` |
| Manifest licence | `NONE` |
| Body classifier | `PMPL-1.0-or-later` |
| Severity | `HIGH-mismatch` |
| Notes | `SPDX=MPL-2.0_but_body=PMPL` |

**Recommended next move:** the SPDX header says `MPL-2.0` but the licence body still uses Palimpsest/PMPL language. Per estate policy (memory: `feedback_estate_lang_policy_2026_05_25`) the migration target is MPL-2.0. Replace the LICENSE body with the canonical MPL-2.0 text (keep SPDX header; can keep a small Palimpsest preamble as commentary).

## 3. Documentation debt

| Field | Value |
|---|---|
| README lines | 212 |
| `docs/` files | 3 |
| `docs/` LoC | 296 |
| CHANGELOG.md | N |
| CONTRIBUTING.md | Y |
| CODE_OF_CONDUCT.md | Y |
| SECURITY.md | Y |
| Severity | `MEDIUM` |

**Recommended next move:** introduce a `docs/` directory. The README at 212 lines has likely grown to do the work of `docs/` — split it into a thin README + `docs/architecture.md`, `docs/usage.md`, etc. Heavy-wiki exemplars to copy from: `affinescript`, `boj-server`, `echidna`, `hypatia`.

Additionally: **CHANGELOG.md is missing.** 65% of estate repos lack one — adopting a CHANGELOG (or auto-generating via `git-cliff`) is a recommended estate-wide follow-up.

## Cross-references

- Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md`
- Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md`
- Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md`

---

🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). This file is informational — closing the debt is follow-up work owned by the maintainer.
