View project on GitHub

ADR-049: Decentralised CI Runner Architecture — Tiered Split with a Mandatory Cheap Central Re-check

Context

unsorry’s soundness gate (Gate A, ADR-006) is the project’s dominant CI cost and its central DoS surface. Per PR it runs a full lake build UnsorryLibrary --wfail elaboration (~16–21 min cold, the dominant cost driver; cached by ADR-045), a serialised axiom_audit (~6–7 GB/process), a leanchecker kernel replay (historically ~20 min/~20 GB, now incremental ~10–30 s via ADR-033), and an ADR-011 statement-binding check. These heavy jobs were already offloaded from free GitHub-hosted runners to paid namespace.so ephemeral runners — a centralised stopgap whose cost grows linearly with merged-PR volume and has no asymptote as the autonomous swarm (ADR-005) scales.

Issue #635 asks us to research a decentralised, secure CI runner architecture — “SETI@Home but for LLMs proving math” — in which the client runs both the agent and the runner, with stringent checks that the runner’s code has not been modified. The investigation, an 8-candidate parallel-agent workflow with adversarial soundness review (full options analysis in docs/proposals/decentralised-ci-runner-architecture.md), produced two load-bearing observations:

1. The client already runs the runner. swarm/agent.sh::prove_local_verify() already performs lake build UnsorryLibrary --wfail + axiom_audit + check_library_options before opening a PR. The open problem is therefore trust, not capability.
2. Lean splits cleanly at a natural seam. Expensive elaboration (the cost driver, and the part that need not be trusted) is separable from cheap kernel checking. A full kernel replay of every swarm proof (~225 s) is already ~4–6× cheaper than one cold elaboration build; an incremental PR replay is ~40–120× cheaper. This makes a mandatory central re-check affordable on every PR.

The decision is bounded by the project’s standing, non-negotiable invariants: the Lean kernel is the only truth oracle; every contribution must be re-checkable on a trusted surface before it lands in the commons; identity is hygiene, never soundness (ADR-007); the CI trust surface is SHA-pinned and CODEOWNERS-gated (ADR-019); mathlib/toolchain are release-pinned for reproducibility (ADR-002). This decision records the recommended direction (Status: Accepted). Its substance was already live via ADR-033 (incremental replay/audit) and ADR-045 (olean cache); the implementation contract in SPEC-049-A is phased. Phase 0 is delivered — the §5 conformance regression suite (tools/gate_a/tests/test_decentralised_runner_conformance.py, PR #926) that locks in the §2 soundness invariant. Phase 1 (scoping the central elaboration build to the changed closure) is closed — not pursued (#942): the cost measurement showed the redundant unchanged-module build is already eliminated by ADR-033/045. On a warm-cache CI run the once-per-PR --wfail build is ~41 s of a ~8 runner-min/PR gate that is dominated by fixed mathlib-environment loading (axiom audit ~165 s, leanchecker replay ~60 s, three ~25–60 s cache restores — none of which Phase 1 touches), so narrowing the build target buys only low-single-digit % per PR — not worth a soundness-surface change to the TCB control flow. The §5 conformance suite (#926) remains the standing guard. Phases 2–3 remain future / pilot-gated, each its own decision.

WH(Y) Decision Statement

In the context of unsorry’s heavy Gate A verification compute running on paid, centralised namespace.so ephemeral runners whose cost grows linearly and without asymptote as the autonomous swarm scales, with issue #635 proposing to move heavy CI onto contributor machines (which already run the prover via prove_local_verify()),

facing the inviolable invariant that the Lean kernel is the only truth oracle and every contribution must be re-checkable on a trusted surface before it lands — so that the issue’s literal “prove the runner code was not modified” requirement, if taken at face value (BYO self-hosted runners, redundant peer consensus, probabilistic spot-audit, or TEE/hardware attestation), would each make runner integrity, a probabilistic vote, an economic penalty, or a silicon vendor’s signature load-bearing for mathematical correctness, all defeatable by a contributor with physical access or a throwaway non-cryptographic identity (ADR-007),

we decided for a tiered split: push the expensive elaboration (lake build --wfail + axiom audit) onto the untrusted contributor (which prove_local_verify() already runs), and keep a mandatory, cheap, trusted central re-check as the sole load-bearing soundness gate, run at sampling probability p = 1 on every PR — a re-check that never trusts a client-supplied .olean but instead re-derives the statement from canonical goal source (ADR-018/ADR-011), re-elaborates the changed-module reverse-import closure from source against dependency oleans that are either rebuilt on trusted CI or restored from a commit-exact trusted-CI cache with provenance, then runs leanchecker + axiom_audit + statement-binding on that,

and neglected BYO self-hosted GitHub Actions runners (a fork PR on a public repo would run the PR head’s own gate on contributor-controlled hardware — a forged green Gate A), redundant N-of-M peer consensus (a defeatable vote among non-cryptographic identities; ADR-030 reserves CONSENSUS for domains with no cheap verifier, and Lean is VERIFIED), probabilistic spot-audit with reputation (admits a 1 − p fraction with no trusted re-check, making penalties load-bearing for correctness), TEE/hardware-attested runners (the contributor owns the hardware and has physical access — out of TEE scope; the research surfaced sub-$1000 attestation-key extraction), and the naive “trust client oleans + leanchecker” reading of the split (unsound on crafted-invalid oleans and on real proofs of weakened/renamed statements — the ADR-011 vacuity class),

to achieve verification capacity that scales with the swarm while keeping the kernel as the sole oracle on ground the adversary never touches, dissolving the “prove the runner was not tampered with” requirement by detecting tampering through outcome rather than attestation (a tampered runner can at worst produce something the central kernel rejects),

accepting that the headline central-cost reduction is modest, not SETI-scale — ADR-033 incremental replay and ADR-045 olean caching already captured most per-PR savings, and the changed-closure re-elaboration is a scoped source build that cannot be safely offloaded without trusting client oleans, so the v1 win is the elimination of the redundant build of unchanged modules plus a sub-linear cost slope; that any global-impact change (toolchain/lakefile/gate tooling) forces a full central re-check, so the cost bound is soft and griefable; and that v1 decentralisation is shallow because the irreducible trusted re-elaboration and merge stay central by necessity — that central surface is the soundness guarantee.

Soundness argument (explicit)

1. Acceptance is decided only by the central re-check. Nothing lands in UnsorryLibrary except by a deterministic verdict produced on a project-controlled surface the adversary never touches. The client’s prove_local_verify() is advisory, exactly as today.
2. The central PR-time re-check is the ADR-048 ingest verification. Once trusted CI verifies an exact proof artifact for a pinned toolchain/mathlib context, later systems may carry that trust forward only through provenance + immutability/byte-identity, never through client attestation.
3. The central re-check consumes no client artifact as a trusted input. It (a) re-derives the statement from canonical goal source (ADR-018 create-only goals, ADR-011 binding), (b) re-elaborates the changed-module reverse-import closure from source against dependency oleans that were rebuilt on trusted CI or restored from a commit-exact trusted-CI cache, (c) runs leanchecker, (d) runs the serialised axiom_audit against the whitelist {propext, Classical.choice, Quot.sound}, (e) defeq-binds the proved term to the re-derived statement.
4. The footgun is named and forbidden. leanchecker replays the environment it is given — it trusts olean structure (“prone to crafted invalid .olean files”) and does not re-derive the statement. So “leanchecker a client-supplied olean” is unsound on (i) crafted-invalid oleans and (ii) real proofs of weaker/renamed statements (the PR-#64 vacuity class). The design closes both by central source re-elaboration and central statement re-derivation; no code path may let a client olean reach leanchecker as a trusted input.
5. Determinism is the precondition. ADR-002 pinning + Lake lockfile + elan give the ADR-033 byte-identical-rebuild invariant, so the central re-elaboration verifies the same proof the contributor produced. Any trusted-context change forces a full re-check rather than scoping down.
6. Post-merge full replay is defense-in-depth, not the primary trust boundary. ADR-048 permits unchanged, already-ingested artifacts to be trusted through provenance and immutability; scheduled or context-triggered full replay remains valuable as a bookkeeping backstop, but ADR-049 does not require every push to main to re-derive all soundness from scratch.

Conclusion: soundness is preserved at full strength (C1 = 5) under the threat model “a fully malicious/tampered contributor runner.” Identity, reputation, spot-audit sampling, and any peer-consensus signal remain strictly hygiene (ADR-007) — they may throttle abuse or decide how much expensive elaboration to re-run, never whether content is admitted.

Options Considered

Option 1: Tiered split + mandatory cheap central re-check (Selected)

The recommended hybrid above. Pros: the only decentralisation option that keeps soundness at full strength, because acceptance is decided by a mandatory central re-check never by runner integrity/vote/penalty/vendor signature; makes runner tampering detectable by outcome (dissolves the issue’s hardest requirement); composes with ADR-002/004/005/019/033/045 at near-zero conceptual friction; v1 is a small CODEOWNERS-reviewable delta on gate-a.yml. Cons: the cost win is modest (most per-PR savings already captured by ADR-033/045); the cost bound is soft (global-impact PRs force full re-check, which is griefable); v1 decentralisation is shallow (the trusted re-elaboration and merge stay central).

Option 2: Reproducible-build + content-addressed artifact verification (Rejected as v1; adopted as the Phase-3 engine of Option 1)

Deterministic builds → content-addressed lean4export NDJSON, re-checked centrally by a tiny independent checker (e.g. nanoda) with no mathlib resident. Pros: soundness holds and it captures the fullest cost lever (smallest TCB, removes even the elaborator; enables cross-kernel defense-in-depth). Cons: it does not address runner-code integrity; lean4export cross-machine determinism and external-checker wall-clock are open (external checkers can be “>100× slower than Lean”). Rejected as v1 because it needs a determinism + wall-clock pilot first; retained as the Phase-3 upgrade.

Option 3: Client-attested verification + cheap central re-check, as literally scoped (Rejected — collapses into Option 1 once made sound)

The SPEC-030-A §7.2 split at face value. Cons: the obvious implementation (“trust client oleans + leanchecker”) is unsound on crafted-invalid oleans and on proofs of weakened/renamed statements (ADR-011 vacuity class). The fix — central source re-elaboration + statement re-derivation — is Option 1. Rejected for shipping the latent footgun rather than the fix.

Option 4: BYO self-hosted GitHub Actions runners (Rejected)

Donated compute, GitHub-orchestrated. Cons: gating failure on a public repo — because gate-a.yml triggers on: pull_request, a fork PR would run the PR head’s own gate on contributor-controlled hardware (forged green Gate A), plus classic self-hosted persistence/poisoning and fork-PR RCE risk. Sound only by re-adding a central kernel replay, at which point Option 1 dominates without the self-hosted liabilities.

Option 5: Probabilistic spot-audit + reputation / economic disincentive (Rejected)

Trust client attestation, re-verify a random fraction, penalise on detected cheating. Cons: any audit rate p < 1 admits a 1 − p fraction with no trusted re-check, making penalties load-bearing for correctness (violates the invariants and ADR-007) and assuming a merely rational adversary with a penalisable identity. Lean’s re-check is cheap enough to run at p = 1; spot-checking is appropriate only for the expensive elaboration layer as a cost optimisation, never the kernel layer.

Option 6: Redundant N-of-M peer re-verification (BOINC/SETI CONSENSUS tier) (Rejected)

Replicate each unit across K independent clients; accept on quorum + reputation. Cons: quorum among non-cryptographic identities (ADR-007) is a defeatable vote, not a kernel proof. ADR-030 reserves CONSENSUS for domains with no cheap verifier; Lean is VERIFIED, where one valid result is ground truth. Adds 200–300 % wasted client compute to obtain what a single ~10–30 s central replay settles deterministically.

Option 7: TEE / hardware-attested runner (Rejected)

Run Gate A in an enclave that emits a hardware-signed attestation of unmodified code. Cons: the contributor owns the hardware and has physical access — out of TEE scope; the research surfaced practical sub-$1000 attestation-key extraction. Attestation proves code integrity relative to trusting the silicon vendor, not mathematical correctness (the load-bearing-attestation anti-pattern ADR-007 forbids). Unavailable on much consumer hardware (re-centralises to cloud CVMs); a ~20 GB replay does not fit comfortably in an enclave; rendered redundant by the cheap central re-check.

Option 8: Centralised managed runners (baseline / control) (Rejected — it is the problem)

Keep namespace.so; scale by paying. Pros: unimpeachable soundness (kernel on fully-trusted ground); simplest; lowest latency. Cons: solves none of #635 — 0 % heavy compute leaves central infra, cost linear with no asymptote, capacity does not grow with the swarm, and an adversary’s heavy PRs burn paid minutes. The yardstick to beat, not a destination.

Dependencies

References

Status History