Index of the 108 ADRs in this directory, generated from the ADR-*.md headers and kept in sync by the adr-index workflow. See ADR-001 and the development protocols for the WH(Y) format and process.
| ADR | Title | Status | Date |
|---|---|---|---|
| ADR-001 | Adopt Development Protocols | Accepted | 2026-06-10 |
| ADR-002 | Lean 4 + mathlib4 Pinned to Release Tags | Accepted | 2026-06-10 |
| ADR-003 | AISP Coordination Format with In-Repo Validation | Accepted | 2026-06-10 |
| ADR-004 | Claims on a Dedicated Branch, First-Push-Wins | Accepted | 2026-06-10 |
| ADR-005 | Autonomous Merge Policy | Accepted | 2026-06-10 |
| ADR-006 | Gate A Soundness Enforcement | Accepted | 2026-06-10 |
| ADR-007 | Agent Identity and Budgets | Accepted | 2026-06-10 |
| ADR-009 | Goal Decomposition on Prove-Budget Exhaustion | Accepted | 2026-06-10 |
| ADR-010 | Affinity-Weighted, Gap-Based Goal Selection | Accepted | 2026-06-10 |
| ADR-011 | Statement-Binding Gate | Accepted | 2026-06-10 |
| ADR-012 | Backlog Sourcing | Accepted | 2026-06-10 |
| ADR-013 | Model & Effort Policy for Proof Runs | Accepted | 2026-06-11 |
| ADR-014 | Cross-Goal Dependency Reuse | Accepted | 2026-06-11 |
| ADR-015 | Progressive Effort Escalation | Accepted | 2026-06-11 |
| ADR-016 | Infrastructure-Failure Guard | Accepted | 2026-06-11 |
| ADR-017 | Swarm Supervisor and In-Flight-Work Guard | Accepted | 2026-06-11 |
| ADR-018 | Goal-Statement Immutability | Accepted | 2026-06-12 |
| ADR-019 | CI Supply-Chain & Workflow Protection | Accepted | 2026-06-12 |
| ADR-020 | Human-Sponsored Upstreaming | Accepted (sponsor signed up: Chris Barlow, 2026-06-12) | 2026-06-12 |
| ADR-021 | Sponsor PR Helper | Accepted | 2026-06-12 |
| ADR-022 | Local Provider Smoke Mode | Accepted | 2026-06-13 |
| ADR-023 | Optional Proof Provenance and Leaderboard | Accepted | 2026-06-13 |
| ADR-024 | Cross-Cycle Lesson Memory | Accepted | 2026-06-13 |
| ADR-025 | OpenAI-Compatible Local Endpoints and pi-coder Config | Accepted | 2026-06-13 |
| ADR-026 | PR Convention Enforcement and Trunk-Based Workflow | Accepted | 2026-06-13 |
| ADR-027 | Proof / Harness PR Separation | Accepted | 2026-06-13 |
| ADR-028 | Protocol-Compliance Gate (Spec-per-ADR) | Accepted | 2026-06-13 |
| ADR-029 | Harness Commit Authorship from GitHub Identity | Accepted | 2026-06-13 |
| ADR-030 | Domain-Agnostic Distributed-Workload Engine (Plugin Seam) | Proposed | 2026-06-13 |
| ADR-031 | Roadmap to Freek #50 (The Number of Platonic Solids) | Accepted | 2026-06-13 |
| ADR-032 | Proof Graph Visualiser | Accepted | 2026-06-13 |
| ADR-033 | Incremental (Diff-Scoped) Kernel Replay | Accepted | 2026-06-14 |
| ADR-034 | Recompose Failure Must Not Bury a Proved Subtree | Accepted | 2026-06-14 |
| ADR-035 | Non-Trivial Theorem Enforcement | Accepted | 2026-06-14 |
| ADR-036 | Refresh the Targets Board Post-Merge, Not In-PR | Accepted | 2026-06-14 |
| ADR-037 | Corroborated Solver Provenance — a Phantom-Attribution Guard | Accepted | 2026-06-14 |
| ADR-038 | Shared Web-Surface Design Language | Accepted | 2026-06-14 |
| ADR-039 | Re-exec the Agent When the Harness Updates | Accepted | 2026-06-14 |
| ADR-040 | Changelog Fragments (one file per change) | Accepted | 2026-06-14 |
| ADR-041 | Proof Archive Blocks | Accepted | 2026-06-14 |
| ADR-042 | Run the Agent in an Isolated Per-Agent Worktree | Accepted | 2026-06-14 |
| ADR-043 | The Identity Engine — mass-source mathlib-absent elementary identities at scale | Accepted | 2026-06-14 |
| ADR-044 | Idle Recovery of Goals Parked Below the Viability Floor | Accepted | 2026-06-15 |
| ADR-045 | Persistent Library Build Cache for Gate A | Accepted | 2026-06-15 |
| ADR-046 | Namespace .lake Cache Volume for Gate A |
Accepted | 2026-06-15 |
| ADR-048 | Verify-on-Ingest — Kernel-Verify Each Proof Once, Then Trust Immutability | Accepted | 2026-06-15 |
| ADR-049 | Decentralised CI Runner Architecture — Tiered Split with a Mandatory Cheap Central Re-check | Accepted | 2026-06-15 |
| ADR-050 | Autonomous Trunk Skeleton for Reusable Agentic Work Orchestration | Proposed | 2026-06-15 |
| ADR-051 | Autonomous Trunk Experience Layer for Contributors, Operators, and Agent Fleets | Proposed | 2026-06-15 |
| ADR-052 | Verification Tiers and Auditability Evidence for Autonomous Work | Proposed | 2026-06-15 |
| ADR-053 | Volunteer-Scale Claim Substrate | Proposed | 2026-06-15 |
| ADR-054 | Agent Identity, Quotas, and Reputation | Proposed | 2026-06-15 |
| ADR-055 | Repository Runtime Reconciler | Proposed | 2026-06-15 |
| ADR-056 | Repo-as-OS Control Plane and Operator Interface | Proposed | 2026-06-15 |
| ADR-057 | Structured Reasoning and Decision Communication Protocol | Proposed | 2026-06-16 |
| ADR-058 | Runner Pool Segmentation and Verification Capacity Governance | Accepted | 2026-06-16 |
| ADR-059 | Fetch Resilience on the Shared Object Store | Accepted | 2026-06-16 |
| ADR-060 | Contributor-Facing Goal-Sourcing Skill | Accepted | 2026-06-16 |
| ADR-061 | Unique ADR/SPEC Numbering Gate | Accepted | 2026-06-17 |
| ADR-062 | Swarm Goal-Sourcing Runner | Accepted | 2026-06-17 |
| ADR-063 | Sharded Gate A Kernel Replay | Accepted | 2026-06-17 |
| ADR-064 | Goal-Level Dispatch Deduplication | Accepted | 2026-06-17 |
| ADR-065 | Operator Preflight Doctor | Accepted | 2026-06-17 |
| ADR-066 | Queued-Proofs Board | Accepted | 2026-06-17 |
| ADR-067 | Demand-Driven Sourcing | Accepted | 2026-06-17 |
| ADR-068 | Fork-Native Contribution Mode | Accepted | 2026-06-17 |
| ADR-069 | Launcher Demand-Driven Sourcing Arm | Accepted | 2026-06-17 |
| ADR-070 | Duplicate-Verifier-Waste Metric | Accepted | 2026-06-18 |
| ADR-071 | Fresh Pre-Create Dedup Re-check at Dispatch | Accepted | 2026-06-18 |
| ADR-072 | Post-Success Claim Recheck (Prove-Time Race Fix) | Accepted | 2026-06-18 |
| ADR-073 | Generated ADR Index (README + JSON), Refreshed Post-Merge | Accepted | 2026-06-18 |
| ADR-074 | Deterministic Proof Import Narrowing (Best-Effort, Verify-Fallback) | Accepted | 2026-06-19 |
| ADR-075 | Solver-Fair Queue Dispatch Order | Accepted | 2026-06-20 |
| ADR-076 | Sharded Fork Goal Selection | Proposed | 2026-06-20 |
| ADR-077 | Roadmap GitHub Project, Synced from Repo State | Proposed | 2026-06-20 |
| ADR-078 | Sponsor-Registered Targets and Obligation-Discharge Credit | Accepted | 2026-06-20 |
| ADR-079 | Deterministic Solver Provider — Zero-LLM Template/sympy Discharge, Honestly Attributed | Proposed | 2026-06-20 |
| ADR-080 | Platform Generalisation and the Self-Verification Gating Invariant | Accepted | 2026-06-20 |
| ADR-081 | Problem Admission and the Skeleton Intake Pipeline | Accepted | 2026-06-20 |
| ADR-082 | Single-Pass Leaderboard Refresh (--write-if-stale) |
Accepted | 2026-06-22 |
| ADR-083 | The Model → Pokémon Registry and Swarm Operational Tasks | Accepted | 2026-06-22 |
| ADR-084 | Demand-Driven Sourcing Dedup — Skip When a Sourcing PR Is In Flight | Accepted | 2026-06-22 |
| ADR-085 | Isolate the Sourcer in a Per-Sourcer Worktree (ADR-042 parity) | Proposed | 2026-06-22 |
| ADR-086 | seedkit as a Documented Fixture-Generation Path Aligned to the Sourcing Paradigm | Accepted | 2026-06-23 |
| ADR-087 | Backfill Historical seedkit Records to Honest Provenance & Difficulty | Accepted | 2026-06-23 |
| ADR-088 | Extend the Honest-Difficulty Backfill to mac-158f Template Goals | Accepted | 2026-06-23 |
| ADR-089 | Deploy GitHub Pages on a Schedule via Actions, Decoupled from the Push Firehose | Accepted | 2026-06-23 |
| ADR-090 | Periodic Housekeeping — Naming as a Recurring Operational Task | Proposed | 2026-06-23 |
| ADR-091 | Sharded Gate A Axiom Audit | Proposed | 2026-06-24 |
| ADR-092 | Segregated Benchmark Track — Verified pass@k over Registered Suites | Accepted | 2026-06-24 |
| ADR-093 | lean4export + nanoda Independent-Checker Pilot | Proposed | 2026-06-24 |
| ADR-094 | Publish Library Oleans on PRs (reliable per-shard env handoff) | Proposed | 2026-06-24 |
| ADR-095 | Widen the goal difficulty band from 0–5 to 0–9 |
Accepted | 2026-06-24 |
| ADR-096 | Phase 3 — Declaration-Scoped Export + Independent Checker as a Kernel-Diverse Anchor | Proposed | 2026-06-25 |
| ADR-097 | Phase 3b — Replace the Gate A Axiom Audit with the nanoda Scoped-Export Check (p=1 preserved) | Proposed | 2026-06-25 |
| ADR-098 | Leaderboard Freshness Alarm + Refresh Timeout (defence-in-depth) | Accepted | 2026-06-25 |
| ADR-099 | Per-Suite Mathlib Pin for Benchmark Suite Ingestion & Verification | Proposed | 2026-06-25 |
| ADR-099 | Re-attribute Agent-Owned Pipeline Solver to the Pipeline Owner | Accepted | 2026-06-26 |
| ADR-100 | Client-Side Swarm Scripts Auto-Install the Lean Build Tool (lake) |
Proposed | 2026-06-25 |
| ADR-100 | Normalize Deterministic-Template Provenance in the Leaderboard, and Harden the Sweep | Accepted | 2026-06-26 |
| ADR-101 | Per-Generation Leaderboard Regen (directory-scoped attribution + memoised loaders) | Accepted | 2026-06-25 |
| ADR-102 | OpenAI --prove Text-Extraction Fallback |
Accepted | 2026-06-14 |
| ADR-103 | Validator Role — Creditable, Distributed, Reproducible Verification | Proposed | 2026-06-22 |
| ADR-104 | Phase 3c — Sample the Leanchecker Kernel Replay at p < 1 with nanoda as the Every-Proof Kernel (amends ADR-049) | Proposed — design banked, NOT for enablement yet (see §Enablement gates) | 2026-06-26 |
| ADR-105 | Recover stranded mergeable prove PRs (auto-merge enrolment backstop + cancellation-failed gate recovery) | Proposed | 2026-06-26 |
| ADR-106 | Deprioritise low-difficulty template proofs in the queue dispatcher | Proposed | 2026-06-26 |
| ADR-107 | Batch verification — amortise the per-PR Gate A env-load across K proofs | Proposed | 2026-06-26 |
| ADR-110 | Segregate Benchmark Goal Statements From the Repo-Pin Build | Proposed | 2026-06-26 |