ADR-030: Domain-Agnostic Distributed-Workload Engine (Plugin Seam)

Field	Value
Decision ID	ADR-030
Initiative	platform generalization / reusable template
Proposed By	unsorry maintainers
Date	2026-06-13
Status	Proposed

WH(Y) Decision Statement

In the context of unsorry being a working distributed swarm that discharges Lean sorrys into kernel-verified proofs through autonomous agents, a coordination layer (claims branch, ADR-004), soundness/hygiene gates (Gate A/B), provenance and a leaderboard (ADR-023), cross-cycle lesson memory (ADR-024), decomposition (ADR-009), and autonomous merge-on-green (ADR-005) — and a stated intent to reuse it as a template for crowdsourced problem-solving (“SETI@home for verifiable work”) across domains beyond Lean,

facing the fact that most of the engine is already domain-agnostic, but three things are hardwired to Lean — the verifier (Gate A internals: lake build --wfail, axiom_audit, leanchecker, statement-binding), the candidate generator (proof prompts), and work-unit handling (.lean/camel-name, the goal record schema) — so a new domain cannot be onboarded without forking the swarm; and facing that the property which actually distinguishes this from SETI@home — results are self-verifying by a deterministic checker, so one valid result is ground truth and redundant computation is unnecessary for trust — is currently entangled with Lean specifics rather than expressed as a reusable contract,

we decided for defining a narrow domain-plugin seam behind which all domain-specific logic lives (workunit schema; generate; verify → Verdict; optional decompose; assimilate), keeping the swarm loop, provider abstraction, claims/lease coordination, provenance, lesson memory, gates-as-CI, and merge domain-agnostic, with Lean as the first plugin that re-expresses today’s behaviour through the seam; and for adopting an explicit verifiability spectrum — VERIFIED (deterministic checker, one valid result suffices — Lean’s tier), SCORED (verifier returns a score, keep-best), CONSENSUS (no cheap verifier, N independent results with quorum + reputation, the classic SETI/BOINC model) — so domains without a kernel-grade checker degrade gracefully instead of being excluded,

and neglected extracting the engine into a separate package/repo now (premature — the seam is a hypothesis until a second plugin exercises it; prove it in-repo first), replacing the claims branch with a central coordination service (deferred until git-as-database measurably breaks under contention — ADR-004 stands until then), folding deduplication, identity/anti-abuse, and contributor onboarding into this decision (each is an independent decision with its own ADR — see References), and weakening the Lean plugin’s trust model (the kernel gate remains authoritative and unchanged; generalization must not lower the soundness bar),

to achieve a reusable distributed-workload template where onboarding a new problem domain means implementing one plugin against a documented contract — not forking the swarm — while preserving unsorry’s core advantage that verified results need no redundancy,

accepting that the seam is provisional until a second, non-Lean plugin validates the boundary (and may need revision then); that the VERIFIED tier is the deliberate design centre while SCORED/CONSENSUS are secondary and less mature; that some currently-implicit engine/Lean coupling will surface as friction during extraction; and that scale (coordination service), correctness-of-credit (anti-abuse), wasted-work (dedup), and growth (onboarding) remain separate, explicitly-tracked decisions rather than guarantees of this ADR; and that further considerations which are not yet scoped — notably the plugin trust boundary (a third-party plugin’s verify could lie and must not be trusted blindly), verify reproducibility/pinning, the compute cost model, central CI cost/DoS, work-unit ingestion, corpus governance/licensing, and unit privacy — are recorded in SPEC-030-A §7.2 so they are not lost.

References

Status History

| Status | Approver | Date | |——–|———-|——| | Proposed | unsorry maintainers | 2026-06-13 |