# Sl Builder > Interview a human who wants to build a Squeeze Loop (SL) for their problem, then draft a concrete, structured plan. Elicits the deliverable, the upper bound (soft normative authority — spec/standard/policy/contracts), the lower bound (executable oracle — prover/checker/tests/runtime/reference impl), the actors and their disjoint (U,L) pairs, the context barriers, the gates (A editorial / B machine / C coverage-no-blend), the coherent-and-wrong failure to guard, and the stabilizers/collapse modes to pre-empt — then turns the answers into a roles+bounds+barriers+gates+loop-steps plan. Use when the user says any of: "draft a plan to generate a squeeze loop", "draft an SL validation plan", "build an SL strategy for X", "design a squeeze loop for my problem", "help me set up a squeeze loop", "SL validation plan for C code with Frama-C", "an SL that monitors another SL", "nested squeeze loop / monitor of a monitor". Action-oriented: figure out what is known, ASK the missing interview questions, then OUTPUT a plan i - Skill: `canonical/sl-builder` (Agent Skill) - Install (CLI): `npx skillmds@latest add canonical/sl-builder` - Raw SKILL.md: https://api.skillmd.com/api/skills/canonical/sl-builder/raw - Safety review: pending - Works with: Claude Code, Claude.ai, OpenAI Codex - Category: Coding & Dev Tools - Author: canonical (https://skillmd.com/u/canonical) - Updated: 2026-09-17 - Page: https://skillmd.com/skills/canonical/sl-builder --- # SL Builder — interview a human, then draft a Squeeze Loop plan This skill turns a vague wish ("I want correctness for X") into a concrete **Squeeze Loop (SL)** plan. It does two things, in order: 1. **Interview.** Ask the structured questions below that the human has *not* already answered, to elicit the SL design. 2. **Draft.** Synthesize the answers into a plan using the template in *How to draft the plan*. Be action-oriented. When invoked: read the request, mark each interview slot as KNOWN or MISSING, ASK only the MISSING ones (batched, grouped), then DRAFT. If the human is impatient or under-specifies, draft with explicit `ASSUMPTION:` markers and a short list of open questions appended — never stall. ## One-paragraph background (so this skill stands alone) A **squeeze loop** holds every actor between an **upper bound** `U` — a citable, normative **soft** truth (a spec/standard/policy/contract in natural or semi-formal language; the strongest claim an actor may make) — and a **lower bound** `L` — an executable **hard** truth (a runnable oracle whose verdict the actor cannot alter: a test passes or fails, a proof obligation discharges or it does not). A deliverable is **in-band** iff it is a reading of `U` that `L` does not refute. **Coherent-and-wrong** is the dominant enemy: a plausible reading of `U` that `L` contradicts (or an artifact that passes the hard check while betraying the soft intent). The load-bearing rule is **disjointness**: every actor answers to a *different* `(U,L)` pair, chosen so the **intersection** of all in-band sets is the correct deliverable while **no single actor's evidence base certifies it** — so each actor's blind spot is caught by another actor that cannot share it. Barriers are **physical** (in the delegation context), not honorary. **Done** is gate-defined, never self-declared. The canonical cast (five roles; add a role only for a *new evidence base*): **coordinator** (judge/sequencer; never edits source or rubber-stamps; **owns the loop's machine-checkable SL-1.0 `*.sl.json` representation** — see `sl-internal`), **property/spec author** (writes `U` from the requirement; never sees the implementation), **implementer** (builds the artifact to satisfy `U`; never touches the acceptance evidence), **exerciser/verifier** (authors acceptance evidence from the spec+surface only; never reads the implementation), **probe** (one experiment, one recorded verdict; writes verdicts, never fixes). --- ## 1. The interview — questions to elicit an SL design Group the questions; explain *why* each matters; ask only what is MISSING. ### Group 1 — The deliverable and "correct" - **What is the deliverable?** (verified C, a paper, an agent policy, a dataset…) - **What does "correct" mean for it, operationally?** Push for a definition that could in principle be *checked*, not admired. ("Reads well" is what the dominant failure looks like.) - **What is the dominant failure you fear?** Name the *coherent-and-wrong* specific to this problem (see Group 7). ### Group 2 — The upper bound `U` (soft normative authority) - **What is the authority every claim answers to?** Spec, standard, policy, requirement, contracts (e.g. ACSL), a CFP, a global interface spec. - **Does it exist externally, or must it be authored?** This sets the **terrain archetype**: - **A — transcription:** an external written spec already exists; `U` is on disk; dominant failure is unfaithful transcription/improvisation. - **B — authored authority:** no external spec; `U` must be *authored upstream* by someone who never sees the implementation; dominant failure is coherent-and-wrong, and **author independence is the entire soundness argument**. - **C — split planes:** correctness divides across two+ planes, each with its own `(U,L)` and a precedence rule; dominant failure is **blending** (one plane's weak check standing in for the other's strong claim). - **If it must be authored — who authors it, and from what?** (the requirement, a standard, the upstream interface). ### Group 3 — The lower bound `L` (executable oracle) - **What runnable process renders a verdict the actor cannot argue with?** A prover/checker (Frama-C/WP discharge), a test suite, a runtime, a reference implementation, gold tests, a measure, a type checker, link/integration tests. - **Does it exist or must it be built first?** If it must be built, it is the *first work item* (pilot before machinery; pin reality before building on it). - **Is the verdict mechanical and interpretation-free?** If not, it is not yet an `L` — sharpen it until it is (a VC discharges or it does not). ### Group 4 — The actors and their disjoint `(U,L)` pairs - **Who are the actors?** Start from the canonical cast; add a role only for a *new evidence base*. Two actors with identical `(U,L)` are one actor. - **For each actor, what is its `(U,L)` pair?** - **Disjointness check (C1):** do any two actors share a pair? Does any actor's `(U,L)` let it relieve *its own* constraint (e.g. the implementer also writes the tests, or the spec author reads the code)? If yes, the design is not yet compliant — split or rebarrier. - **Catchability check (C2):** for each actor's characteristic blind spot, *which other actor catches it*? If none, you are missing a role or a pair. ### Group 5 — Context barriers (physical, not honorary) - **What must each actor NOT see?** Most importantly: who must be denied the implementation? (The exerciser/verifier and the spec author must not see it.) - **How is each barrier enforced in the delegation context?** Barriers live in *what is in the prompt* (fresh context; surface + acceptance lines only), not in an instruction to refrain. An actor with the internals in context will use them. ### Group 6 — Gates and "done" - **Gate A (editorial):** the coordinator's *judgment* approval of the plan against `U` (amend / cut / sharpen — never a rubber stamp). No source edit from a `DRAFT`. What does Gate A check here? - **Gate B (machine):** the executable acceptance check against `L` — positives pass; negatives fail *at the named site* violating the *named clause*; standing invariants green; nothing smuggled in (no added axioms/assumptions). What runs? - **Gate C (coverage / no-blend / coherent-and-wrong):** each obligation clause maps to a passing check, and *the theorem proved is the property intended* (guard against vacuous/trivial passes and plane-blending). What is the map? - **Done (C4):** "done" = which fixed set of machine-checked gates passes? No actor's self-report counts. ### Group 7 — The coherent-and-wrong failure specific to this problem - **What would a plausible-but-wrong deliverable look like that passes the naive check?** (e.g. a contract so weak it is vacuously true; a proof of an adjacent weaker property; an abstract that over-claims the body.) Name it; it tells you what Gate C and the catchability pairing must target. ### Group 8 — Stabilizers / collapse modes to pre-empt Walk the collapse modes and pick the ones this problem is prone to: - **Self-judging** (an actor edits/authors its own acceptance) → forbidden moves + physical barriers. - **Shared evidence** (two actors, one pair) → the (C1) disjointness audit. - **Self-declared done** → gate-defined done. - **Coherent-and-wrong / weakened clause** → Gate C + "where authority is authored, independence is the soundness argument" + "strictness has a safe direction" (stricter than `U` is legitimate; weaker is a bug). - **Relabel-to-exempt** (a producer meets a principle by parking in-scope work in an exempt bucket — `residual`/`out-of-scope`/`BLOCKED`/`PARTIAL`/"tool limitation") → enumerate the exempt buckets each problem offers and make each evidence-bearing via the **refutation probe** (supply the claimed-impossible piece, re-run the oracle; verdict flips ⇒ REJECT). An exemption verdict without attached probe evidence is a gate failure. - **Emergent obligation absorbed by the residue bucket** (the producer's move-set is all *local* moves, so a cross-cutting obligation that must be invented and threaded across many items has no move and gets exempted) → name the emergent obligation class explicitly as a first-class move in the producer's move-set before dispatch. - **Absorbed surprise** → route surprises to a gap document, never patch locally. - **Rubber-stamp approval** → Gate A must amend/cut/sharpen. - **Unpinned reality / unspecified base** → pilot first; transcribe the de facto base before extending it. - **Unsequenced parallelism** → sequence by mechanism reuse; parallelize only across true independence. - **Un-squeezed coordinator (the soft-side hole)** → the coordinator's *editorial* judgment (Gate~A) is the one actor nothing holds a disjoint `(U,L)` over; the hard side (Gate~B/C against `L`) has no such hole. If soft-side soundness matters, **nest** the loop under a monitor SL (`sl-monitoring-sl`) that squeezes the coordinator's *accepted readings* — and any learned skills — against `U`/`L` from outside. Nesting **closes** the inner coordinator's hole — it is now squeezed by an authority it does not hold — but by *disjoint authority*, not mechanically, so the closure must terminate somewhere. The plan must NAME who supplies the **terminal** check — an external reviewer or a human with true context-independence — and never claim the automation alone closed the soft side. (This is *why* nested SLs exist: the monitor of a monitor is the answer to "who squeezes the coordinator?", with external review as the terminus that actually closes it.) --- ## 2. How to draft the plan (template) Once the slots are filled, emit the plan in this shape, **plus the SL-1.0 `.sl.json`** that encodes the same actors/bounds/barriers machine-checkably (§9). The `*.sl.json` is **owned by the coordinator** — it is one of the coordinator's build products, alongside approvals and gate verdicts. Keep `ASSUMPTION:` and `OPEN QUESTION:` markers where the human under-specified. ``` # SL Plan: ## 0. Deliverable & correctness - Deliverable: ... - "Correct" means (checkable): ... - Terrain archetype: A / B / C (and why) - Dominant coherent-and-wrong to guard: ... ## 1. Bounds - Upper bound U: — exists externally / authored upstream by - Lower bound L: — exists / must be built as item E-0 ## 2. Actors and their disjoint (U,L) pairs | Actor | Builds | U (above) | L (below) | Forbidden move | Must NOT see | |-------|--------|-----------|-----------|----------------|--------------| | coordinator | approvals, sequencing, gate verdicts, **the loop's SL-1.0 `*.sl.json`** | binding spec sections | gate machine output | edit source; rubber-stamp | — | | spec author | ... | | | read the implementation | the implementation | | implementer | ... | | | touch acceptance evidence | acceptance evidence | | exerciser/verifier | ... | | | read the implementation/diff | the implementation | | probe (opt.) | ... | design claim | tool's actual behaviour | implement a fix | — | Disjointness (C1): Catchability (C2): for each actor. ## 3. Gates - Gate A (editorial): coordinator judges the plan against U — . - Gate B (machine): . - Gate C (coverage / no-blend): . ## 4. Loop steps (per item) 1. coordinator delegates item (U sections + barriers + acceptance lines) 2. implementer writes spec-N plan @ STATUS: DRAFT 3. Gate A → APPROVED (judge/amend/cut) 4. implementer implements + runs standing invariant 5. exerciser/verifier authors acceptance evidence from spec+surface only 6. Gate B (machine) → Gate C (coverage/no-blend) 7. item DONE → next; any divergence → gap-N doc → re-plan (N:=N+1) ## 5. Executable oracle setup ## 6. Done criteria ## 7. Stabilizers engaged ## 8. Execution order ## 9. SL-1.0 representation (coordinator-owned) - Emit `.sl.json` conforming to `sl-internal/references/sl-schema-1.0.json`: a `sources[]` registry (every U/L authority, artifact, rationale, terminus) + one `actors[]` row per actor above (each with `upper_bound.sources`, `lower_bound.sources`, `must_not_see`, `produces`) + the `disjointness` block. - **Owner: the coordinator.** It is the coordinator's build product and the artifact a downstream `sl-auditor` / `sl-monitoring-sl` monitor reads. The coordinator authoring the loop's *self-description* is NOT self-certification: the JSON is not a bound any actor judges its deliverable against — it is checked from a disjoint base (the auditor/monitor), exactly as self-description drift is routed in `sl-internal`. - Validate it with `sl-internal/scripts/sl_disjointness_check.py .sl.json` before delivering (this is the C1/C2/C3 + endogeneity set-algebra check). - **Nested designs (a controlling SL over a base SL):** disjointness extends *across levels*. The controlling coordinator requests the base coordinator's `*.sl.json` (request/response; only the registry crosses, never the base's implementation or rationale) and runs the **cross-loop source-of-truth check** (see `sl-monitoring-sl`): `controlling.bound_sources ∩ base.internal_sources = ∅` (base-internal = `produced_by != null` or `provenance ∈ {endogenous, internal}`; the only sanctioned base→controller link is a `sub_loop` bridge row), and no shared source id carries a conflicting `(type, provenance, produced_by)`. A shared id is legitimate only for the genuinely-same exogenous authority both levels cite. Flag any collision as an `OPEN QUESTION:` — a controller bounding itself on base-internal evidence is not disjoint. ## 10. Packaging — ship the SL as a skill (standing convention) Every new SL is delivered as a **skill**, not a loose plan. The convention has four artifacts, all carrying the same kebab-case `` = the loop `id`: - **Skill directory.** `config/skills//SKILL.md` — the SL written up as a triggerable skill (the `.claude/skills/` path is a symlink into `config/skills/`, so author under `config/skills/` only). - **SL-1.0 self-description.** `.sl.json` — the §9 coordinator-owned registry, validated by `sl_disjointness_check.py` before delivery. - **Companion doc.** `docs/.md` with three sections: (1) the **rationale** behind the SL (the deliverable, the dominant coherent-and-wrong it guards, why the bounds are what they are); (2) the **graphical representation**, embedding the SVG as `img/.svg`; (3) a **Disjointness at a glance** section — the disjointness hypothesis, the load-bearing barrier, the catchability table (each blind spot → the *other* actor that catches it), and the terminus. - **Both renderings in `docs/img/`.** Generate a PNG *and* an SVG from the `.sl.json`, written to the `docs/img/` directory (the standing convention for all SL diagrams): python sl-internal/scripts/sl2plantuml.py .sl.json -o docs/img/.png python sl-internal/scripts/sl2plantuml.py .sl.json --svg -o docs/img/.svg (add `--direction tb` for large, dense loops). Embed the SVG in `docs/.md` as `img/.svg` (scalable, zoom-lossless); keep the PNG for renderers that do not display SVG. ``` --- ## 3. Worked example A — Frama-C C validation (single SL) Request: *"Draft a plan to generate an SL validation of C code using Frama-C."* **Deliverable:** C code proven to satisfy its requirement. **Terrain:** A/B mix — the *requirement* is external (transcription) but the **ACSL contracts** that make it checkable must be **authored upstream** (authored authority), so author independence is load-bearing. **Dominant coherent-and-wrong:** a **vacuously-true contract** — `ensures \true`, an `assigns` clause so loose nothing is constrained, a postcondition implied by a too-strong (unreachable) precondition. WP discharges, but the proved theorem is not the property intended. **Bounds** - `U` = the requirement (plain English) **plus** a coding standard, made precise as ACSL contracts (requires/ensures/assigns/loop invariants). - `L` = **Frama-C/WP proof-obligation discharge** — each VC discharges or it does not — **plus** test execution of the compiled code. **Actors and disjoint (U,L) pairs** | Actor | Builds | U (above) | L (below) | Forbidden move | Must NOT see | |-------|--------|-----------|-----------|----------------|--------------| | coordinator | approvals, sequencing, gate verdicts, the SL-1.0 `framac.sl.json` | the requirement + plan sections | gate output (WP logs, test logs) | edit C/ACSL; approve an unjudged plan | — | | contract/spec author | the ACSL contracts from the requirement | the requirement + coding standard | expressibility: each clause dischargeable by *some* WP/test mechanism | propose or read the implementation | the C implementation | | implementer | the C code satisfying the contracts | the ACSL contracts (strongest mandated claim) | WP discharge + standing test suite | weaken a contract/gate to land; touch acceptance properties | the acceptance/adversarial properties | | exerciser/verifier | runs WP; authors adversarial properties from the spec only | the requirement's acceptance clauses + the documented surface | what actually discharges/proves when WP is run | read the implementation or any diff | the C implementation | | probe (opt.) | minimal Frama-C experiments (does WP handle this construct?) | one design claim per probe | Frama-C's actual behaviour | implement a fix | — | Disjointness (C1): the author holds the requirement (never the code); the implementer holds the contracts (never the adversarial properties); the verifier holds the spec + the runnable WP (never the code). No actor can relieve its own constraint. Intersection = C that *both* discharges all VCs and meets adversarial properties derived independently from the spec. Catchability (C2): implementer's blind spot (writing C that games a weak contract) is caught by the verifier's adversarial properties + the author's clause coverage; the author's blind spot (a vacuous contract) is caught at **Gate C** by the verifier (who proves the contract is non-trivial) and by the adversarial properties that *should* fail against a vacuous spec. **Gates** - **Gate A (editorial):** coordinator approves the contract & plan — each requirement clause is typed and pre-bound to an ACSL obligation; the strongest-claim check; NOT-claims named. Amend/cut/sharpen, never rubber-stamp. - **Gate B (machine):** all VCs **discharged** by WP; tests pass; **no axioms or `assumes`/`admit`/`lemma`-as-axiom smuggled in** to make a VC vanish; standing proof count (previously discharged VCs stay discharged — total additivity). - **Gate C (coverage / no-blend / coherent-and-wrong):** every requirement clause maps to a *proven* contract clause, **and the proved theorem is the property intended** — i.e. guard against vacuous/trivial contracts: a non-vacuity check (the postcondition is reachable and constrains the output; the `assigns` set is tight; mutation of the implementation that violates the requirement is *caught* by some VC or adversarial property). Two planes — the *proof plane* (WP discharge) and the *test plane* (execution) — must never blend (a discharged VC never stands in for an untested runtime behaviour, and vice versa). **Loop steps:** coordinator delegates a function/unit → contract author writes ACSL @ DRAFT → Gate A → implementer writes C, runs WP locally → verifier runs WP fresh + authors adversarial properties from the spec → Gate B → Gate C → DONE. Divergence (a VC won't discharge, or a vacuity probe fires) → gap doc → re-plan. **Executable oracle setup:** `frama-c -wp` over the unit; "a verdict" = the per-VC discharge status; build the WP invocation + a determinism re-run convention as the first item (pilot on the smallest function end-to-end before any sweep). **Done:** **all proof obligations discharged** (no `Admitted`/axiom/`assumes` shortcut), tests pass, Gate C coverage map complete, no vacuous contract. **Stabilizers engaged:** guard against **vacuously-true contracts** (Gate C non-vacuity check); **assigns/ensures gaming** (tight `assigns`; mutation check); no smuggled axioms (Gate B); **strictness has a safe direction** (the C may be stricter than the contract, never weaker); **author independence** (contract author and verifier never see the code); **done is gate-defined**. --- ## 4. Worked example B — Nested SL (a monitor of a monitor) Request: *"Draft a plan to generate an SL validating a bunch of C files. This SL monitors another SL validating C code with Frama-C. The top-level SL starts with leaf functions and coordinates contracts between compilation units."* This is **two levels**. Use the `sl-monitoring-sl` meta-pattern (a loop monitoring a loop): the top SL squeezes the **base SL's soft outputs** (the contracts it infers or strengthens) against the **global spec**, from a disjoint evidence base. ### Level 0 — the base SL (per compilation unit) Exactly Example A, instantiated **once per compilation unit (CU)**. Each base SL validates one CU with Frama-C/WP; its deliverable is that CU's functions proven against their ACSL contracts. Its `U` = that CU's local contracts + the requirement; its `L` = WP discharge + unit tests. ### Level 1 — the top-level SL (cross-CU contract coordination) - **Deliverable:** a coherent set of **interface contracts across compilation units** such that every caller/callee pair is consistent and the whole program meets the global spec. - **Strategy — bottom-up:** process **leaf functions first** (functions calling nothing un-contracted), then their callers. Propagate each callee's proven **`ensures` as the caller's `assumes`/`requires`**; reconcile interface contracts where a caller's expectation and a callee's guarantee disagree. - **Upper bound `U_top`:** the **global / interface specification** (the cross-CU requirement: what the whole program must guarantee at its module boundaries). - **Lower bound `L_top`:** the **base SLs' machine verdicts** — WP discharge *across* units (a callee's `ensures` actually proves; the caller's assumed `requires` is actually established at the call site) — **plus integration / link tests** of the linked binary. - **It monitors the base SL (`sl-monitoring-sl`):** the base SL's *soft outputs* are the contracts it **infers or strengthens** while proving a CU. Those are learned, one-signal artifacts — they can be **coherent-and-wrong**: a contract the base loop strengthened to make *its own* VCs discharge may over-constrain a callee in a way the *global* spec forbids, or weaken an interface the global spec relies on. The top SL squeezes each such contract between `U_top` (the global spec — the contract must not contradict it) and `L_top` (cross-unit WP discharge + integration tests — the differential comparator), **from an evidence base the base SL's actors do not hold**. **Two-level actor map** | Level | Actor | Builds | U | L | Must NOT see | |-------|-------|--------|---|---|--------------| | base (per CU) | base coordinator / contract author / implementer / verifier | per-CU proofs (Example A) | local contracts + requirement | per-CU WP discharge + unit tests | (Example A barriers) | | top | top coordinator | the bottom-up schedule; cross-CU gate verdicts; the contract-reconciliation ledger; the top loop's SL-1.0 `*.sl.json` (each base loop owns its own) | global/interface spec | cross-unit WP verdicts + integration tests | the CU implementations | | top | interface-spec author | the global interface contracts (what each boundary must guarantee) | the global requirement | expressibility across units | any CU implementation | | top | **base-SL monitor** | per-contract verdicts on the base SLs' inferred/strengthened contracts | `U_top` (global spec the contract must not contradict) | `L_top` (cross-unit WP + integration tests, used as differential comparator) | the base SL's *rationale* for the contract; the CU code | **The monitor's discipline (from `sl-monitoring-sl`):** - It judges each inferred/strengthened contract **against `U_top` and `L_top` only** — never the base loop's account of *why* it inferred the contract, and it never edits the base SL's implementation. It emits a **verdict** (and a carve-out), never a silent fix. - Verdicts: **PASS** (the contract agrees with the global spec, confirmed across units), **CARVE-OUT** (the contract over-reaches on some reachable cross-unit input → narrow it with an exception citing the global-spec clause it defers to), **REJECT/loud-fail** (the strengthened contract contradicts the global spec and cannot be reconciled → discard, gap doc, re-plan). - Classify the contract by kind: a contract that **drops/ignores** a precondition the global spec needs is the high-risk *ignore-signal* kind → **trigger test** (perturb the dropped input across the link boundary; does a cross-unit VC or integration test move?) → carve-out. A contract that merely **follows** a callee guarantee the global spec sanctions is *defer-to-oracle* → **validity test** (does WP actually distinguish that case across units?) → usually PASS. **How the top SL coordinates and audits the base SL** 1. Topo-sort the call graph; schedule **leaves first** (bottom-up). 2. For each function: run its **base SL** (Example A) to prove it against its contract. The base SL emits the proven `ensures` (and any contract it had to strengthen to discharge). The top coordinator **requests each base loop's `*.sl.json`** from its base coordinator and runs the **cross-loop source-of-truth check** (`U_top`/`L_top` bound sources disjoint from any base-internal/endogenous source; no conflicting shared ids) — so the two levels are verified-disjoint before any base output is trusted, not merely asserted. 3. **Propagate:** the top coordinator installs each proven callee `ensures` as the caller's `assumes`, and records the binding in the reconciliation ledger. 4. **Audit (monitor):** before accepting a *strengthened* contract, the base-SL monitor squeezes it against `U_top`/`L_top` — does it hold across *all* callers (cross-unit WP), and does it contradict the global spec? PASS / CARVE-OUT / REJECT. 5. **Reconcile interfaces:** where a caller's required precondition and a callee's guarantee disagree, the divergence is a gap doc against the interface spec, not a silent edit; the interface-spec author re-authors the boundary contract, re-running affected base SLs. 6. **Top Gate C:** every global-spec clause maps to a cross-unit-proven interface contract; **no plane blends** — a *base* SL's local WP verdict never stands in for the *cross-unit* obligation or the integration test, and an inferred contract never silently substitutes for the global spec. **Why two levels are disjoint (the soundness argument):** the base SLs hold "what discharges within this CU"; the top SL holds "what the global spec mandates across CUs" + "what discharges/links across CUs." These are **disjoint evidence bases** — so a contract the base loop strengthened for *local* convenience that is *globally* wrong is exactly the coherent-and-wrong the monitor is positioned to catch, and the carve-out (the cross-unit exception) can only come from the actor holding `U_top` and `L_top`, never from the base loop that produced the contract. **Nesting closes the base coordinators' hole — by disjoint authority, so it must terminate.** The top SL squeezes the base coordinators (each now answers to an authority it does not hold). The closure is by disjoint authority, not mechanical, so it terminates: the *top* coordinator's editorial judgment is closed only when an **external reviewer or a human** with true context-independence squeezes it. State plainly who supplies that terminal check. A nested SL that claims its automation alone *fully* verified the soft side of the system is making the coherent-and-wrong claim it was built to catch. **Done (top level):** every CU's base SL DONE; every interface contract proven consistent across all callers (cross-unit WP discharged); integration/link tests pass; the reconciliation ledger complete; every base-SL-inferred contract has a monitor verdict (PASS or carved); no global-spec clause unmapped. --- ## When invoked — operating procedure 1. Parse the request; mark each interview slot (Groups 1–8) KNOWN or MISSING. 2. If the request matches Example A or B, use it as the scaffold and ask only what diverges from it. 3. **ASK** the MISSING questions, grouped, with one-line rationale each. If the human wants the plan now, proceed with `ASSUMPTION:` markers. 4. **DRAFT** the plan in the §2 template, and emit the coordinator-owned SL-1.0 `.sl.json` (§9) encoding the same actors/bounds/barriers. 5. Run the two checks before delivering: **(C1) disjointness** (no shared pair; no actor relieves its own constraint) and **(C2) catchability** (every blind spot has a catcher) — mechanically via `sl-internal/scripts/sl_disjointness_check.py .sl.json`. For a **nested** design, also run the **cross-loop source-of-truth check** (§9) between the controlling and controlled `*.sl.json` — no shared base-internal sources, no conflicting shared ids. Surface any unmet check as an `OPEN QUESTION:`. 6. **Specify packaging (§10).** The plan must name the SL's four delivery artifacts — the `config/skills//` skill dir, the `.sl.json`, the `docs/.md` companion, and both `docs/img/.{png,svg}` renderings — with the `sl2plantuml.py` commands that produce the diagrams. This is the standing convention for *every* new SL, single or nested. Do not run git or commit. This skill produces a *plan* (plus the coordinator-owned `.sl.json` it is asked to emit), not the loop's implementation. When the human moves from plan to build, the deliverable is packaged per §10: as a skill with its `.sl.json` and its `docs/.md` companion carrying both the SVG and PNG.