ADRs not yet approved, and the ADRs driving the centralised → distributed CI runner migration

[cgbarlow]

Update (2026-06-20 NZT): An audit of every Proposed ADR found 8 whose implementations had already shipped and released on main while their status still read Proposed. Those were corrected to Accepted in #2844 (merged). The lists below reflect the corrected state; the 8 are recorded in the "Corrected" table.

This discussion tracks two related views over the ADR catalogue (docs/adrs/adrs.json, 73 ADRs): (1) every ADR not yet at the Accepted approval state, and (2) the subset of ADRs — Accepted and Proposed — that drive the migration away from paid, centralised CI runners toward a distributed/decentralised runner model.

The repo has no literal approved status string; the canonical approval state is Accepted. "Other than approved" below therefore means not Accepted — the 9 Proposed ADRs. (ADR-020 carries Accepted (sponsor signed up: Chris Barlow, 2026-06-12) — it is approved, just annotated, so it's excluded from List 1.)

List 1 — ADRs with status other than approved (Proposed)

These are genuine roadmap proposals: at most a spec exists, with no shipped implementation.

ADR	Title
ADR-030	Domain-Agnostic Distributed-Workload Engine (Plugin Seam)
ADR-050	Autonomous Trunk Skeleton for Reusable Agentic Work Orchestration
ADR-051	Autonomous Trunk Experience Layer for Contributors, Operators, and Agent Fleets
ADR-052	Verification Tiers and Auditability Evidence for Autonomous Work
ADR-053	Volunteer-Scale Claim Substrate
ADR-054	Agent Identity, Quotas, and Reputation
ADR-055	Repository Runtime Reconciler
ADR-056	Repo-as-OS Control Plane and Operator Interface
ADR-057	Structured Reasoning and Decision Communication Protocol

Corrected Proposed → Accepted in #2844 (implementations had shipped)

ADR	Implementation	PR(s)
ADR-058	Gate A job routing	#1915
ADR-060	goal-sourcing skill / gen_triples / leaderboard	#1836, #1837, #1838
ADR-062	swarm/sourcing.sh runner	#1898
ADR-063	sharded replay, now the required Gate A job	#1917
ADR-067	--if-pool-empty sourcing	#2112
ADR-068	Phase 1 fork mode + auto-merge enabler	#2152, #2158
ADR-069	launcher sourcing arm	#2148
ADR-070	duplicate-verifier-waste metric	#2161

List 2 — ADRs contributing to the centralised → distributed runners migration

This list spans both Accepted and Proposed ADRs. After #2844, the entire runner-architecture group is now Accepted (shipped) — only the broad reusable-engine vision (ADR-030) remains a proposal.

The spine is ADR-049 (Accepted), which names the problem directly: heavy Gate A verification runs on paid, centralised namespace.so ephemeral runners whose cost grows linearly with no asymptote as the autonomous swarm (ADR-005) scales. Issue #635 framed the goal as "SETI@home but for LLMs proving math." ADR-049's recommended direction is a tiered split — contributor-run runners with a mandatory cheap central re-check that keeps the Lean kernel as the sole truth oracle.

Runner architecture / topology — all now shipped

• ADR-049 — Decentralised CI Runner Architecture (Accepted) — the decision: tiered split + mandatory central re-check; detects a tampered runner by outcome, not attestation.
• ADR-058 — Runner Pool Segmentation & Verification Capacity Governance (Accepted — shipped ci(gate-a): route jobs to dedicated Namespace profiles #1915) — GitHub-hosted cheap/intake lane vs namespace.so trusted lane, codified in gate-a.yml.
• ADR-063 — Sharded Gate A Kernel Replay (Accepted — shipped feat: sharded Gate A kernel replay (ADR-063, #1909) #1917) — distributes the leanchecker replay across separate runners; now the required gate.
• ADR-062 — Swarm Goal-Sourcing Runner (Accepted — shipped feat: swarm goal-sourcing runner (ADR-062) #1898) — an unattended runner driven against a maintainer's own quota.
• ADR-068 — Fork-Native Contribution Mode (Accepted — Phase 1 shipped feat(swarm): fork-native contribution mode (ADR-068) #2152/feat(ci): fork auto-merge enabler (ADR-068 / SPEC-068-A §6) #2158) — fork PRs re-verified on upstream-hosted runners; a decentralised contribution path.

Central-cost reducers ADR-049 explicitly depends on

(These already captured most per-PR savings, which is what makes a mandatory central re-check affordable.)

• ADR-033 — Incremental (Diff-Scoped) Kernel Replay (Accepted)
• ADR-045 — Persistent Library Build Cache for Gate A (Accepted)
• ADR-046 — Namespace .lake Cache Volume for Gate A (Accepted)
• ADR-048 — Verify-on-Ingest (Accepted)

Driver & broader distributed vision

• ADR-005 — Autonomous Merge Policy (Accepted) — the scaling driver that makes centralised runner cost unbounded.
• ADR-030 — Domain-Agnostic Distributed-Workload Engine (Proposed) — the reusable "SETI@home for verifiable work" template; the one piece of this list still unbuilt.

---

Generated from docs/adrs/adrs.json (73 ADRs) — an auto-maintained index on main (added by #2253, refreshed post-merge). All linked ADR files are on main.

[cgbarlow]

The status correction described in the Update note above has landed: #2844 — docs(adr): correct status of 8 shipped ADRs from Proposed to Accepted (squash-merged to main).

It flips ADR-058, 060, 062, 063, 067, 068, 069 and 070 from Proposed → Accepted, each with a Status-History row citing its implementing PR. Source-only — the README.md / adrs.json index regenerated automatically via the post-merge adr-index workflow (ADR-073).

[cgbarlow]

Status refresh — 2026-06-22 (NZT)

Re-audited against docs/adrs/adrs.json on main. Since this discussion was written the catalogue has grown 73 → 84 ADRs, and the non-Accepted set has grown from 9 to 16 (14 Proposed + 2 Draft). None of the original List 1 nine have advanced — ADR-030 and ADR-050–057 are all still Proposed. Seven new non-Accepted ADRs have landed; the runner-migration picture (List 2) is unchanged.

List 1 update — new non-Accepted ADRs since #2844

Platform generalisation / "architected packages" — the Phase 6 frontier, pending founder ratification

ADR	Status	Title
ADR-078	Proposed	Sponsor-Registered Targets and Obligation-Discharge Credit
ADR-080	Draft	Platform Generalisation and the Self-Verification Gating Invariant
ADR-081	Draft	Problem Admission and the Skeleton Intake Pipeline

Fork / sourcing increments

ADR	Status	Title
ADR-076	Proposed	Sharded Fork Goal Selection
ADR-085	Proposed	Isolate the Sourcer in a Per-Sourcer Worktree (ADR-042 parity)

Other

ADR	Status	Title	Note
ADR-077	Proposed	Roadmap GitHub Project, Synced from Repo State	⚠️ implementation present (tools/project_sync, runs post-merge) — looks like a status-lag candidate for a #2844-style correction
ADR-079	Proposed	Deterministic Solver Provider (zero-LLM template/sympy)	correctly Proposed — rollout is deliberately sequenced behind ADR-078 / ADR-035, so not a status-lag

The original List 1 nine (ADR-030, 050, 051, 052, 053, 054, 055, 056, 057) are unchanged — still Proposed.

List 2 update — centralised → distributed runner migration

No change to the spine. The runner-topology group (ADR-049 / 058 / 062 / 063 / 068 / 069) remains Accepted (shipped), and the central-cost reducers (ADR-033 / 045 / 046 / 048) remain Accepted. ADR-030 is still the one unbuilt reusable-engine proposal. The newer ADR-076 (sharded fork goal selection) and ADR-085 (per-sourcer worktree isolation) are Proposed increments to the fork/sourcing path, not core topology.

What's outstanding

1. Runner-migration tail. The topology is shipped, but the decentralisation itself is not: full client-side / contributor-run runners and a lean4export cross-checker still have no Accepted ADR (tracked in README Roadmap Phase 5).
2. Generalised-platform vision (Phase 6). ADR-030 + the substrate cluster (ADR-050–056) plus the new generalisation decisions (ADR-078 Proposed, ADR-080 / 081 Draft) are all proposal/draft, pending founder ratification of the scope change — ADR-080 is explicitly flagged for Chris / Ocean to ratify. A first non-maths target (a verified-microkernel proof) is inbound.
3. ADR-057 (Structured Reasoning and Decision Communication Protocol) — still Proposed, no implementation.
4. Cleanup. ADR-077 status-lag (see table above) — worth folding into the next status-correction sweep.

The README Roadmap has been updated to reflect the Phase 6 generalisation work in #4836.

---

Re-generated from docs/adrs/adrs.json (84 ADRs) on main, 2026-06-22 NZT.

[cgbarlow]

Phase 5 — what's left for the decentralised-runner vision, and a decision tree

Analysis — 2026-06-23 (NZT). Research/ideation; nothing shipped.

Posting this because runners are currently the throughput bottleneck — they're verifying as fast as they can but the queue keeps growing. Here's where Phase 5 actually stands against ADR-049 / SPEC-049-A / the research proposal, and a decision tree for the path(s) forward (more than one can be true at once).

The crux

ADR-049 deliberately chose soundness over deep decentralisation, and says so in its own accepting that clause:

the headline central-cost reduction is modest, not SETI-scale … v1 decentralisation is shallow because the irreducible trusted re-elaboration and merge stay central by necessity — that central surface is the soundness guarantee.

So the half of Phase 5 that has shipped is the half that was never going to drain the queue. The bottleneck you're feeling is central Gate A capacity saturation, and the v1 architecture doesn't touch it. The one lever that breaks the linear cost — Phase 3 (lean4export + a tiny mathlib-free checker) — has not been started and is gated behind two unrun pilots.

Why the bottleneck persists (the technical crux — proposal Appendix A)

The central re-check must re-elaborate from source and run leanchecker + axiom_audit, all of which need the full mathlib environment resident (~12–20 GB). Per PR that's ~8 runner-min dominated by fixed environment-loading overhead, not the proof itself:

Operation	Cost
axiom_audit (serialised, 6–7 GB/process)	~165 s ← biggest single chunk, never scoped
leanchecker replay (incremental, ADR-033)	~60 s
3× cache restores	~25–60 s each
lake build --wfail (warm, ADR-045)	only ~41 s

That fixed cost × queue volume on a bounded set of paid runners (~4×16 GB today) is the wall. Phase 1 — the obvious "scope the build smaller" fix — was measured and closed: ADR-033/045 already captured those savings.

Shipped vs. left

Shipped: ADR-049 decision + Phase 0 conformance suite (#926); cost reducers (ADR-033/045/046/048); capacity governance (ADR-058 segmentation, ADR-063 sharded replay); decentralised contribution path (ADR-062 sourcing runner, ADR-068/069 fork-native — these let anyone prove, not verify).

Left:

• Phase 2 — advisory pre-filters + per-contributor rate-limiting (anti-abuse hygiene; non-merge-gating). Not built.
• Phase 3 — lean4export NDJSON + an independent checker (nanoda, <5 kLOC Rust) that re-checks with no mathlib, no Lean resident, trivially parallel, runnable anywhere. The asymptote-breaker. Not started, pilot-gated.
• Phase 4 — peer-consensus / spot-audit overlay; advisory-only, own anti-sybil ADR.
• Volunteer-scale substrate (all Proposed): verification tiers + auditability (ADR-052), claim substrate (ADR-053), identity/quotas/reputation (ADR-054).

Note: the literal "SETI@home" readings (BYO self-hosted runners, N-of-M peer consensus, TEE attestation) are explicitly rejected as unsound (ADR-049 Options 4/6/7). For a domain with a cheap exact verifier, one kernel verdict is ground truth — you don't vote on it. "Fully decentralised" realistically means Phase 3's end-state: elaboration offloaded to the swarm, the central gate shrunk to a seconds-long mathlib-free re-check that parallelises without bound.

The three tracks

• Track A — Capacity (buys runway; slope stays linear). Drains the queue now. Not decentralisation.
• Track B — Structural (changes the slope). Phase 3. The only path where capacity scales with the swarm instead of with the namespace bill.
• Track C — Volunteer scale. Untrusted contributors running verification, not just proving. Downstream of B.

Decision tree

flowchart TD
    S["Runners are the bottleneck: queue not draining"] --> Q0{"What are we actually solving?"}
    Q0 -->|"Drain the queue now"| A["TRACK A — Capacity<br/>buys runway, slope stays linear"]
    Q0 -->|"Make capacity scale with the swarm"| B["TRACK B — Structural<br/>changes the cost slope"]
    Q0 -->|"Open verification to untrusted volunteers"| C["TRACK C — Volunteer scale"]

    A --> A1{"Where is the cost?"}
    A1 -->|"Fixed per-PR overhead (axiom_audit ~165s)"| A1a["Scope / parallelise axiom_audit to the changed closure"]
    A1 -->|"Throughput per runner"| A2["Batch verification: load mathlib once, verify K proofs, merge the greens"]
    A1 -->|"Raw parallelism"| A3["Add namespace shards / raise in-flight cap (pure spend, linear)"]

    B --> B1{"Phase-3 pilot Q2: is lean4export deterministic across machines?"}
    B1 -->|"No"| Bx["Export usable only as tamper-evidence / dedup, not a cross-machine oracle → stay central, lean on Track A"]
    B1 -->|"Yes"| B2{"Phase-3 pilot Q3: is the independent-checker wall-clock bounded? (no 100x pathology)"}
    B2 -->|"No"| By["Keep leanchecker authoritative; export stays advisory defense-in-depth only"]
    B2 -->|"Yes"| B3["Adopt export re-check as a 2nd, kernel-diverse anchor"]
    B3 --> B4["Promote to the cheap central gate: NO mathlib resident → re-check parallelises without bound"]
    B4 --> B5["FULLY DECENTRALISED verification: seconds-long re-check runs anywhere, even on contributor machines"]

    C --> C1{"Is Track B's cheap re-check real yet? (reached B4)"}
    C1 -->|"No"| Cx["Premature: volunteers cannot run a ~20GB mathlib-resident gate"]
    C1 -->|"Yes"| C2["Add anti-abuse: Phase 2 pre-filters + per-contributor rate-limits"]
    C2 --> C3["Build the substrate: ADR-052 tiers, ADR-053 claims, ADR-054 identity/quotas/reputation"]
    C3 --> C4["Volunteer-scale verification; identity stays hygiene, the kernel still decides"]

    A1a -.->|"buys runway for"| B
    A2 -.->|"buys runway for"| B

Loading

Decisions to be made

#	Decision	Type	If yes →	If no →
D1	Pursue capacity relief now (Track A)?	Operational	Pick any/all of D1a–c below — they compose	Queue latency keeps growing until Track B lands
D1a	Scope/parallelise axiom_audit to the changed closure?	Eng (likely biggest near-term win — it's the ~165 s chunk and was never scoped)	Real per-PR saving, no soundness-surface change to control flow	—
D1b	Batch verification (one mathlib load, K proofs)?	Eng + dispatch model	Throughput multiplies per runner-minute	— interacts with per-PR auto-merge (ADR-005)
D1c	Add namespace shards / raise in-flight cap?	Spend	Immediate parallelism	Linear cost, no asymptote (the baseline we're trying to escape)
D2	Commit to running the Phase-3 pilot (Track B)?	Strategic	Run the two experiments below — the only slope-changer	The cost slope stays linear forever; capacity = spend
D3 (Q2)	Is lean4export deterministic across contributor↔central machines for unsorry-scale closures?	Empirical — answered by the pilot	Export hashing is a valid cross-machine oracle → proceed to Q3	Export is tamper-evidence/dedup only; Phase-3-as-decentralisation is dead, stay on Track A
D4 (Q3)	Is the independent checker's wall-clock bounded (no "100× slower" pathology)?	Empirical — answered by the pilot	Adopt export re-check as a 2nd anchor → promote to cheap gate → fully decentralised	Keep leanchecker authoritative; export stays advisory only
D5	Open verification to untrusted volunteers (Track C)?	Strategic + founder scope	Requires D2→B4 and Phase 2 anti-abuse and ratifying ADR-052/053/054	Verification stays project-run (contribution can still be fork-native)

Invariant on every path: soundness is always the central kernel verdict at p = 1; identity/reputation/consensus stay hygiene, never load-bearing (ADR-007). Track B doesn't remove the central gate — it makes it cheap enough to run anywhere and in parallel.

Recommended shape (multiple true at once)

1. Now — D1a + D1b (Track A): scope axiom_audit and prototype batch verification. Biggest near-term queue relief without touching the soundness surface. Buys runway.
2. In parallel — D2 (Track B): run the Phase-3 pilot (small, self-contained: export ~10–20 real closures on two machines → determinism rate; run nanoda over them → wall-clock + timeout-hit rate). This is the only decision that changes the slope; everything in Track A just buys time for it.
3. Later — D5 (Track C): only meaningful once B reaches B4 (cheap re-check) and the substrate ADRs are ratified.

The clean mental model: Track A buys runway, only Track B changes the slope, Track C rides on B.

Happy to spec the Phase-3 pilot (the determinism + wall-clock experiment design) or cost-model the axiom_audit/batching options against the current ~4×16 GB setup as a next research step — design only, nothing shipped.