docs: scope README/ROADMAP claims to shipped reality (ADR-0007, closes #51)

.machine_readable/6a2/STATE.a2ml

@@ -41,8 +41,8 @@ signaling-relay = { status = "consolidated", canonical = "signaling/relay.js", r
 [blockers-and-issues]
 doc-reality-drift = [
   "RESOLVED 2026-04-21: LLM service fully wired — AnthropicProvider, circuit breaker, per-user rate limit, NimblePool concurrency gating, SSE streaming, REST /llm/query + /llm/stream + /llm/status",
-  "ROADMAP.adoc claims Formal Proofs DONE — Avow attestation is data-type-only, no dependent-type enforcement",
-  "README.adoc PTP claim sub-microsecond assumes hardware — code falls back to system clock without NIF"
+  "RESOLVED 2026-05-19: Formal-proof claim scoped to compile/type-check only; runtime enforcement is roadmap per ADR-0008 (Option C, PoC #55) + ADR-0007 claim discipline",
+  "RESOLVED 2026-05-19: README comparison table + Status note state PTP <1us needs a PTP NIC (NTP ~1ms fallback), hardware unvalidated, per ADR-0007"
 ]
 resolved-2026-04-16 = [
   "Opus naming/contract drift: Backend.audio_encode/4 + audio_decode/3 docstrings rewritten to state explicitly that they are PCM frame pack/unpack, NOT Opus. Added explicit Backend.opus_transcode/4 callback returning {:error, :not_implemented} on every backend (ElixirBackend, ZigBackend, SmartBackend, SNIFBackend). Added opus_available?/0 callback (always false). Pinned by opus_contract_test.exs."

CHANGELOG.md

@@ -10,6 +10,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Changed
+- README/ROADMAP claims scoped to the shipped build per ADR-0007: QUIC & SNIF marked experimental (optional NIFs disabled by default), PTP <1µs flagged hardware-gated, Idris2 proofs flagged type-check-only (runtime enforcement = ADR-0008 Option C), latency/scale flagged unbenchmarked; added a README Status section. Closes the STATE.a2ml doc-reality-drift entries (issue #51)
+
 ### 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 (Accepted, Option C): scope the "formally verified" claim now (per ADR-0007) and fund a single-module runtime-enforcement PoC (issue #55)

README.adoc

@@ -15,6 +15,28 @@ modern browser-based joining — no downloads, no accounts, no friction.
 
 **One command to deploy. Sub-second to join. Your server, your rules.**
 
+== Status
+
+Burble is **pre-production** (targeting CRG grade C). The core — self-hosted
+WebRTC voice, browser join, OTP fault isolation — is operational and tested.
+Per link:docs/decisions/0007-claims-to-evidence-discipline.adoc[ADR-0007],
+every claim below maps to code + a test, or is flagged here:
+
+* *Experimental (optional, off by default):* QUIC transport and SNIF WASM
+  crash-isolation require optional NIFs (`quicer`/msquic, `wasmex`) that are
+  **disabled in the default build**; the runtime degrades gracefully without
+  them.
+* *Hardware-gated:* sub-microsecond PTP needs a PTP-capable NIC; without one
+  the system uses NTP (~1ms). PTP hardware is **unvalidated** (I210 pending).
+* *Roadmap:* the Idris2 ABI proofs compile and type-check; *runtime*
+  enforcement is not yet wired
+  (link:docs/decisions/0008-formal-proof-enforcement-vs-scope.adoc[ADR-0008],
+  Option C; PoC tracked in issue #55).
+* *Not yet benchmarked:* end-to-end mic-to-speaker latency and 500+
+  concurrent scale (issue #52).
+
+Foundational hardening is tracked in the "Earn the Core" epic (issue #53).
+
 == Why Burble?
 
 [cols="1,1,1,1,1"]
@@ -34,7 +56,7 @@ modern browser-based joining — no downloads, no accounts, no friction.
 | Yes
 
 | **Latency**
-| <10ms (Zig SIMD NIFs)
+| <10ms* (kernel-path target)
 | ~15ms
 | ~50-100ms
 | ~30ms
@@ -46,7 +68,7 @@ modern browser-based joining — no downloads, no accounts, no friction.
 | E2EE optional
 
 | **Precision timing**
-| IEEE 1588 PTP (<1us)
+| IEEE 1588 PTP (<1µs)*
 | No
 | No
 | No
@@ -58,6 +80,15 @@ modern browser-based joining — no downloads, no accounts, no friction.
 | Partial
 |===
 
+[NOTE]
+====
+*Honest status (link:docs/decisions/0007-claims-to-evidence-discipline.adoc[ADR-0007]):*
+`<10ms` is a Zig kernel-path target — end-to-end mic-to-speaker latency and
+500+ concurrent scale are **not yet benchmarked** (issue #52). `IEEE 1588
+PTP <1µs` requires a PTP-capable NIC; without one the system falls back
+to NTP (~1ms) and the PTP hardware path remains **unvalidated**.
+====
+
 == Key Features
 
 **Audio performance** — Zig SIMD coprocessor NIFs deliver 26,350x speedup over

ROADMAP.adoc

@@ -9,7 +9,7 @@ However, beneath this simple surface lies a **"Majestic"** architecture. For pow
 
 == Current Status
 
-Burble has cleared its foundational milestones. Test suite: 222+ Elixir tests + Zig coprocessor tests + 6 channel safety-contract tests + 6 Opus-contract tests + 5 AI bridge Deno tests (round-trip, ordering, reconnect, heartbeat). We are currently in a **phased hardening** cycle: audio reliability (Phase 1), P2P AI bridge dependability (Phase 2), then signaling/channels (Phase 3) and PTP hardware integration (Phase 4). See `.machine_readable/6a2/STATE.a2ml` for the authoritative status.
+Burble has cleared its foundational milestones. Test suite: 222+ Elixir tests + Zig coprocessor tests + 6 channel safety-contract tests + 6 Opus-contract tests + 5 AI bridge Deno tests (round-trip, ordering, reconnect, heartbeat). We are currently in a **phased hardening** cycle: audio reliability (Phase 1), P2P AI bridge dependability (Phase 2), then signaling/channels (Phase 3) and PTP hardware integration (Phase 4). See `.machine_readable/6a2/STATE.a2ml` for the authoritative status. Claim honesty is governed by ADR-0007; foundational hardening is tracked in the "Earn the Core" epic (#53).
 
 == Milestones
 
@@ -18,15 +18,15 @@ Burble has cleared its foundational milestones. Test suite: 222+ Elixir tests +
 * [x] WebRTC voice engine (SFU, Opus, ExWebRTC)
 * [x] E2EE via Insertable Streams (X25519 + AES-256-GCM)
 * [x] VeriSimDB integration & LMDB zero-copy playout buffering
-* [x] QUIC transport (0-RTT, multiplexed streams)
+* [x] QUIC transport (0-RTT, multiplexed streams) — _experimental: needs the optional `quicer`/msquic NIF, disabled in the default build (ADR-0007)_
 * [x] Zig SIMD coprocessor (audio, DSP, neural, compression)
 * [x] Groove discovery endpoint (/.well-known/groove)
 
 === v1.0.0 — Stable Release (DONE)
 
-* [x] QUIC hardening (rate limiting, datagram size enforcement)
+* [x] QUIC hardening (rate limiting, datagram size enforcement) — _experimental; see QUIC transport note (ADR-0007)_
 * [x] Bebop codegen & wire protocol schemas
-* [x] Idris2 ABI formal proofs (Avow consent, Vext integrity, Permissions)
+* [x] Idris2 ABI formal proofs (Avow consent, Vext integrity, Permissions) — _proofs compile/type-check; runtime enforcement is roadmap (ADR-0008 Option C; PoC #55)_
 * [x] Chainguard base Containerfile pinned by digest
 * [x] **Rate Limiting:** ETS Token Bucket algorithm for authentication paths.