hyperpolymath · hyperpolymath · May 19, 2026 · May 19, 2026
@@ -11,6 +11,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## [Unreleased]
 
 ### Added
+- ADR-0007 (Accepted): claims-to-evidence discipline & optional-dependency policy — every headline claim maps to code+test or is labelled experimental; optional NIF deps are experimental-until-wired. Closes the recurring `doc-reality-drift` blocker. Earn-the-Core epic #53
+- ADR-0008 (Proposed): formal-proof enforcement vs. scoping the "formally verified" claim — frames the maintainer decision (wire enforcement / scope the claim / hybrid), does not pre-decide it
+- Earn-the-Core foundational-hardening program filed as tracked issues (#53 epic; #48–#52 children)
 - ADR-0006: scoped and formally declined `proven-frame` hardening of `Burble.Bolt.Packet` (category mismatch — stream-framing core vs. a single-datagram record already total/safe via BEAM binary matching); closes the ADR-0005 backlog item
 - Typed `NifEvent` ADT for Zig NIF audio events (VadStateChange, AgcLevelChange, DenoiserConfidence)
 - Safe `pollEvents` returning `Maybe NifEvent` instead of raw `Bits64`

@@ -0,0 +1,67 @@
+= Architecture Decision Record: 0007-claims-to-evidence-discipline
+<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
+
+# 7. Claims-to-evidence discipline & optional-dependency policy
+
+Date: 2026-05-19
+
+## Status
+
+Accepted
+
+Formalises the recurring `STATE.a2ml [blockers-and-issues] doc-reality-drift`
+problem. Implements the doc-honesty half of the "Earn the Core" program
+(tracking epic + issue #51).
+
+## Context
+
+Doc-reality drift is a recurring, self-acknowledged failure mode: the
+README/ROADMAP have repeatedly claimed as DONE things that are partial in
+the shipped build (Formal Proofs "DONE" but no runtime enforcement; PTP
+"sub-microsecond" but the hardware clock NIF is unvalidated and absent;
+QUIC and SNIF marketed while `quicer`/`wasmex` are disabled optional deps;
+"<10 ms" / "500+ concurrent" unbenchmarked).
+
+Each overclaim taxes the credibility of the *true* core claims. The
+`EXPLAINME.adoc` "show me the receipts, with honest caveats" pattern is
+the correct instinct but is not enforced repo-wide, and "optional" NIF
+dependencies are described as if always present.
+
+## Decision
+
+1. **Claims map to evidence.** Every capability stated as fact in
+   `README.adoc` / `ROADMAP.adoc` / marketing-facing docs MUST map to (a)
+   a concrete code path and (b) an automated test. Anything not meeting
+   both goes in an explicit **Experimental** or **Aspirational** section,
+   clearly labelled as such.
+2. **Optional dependencies are experimental-until-wired.** A capability
+   that depends on an optional/disabled NIF (`quicer`/msquic,
+   `wasmex`/SNIF, `elmdb`, …) is **Experimental** in user-facing docs
+   until the dependency is built, enabled, and covered by a test in CI.
+   Runtime code already degrades gracefully (the `:quicer` /
+   `Burble.Bolt.Quic` pattern, ADR-0004; SNIF/`Wasmex`, PR #46) — the
+   *claims* must match that reality.
+3. **Drift is a release gate.** Re-attaining/holding CRG C includes a
+   check that headline claims have not regressed against this policy.
+
+## Consequences
+
+### Positive
+
+- The README's core claims become trustworthy; the strong core stops
+  being obscured by the augmented layer's ambition.
+- A single, citable policy to close `doc-reality-drift` entries against.
+
+### Negative
+
+- The README will, in the short term, *look* less impressive: several
+  features move under "Experimental". This is the point — honest scope
+  is the asset.
+
+### Neutral
+
+- No code change. Enforcement is editorial + a CI doc-claim check
+  (scoped under issue #51 / CRG-C #50).
+- The formal-proof "DONE vs enforced" claim is the subject of its own
+  decision — see ADR-0008.
@@ -0,0 +1,69 @@
+= Architecture Decision Record: 0008-formal-proof-enforcement-vs-scope
+<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
+
+# 8. Formal-proof enforcement vs. scoping the "formally verified" claim
+
+Date: 2026-05-19
+
+## Status
+
+Proposed
+
+This ADR frames a genuine open strategic decision for the maintainer; it
+deliberately does **not** pre-decide it. Part of the "Earn the Core"
+program.
+
+## Context
+
+Burble markets a "Majestic / Dual-Track" formally-verified posture. The
+reality (`BURBLE-PROOF-STATUS.md`, `PROOF-NEEDS.md`, `READINESS.adoc`):
+
+- All six Idris2 ABI proof modules **compile and type-check**
+  (Types, Permissions, Avow, Vext, MediaPipeline, WebRTCSignaling).
+- But **runtime enforcement is not wired**: `Burble.Verification.Avow`
+  is data-type-only; there is no bridge making the Elixir runtime reject
+  values that violate the proven types. `READINESS.adoc`: *"safe by
+  construction for current use cases. Dependent-type enforcement is a
+  correctness hardening measure, not a security boundary."*
+
+So "formally verified" is true at the *type-check* level and aspirational
+at the *runtime-enforcement* level. ADR-0007 requires this gap be either
+closed or scoped honestly; which one is a strategic choice with real cost.
+
+## Decision
+
+**To be decided by the maintainer.** Options:
+
+* **Option A — Wire enforcement.** Build the Idris2→runtime enforcement
+  bridge (proof-derived validators at the Elixir/Zig ABI boundary) as a
+  scheduled phase. Highest rigor; substantial effort; turns the
+  differentiator into a real moat (supports Route B "Majestic").
+* **Option B — Scope the claim.** State precisely: "ABI proofs compile
+  and type-check; runtime enforcement is on the roadmap." Cheap, honest,
+  immediately removes the overclaim; keeps the proofs as design
+  assurance rather than a runtime guarantee.
+* **Option C — Hybrid.** Scope the claim now (Option B wording) **and**
+  schedule enforcement for one high-value module (e.g. `Permissions` or
+  `Avow`) as a proof-of-concept before committing to the full bridge.
+
+Recommendation (non-binding): **Option C** — it satisfies ADR-0007
+immediately (no overclaim) while preserving the Majestic differentiator
+as a funded, scoped experiment rather than perpetual aspiration.
+
+## Consequences
+
+### Positive
+
+- Removes a long-standing overclaim regardless of which option is chosen.
+- Forces an explicit, recorded decision instead of silent drift.
+
+### Negative
+
+- Option A is expensive; Option B narrows the marketing story.
+
+### Neutral
+
+- Until accepted, ADR-0007 governs: the "formally verified" claim must
+  read as type-check-level only, with runtime enforcement labelled
+  Experimental/Aspirational.
@@ -35,4 +35,12 @@ New ADRs copy `0000-template.adoc` and take the next number.
 | link:0006-proven-frame-not-applicable-to-bolt-packet.adoc[0006]
 | proven-frame is not applicable to Burble.Bolt.Packet
 | Accepted
+
+| link:0007-claims-to-evidence-discipline.adoc[0007]
+| Claims-to-evidence discipline & optional-dependency policy
+| Accepted
+
+| link:0008-formal-proof-enforcement-vs-scope.adoc[0008]
+| Formal-proof enforcement vs. scoping the "formally verified" claim
+| Proposed
 |===