# revl for AI agents

You are writing components in **revl 2.0**, a language for systems where
components load, unload, and hot-swap with *compile-time* safety. This guide is
written for you: the syntax was designed around what you already write well,
and around the mistakes you actually make.

> **Repo map, two lines.** The compiler is `src/revl/` (`parser.py` →
> `typecheck.py` → `lower.py` → `apply.py`). The **emitters are NOT under
> `src/`**: each tier lives in `backends/{python,typescript,rust,go,java,wasm}/`,
> its `emit.py` is the IR→host-language renderer, and most carry two or more
> expression dispatchers inside it (component vs fn-body; wasm has three),
> patch every dispatcher a change touches, and keep the `EXPR_DISPATCHERS` /
> `EXPR_REFUSED` tables in each emit.py in step (the conformance test
> `tests/test_expr_dispatcher_conformance.py` makes "did you patch both paths"
> a red test). Run `pytest tests/test_frontend.py tests/test_doc_examples.py`
> for the fast frontend loop; run `make pre-merge-affected` for the lane gate
> and selector receipt. If it reports `FULL` or the selector is unavailable,
> it stops without starting the full gate. Review the receipt before explicitly
> escalating with `make pre-merge`; CI runs the full suite.

If you are changing RevL itself, follow [CONTRIBUTING.md](../CONTRIBUTING.md)
and [the agent workflow](process.md). Run `./tools/pre_pr.sh --merge-ref`
before the first push and again before merge so checks cover the current
`origin/main` merge tree as well as your branch.

## The one rule

> **Same meaning → same syntax. Different meaning → different syntax.**

revl 2.0 is four strata. Know which one you're in before you write:

| stratum | allegiance | your job |
|---|---|---|
| 1. Pure expressions & functions | TypeScript subset | write it like TS; it is correct |
| 2. Types & data | revl's own | capitalized names, `[]` generics |
| 3. Components & effects | revl's own | slow down; this is the paradigm |
| 4. Host blocks | verbatim host language | label it `pure`/`acquire`/`emission` |

## Stratum 1: the TypeScript you already know

`fn`, `let`, `var`, `if`/`else`, ternary, `while`, `for (x of xs)`, arrow
lambdas, records `{a: 1}`, lists `[1, 2]`, indexing `xs[i]`, calls, `&&`/`||`,
`==`/`===` (identical), `!=`/`!==`, template strings `` `...${expr}...` ``.

```revl
fn fib(n: Int) -> Int {
  var a = 0
  var b = 1
  var i = 0
  while (i < n) {
    let t = a + b
    a = b
    b = t
    i += 1
  }
  return a
}
```

This compiles and runs as written. Write this stratum on autopilot.

## The traps (things that look like TS but aren't)

These are **excluded and named in diagnostics** ([syntax-2.0.md](syntax-2.0.md)
§3.3). Do not write them:

| you wrote | the problem | write instead |
|---|---|---|
| `n++` / `n--` | mutation; expressions are pure | `n += 1` on a `var` |
| `null` / `undefined` | no null in the type system | `None` (an `Opt[T]`), see below |
| `class`, `new`, `this`, `function`, `import`, `export`, `typeof`, `delete` | excluded | `type` / `fn` / `use` |
| `try { } catch { }` | failure is typed | `Result[T, E]`, or `fail` in a component body |
| `async` arrows in pure code, generators | excluded | `async fn` in a *service* |

## Small print (four things that are not TS)

- **`let`/`var` bind function-wide, not block-wide.** A `let` inside an `if`
  or `while` block is still in scope after the block ends. (Shadowing an outer
  name is refused, so this is safe.)
- **Statements are separated by newlines; `;` is not a separator.** One
  statement per line is the whole rule.
- **Strings have no escape sequences.** `"a\nb"` is four characters,
  backslash, `n` and all. Build multi-line output by concatenation and
  `` `${…}` `` templates.
- **A component activation body records effects only** (`let x = effect …
  undo …`, `emit`, `fail`, `if`, `return`), plain computation does not belong
  there. Put helper functions at top level and delegate from `provide { }`.

## Null safety (read this twice)

There is **no `null`**. Absence is `Opt[T]`, the ADT `Some(value) | None`.
`T?` is sugar for `Opt[T]`.

- `T` flows into `Opt[T]` automatically (you may pass `Some(5)`, or just `5`,
  where `Opt[Int]` is expected).
- `Opt[T]` does **not** flow back into `T`. If a function returns `Opt[Str]`,
  unwrap before using the value:

```revl
fn describe(name: Opt[Str]) -> Str {
  return match name {
    Some(n) => `hello ${n}`,
    None    => "anonymous",
  }
}
```

The diagnostic says: *`X` expects `T`, got `Opt[T]`, unwrap the optional
first: `match` on it, or use `??` to supply a fallback.*

## Types & match

```revl
type Row = { id: Int, name: Str }
type Outcome = Ok(Row) | NotFound | Invalid(Str)
```

- Records are structural; ADTs are nominal.
- `match` over an ADT is **exhaustiveness-checked**: omit a case and it won't
  compile, and the error names the missing case. Use `_` for "everything else".

```revl fragment
return match outcome {
  Ok(row)      => row.name,
  NotFound     => "-",
  Invalid(why) => why,
}
```

## Stratum 3: components & effects (slow down here)

This is the paradigm, deliberately **not** TS syntax. A component declares
what it requires and provides; its body is *revertible effects*.

```revl
service Database {
  emission fn execute(sql: Str) -> Int    // crosses the system boundary
}

service Cache {
  fn get(key: Str) -> Opt[Str]
  emission fn put(key: Str, value: Str)   // its body emits (see "rules that bite")
}

component UserCache requires db: Database provides cache: Cache {
  let store = effect Map.new() undo store.drop()

  provide cache {
    fn get(key) = store.get(key)
    fn put(key, value) {
      effect store.insert(key, value)
      undo   store.remove(key)
      emit db.execute(`INSERT INTO cache_log VALUES (${key})`)
    }
  }
}
```

Rules that will reject you if you forget them:

- **`effect E undo U`**, every mutation needs an inverse. A non-pure
  acquisition without `undo` is a compile error (G4).
- **`emit`**, calling a declared `emission` operation without the `emit`
  marker is an error (G4). An emission is irreversible; it must be *visible*.
- **Undeclared access**, a component reaches the world only through its
  `requires` (G1). Using an undeclared name won't compile.
- **`requires` and `provides` go on the header line**, `component C requires
  db: Database provides cache: Cache {`, never as statements inside the body.
  Written in the body, the refusal says so and its `fix` is the corrected
  header line.
- **No acquisition after `provide`** (A2); **no `await` in a provide-method
  body unless the operation is declared `async fn`** (A1).
- **`fail "msg"`**, deliberate L-Raise: reverts accumulated effects and lands
  the component FAILED. A FAILED component's `revl_state` row carries
  `error: {type, message}`, what its activation raised, and a call on a key it
  provides names that provider and that error (issue #1895), so a raising
  host body is never mistaken for an unmet `requires`.

## The guarantees are your safety net

The checker enforces, at compile time, the invariants a runtime can't
([DESIGN.md](../DESIGN.md) §4): G1 declared-only access · G2 provision
disjointness · G3 no dependency cycles · G4 inverse-or-emit · G5 no teardown
effects · G6 purity outside `effect` · G7 LIFO-complete teardown · G8
enumerable boundary. A program that compiles satisfies them. That is the
contract, and it is why a *generated* component is safe to self-deploy.

## Host blocks

When you need host power, say so honestly and classify it:

```revl
extern pure fn sha256(data: Bytes) -> Str
  = @ts { return crypto.createHash("sha256").update(data).digest("hex") }
  = @py { import hashlib; return hashlib.sha256(data).hexdigest() }
```

`pure` / `acquire` (needs `undo`) / `emission` (may have `compensate`).
Unclassified → no compile. The inverse/compensation slots sit on the
*declaration*, between the return type and the first host body:

```revl
extern pure fn close_ledger(h: LedgerHandle) = @py { pass }

extern acquire fn open_ledger(path: Str) -> LedgerHandle undo close_ledger(result)
  = @py { return abs(hash(path)) % 100000 }
```

An `acquire` return is a NOMINAL OPAQUE HANDLE type (`LedgerHandle`), never a
bare primitive: the handle carries the identity the ownership checks track
(item 308). The `undo` names the inverse over the implicit `result` binding.

| classification | `undo <expr>` | `compensate <expr>` |
|---|---|---|
| `pure` | refused (nothing to invert) | refused |
| `acquire` | **required** | optional |
| `emission` | refused (one-way crossing) | optional |

The same slots exist where you *call*: `effect E undo U` in a component body,
and an emission call site takes a best-effort cleanup after `compensate`:

```revl fragment
provide audit {
  fn record(line) {
    emit bus.send(line) compensate bus.send(`retract ${line}`)
  }
}
```

## Rules that bite (learned the hard way)

These are the refusals most likely to stop a generated component. Each was
added because real code got them wrong.

**A service declaration bounds its providers.** If a method's body reaches an
emission, directly, through an `emission` extern, or through a function that
does, the *service* must declare it:

```revl
service Cache {
  fn get(k: Str) -> Opt[Str]
  emission fn put(k: Str, v: Str)   // its body emits, so the interface says so
}
```

A provider may be purer than declared, never less pure. Skipping this is the
single most common rejection when a component writes anywhere.

**`emit` yields a value.** Use it in value position when you need the result.
One marker covers one crossing, so a crossing whose result feeds another gets
its own `emit` first:

```revl fragment
fn once(goal) {
  let draft = emit assistant.complete(goal)
  return emit compiler.propose(draft)
}
```

**Provide-methods take plain `fn`, no purity modifiers.** You cannot restate
`emission` (or `async`) on a provider: emission-ness is inherited from the
service declaration, which is the upper bound on every provider. Writing
`emission fn submit(…)` inside a `provide` block is refused before typechecking;
the modifier lives only in the service:

```revl fragment
provide queue {
  fn submit(id, payload) {        // plain `fn`; `emission` comes from JobQueue
    effect store.insert(id, payload)
    undo   store.remove(id)
    emit audit.record(`job ${id}`)
  }
}
```

**Method bodies take plain bindings.** Name intermediates instead of nesting:

```revl fragment
provide greet {
  fn hello(name) {
    let prefix = "hi, "        // plain value binding
    return prefix + name
  }
}
```

`let x = effect … undo …` still means the acquisition. In a component
*activation* body a plain binding is refused: that body records effects.

**`??` needs an optional on its left.** `a ?? b` on a non-optional is a type
error: the fallback would be dead.

**A void operation ends with a bare `return`** (or omits the return type and
returns nothing).

**`match` works in component and method bodies**, not only in `fn` bodies.

## Driving a running system (MCP)

`revl mcp serve` exposes the compiler over MCP (the documented happy path;
issues #317 and #336 note that a script entry point is window-free by design).
The absolute-interpreter fallback is `python -P -m revl mcp serve` (the `-P`
is PYTHONSAFEPATH, the safety bit; without it, `-m` puts the CWD at
`sys.path[0]`), and the loop it enables is the point: a draft component
never has to touch the filesystem. This is your primary interface.

<!-- docgen:agents-mcp-count begin -->
The complete verb set comes from
`src/revl/mcp/server.py` and `query_tools.py`. `tools/list` shows the
core tier by default; call `revl_verbs` for any other verb's
schema; pass it `name` and `args` to call a verb. This makes every
verb reachable from the list you were given. The verbs are
grouped below by what you reach for; each verb's exact inputs and
outputs are in [mcp-reference.md](mcp-reference.md).
<!-- docgen:agents-mcp-count end -->

| verb(s) | use | detail |
|---|---|---|
| `revl_verbs` | find a verb `tools/list` does not show: every verb by topic, then the schemas of a topic or of named verbs | [mcp-reference.md](mcp-reference.md#revl_verbs) |
| `revl_brief` | between loop steps: one compact answer with what is loaded and at which generation, the last refusal (code, `file:line`, repair) or check verdict, any pending proposal or draft, and the one call to make next, capped at 1200 characters and derived from session state so it cannot drift from `revl_state` | [mcp-reference.md](mcp-reference.md#revl_brief) |
| `revl_scaffold` | start from a typed, holed skeleton instead of a whole invented component; every hole comes back with its `fillSpec` | [scaffold.md](scaffold.md) |
| `revl_check` | does this compile? structured diagnostics (code, guarantee, and the `fix` rewrite) **and open holes' `fillSpec`** if not; with no candidate it checks the composition the session holds | [mcp-reference.md](mcp-reference.md#revl_check) |
| `revl_admit` | may it enter **this running composition**? | [mcp-reference.md](mcp-reference.md#revl_admit) |
| `revl_plan` | and then what? the delta a swap would produce, without applying it | [plan.md](plan.md) |
| `revl_ship` | check → admit → plan in one early-exit call; `apply:true` also swaps | [token-economy.md](token-economy.md) |
| `revl_deploy` | push the running composition onto a **second host** through the ssh leg: admission-gated and approval-gated; without `apply:true` it rehearses | [deploy.md](deploy.md) |
| `revl_update_check` | compare the running toolchain with the newest release on the operator's feed, its manifest and compatibility statement (no fetch, no compile) | [updates.md](updates.md) |
| `revl_update_apply` | stage and admit a verified release against the running manifest and plan it, then apply the plan by hash: a stale plan or a widened irreversible reach is refused, and a successor that does not serve the running keys is reverted | [updates.md](updates.md) |
| `revl_update_status` | feed configuration, running identity and generation, staged releases, held plans and the update journal | [updates.md](updates.md) |
| `revl_update_rollback` | return to the generation before the last applied release through the admitted undo | [updates.md](updates.md) |
| `revl_resolve` | is there already an admission-compatible component to **import** instead of regenerating? | [registry.md](registry.md) |
| `revl_audit` · `revl_tools` · `revl_grammar` | the G8 boundary, the projected tool set, the prompt-sized language surface | [mcp-reference.md](mcp-reference.md#revl_audit) |
| `revl_idiom` | the minimal admitted example of one construct (every hole's fillSpec carries its own) | [mcp-reference.md](mcp-reference.md#revl_idiom) |
| `revl_act` | one call per action through the approval gate: its class, and executed (a), deferred to commit (b) or ticketed (c), with a receipt the commit manifest lists | [mcp-reference.md](mcp-reference.md#revl_act) |
| `revl_counterfactual` | replace, insert or drop one action of the `revl_act` log and see how the gate's decisions would differ, with nothing run | [mcp-reference.md](mcp-reference.md#revl_counterfactual) |
| `revl_load` · `revl_call` · `revl_state` | boot in memory, invoke a provided operation, inspect what is loaded | [mcp-reference.md](mcp-reference.md#revl_load) |
| `revl_knowledge` | leave a **note** on a declaration (rationale, invariant, trap, ...); notes ride on later edits of it, go stale when its code changes, and survive the session through `revl_export {with_knowledge: true}` | [mcp-reference.md](mcp-reference.md#revl_knowledge) |
| `revl_export` | write the committed (held) source to disk, on request: disk is an export, never a side effect | [mcp-reference.md](mcp-reference.md#revl_export) |
| `revl_change` | **propose, verify, commit**: speculative by default (nothing swaps until `commit: true`), one call for a whole change: `{edit}`, `{replace: {component, source}}` or `{withdraw}`; loads if needed, plans (the withdrawal cascade), verifies (admission, gates, optional gauntlet) and commits only if all pass, naming every component touched | [mcp-reference.md](mcp-reference.md#revl_change) |
| `revl_source` | read **one declaration** by symbol (`NotesHttp`, `<file>:Name`, `<file>:<line>`), optionally with the declarations it names and without comments, instead of the whole file | [mcp-reference.md](mcp-reference.md#revl_source) |
| `revl_edit` | patch the **server-side** source with a delta (hole-fill / range / anchor / symbol), you send the change, not the file | [mcp-reference.md](mcp-reference.md#revl_edit) |
| `revl_affected_tests` | map changed repository paths to the shared pre-merge test selection; unavailable worktree/base returns `FULL` with a reason | [mcp-reference.md](mcp-reference.md#revl_affected_tests) |
| `revl_swap` · `revl_rollback` · `revl_undo` · `revl_unload` | replace a generation, undo the last swap, return to an earlier generation through the gate, tear down + prove no residue (R4) | [mcp-reference.md](mcp-reference.md#revl_swap) · [generation-history.md](generation-history.md) |
| `revl_gauntlet` · `revl_quarantine` | grade a candidate (proved / tested / claimed), or prove an untrusted one in the wasm sandbox | [gauntlet.md](gauntlet.md) · [quarantine-tier.md](quarantine-tier.md) |
| `revl_test_run` | run a selected test suite under the server's interpreter and read per-test outcomes, counts and verdict instead of scraping runner text | [mcp-reference.md](mcp-reference.md#revl_test_run) |
| `revl_repair` · `revl_canary` | run the repair loop within policy, or canary a successor onto one realm slice and decide on evidence | [repair-loop.md](repair-loop.md) · [verified-canary.md](verified-canary.md) |
| `revl_lease` | claim/renew/release a TTL-bound lease on a component so co-agents do not replace it under you | [component-leases.md](component-leases.md) |
| `revl_snapshot` · `revl_restore` | capture / re-admit your evolved composition across a restart | [persistence.md](persistence.md) |
| `revl_timeline` · `revl_inspect_step` · `revl_step_back` · `revl_replay_bisect` · `revl_replay_forward` | walk, inspect, unwind, binary-search and re-run a recorded accumulator | [replay.md](replay.md) |
| `revl_explain` · `revl_fmt` | what a diagnostic code guarantees and how to satisfy it; canonical formatting of inline source, IR-equivalence gated | [mcp-reference.md](mcp-reference.md#revl_explain) · [fmt.md](fmt.md) |
| `revl_commit` · `revl_commit_confirm` · `revl_abort` | the session commit protocol: enumerate the irreversible residue, confirm it by hash, or abort and replay the inverses | [mcp-reference.md](mcp-reference.md) |
| `revl_approve` · `revl_revoke` | say yes to one outstanding class-(c) crossing, or mint and later withdraw a session-scoped standing grant | [mcp-reference.md](mcp-reference.md#revl_approve) |
| `revl_escalate` · `revl_override` · `revl_quorum` | hand a stalled multi-party approval question up, admit one without its count (its own `override` verb, recorded as an override), read the decision graph and its admission receipt | [mcp-reference.md](mcp-reference.md#revl_escalate) |
| `revl_distillation_offers` · `revl_apply_distillation` · `revl_revoke_distillation` | fold repeated yeses into a proposed auto-approve rule, install it, retire it | [mcp-reference.md](mcp-reference.md#revl_distillation_offers) |
| `revl_estop` · `revl_estop_report` | the operator's emergency halt (a latch flip, not an unwind), and reading back what it stranded | [mcp-reference.md](mcp-reference.md#revl_estop) |
| `revl_fork` · `revl_fork_confirm` | enumerate what forking the session at step k would rewind and what it cannot, then perform it and mint the branch | [mcp-reference.md](mcp-reference.md#revl_fork) |
| `revl_query_{emitters,withdraw,dependents,reach,drift}` · `revl_live_query` | who emits to X? what breaks if I withdraw C? over source, or against the live session | [queries.md](queries.md) |
| `revl_history_emitted_between` · `revl_history_lifetime` | the same query envelope over a recorded run | [queries.md](queries.md) |

Two properties worth relying on: a **rejected candidate cannot deploy** (the
compile runs before the transition, so the running system keeps serving), and
`revl_unload` **proves** the component left nothing behind before you commit
it to disk. And every rejection carries its `fix` beside the guarantee, so the
diagnostic tells you the rewrite, not just the rule. See
[mcp-reference.md](mcp-reference.md) for the full verb set and
[docs/mcp-bridge.md](mcp-bridge.md) for the shapes.

MCP is your interface, but a human editing the same sources gets the same
checker through a language server. `python -P -m revl.lsp` speaks LSP over
stdio (it is a module entry point, not a `revl lsp` subcommand, run with the
`-P` safety bit): diagnostics from the checker, hover from the diagnostic
explanations, and go-to-definition from the resolver (`src/revl/lsp/`).
Same admission gate, a different transport.

### Wiring `revl mcp serve` into a working session

The MCP server is only useful to a session that has it connected. A developer
or agent working on a downstream project (a repo that depends on revl but is not
the revl checkout) gets `revl_check`, `revl_plan` and `revl_swap` by adding
`revl mcp serve` to the config of an MCP client. It speaks stdio, so a client
needs four values: a command, its args, a working directory and an environment
(no port, no token).

Run `revl mcp serve --print-config` from your project to have the config block
written for you: it names an absolute interpreter that imports both revl and
cordis (the runtime venv `setup.sh` builds, else the interpreter running the
command), the `-P -m revl mcp serve` invocation and a `--root` for the current
directory, then exits without serving. The check ignores the PYTHONPATH of the
shell that ran it, because the client will not have it; a source checkout that
only works with a `PYTHONPATH` gets exactly that value in an `env` key. Serve
flags you add (`--root DIR`, `--grant`, `--operator-profile`, `--all-tools` and
so on) are carried into the block with their paths made absolute; flags that
open a listener (`--http`, `--tls-*`) are refused by name, since a stdio config
cannot carry them. It exits 1 and names the fix when no interpreter qualifies,
and `revl doctor` reports the same answer on its `mcp client config` row. Paste
the output into your MCP client's server list, usually a project-level
`.mcp.json` or the client's own settings file. Some clients use a different
top-level key (for example `servers` instead of `mcpServers`); check your
client's documentation for the exact file and key. The manual recipes below are
for the cases it does not cover (a console script).

If revl is installed in a virtualenv (a wheel, or `sh backends/python/setup.sh`
in a checkout, which installs revl and the pinned cordis-py editable), the
shortest config is that venv's console script, and no environment is needed:

```json
{
  "mcpServers": {
    "revl": {
      "command": "/path/to/revl/backends/python/.venv/bin/revl",
      "args": ["mcp", "serve"],
      "cwd": "/path/to/your-project"
    }
  }
}
```

If you run revl from a source checkout without installing it, point an
interpreter at the checkout with `PYTHONPATH`. Do not write that value by hand:
`revl doctor` run from the checkout prints the exact line for that checkout, and
`revl doctor --json` carries it as `checkout.pythonpath` (a list) and
`checkout.export`:

```text
$ revl doctor --no-smoke
...
source checkout: to boot a composition from it with another interpreter, run
  export PYTHONPATH=/path/to/revl/src:/path/to/revl/backends/python/.cordis-py/src:/path/to/revl/backends/python
```

The three entries are `<revl>/src`, cordis-py's `src` and
`<revl>/backends/python`. Put them in the client's `env`, joined with `:` (`;` on
Windows), and run the module with `-P`:

```json
{
  "mcpServers": {
    "revl": {
      "command": "python3",
      "args": ["-P", "-m", "revl", "mcp", "serve"],
      "cwd": "/path/to/your-project",
      "env": {
        "PYTHONPATH": "/path/to/revl/src:/path/to/revl/backends/python/.cordis-py/src:/path/to/revl/backends/python"
      }
    }
  }
}
```

Field names differ between clients (`command`, `args`, `cwd` and `env` are the
common spelling); the values are what matter. `cwd` is the project the session
works on, so the paths the agent passes resolve against it. Use a `python3` that
has revl's dependencies, which the checkout's virtualenv does.

Check the connection by asking the client to list the server's tools: the core
tier includes `revl_check`, `revl_plan` and `revl_swap`. `revl_swap` and the other
verbs that need a live composition require the cordis-py runtime. If the server
cannot import it, it starts anyway, names those verbs on stderr and answers each
with a refusal whose `next` is the fix; when `revl doctor` prints
`cordis-py not found, expected at ...`, run `sh backends/python/setup.sh` from the
revl checkout (or point `CORDIS_PY` at an existing clone) and restart the server.

A bare `ModuleNotFoundError: No module named 'cordis'` from a revl command means
the same thing: the interpreter that ran it has no cordis on its path. Run
`revl doctor` with that interpreter; its `cordis-py runtime` row and the
`PYTHONPATH` line say where cordis is expected.

### The modern agent loop, scaffold → fill → resolve → admit

For the CLI-side counterpart of this loop (`revl scaffold` generating the
holed skeleton itself, plus `revl fmt` and `revl explain`), see
[authoring-for-agents.md](authoring-for-agents.md); step 1 below writes the
skeleton by hand, `revl scaffold` is the same shape from a spec instead.

The verbs above compose into one workflow, and it is the discoverable path from
a vague need to an admitted component. Nothing touches the filesystem until the
last step:

1. **Scaffold with holes.** Write the component's shape and leave the parts you
   are unsure of as typed holes, `let cap: Int = hole "worker pool size"`. A
   hole type-checks, so the rest of the draft still checks ([holes.md](holes.md)).
2. **`revl_check` returns fill-specs.** A draft with holes compiles but can
   never admit; `revl_check` comes back with each open hole's `fillSpec`, its
   `line` and expected type. That is your worklist. Call it with no `source`
   and it checks the composition the session holds (the draft you are filling),
   so you read your own worklist without re-sending the file you are building;
   `source`/`files` still check a candidate you have not loaded, but not while
   a draft is held: that combination is refused, because the load it would run
   is what replaces the draft (issue #2111).
3. **Fill via `revl_edit` deltas.** Send a `{hole: <line>, expr: "<fill>"}` edit
   per hole, the server holds the source, so you transmit only the change, not
   the file. Deltas accumulate across calls; a refused patch advances nothing,
   so the working buffer never breaks. An edit that scaffolds a *new* hole comes
   back as another obligation with its own `fillSpec`, so you can iterate holes
   ([mcp-bridge.md §Deltas, not documents](mcp-bridge.md#deltas-not-documents--revl_edit)).
4. **`revl_resolve` before you regenerate.** For any hole or requirement that is
   a whole service, pass the need to `revl_resolve`, if an admission-compatible
   component already exists, importing it beats writing one, and the matched
   `source`/`manifest` ride back inline ([registry.md](registry.md)).
5. **`revl_gauntlet` / `revl_admit` to land it.** When the draft is hole-free,
   `revl_admit` answers "may this enter **this** composition?" mechanically, and
   `revl_gauntlet` upgrades that to a graded dossier (a boot/unload no-residue
   lifecycle in an isolated scratch session). Only what passes gets written out.

The whole loop runs server-side against the admission gate, so every
intermediate state is one the compiler already accepted.

**The one way to lose the draft is to load over it.** Nothing in steps 1-5
replaces the held set: `revl_check` with no `source` reads it, `revl_edit`
patches it, and both refuse a `source`/`files` argument while a draft is held
(issue #2111) instead of silently loading it. That refusal is a usage error
(`category: "usage"`, never a `selfCheck`), and its message names the draft the
call would have cost, with its components and its open holes, rather than
reporting a line number in a composition that no longer exists. Send the `next`
it carries (`revl_check {"session": true}` for the check; the same edit with the
load dropped for the edit) and the loop continues where it was. A draft lives in
memory only, so a load over it loses it for good: no file on disk has it.

Where that is checked: the tool surface, its annotations and its structured
rejections are gated by `tests/test_mcp.py`. Both properties above are gated
by `tests/test_mcp_session.py`
(`test_a_rejected_swap_leaves_the_running_system_serving`,
`test_load_call_and_unload_with_no_residue`), which needs the cordis-py
runtime and **skips in CI**. Run it yourself with
`sh backends/python/setup.sh` before relying on it.

## The check → run loop

Close the generate→check→run loop inside one file:

```revl
verified fn add(a: Int, b: Int) -> Int { return a + b }

test "add works" {
  assert add(1, 2) == 3
}
```

`verified` opts into the totality tier (no unbounded recursion/loops); `test`
blocks run under `revl test`.

## Driving a live composition: lifecycle and fault tests

`test` blocks check pure functions. Two more test kinds assert the paradigm's
own guarantees over a *live* composition (they need the cordis-py runtime;
`sh backends/python/setup.sh` installs it):

**`lifecycle test`**, load, call through provision keys, unload, and assert
nothing was left behind ([syntax-2.0.md](syntax-2.0.md) §7.1):

```revl
service Cache {
  fn get(key: Str) -> Opt[Str]
  emission fn put(key: Str, value: Str)
}

component C provides cache: Cache {
  let store = effect Map.new() undo store.drop()

  provide cache {
    fn get(key) = store.get(key)
    fn put(key, value) {
      effect store.insert(key, value)
      undo   store.remove(key)
    }
  }
}

lifecycle test "a submitted job reverts cleanly" {
  load C
  call cache.put("k", "v")
  let hit = call cache.get("k")
  assert hit == Some("v")
  unload C
  assert no_residue
}
```

The statements are `load X` (optionally `with { field: value, … }` for the
component's config), `call key.op(args)` (bind its result with `let`),
`unload X`, and `assert no_residue`.

**`fault test "…" for Component`**, declares that activation *fails* at a
named step, then asserts the revert left nothing behind
([fault-tests.md](fault-tests.md)):

```revl
service P { fn ping(tag: Str) -> Str }

component Fragile provides p: P {
  let scratch = effect Map.new() undo scratch.drop()
  fail "deliberate L-Raise at activation"
  provide p { fn ping(tag) = tag }
}

fault test "mid-activation failure reverts its acquisition" for Fragile {
  fail at step 2
  assert no residue
}
```

`fail at step N` pairs with the Nth effect form (or `fail`) in the component's
activation body; the body may also say `assert effect <name>`. A fault test
body allows only `fail at …` and `assert …`, nothing else parses.

**Typed holes** round out the drafting loop: `let cap: Int = hole "worker pool
size"` compiles, the obligation is listed with its expected type, and admission
refuses the draft until you fill it ([holes.md](holes.md)).

## Reading error messages

Error messages are the interface, each names the guarantee and the fix.
Example:

> `` `missing` is not declared in this function ``, hint: declare it with
> `let`/`var` or add it as a parameter (G1).

When a compile fails, read the *hint*; it usually states the exact rewrite.

Three rejections are the verdict of a search over the whole composition, the
G4 emission fixed point, a G3 dependency cycle, a G2 provision conflict, and
those carry the derivation with them: the call chain, the cycle path, both
providers, each with a source location. It renders under the hint, and rides
in the structured diagnostic (and every MCP rejection) under `why`. See
[why-traces.md](why-traces.md). `revl explain <code>` turns any code back into
the guarantee it enforces and the rewrite that satisfies it.

## Common failure modes (check before you write)

1. Did you write `null`? → `None` / `Opt[T]` / `match`.
2. Did you mutate without `effect … undo …` (or `emit` for emissions)? → G4.
3. Did you use an undeclared requirement? → G1.
4. Is your `match` missing a case? → the error names it; add it or `_`.
5. Did you call an unknown method on a `List`/`Str`? → check the stdlib surface
   ([stdlib-2.0.md](stdlib-2.0.md)); note `push` is persistent
   (`out = out.push(v)`), never in-place.
6. Did you use 1.x `"$name"` interpolation? → `` `${name}` `` templates
   (`revl fmt --migrate` rewrites old sources).
7. Is your `extern` unclassified? → `pure`/`acquire`/`emission`.

## How you're measured

The 2.0 syntax ships only if you write it well ([syntax-2.0.md](syntax-2.0.md)
§10): the acceptance benchmark measures **first-pass compile rate** and
**iterations-to-green** across component specs written in {1.x, 2.0,
2.0+host-blocks}. First-pass compile rate is the metric. Treat the strata
boundary as the signal it is: autopilot in stratum 1, deliberate in stratum 3,
and let the exclusion diagnostics correct the rest in one shot.

The corpus is committed under `bench/results/`, and
`python3 bench/rescore.py --run all` recompiles it against the current
checker and prints a failure taxonomy. Read that taxonomy before writing:
its largest bucket has been "a `provide` method emits, but the service
declared the operation plain `fn`", the rule at the top of *Rules that
bite*.