Supervise & Heal

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

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 (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:

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 <expr> 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 <expr>	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 <expr> (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).

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:<id> 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:

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/<run-id>/journal.jsonl, hash-chain and timestamps elided) records every rung:

{"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 — drift verdicts and degrade as the model-swap alternative to a code patch.
• Policies — the policy envelope healing runs under.
• Provenance & Trust — trust labels and why untrusted data cannot be endorsed by a healer.
• Reflection & Staged Code — code.patches(), code.revert(), and the staged-code path that patch application shares.