The repo's own bar (ROADMAP.adoc:337-346): "zero known soundness bugs" ; the anti-definition is CAPABILITY-MATRIX.adoc:211-216 — v1 is the state in which every clause of that section can be deleted truthfully. This umbrella is the single map from today (2026-06-11, 416-test green gate, CORE-01 closed) to a defensible v1 claim. Derived from the 2026-06-11 whole-picture + estate inventory (47 local issues, 56 external items, 42 doc-stated untracked items).
T0 — soundness/correctness ("no reservations this is a language")
Order matters; all are accepts-wrong-program or silent-wrong-output classes:
soundness: use-after-move through a callee-returned borrow is accepted end-to-end (post-CORE-01 hole) #554 — use-after-move via callee-returned borrow (execution-verified). Fix or loud over-reject; the repo's own v1 bar forbids shipping this open.
tracking: general effect-handler dispatch (post-CORE-02 residual) — silent arm-drop on 3 backends; DECISION: back-port loud failure now? #555 — silent handler arm-drop on core-WASM/JS-text/Deno-ESM (execution-verified 41-vs-42 on an effects-free program). Decision in-issue: back-port loud failure now.
codegen: Async CPS table-miss silently falls back to synchronous lowering — should fail loudly #556 — Async CPS table-miss silently lowers synchronously.
soundness: refinement-type predicates parse but are silently not enforced (TRefined) #558 — refinement predicates parse but silently don't enforce; loud-reject until enforced.
tracking: CORE-04 traits residual — associated-type substitution, where-clause supertraits, coherence checking #559 — trait coherence absence (overlapping impls resolve arbitrarily) — the T0 slice of CORE-04.
gate hardening: auto-merge has fired on red builds (#334-#336, #344) — require status checks #557 — gates that gate: branch protection + promote --typed-wasm verification from informational to blocking (Tranche A1).
T1 — v1-blocking completeness
tracking: ADR-022 Polonius origin/region variables — implementation M1–M4 (lib/borrow_polonius/) #553 — ADR-022 Polonius M1–M4 (~6–12 wks, the dominant item) or a recorded v1 cut: lexical checker + soundness: use-after-move through a callee-returned borrow is accepted end-to-end (post-CORE-01 hole) #554 fixed + disclosed over-rejection. The "zero known soundness bugs" bar permits incompleteness, not unsoundness.
codegen wall 1: variable-string wasm backend ops (String.length / indexing / startsWith / fromCharCode) #560 / codegen wall 2: effect codegen — module-level mutable state / Date.now / Console.log on core-WASM #561 — the two codegen walls (variable strings; module-state/host effects) — together they gate ~32% of the real-world migration corpus on the blessed backend.
tracking: CORE-04 traits residual — associated-type substitution, where-clause supertraits, coherence checking #559 — CORE-04 completeness slice (associated-type substitution in bodies, where-clause supertraits).
Stage E1 / CONV-05 / INT-12: emit known-good + known-bad fixture corpus into typed-wasm cross_compat (C5.1) #562 — Stage E1/CONV-05/INT-12 fixture corpus into typed-wasm cross_compat (Stage E exit criterion; harness side already landed upstream).
Umbrella: standard library roadmap (50 items, 5 tiers) #412 Phase A — stdlib Tier-1 (runtime/codegen items where check passes but eval/wasm fails).
INT-04 residual — flip the JSR/npm publish go-switch (dry-run green, owner-gated).
Doc-truth refresh — CAPABILITY-MATRIX borrow row + :213, README.adoc:36, "interpreter-complete" cell (PR in flight 2026-06-11). Trap recorded in soundness: use-after-move through a callee-returned borrow is accepted end-to-end (post-CORE-01 hole) #554 : refresh only WITH the new holes documented.
T2 — v1-scoping decisions to record (each needs an explicit, written cut)
#245 (raw/FFI doctrine — recommend "no raw escape" reaffirmed), #249 (:: value-call doctrine), #262 (one-module-per-file doctrine), #228 (ADR-014 formal close — parse blockers all landed), #235 (closure-ABI: accept static+single-engine validation for v1?), #513 (proof programme: defer #514 –#521 post-v1 with disclosure , they are the formal backstop not the v1 gate), WasmGC ships as disclosed-partial (all gaps fail loudly — shippable), effects surface (handlers = interpreter-only-and-shallow, disclosed, after #555 fences land), ADR-020/021 + Tranche B1/D1 (cheap ADRs, land early), INT-05/INT-06 spinouts, benchmark-gate promotion, ADR-023 finality-types (Draft stub, post-#554 /#553 sequencing per its own constraints).
T3 — post-v1 (explicitly NOT v1 work)
Campaigns #229 /#230 /#406 ; bindings #446 + #450 –#454 + #497 /#498 /#501 ; satellites #56 /#182 /#183 /#392 /#489 + #413 ; proofs #514 –#521 ; #444 encoder dedup; #485 /#486 /#487 WASI tranche; #462 access-sites carrier (after #444 ); coprocessor framework ask (hyperpolymath/developer-ecosystem#110 , #114 ).
Estate cross-reference map (direction-tagged)
Upstream obligations (we owe them): hyperpolymath/echo-types#174 , hyperpolymath/echo-types#175 , hyperpolymath/echo-types#176 (db-theory proof carriers; #176 also expects stdlib/Select.affine + back-link which do not exist yet — re-scope when picked up). Local staged-not-filed: proposals/echo-types/EchoEncodingFaithfulness.agda.
Coordination (shared decisions/contracts): hyperpolymath/typed-wasm#35 (L13 mirror + needs our fixture corpus → #562 ), hyperpolymath/typed-wasm#50 (multi-producer adoption — we are the only realistic adopter), hyperpolymath/typed-wasm#54 , hyperpolymath/typed-wasm#126 (checker diagnostics seeded from our Checker.affine), hyperpolymath/ephapax#251 (sibling producer of the access-sites carrier — coordinate wire format with #462 ), hyperpolymath/standards#282 , hyperpolymath/standards#313 (Track-C roll-up → our #378 , triaged 2026-06-11), hyperpolymath/standards#343 (dotfile drift cluster).
Downstream (waiting on us — the v1 pressure): standards campaigns hyperpolymath/standards#239 (TS→AS umbrella; STEP items #243 , #245 , #276 , #278 , #279 incl. the only panll-726-file tracker, #280 , #281 , #326 (Bytes/binary-IO stdlib ask), #327 (random/time stdlib ask)), hyperpolymath/standards#252 (RS→AS umbrella), hyperpolymath/idaptik#84 + hyperpolymath/idaptik#137 + hyperpolymath/idaptik#150, hyperpolymath/reposystem#33 + hyperpolymath/reposystem#93 , hyperpolymath/stapeln#92 + hyperpolymath/stapeln#93 , hyperpolymath/svalinn#34 (affine-typing-gated escape-hatch elimination), hyperpolymath/neurophone#93 (affine lifecycle proofs) + hyperpolymath/neurophone#114 (first Gossamer AS UI), hyperpolymath/proven#86 + hyperpolymath/proven#88 , hyperpolymath/echidna#117 + hyperpolymath/echidna#240 , hyperpolymath/quandledb#43 , hyperpolymath/boj-server#67 + hyperpolymath/boj-server#202 , hyperpolymath/burble#53 + hyperpolymath/burble#91 , hyperpolymath/proof-burrower#14, hyperpolymath/my-lang#85 , hyperpolymath/gossamer#71 , hyperpolymath/developer-ecosystem#83 /#108 /#110 /#114 /#115 , hyperpolymath/gitbot-fleet#214 , hyperpolymath/verisimdb#84 (adjacency).
Stale-blocker re-triage (downstream cites closed blockers): idaptik#84 and boj-server#67 cite #160 /#161 /#162 (all CLOSED); quandledb#43 cites #508 (CLOSED); #446 /#450 /#489 cite #255 (CLOSED); #175 index lists closed children. Comments dispatched.
Calendar honesty
The repo's own estimate (STATE-2026-05-26.adoc:183): Polonius alone ~6–12 weeks single-author; everything else parallel-friendly ~4–8 weeks wall if typed-wasm coordination is prompt. T0 items 2–6 are days, not weeks — they should land first regardless of the Polonius decision, because they convert every silent failure to a loud one and make the v1 claim honest even while incomplete.
Umbrella filed 2026-06-11 from the whole-picture + estate inventory; supersedes nothing — #175 remains the doc-truthing index, #406 /#446 remain campaign umbrellas.
The repo's own bar (ROADMAP.adoc:337-346): "zero known soundness bugs"; the anti-definition is CAPABILITY-MATRIX.adoc:211-216 — v1 is the state in which every clause of that section can be deleted truthfully. This umbrella is the single map from today (2026-06-11, 416-test green gate, CORE-01 closed) to a defensible v1 claim. Derived from the 2026-06-11 whole-picture + estate inventory (47 local issues, 56 external items, 42 doc-stated untracked items).
T0 — soundness/correctness ("no reservations this is a language")
Order matters; all are accepts-wrong-program or silent-wrong-output classes:
--typed-wasmverification from informational to blocking (Tranche A1).T1 — v1-blocking completeness
cross_compat(Stage E exit criterion; harness side already landed upstream).T2 — v1-scoping decisions to record (each needs an explicit, written cut)
#245 (raw/FFI doctrine — recommend "no raw escape" reaffirmed), #249 (
::value-call doctrine), #262 (one-module-per-file doctrine), #228 (ADR-014 formal close — parse blockers all landed), #235 (closure-ABI: accept static+single-engine validation for v1?), #513 (proof programme: defer #514–#521 post-v1 with disclosure, they are the formal backstop not the v1 gate), WasmGC ships as disclosed-partial (all gaps fail loudly — shippable), effects surface (handlers = interpreter-only-and-shallow, disclosed, after #555 fences land), ADR-020/021 + Tranche B1/D1 (cheap ADRs, land early), INT-05/INT-06 spinouts, benchmark-gate promotion, ADR-023 finality-types (Draft stub, post-#554/#553 sequencing per its own constraints).T3 — post-v1 (explicitly NOT v1 work)
Campaigns #229/#230/#406; bindings #446 + #450–#454 + #497/#498/#501; satellites #56/#182/#183/#392/#489 + #413; proofs #514–#521; #444 encoder dedup; #485/#486/#487 WASI tranche; #462 access-sites carrier (after #444); coprocessor framework ask (hyperpolymath/developer-ecosystem#110, #114).
Estate cross-reference map (direction-tagged)
Upstream obligations (we owe them): hyperpolymath/echo-types#174, hyperpolymath/echo-types#175, hyperpolymath/echo-types#176 (db-theory proof carriers; #176 also expects
stdlib/Select.affine+ back-link which do not exist yet — re-scope when picked up). Local staged-not-filed:proposals/echo-types/EchoEncodingFaithfulness.agda.Coordination (shared decisions/contracts): hyperpolymath/typed-wasm#35 (L13 mirror + needs our fixture corpus → #562), hyperpolymath/typed-wasm#50 (multi-producer adoption — we are the only realistic adopter), hyperpolymath/typed-wasm#54, hyperpolymath/typed-wasm#126 (checker diagnostics seeded from our Checker.affine), hyperpolymath/ephapax#251 (sibling producer of the access-sites carrier — coordinate wire format with #462), hyperpolymath/standards#282, hyperpolymath/standards#313 (Track-C roll-up → our #378, triaged 2026-06-11), hyperpolymath/standards#343 (dotfile drift cluster).
Downstream (waiting on us — the v1 pressure): standards campaigns hyperpolymath/standards#239 (TS→AS umbrella; STEP items #243, #245, #276, #278, #279 incl. the only panll-726-file tracker, #280, #281, #326 (Bytes/binary-IO stdlib ask), #327 (random/time stdlib ask)), hyperpolymath/standards#252 (RS→AS umbrella), hyperpolymath/idaptik#84 + hyperpolymath/idaptik#137 + hyperpolymath/idaptik#150, hyperpolymath/reposystem#33 + hyperpolymath/reposystem#93, hyperpolymath/stapeln#92 + hyperpolymath/stapeln#93, hyperpolymath/svalinn#34 (affine-typing-gated escape-hatch elimination), hyperpolymath/neurophone#93 (affine lifecycle proofs) + hyperpolymath/neurophone#114 (first Gossamer AS UI), hyperpolymath/proven#86 + hyperpolymath/proven#88, hyperpolymath/echidna#117 + hyperpolymath/echidna#240, hyperpolymath/quandledb#43, hyperpolymath/boj-server#67 + hyperpolymath/boj-server#202, hyperpolymath/burble#53 + hyperpolymath/burble#91, hyperpolymath/proof-burrower#14, hyperpolymath/my-lang#85, hyperpolymath/gossamer#71, hyperpolymath/developer-ecosystem#83/#108/#110/#114/#115, hyperpolymath/gitbot-fleet#214, hyperpolymath/verisimdb#84 (adjacency).
Stale-blocker re-triage (downstream cites closed blockers): idaptik#84 and boj-server#67 cite #160/#161/#162 (all CLOSED); quandledb#43 cites #508 (CLOSED); #446/#450/#489 cite #255 (CLOSED); #175 index lists closed children. Comments dispatched.
Calendar honesty
The repo's own estimate (STATE-2026-05-26.adoc:183): Polonius alone ~6–12 weeks single-author; everything else parallel-friendly ~4–8 weeks wall if typed-wasm coordination is prompt. T0 items 2–6 are days, not weeks — they should land first regardless of the Polonius decision, because they convert every silent failure to a loud one and make the v1 claim honest even while incomplete.
Umbrella filed 2026-06-11 from the whole-picture + estate inventory; supersedes nothing — #175 remains the doc-truthing index, #406/#446 remain campaign umbrellas.