# Supervise & Heal > Governed self-healing in Sema — supervise scopes with enforced restart and heal budgets, an acceptance gauntlet over real predicates, staged/live/persistent patch application, and a journal record for every step. `supervise` is Sema's structural recovery construct, and `heal` is its most powerful — and most tightly governed — rung. Where an ordinary program crashes or silently retries forever, a supervised scope follows a *fixed triage ladder*: clean-state restart, then a contract-declared fallback, then — only if you opted in — a synthesized repair that must pass an acceptance gauntlet before it touches anything. The design lesson, borrowed from Erlang, is that recovery policy is *structural*, not a flag: supervision scopes with blast-radius scoping and restart budgets. And the LLM lesson is that intrinsic self-repair without external grounded feedback often costs more than resampling and can degrade results — so healing is deliberately the *last* option, budgeted and gated. ## Why healing is a supervision-scope property A program-wide "self-heal" mode is the wrong shape: it has no blast radius, no restart budget, and no acceptance criterion. Sema makes healing a property of a `supervise` scope with a fixed triage ladder and a journaled acceptance gauntlet. Recovery escalates only as far as it must, everything is journaled, and no step is ever silent. ## Syntax ```sema supervise ingest_workers: restart limit=3 # Armstrong first: clean-state retry fallback cached_summaries() # contract-declared degraded mode heal budget=2: # synthesis is the LAST rung require smoke_suite_passes() # gates are ordinary boolean expressions require not regression_detected() rollout shadow -> canary -> full # stages recorded in the journal return batch_work() # the supervised body follows the clauses ``` The config clauses come first, in the same block as the work they protect. Two honesty notes up front: - **`restart window="…"`, `heal window="…"`, and `heal scope=…` parse and are recorded in the journal, but are not enforced yet** — they are §5.11 target spec. `sema check` warns on each of them so a program cannot silently rely on a time-window or scope bound that nothing implements. `restart limit=` and `heal budget=` are the enforced bounds. - **`lane` and `enter` are not supervise vocabulary.** They never had semantics inside a `def` body, and `sema check` now flags them as unrecognized statements instead of accepting them silently. `lane` is a real clause in [`worker` execution profiles](/quick/declarations/) (`worker Pool: lane best_effort`), where it governs `parallel … by` scheduling. ## Execution order What actually happens at runtime, with the journal record written at every edge: ```mermaid flowchart TD E["supervise <scope>: entered"] -->|"journal: supervise.enter"| A["run the body (attempt n)"] A -->|"no failure"| OK["scope completes normally"] A -->|"journal: supervise.failure"| R{"restart limit\nleft?"} R -->|"yes — journal: decision restart"| A R -->|"exhausted"| H{"heal declared and\nattempts < budget?"} H -->|"yes"| G["heal gauntlet:\nmodel proposes a minimal patch"] G --> Q{"all require gates hold?\n(each gate journaled:\ndecision heal.gate)"} Q -->|"accepted — journal: modification heal.patch\nstages journaled: decision heal.rollout"| M{"apply mode"} M -->|"live / persistent — hot-swap;\njournal: decision heal (retry)"| A M -->|"staged (default) — recorded\nfor external application"| F Q -->|"any gate fails — patch rejected"| F{"fallback\ndeclared?"} H -->|"no — budget spent\nor no heal clause"| F F -->|"yes — journal: decision fallback\n(value evaluated, then discarded)"| C["scope recovers; execution\ncontinues after the block"] F -->|"no"| X["failure re-raised\nto the caller"] ``` Two consequences worth reading twice: - **The fallback value is discarded.** `fallback ` is evaluated and journaled, but it is *not* the value of the scope. The scope recovers and execution continues after the `supervise` block — a `return` inside the supervised body that never succeeded does not happen. Fallback is a declared degraded *action*, not a substitute return value. - **The body re-runs from the top on every restart** — clean-state retry means the whole supervised body, not the failing statement. ## Clause table: enforced vs recorded | Clause | Semantics | Status | | --- | --- | --- | | `restart limit=N` | At most N clean re-runs of the body per scope entry; each one journals `decision: restart` | **Enforced** | | `restart window="…"` | Restart-intensity window | Recorded in the journal only; `sema check` warns (§5.11 target) | | `fallback ` | On exhaustion: evaluated, journaled (`decision: fallback`), value discarded, scope recovers | **Enforced** | | `heal budget=N:` | At most N gauntlet attempts per scope entry. Non-positive or non-integer budgets are a typed error — fail-closed, never a silent default | **Enforced** | | `heal window="…"` / `heal scope=…` | Heal-rate window / blast-radius scope | Recorded in the journal only; `sema check` warns (§5.11 target) | | `require ` (inside `heal:`) | An acceptance gate — an ordinary boolean expression, evaluated after the patch proposal; every gate journals `decision: heal.gate` with `pass`/`fail` | **Enforced** | | `rollout a -> b -> c` (inside `heal:`) | Deployment stages of an accepted patch, journaled as `decision: heal.rollout` per stage | Journal-recorded (observed) only | | `rollout` outside `heal:` | Nothing — parsed but ignored | `sema check` warns: move it under `heal:` | | `lane` / `enter` | Nothing — removed from supervise vocabulary | `sema check` flags them; `lane` belongs to `worker` profiles | ## The heal gauntlet When restarts are exhausted and the gauntlet budget (`heal budget=N`) has attempts left, the runtime: 1. **Proposes a patch.** The failure (error, location, source context) is packed into a prompt and the configured model is asked for a *minimal* fix, capped at 128 output tokens. The call and the proposal are journaled (`decision: model.invoke`, `decision: heal.suggestion`). With no generation model configured, the deterministic engine returns a placeholder proposal — which the gates then judge like any other candidate. 2. **Evaluates every gate.** Each `require` in the `heal:` block is an ordinary boolean expression evaluated in the enclosing scope. Every gate lands in the journal as `decision: heal.gate` with its source text and `pass`/`fail` result. A gate that raises is a failed gate — fail-closed. 3. **Accepts or rejects atomically.** Any failed gate rejects the candidate (`decision: heal` with `verdict: rejected`) and the ladder falls through to `fallback`. If every gate holds, the patch is journaled as a substantial modification (`modification: heal.patch`, status `staged` or `applied`), and each `rollout` stage is journaled as `decision: heal.rollout`. 4. **Applies per the configured mode** — see the next section. A hot-swapped patch (`live` or `persistent` mode) re-runs the body (journaled as `decision: heal` with `attempt`/`of` counters against the budget); a `staged` one is recorded for external application and the scope recovers via `fallback`. A hot-swapped patch that fails again re-enters the ladder and may trigger another gauntlet run — until `budget=N` is spent, after which the scope falls through to `fallback` (or re-raises). :::caution[Target spec, not today's builtins] The language spec (§5.11) sketches a vocabulary of gate *builtins* — `passes(pre_patch_assure)`, `passes(new_obligations)`, `replay(failing_trace)`, `monitors.conforming_after_burnin`. **None of these exist yet.** A `require` gate is a plain expression: if you write the spec's builtins today, each gate raises `NameError`, lands in the journal as `result: "error"` with the message, and the candidate is rejected — deterministically, but for the wrong reason. Write predicates that exist: call your own smoke checks, inspect real state, compare real values. The builtin gauntlet vocabulary is target spec and will be documented when it is enforced. ::: ## Applying a patch: `staged`, `live`, `persistent` Patch *acceptance* (the gauntlet) and patch *application* are separate switches. Application is governed by `[heal] apply` in `sema.toml`, overridable by the `SEMA_HEAL_LIVE` environment variable: | Mode | `[heal] apply` | `SEMA_HEAL_LIVE` | What an accepted patch does | | --- | --- | --- | --- | | **staged** (default) | `"staged"` | `0`, `false`, `off`, `staged` | Recorded in the journal only (`modification: heal.patch`, status `staged`). Running code is never rewritten; applying the patch stays an external, human path. | | **live** | `"live"` | `1`, `true`, `live`, `in-process`, `ephemeral` | Erlang-style in-process hot swap: the patched function body replaces the running one and the supervised body re-runs. Ephemeral — gone at process exit. | | **persistent** | `"persistent"` | `persistent`, `persist`, `durable` | Live, plus the patch is committed to a hash-chained durable ledger, replayed at load, and managed via `code.patches()` / `code.revert()`. | Both switches parse **fail-closed**: any other value is a typed error at startup (`SEMA_HEAL_LIVE must be staged|live|persistent (or 0|1)`), never a silent default. Unknown values never grant self-modification authority. ## Debugging a supervise block The debugger is honest about what can and cannot fire inside `supervise`: - **Breakpoints in the supervised body fire on every attempt.** The statement hook runs per statement per attempt, so a breakpoint in the body pauses on the first run *and* on each restart — you can watch the state the retry sees. - **Breakpoints on config-clause lines never fire — and now say so.** Lines holding `restart`, `fallback`, `on_error`, and everything inside a `heal:` body are configuration consumed when the scope is set up; the heal gates are evaluated by the gauntlet, outside the statement hook. A breakpoint set there verifies as `false` with an honest reason instead of silently never triggering. - **The fallback expression is hookless, but the functions it calls are not.** You cannot break on the `fallback cached_summaries()` line itself; set the breakpoint inside `cached_summaries` and it pauses normally when the ladder reaches the fallback rung. - **Live patches are journal-only sources.** A hot-swapped body is not registered into the debugger's source map, so stepping through a live-patched function is line-misaligned relative to the file on disk, and debug snapshots record `none_at_publication` for its source. For post-mortem patch debugging use **persistent** mode: ledger patches are immutably captured as `patch:` snapshot origins, so the source the process actually ran is the source you step through. ## Worked example: failure → restart → heal rejected → fallback A complete program, run under the deterministic engine (`[engine] deterministic = true`) with the default `staged` apply mode. The body always fails; the restart budget is spent; the gauntlet proposes a patch, one gate rejects it; the fallback recovers the scope: ```sema def parse_batch(path: str) -> int !{}: ensure 1 == 2 # the batch always fails: drives the ladder return 0 def main() -> int !{}: supervise ingest: restart limit=1 fallback 0 heal budget=1: require 1 == 1 # first gate holds ... require 1 == 2 # ... second gate rejects the candidate rollout shadow -> canary -> full return parse_batch("statements.csv") print("recovered; execution continues after the block") return 0 ``` `sema run` prints the post-recovery line and exits 0. The journal (`.sema/runs//journal.jsonl`, hash-chain and timestamps elided) records every rung: ```json {"seq": 2, "kind": "supervise.enter", "scope": "ingest"} {"seq": 3, "kind": "supervise.failure", "scope": "ingest", "attempt": "0", "error": "ContractViolation: ensure failed in parse_batch(): 1 == 2 [main.sema:2:12]"} {"seq": 4, "kind": "decision", "decision": "restart", "scope": "ingest", "attempt": "1", "of": "1"} {"seq": 5, "kind": "supervise.failure", "scope": "ingest", "attempt": "1", "error": "ContractViolation: ensure failed in parse_batch(): 1 == 2 [main.sema:2:12]"} {"seq": 6, "kind": "decision", "decision": "heal", "scope": "ingest", "verdict": "attempt", "attempt": "1", "budget": "1", "window": ""} {"seq": 7, "kind": "decision", "decision": "model.invoke", "verdict": "ok", "model": "builtin-mock", "backend": "deterministic-mock", "max_tokens": "128", "prompt_preview": "A supervised Sema scope failed. Propose the minimal fix. ## Error **ContractViolation** — ensure…"} {"seq": 8, "kind": "decision", "decision": "heal.suggestion", "scope": "ingest", "patch_preview": "(configure [models] generate for a heal suggestion)"} {"seq": 9, "kind": "decision", "decision": "heal.gate", "scope": "ingest", "gate": "1 == 1", "result": "pass"} {"seq": 10, "kind": "decision", "decision": "heal.gate", "scope": "ingest", "gate": "1 == 2", "result": "fail"} {"seq": 11, "kind": "decision", "decision": "heal", "scope": "ingest", "verdict": "rejected", "reason": "a required acceptance gate did not hold"} {"seq": 12, "kind": "decision", "decision": "fallback", "scope": "ingest", "value": "0"} {"seq": 13, "kind": "print", "text": "recovered; execution continues after the block"} ``` Read the ladder off the records: one failure per attempt (`supervise.failure`), one `decision: restart` while the limit lasts, the gauntlet's model call and suggestion, one `decision: heal.gate` per gate with its verbatim source text, the atomic rejection, and the journaled-then-discarded fallback value. Note what is *absent*: no `modification: heal.patch` and no `decision: heal.rollout` — a rejected candidate stages nothing and rolls out nothing. ## Journal records | Record | When | Fields to know | | --- | --- | --- | | `supervise.enter` | Scope entered | `scope` | | `supervise.failure` | A body attempt failed | `scope`, `attempt`, `error` | | `decision: restart` | Clean re-run while `limit` lasts | `attempt`, `of` (the limit) | | `decision: heal` (`verdict: attempt`) | Gauntlet begins | `attempt`, `budget`, recorded `window` | | `decision: model.invoke` | The patch-proposal model call | `backend`, `max_tokens` (128), `prompt_preview` | | `decision: heal.suggestion` | The proposed patch | `patch_preview` | | `decision: heal.gate` | Each `require` gate | `gate` (source text), `result: pass\|fail\|error`, `error` (the raised message, if any) | | `modification: heal.patch` | All gates held | `status: staged\|applied`, the patch | | `decision: heal.rollout` | Each rollout stage of an accepted patch | `stage` | | `decision: heal` (`verdict: applied`) | Hot-swapped patch re-runs the body | `attempt`, `of` (the heal budget) | | `decision: heal` (`verdict: rejected`) | A gate failed | `reason` | | `decision: fallback` | Fallback evaluated; scope recovers | `value` (journaled, then discarded) | ## How it's checked - `sema check` validates that `heal` appears only inside `supervise`, and warns honestly on every accepted-but-unenforced clause: `restart window=`, `heal window=`, `heal scope=` ("recorded in the journal but not enforced yet"), and `rollout` outside a `heal:` block. `lane` and `enter` in a `def` body are flagged as unrecognized statements. - `heal budget=` is validated at runtime, fail-closed: a non-positive or non-integer budget raises a typed `HealConfigError` that even the scope's own `fallback` does not swallow — never a silently clamped value. - Every attempt — restart, gate verdict, acceptance, rejection, rollout stage, fallback — is a journal record in the hash-chained run journal, so a healing episode is auditable and replayable after the fact. ## See also - [Monitors & Drift](/governance/monitor/) — drift verdicts and `degrade` as the model-swap alternative to a code patch. - [Policies](/governance/policy/) — the policy envelope healing runs under. - [Provenance & Trust](/governance/provenance/) — trust labels and why untrusted data cannot be endorsed by a healer. - [Reflection & Staged Code](/guides/reflection/) — `code.patches()`, `code.revert()`, and the staged-code path that patch application shares.