diff --git a/NEXT.md b/NEXT.md
index 7049068..8ae1b0f 100644
--- a/NEXT.md
+++ b/NEXT.md
@@ -2,44 +2,30 @@
 
 ## Start here — next session
 
-**Branch `dev-loop`, 14 commits, working tree clean, `dune test` green.**
+**Branch `dev-loop`, 15 commits, working tree clean, `dune test` green.**
 
 The dev loop works end to end: `flan dev program.flan`, then `C-c C-c`,
 `C-x C-e` and `C-c C-r` in Emacs against the running process. Conditions are
-one step in of four.
+two steps in of four.
 
-**The next task is conditions step 2: `restart-case` and `invoke-restart`.**
-Everything it needs has been decided; nothing has been written.
+**The next task is the dev-build break loop, `spec-conditions.md` §2** — where
+an unhandled `error` stops and talks to the daemon instead of `rt_die()`, and
+where **"a crash kills the program"** finally gets fixed. The transfer it needs
+exists now: §6's channel is in every signature and `restart-case` catches on
+it, so a break loop is a place to *stand* while the program is stopped, not a
+new way to move.
 
-- Read `spec-conditions.md` §3–§6. §6 was amended in `0fea971` and now names
-  both the reason transfer is lowered explicitly and the channel it uses.
-- **The channel is an out-parameter**: a `ptr` appended to every Flan
-  function's signature, written by a transfer and checked after each call. Not
-  a discriminated return value, and not a global — a global is not re-entrant
-  because §5 runs defers *during* a transfer.
-- **Scope v1 deliberately smaller than the spec**, and reject the rest by name
-  as the house rule requires:
-  - **every Flan function is transfer-transparent**, in release too. §6's
-    escape analysis is an optimisation for later; uniform is correct and
-    simple now.
-  - **restarts take no parameters.** That covers the spec's own `load-texture`
-    example, and skips argument marshalling and §3's runtime arity check.
-- **A transfer target is a static clause id.** It can be static even though a
-  `restart-case` may be re-entered, because unwinding stops at the first frame
-  carrying that id — walking outward, the first is the innermost, which is the
-  activation §4's lookup found.
-- A caught transfer must pop the restart frames and run the defers between
-  (§5) before the clause body starts. `errdefer` must *not* run: a restart is a
-  chosen recovery, not a failure.
-- Sand has no raylib callback, so nothing in the demo path hits §6's "a
-  transfer cannot cross a foreign frame" wall.
+Then restarts offered in the Emacs minibuffer, which wants `compute-restarts`
+plus two protocol ops. SBCL's restart struct carries `report-function` and
+`interactive-function` for exactly that prompt and `spec-conditions.md`
+mentions neither — worth adding before that step. `find-restart` and
+`compute-restarts` are both named in §4 and neither exists yet; the runtime
+already has the stack they would walk.
 
-After step 2: the dev-build break loop (§2), which is where **"a crash kills
-the program"** finally gets fixed; then restarts offered in the Emacs
-minibuffer, which wants `compute-restarts` plus two protocol ops. SBCL's
-restart struct carries `report-function` and `interactive-function` for exactly
-that prompt and `spec-conditions.md` mentions neither — worth adding before
-that step.
+Still open from §3, and each refused by name today: **restarts with
+parameters** (argument marshalling plus the runtime arity check), and
+`handler-case`, which §"What this does not settle" leaves open as possibly a
+macro over `handler-bind` plus a transfer.
 
 Read SBCL for what restarts should *mean* and ignore how it moves control: it
 transfers with `block`/`return-from`, which §6 rules out.
@@ -102,6 +88,7 @@ reader ✅ → parse ✅ → load ✅ → check ✅ → emit ✅ → clang ✅
 | `test/test_dev.ml` | **the daemon, driven the way an editor drives it** |
 | `test/test_repl.ml` | **`C-x C-e`: an expression evaluated inside a running program** |
 | `test/programs/conditions.flan` | **`handler-bind` and `signal`, the accumulation case** |
+| `test/programs/restarts.flan` | **`restart-case` and `invoke-restart`: the transfer, across two frames** |
 | `test/test_emacs.ml` | **the client, driven against a real daemon and a real program** |
 | `test/reload_host.c` | the C host that loads and installs two rebuilds, in one process |
 
@@ -924,29 +911,109 @@ Which gives the two refusals, both by the house rule rather than by accident:
   on the way out and an early exit would leave them on the stack pointing into
   a function that has gone. Same shape as `defer` inside a block.
 
-### Conditions — what step 1 does not do
+### Conditions — step 2: `restart-case` and `invoke-restart`
 
-- `restart-case` and `invoke-restart`, which are the transfer, and with it §6's
-  calling-convention change: a transfer-transparent function returns a
-  discriminated "value / transferring to frame N" and forwards it after each
-  call. **Settled in advance:** in a dev build every function is
-  transfer-transparent, because a cell can hold anything and the honest answer
-  to "what can this call?" is "anything". That is the same bargain as the
-  indirect call, and it means redefinition acquires *no* new refusal class.
-  Release builds keep escape analysis and pay nothing. What is *not* settled is
-  whether the discriminated result is returned by value or through an
-  out-parameter; the spec leaves it open and it is in every signature, so it is
-  the thing to decide before writing that step.
-- `handler-case`, which §"What this does not settle" leaves open as possibly a
-  macro over `handler-bind` plus a transfer.
-- The **dev-build break loop** of §2 — where an unhandled `error` stops and
-  talks to the daemon instead of `rt_die()`. That is where "a crash kills the
-  program" finally gets fixed.
-- Restarts offered in the minibuffer, which needs `compute-restarts` and two
-  protocol ops.
+`spec-conditions.md` §3 to §6: the transfer. A handler runs where the signal
+was, decides, and control resumes at a `restart-case` further out.
 
-Checked on the way: sand has no raylib callback anywhere, so nothing in the
-demo path would hit §6's "a transfer cannot cross a foreign frame" wall.
+```
+(defn fetch [n i32] i32
+  (restart-case (middle n)          ; its value if nothing transfers
+    (use-placeholder [] -1)
+    (retry           [] 7)))
+
+(handler-bind [(AssetMissing [c] (invoke-restart 'use-placeholder))]
+  (fetch 2))                        ; -1
+```
+
+**The channel is an out-parameter**, as §6 now says: one `ptr` appended to
+every Flan signature, written by an `invoke-restart` and checked after every
+call. The return type stays what the source says, so the disassembly is the
+release one plus a guard, and one pointer threads down the whole chain — a
+callee writes the target into its caller's slot and each frame only has to
+check and return early, which reuses the existing `return` path and with it
+§5's defers. `Emit.signature` was already the one place a signature is spelled,
+which is what made this a three-line change rather than a hunt.
+
+**Every function is transfer-transparent**, release included. §6's escape
+analysis is an optimisation, and in a dev build a cell can hold anything, so
+the honest answer to "what can this call?" is "anything" — the same bargain as
+the indirect call. Uniform also means redefinition acquires no new refusal
+class.
+
+**The transfer target is the restart frame's own address, not a clause id.**
+This is a correction to what the previous note settled. A static id has to be
+unique against every module a running program may *later* load, and a hash is
+only probably unique — two `restart-case`s colliding means the inner one
+silently catches a transfer aimed at the outer. The frame is an `alloca` in the
+function that offers it, so its address is exact, and it also says *which*
+clause, which is how clause ids disappeared entirely. §6 says "transferring to
+frame N" and this is closer to it than the number was. Re-entering a
+`restart-case` then works with nothing extra: each activation allocates its
+own frames, and §4's "innermost offering the name" is just the order of the
+walk.
+
+**Cleanup happens in landing blocks, one per region.** A guard branches to the
+innermost open one, which pops whatever frames it established and either
+catches the transfer or forwards it outward:
+
+- a `restart-case`'s pops its restart frames, compares the target against its
+  own, and either runs that clause or puts the target back and goes on out;
+- a `handler-bind`'s pops its handler frames and goes on out — which is the
+  path a transfer out of a handled body takes, and without it the handler stack
+  would be left pointing into a frame that has gone;
+- the function's own runs its defers (§5) and returns early. `errdefer` does not
+  run and never could: `try`/`Result` is still refused by name.
+
+A single function-wide unwind block would have been wrong for the first two:
+a call inside a `restart-case` body would jump straight past the very form that
+was supposed to catch it.
+
+**The channel is cleared before any cleanup runs and put back after.** A defer
+makes ordinary calls and each one is guarded; with the channel still set the
+first of them would branch straight back into the landing block it came from.
+Same reason the clause body starts with it null.
+
+`flan_signal` takes the channel and passes it to each handler, and stops
+walking once one has written to it. That makes the one C frame every handler is
+reached through transparent to a transfer — it has to be, or §6's "a transfer
+cannot cross a foreign frame" would make `restart-case` useless. It is also the
+only such frame: `extern` is Flan-to-C only and there are no function values
+yet, so nothing can call *back* into Flan across one.
+
+Scope, each piece refused by name with its reason and a test on the reason:
+
+- **restarts take no parameters.** That covers §1's own `load-texture` example
+  and skips argument marshalling and §3's runtime arity check.
+- `return` inside a `restart-case` body, exactly as inside `handler-bind`: a
+  bare `ret` skips the pops.
+- one `restart-case` offering a name twice — §4 finds the first frame offering
+  it, and two in one frame makes that a choice nothing in the source shows.
+- `invoke-restart` inside a `defer`. A defer *is* the cleanup a transfer runs
+  on its way out, so a transfer starting there leaves the function's defers
+  half run with two targets and no way to choose. The lexical case is the
+  checker's; a defer that reaches one through a call is trapped at run time by
+  `flan_transfer_fail`, because nothing static could see it.
+- no restart of that name is active: a runtime error at the invoke site, named
+  and located, rather than an unwind past everything. There is nowhere to
+  resume, so there is nothing else to do.
+
+Two things found by writing it:
+
+- **`{ ctx with in_handler = true }` was a latent bug.** `ctx.slots` and
+  `ctx.slot_tys` are mutable, so a copy allocates the body's slots into a
+  record the function never sees again and the indices collide. It was harmless
+  only because no `handler-bind` body in the tests had a `let` in it. The flags
+  are set on `ctx` and restored now.
+- **`test/reload_host.c` had to learn the parameter.** It calls `flan.outer`
+  through an `__asm__` label, which does not fail at link time when the
+  prototype is a parameter short — it reads a garbage pointer as the channel
+  and dies somewhere else entirely.
+
+`test/programs/restarts.flan` runs in the acceptance table at `-O2`, at `-O0`
+and as a dev build. `-O0` is not redundant here: the guard after every call is
+control flow the optimiser would otherwise launder, and the dev build is where
+each of those calls goes through a cell.
 
 ### What is left
 - **Editor comforts**: completion, eldoc, jump-to-definition, error overlays.
diff --git a/lib/ast.ml b/lib/ast.ml
index e8d051a..a641c56 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -57,8 +57,13 @@ and expr_kind =
      A clause binds a name for the condition, so this cannot be a call. *)
   | HandlerBind of hclause list * expr list
   | Signal  of expr                           (* (signal c) : Unit             *)
+  (* (restart-case body (name [] body ...) ...) and (invoke-restart 'name).
+     Both alter control flow, so neither can be a call. *)
+  | RestartCase of expr * rclause list
+  | InvokeRestart of string
 
 and hclause = { hty : texpr; hname : string; hbody : expr list; hloc : Loc.t }
+and rclause = { rname : string; rbody : expr list; rloc : Loc.t }
 
 (* Two unwrap operators, because they are two different things — plan.org. *)
 and unwrap = Usome | Utry
diff --git a/lib/check.ml b/lib/check.ml
index 10f9633..a3a7eb1 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -93,7 +93,17 @@ type ctx = {
      locals can be refused for the reason it is really refused for rather than
      as an unknown name. *)
   outer : (string * binding) list;
-  in_handler : bool;
+  mutable in_handler : bool;
+  (* True wherever handler or restart frames established by this function are
+     on the stack. A [return] from there would leave them pointing into a frame
+     that has gone, so it is refused — the same rule as [defer] inside a
+     block. *)
+  mutable in_frames : string option;
+  (* True inside a [defer]'s forms. A defer is the cleanup a transfer runs on
+     its way out (§5), so a transfer *starting* there has no answer: this
+     function's defers are already half run and the first transfer's target is
+     already in hand. Refused where it is written. *)
+  mutable in_defer : bool;
 }
 
 let fresh_slot ctx ty =
@@ -330,15 +340,16 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
     let c = check ctx ~want:Types.Bool c in
     let body = scoped ctx (fun () -> map_lr (fun b -> check ctx b) body) in
     expect loc ~want (mk loc Types.Unit (Tast.While (c, body)))
-  | Ast.Return v when ctx.in_handler ->
+  | Ast.Return v when ctx.in_frames <> None ->
     ignore v;
     (* The frames are pushed and popped around the body, so an early exit would
-       leave them on the handler stack pointing into a function that has gone.
-       Rejected rather than left to corrupt it, the same rule as defer inside a
-       block. *)
+       leave them on the handler or restart stack pointing into a frame that
+       has gone. Rejected rather than left to corrupt it, the same rule as
+       defer inside a block. *)
     fail loc
-      "return is not allowed inside handler-bind yet — the handler frames are \
+      "return is not allowed inside %s yet — the frames it established are \
        popped on the way out and an early exit would leave them on the stack"
+      (match ctx.in_frames with Some n -> n | None -> assert false)
 
   | Ast.Return v ->
     let v =
@@ -410,6 +421,23 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
 
   | Ast.HandlerBind (clauses, body) -> check_handler_bind ctx ?want loc clauses body
 
+  (* spec-conditions.md §3–§6: the transfer. Neither of these is a call — one
+     establishes frames around a body, and the other leaves the function it is
+     written in — so both are their own nodes all the way down. *)
+  | Ast.RestartCase (body, clauses) -> check_restart_case ctx ?want loc body clauses
+  | Ast.InvokeRestart name ->
+    (* Never: control resumes at the restart-case, which yields the clause's
+       value to *its* continuation, so nothing here has a value and nothing
+       after it runs. The lookup is at run time because restarts are
+       dynamically scoped and named — §4. *)
+    if ctx.in_defer then
+      fail loc
+        "invoke-restart is not allowed inside a defer — a defer is the cleanup \
+         a transfer runs on its way out, so starting one there would leave \
+         this function's defers half run with two targets and no way to \
+         choose";
+    expect loc ~want (mk loc Types.Never (Tast.InvokeRestart (type_id name, name, loc)))
+
   | Ast.Defer _ ->
     (* Registered by [check_fn], which is the only place that sees a form's
        position. A defer anywhere else would run at function exit rather than
@@ -524,7 +552,7 @@ and check_handler_bind ctx ?want loc clauses body =
             the enclosing one. *)
          let hctx =
            { env = ctx.env; ret = Types.Unit; slots = 0; slot_tys = [];
-             scope = []; defers = []; outer = ctx.scope; in_handler = true }
+             scope = []; defers = []; outer = ctx.scope; in_handler = true; in_frames = None; in_defer = false }
          in
          (* The condition crosses as a pointer, because the handler runs while
             the signalling frame is still alive and there is nothing to copy.
@@ -551,16 +579,74 @@ and check_handler_bind ctx ?want loc clauses body =
          ctx.env.lifted <-
            { Tast.name = fname; params = [ Types.Ptr ty ];
              slots = Array.of_list (List.rev hctx.slot_tys);
-             ret = Types.Unit; body = hbody; floc = c.Ast.hloc }
+             ret = Types.Unit; body = hbody; fdefers = []; floc = c.Ast.hloc }
            :: ctx.env.lifted;
          { Tast.htype = type_id name; hfn = fname })
       clauses
   in
-  let body =
-    map_lr (fun e -> check { ctx with in_handler = true } e) body
-  in
+  (* The flag is set on [ctx] itself and restored, not on a copy: [ctx.slots]
+     and [ctx.slot_tys] are mutable, so a copy would allocate the body's slots
+     into a record the function never sees again and the indices would
+     collide. *)
+  let saved = ctx.in_frames in
+  ctx.in_frames <- Some "handler-bind";
+  let body = map_lr (fun e -> check ctx e) body in
+  ctx.in_frames <- saved;
   mk loc Types.Unit (Tast.Handled (frames, body))
 
+(* (restart-case BODY (name [] BODY-1) ...) — spec-conditions.md §3 and §6.
+
+   Unlike a handler, a clause runs *at* the restart-case, which is where it was
+   written, so it is a branch in this function and sees this function's scope.
+   What arrives from elsewhere is only the answer to "which clause": a transfer
+   names the frame it is aimed at, and this form compares that against the
+   frames it itself pushed.
+
+   Every clause body and the body have the same type, and that is the type of
+   the whole form — which is what makes the fall-through path visible in the
+   source (§1): a restart-case in value position has to produce its type when
+   no restart is invoked too. *)
+and check_restart_case ctx ?want loc body clauses =
+  let saved = ctx.in_frames in
+  ctx.in_frames <- Some "restart-case";
+  let tbody = check ctx ?want body in
+  ctx.in_frames <- saved;
+  (* With no expectation from outside, the body's own type is the expectation
+     the clauses are checked against — unless it produced no value at all, in
+     which case the first clause that does decides. *)
+  let want =
+    match want with
+    | Some _ -> want
+    | None -> if tbody.Tast.ty = Types.Never then None else Some tbody.Tast.ty
+  in
+  let ty = ref (match want with Some t -> Some t | None -> None) in
+  let seen = ref [] in
+  let clauses =
+    map_lr
+      (fun (c : Ast.rclause) ->
+         (* Two clauses of one name would make §4's "the first frame offering
+            the name" pick between them by an order nothing in the source
+            shows. *)
+         if List.mem c.Ast.rname !seen then
+           fail c.Ast.rloc "this restart-case offers %s twice" c.Ast.rname;
+         seen := c.Ast.rname :: !seen;
+         let b = block ctx ?want:!ty c.Ast.rloc c.Ast.rbody in
+         if b.Tast.ty <> Types.Never then begin
+           match !ty with
+           | None -> ty := Some b.Tast.ty
+           | Some t when not (Types.fits ~expected:t ~actual:b.Tast.ty) ->
+             fail c.Ast.rloc
+               "the %s clause has type %s but this restart-case has type %s —                 every clause and the body must agree, since the form yields                 whichever of them ran"
+               c.Ast.rname (Types.to_string b.Tast.ty) (Types.to_string t)
+           | Some _ -> ()
+         end;
+         { Tast.rname_id = type_id c.Ast.rname; rname = c.Ast.rname;
+           rbody = [ b ] })
+      clauses
+  in
+  let ty = match !ty with Some t -> t | None -> Types.Never in
+  mk loc ty (Tast.RestartCase (clauses, tbody))
+
 and check_let ctx ?want loc bs body =
   scoped ctx (fun () ->
     let bs =
@@ -1275,7 +1361,7 @@ let collect env (decls : Ast.decl list) =
      run without swallowing it. *)
   let infer (_, v) =
     (check { env; ret = Types.Unit; slots = 0; slot_tys = []; scope = []; defers = [];
-      outer = []; in_handler = false } v).Tast.ty
+      outer = []; in_handler = false; in_frames = None; in_defer = false } v).Tast.ty
   in
   let pending = ref (List.rev !untyped) in
   let rec settle () =
@@ -1328,7 +1414,7 @@ let check_finite env =
 let check_fn env (fn : Ast.fn) : Tast.fn =
   let params, ret = Hashtbl.find env.fns fn.Ast.name in
   let ctx = { env; ret; slots = 0; slot_tys = []; scope = []; defers = [];
-                outer = []; in_handler = false } in
+                outer = []; in_handler = false; in_frames = None; in_defer = false } in
   List.iter2
     (fun (p : Ast.field) ty ->
        if List.mem_assoc p.Ast.fname ctx.scope then
@@ -1352,7 +1438,9 @@ let check_fn env (fn : Ast.fn) : Tast.fn =
       let defer_here (e : Ast.expr) =
         match e.Ast.e with
         | Ast.Defer forms ->
+          ctx.in_defer <- true;
           let forms = map_lr (fun d -> check ctx d) forms in
+          ctx.in_defer <- false;
           let d = mk e.Ast.loc Types.Unit (Tast.Do forms) in
           ctx.defers <- d :: ctx.defers;
           Some (unit_at e.Ast.loc)
@@ -1394,11 +1482,13 @@ let check_fn env (fn : Ast.fn) : Tast.fn =
   in
   { Tast.name = fn.Ast.name; params;
     slots = Array.of_list (List.rev ctx.slot_tys);
-    ret; body; floc = fn.Ast.nloc }
+    (* The same defers again, for the transfer exit path §5 describes. The
+       normal path has them spliced into [body] above. *)
+    ret; body; fdefers = ctx.defers; floc = fn.Ast.nloc }
 
 let check_global env (d : Ast.decl) : Tast.global option =
   let ctx () = { env; ret = Types.Unit; slots = 0; slot_tys = []; scope = []; defers = [];
-      outer = []; in_handler = false } in
+      outer = []; in_handler = false; in_frames = None; in_defer = false } in
   match d.Ast.d with
   | Ast.Defvar (n, _, init) ->
     let ty, _ = Hashtbl.find env.globals n in
@@ -1502,7 +1592,7 @@ let program (decls : Ast.decl list) : Tast.program = fst (program_with_env decls
 let expression env (e : Ast.expr) : Tast.expr * Types.t array =
   let ctx =
     { env; ret = Types.Unit; slots = 0; slot_tys = []; scope = []; defers = [];
-      outer = []; in_handler = false }
+      outer = []; in_handler = false; in_frames = None; in_defer = false }
   in
   let t = check ctx e in
   (t, Array.of_list (List.rev ctx.slot_tys))
diff --git a/lib/emit.ml b/lib/emit.ml
index 34144fb..daef9f8 100644
--- a/lib/emit.ml
+++ b/lib/emit.ml
@@ -65,6 +65,11 @@ let cellname n = "@" ^ quoted ("flan.cell." ^ n)
    [flan_dev_cell] / [flan_dev_global] and the answer is cached in one of these
    module-local slots. One indirection more than a name the host has, which is
    why the compiler picks per name rather than routing everything this way. *)
+(* The transfer channel's parameter, the one name that is not a Flan name. It
+   is not a slot: nothing in the language can address it, and it is read and
+   written only by the guards this file emits. *)
+let xfer_param = "%xfer"
+
 let cellptr n = "@" ^ quoted ("flan.cellp." ^ n)
 let globalptr n = "@" ^ quoted ("flan.gp." ^ n)
 
@@ -123,6 +128,16 @@ type f = {
   ret           : Types.t;
   slots         : string array;
   slot_tys      : Types.t array;
+  (* The transfer channel's landing blocks, spec-conditions.md §6. A guard
+     after a call branches to the innermost one; each pops whatever frames it
+     established and either catches the transfer or forwards it outward. The
+     innermost is first, and with none open a transfer leaves the function
+     through [unwind], which runs its defers (§5) and returns early. The flag
+     says the block was branched to, so an unused one is not emitted. *)
+  mutable pads  : (string * bool ref) list;
+  unwind        : string;
+  mutable unwound : bool;
+  defers        : Tast.expr list;
 }
 
 let fresh f = f.n <- f.n + 1; Printf.sprintf "%%t%d" f.n
@@ -315,9 +330,28 @@ let rec value f (e : Tast.expr) : string =
      frame is still alive, so there is nothing to copy and nothing to own. *)
   | Tast.Signal (id, c) ->
     let p = addr f c in
-    ins f "call void @flan_signal(i32 %d, ptr %s)" id p;
+    ins f "call void @flan_signal(i32 %d, ptr %s, ptr %s)" id p xfer_param;
+    guard f;
     "zeroinitializer"
   | Tast.Handled (frames, body) -> emit_handled f frames body
+  | Tast.RestartCase (clauses, body) -> emit_restart_case f e.Tast.ty clauses body
+  (* §4's lookup, then the transfer itself: the frame that was found goes into
+     the channel and this function leaves through its landing block. Type
+     Never, so nothing follows. *)
+  | Tast.InvokeRestart (id, name, rloc) ->
+    let t = fresh f in
+    ins f "%s = call ptr @flan_find_restart(i32 %d)" t id;
+    let ok = fresh f in
+    ins f "%s = icmp ne ptr %s, null" ok t;
+    (* No frame offers the name. That is a runtime error at the invoke site —
+       not an unwind past everything — because there is nowhere to resume. *)
+    fail_block f rloc ok (fun id n ->
+      let nid, nn = string_bytes f.md name in
+      ins f "call void @flan_restart_fail(ptr %s, i64 %d, ptr %s, i64 %d)"
+        id n nid nn);
+    ins f "store ptr %s, ptr %s" t xfer_param;
+    term f "br label %%%s" (current_pad f);
+    "zeroinitializer"
 
 (* Where a global's storage is. A global the host was built with is a symbol;
    one introduced since lives wherever [flan_dev_global] put it. *)
@@ -453,9 +487,32 @@ and call f ret flan args =
     end
   in
   let t = fresh f in
-  ins f "%s = call %s %s(%s)" t (ll ret) callee (String.concat ", " vs);
+  ins f "%s = call %s %s(%s)" t (ll ret) callee
+    (String.concat ", " (vs @ [ "ptr " ^ xfer_param ]));
+  guard f;
   t
 
+(* The check after a call, which is the whole of §6's lowering at a call site:
+   a load, a compare and a branch that reads like ordinary code. A foreign call
+   gets none — a transfer cannot cross a C frame, so there is nothing a guard
+   there could find. *)
+and guard f =
+  if f.live then begin
+    let t = fresh f in
+    ins f "%s = load ptr, ptr %s" t xfer_param;
+    let c = fresh f in
+    ins f "%s = icmp ne ptr %s, null" c t;
+    let cont = fresh_label f "on" in
+    let pad = current_pad f in
+    term f "br i1 %s, label %%%s, label %%%s" c pad cont;
+    label f cont
+  end
+
+and current_pad f =
+  match f.pads with
+  | (p, used) :: _ -> used := true; p
+  | [] -> f.unwound <- true; f.unwind
+
 (* A foreign call, where the same rule applies as to the runtime shims: a slice
    or a string crosses as ptr+len and never as a struct by value. Every other
    argument type is a scalar, because [check.ml] rejects an extern signature
@@ -505,13 +562,108 @@ and emit_handled f frames body =
          slot)
       frames
   in
+  let pop () =
+    (* Innermost first, which is the order they were pushed in reverse. *)
+    List.iter
+      (fun slot -> ins f "call void @flan_handler_pop(ptr %s)" slot)
+      (List.rev allocated)
+  in
+  let ld = fresh_label f "endhandled" in
+  let pad = fresh_label f "hxfer" and used = ref false in
+  f.pads <- (pad, used) :: f.pads;
   let last = block f body in
-  (* Innermost first, which is the order they were pushed in reverse. *)
-  List.iter
-    (fun slot -> ins f "call void @flan_handler_pop(ptr %s)" slot)
-    (List.rev allocated);
+  f.pads <- List.tl f.pads;
   ignore last;
-  "zeroinitializer"
+  let reached = f.live in
+  if f.live then begin pop (); term f "br label %%%s" ld end;
+  (* A transfer passing through: these frames are on the establishing
+     function's stack and must come off before it goes any further, and this is
+     the only path out that the checker's refusal of [return] leaves. Nothing
+     here calls Flan, so the channel can stay as it is. *)
+  if !used then begin
+    label f pad;
+    pop ();
+    term f "br label %%%s" (current_pad f)
+  end;
+  if not reached then begin f.live <- false; "zeroinitializer" end
+  else begin label f ld; "zeroinitializer" end
+
+(* (restart-case BODY (name [] BODY-1) ...) — §3, §4 and §6 together.
+
+   One frame per clause, so that the frame a transfer names says which clause
+   to run: the address is the identity, which is exact where a number would
+   have to be unique against every module the running program might later load.
+   §4's "innermost offering the name" falls out of the stack walk, and
+   re-entering a restart-case works because each activation allocates its own
+   frames.
+
+   §5's defers between here and the invoke have already run — each function on
+   the way out ran its own before returning. What is left here is to take these
+   frames off and start the clause. *)
+and emit_restart_case f ty clauses body =
+  let result = if is_void ty then None else Some (alloca f ty) in
+  let frames =
+    map_lr
+      (fun (c : Tast.rclause) ->
+         let slot = alloca_raw f "%restart" in
+         let nid = fresh f in
+         ins f "%s = getelementptr inbounds %%restart, ptr %s, i32 0, i32 1"
+           nid slot;
+         ins f "store i32 %d, ptr %s" c.Tast.rname_id nid;
+         ins f "call void @flan_restart_push(ptr %s)" slot;
+         slot)
+      clauses
+  in
+  let pop () =
+    List.iter
+      (fun slot -> ins f "call void @flan_restart_pop(ptr %s)" slot)
+      (List.rev frames)
+  in
+  let ld = fresh_label f "endrestart" in
+  let pad = fresh_label f "rxfer" and used = ref false in
+  let reached = ref false in
+  let yield v =
+    if f.live then begin
+      (match result with
+       | Some r -> ins f "store %s %s, ptr %s" (ll ty) v r
+       | None -> ());
+      reached := true;
+      term f "br label %%%s" ld
+    end
+  in
+  f.pads <- (pad, used) :: f.pads;
+  let v = value f body in
+  f.pads <- List.tl f.pads;
+  if f.live then pop ();
+  yield v;
+  label f pad;
+  let tgt = fresh f in
+  ins f "%s = load ptr, ptr %s" tgt xfer_param;
+  (* Cleared before the clause runs, and put back if this transfer turns out to
+     be aimed further out. A clause body is ordinary code and its calls are
+     guarded like any other; it must not start with the channel still set. *)
+  ins f "store ptr null, ptr %s" xfer_param;
+  pop ();
+  let rec dispatch = function
+    | [] ->
+      ins f "store ptr %s, ptr %s" tgt xfer_param;
+      term f "br label %%%s" (current_pad f)
+    | (slot, (c : Tast.rclause)) :: rest ->
+      let hit = fresh_label f "restart" and next = fresh_label f "outer" in
+      let t = fresh f in
+      ins f "%s = icmp eq ptr %s, %s" t tgt slot;
+      term f "br i1 %s, label %%%s, label %%%s" t hit next;
+      label f hit;
+      yield (block f c.Tast.rbody);
+      label f next;
+      dispatch rest
+  in
+  dispatch (List.combine frames clauses);
+  if not !reached then begin f.live <- false; "zeroinitializer" end
+  else begin
+    label f ld;
+    match result with Some r -> load f r ty | None -> "zeroinitializer"
+  end
 
 and emit_if f ty c t e =
   let cv = value f c in
@@ -830,6 +982,12 @@ let signature ~named (fn : Tast.fn) =
       (fun i ty -> if named then Printf.sprintf "%s %%p%d" (ll ty) i else ll ty)
       fn.Tast.params
   in
+  (* The transfer channel, spec-conditions.md §6: one [ptr] appended to every
+     signature, written by an [invoke-restart] and checked after every call.
+     Uniform rather than only on the functions that need it — the spec's escape
+     analysis is an optimisation, and in a dev build a cell can hold anything,
+     so the honest answer to "what can this call?" is "anything". *)
+  let params = params @ [ (if named then "ptr " ^ xfer_param else "ptr") ] in
   Printf.sprintf "%s %s(%s)" (ll fn.Tast.ret) (fname fn.Tast.name)
     (String.concat ", " params)
 
@@ -848,6 +1006,7 @@ let emit_fn m ?(hidden = false) (fn : Tast.fn) =
     ret = fn.Tast.ret;
     slots = Array.init n (fun i -> Printf.sprintf "%%s%d" i);
     slot_tys = fn.Tast.slots;
+    pads = []; unwind = "unwind"; unwound = false; defers = fn.Tast.fdefers;
   } in
   (* Every slot is an alloca in the entry block, because [addr] may take the
      address of any of them and mem2reg only promotes entry-block allocas. *)
@@ -869,6 +1028,38 @@ let emit_fn m ?(hidden = false) (fn : Tast.fn) =
      discarded, so the return is the Unit constant rather than that value. *)
   if Types.equal fn.Tast.ret Types.Unit then last := "zeroinitializer";
   term f "ret %s %s" (ll fn.Tast.ret) !last;
+  (* The transfer exit, spec-conditions.md §5 and §6. A transfer that reached
+     the top of this function without a restart-case to catch it leaves the
+     same way a [return] does — which is what reuses the existing return path,
+     and with it the defers, for free. The value returned is meaningless: the
+     caller's guard sees the channel set and never looks at it. *)
+  if f.unwound then begin
+    label f f.unwind;
+    let cleanup = "unwind.cleanup" and used = ref false in
+    if f.defers <> [] then begin
+      (* The channel is cleared while the defers run and put back after. A
+         defer makes ordinary calls and each one is guarded; with the channel
+         still set the first of them would branch straight back here. *)
+      let tgt = fresh f in
+      ins f "%s = load ptr, ptr %s" tgt xfer_param;
+      ins f "store ptr null, ptr %s" xfer_param;
+      f.pads <- [ (cleanup, used) ];
+      List.iter (fun e -> ignore (value f e)) f.defers;
+      f.pads <- [];
+      ins f "store ptr %s, ptr %s" tgt xfer_param
+    end;
+    term f "ret %s zeroinitializer" (ll fn.Tast.ret);
+    (* A defer that starts a *second* transfer while the first is unwinding.
+       §6's per-frame slot nests, but nothing here does: the first transfer's
+       target is in hand and the defers are half run. Refused loudly rather
+       than resolved to one of them. *)
+    if !used then begin
+      label f cleanup;
+      let id, n = string_bytes f.md (Loc.to_string fn.Tast.floc) in
+      ins f "call void @flan_transfer_fail(ptr %s, i64 %d)" id n;
+      term f "unreachable"
+    end
+  end;
   Buffer.add_string m.out
     (Printf.sprintf "\ndefine %s%s {\nentry:\n%s%s}\n"
        (if hidden then "hidden " else "") (signature ~named:true fn)
@@ -921,6 +1112,11 @@ let header = {|; Generated by flan. The layout is C's: no object headers anywher
 ; A handler frame: the one it displaced, the condition type it matches, and
 ; the lifted function that runs. Allocated on the establishing frame's stack.
 %handler = type { ptr, i32, ptr }
+; A restart frame: the one it displaced and the name it offers. There is no
+; target field, because the frame's own address *is* the target — which makes
+; a transfer's aim exact, and makes re-entering a restart-case work with
+; nothing extra, since each activation allocates its own.
+%restart = type { ptr, i32 }
 
 declare void @flan_rt_init(i32, ptr)
 declare void @flan_argv(ptr)
@@ -932,7 +1128,12 @@ declare void @flan_f64_to_bytes(double, ptr)
 declare void @flan_i64_to_bytes(i64, ptr)
 declare void @flan_handler_push(ptr)
 declare void @flan_handler_pop(ptr)
-declare void @flan_signal(i32, ptr)
+declare void @flan_signal(i32, ptr, ptr)
+declare void @flan_restart_push(ptr)
+declare void @flan_restart_pop(ptr)
+declare ptr @flan_find_restart(i32)
+declare void @flan_restart_fail(ptr, i64, ptr, i64) noreturn cold
+declare void @flan_transfer_fail(ptr, i64) noreturn cold
 declare void @flan_bounds_fail(ptr, i64, i64, i64) noreturn cold
 declare void @flan_slice_fail(ptr, i64, i64, i64, i64) noreturn cold
 |}
@@ -943,6 +1144,13 @@ let emit_main m (fn : Tast.fn) =
   let b = Buffer.create 256 in
   Buffer.add_string b "\ndefine i32 @main(i32 %argc, ptr %argv) {\nentry:\n";
   Buffer.add_string b "  call void @flan_rt_init(i32 %argc, ptr %argv)\n";
+  (* The program's own end of the transfer channel. Nothing can be transferring
+     when [main] returns: a restart is found by name on the restart stack, and
+     an [invoke-restart] that finds none fails at the invoke site rather than
+     unwinding past everything. *)
+  Buffer.add_string b (Printf.sprintf "  %s = alloca ptr\n" xfer_param);
+  Buffer.add_string b
+    (Printf.sprintf "  store ptr null, ptr %s\n" xfer_param);
   let args =
     if fn.Tast.params = [] then ""
     else begin
@@ -954,7 +1162,8 @@ let emit_main m (fn : Tast.fn) =
   in
   Buffer.add_string b
     (Printf.sprintf "  %%r = call %s %s(%s)\n" (ll fn.Tast.ret)
-       (fname "main") args);
+       (fname "main")
+       (if args = "" then "ptr " ^ xfer_param else args ^ ", ptr " ^ xfer_param));
   (* Flushing matters: stdout is a FILE* and the acceptance test reads it. *)
   Buffer.add_string b "  call void @flan_exit(i32 ";
   Buffer.add_string b
@@ -1199,8 +1408,10 @@ let redefinition ?(checks = true) ?(dev = false) ?(known = fun _ -> true)
     | Some fn ->
       Buffer.add_string m.out
         (Printf.sprintf
-           "\ndefine void @flan_reload_call() {\nentry:\n  call %s %s()\n  \
-            ret void\n}\n" (ll Types.Unit) (fname fn));
+           "\ndefine void @flan_reload_call() {\nentry:\n  \
+            %s = alloca ptr\n  store ptr null, ptr %s\n  \
+            call %s %s(ptr %s)\n  ret void\n}\n"
+           xfer_param xfer_param (ll Types.Unit) (fname fn) xfer_param);
       (* Nothing outside this module refers to anything in it once the call has
          returned — no cell holds an address in its text, the registry has no
          slot for it, and the value it produced was copied out. So it says so,
diff --git a/lib/load.ml b/lib/load.ml
index 79a08ba..8e39528 100644
--- a/lib/load.ml
+++ b/lib/load.ml
@@ -175,6 +175,16 @@ let rec rename_expr owned alias bound (e : Ast.expr) : Ast.expr =
     | Ast.Defer body -> Ast.Defer (gos body)
     | Ast.Unwrap (u, v) -> Ast.Unwrap (u, go v)
     | Ast.Signal c -> Ast.Signal (go c)
+    (* A restart name is not a top-level name — it is looked up on the restart
+       stack, not in the environment — so an import does not qualify it. Only
+       the bodies are rewritten. *)
+    | Ast.RestartCase (body, clauses) ->
+      Ast.RestartCase
+        (go body,
+         List.map
+           (fun (c : Ast.rclause) -> { c with Ast.rbody = gos c.Ast.rbody })
+           clauses)
+    | Ast.InvokeRestart _ -> e.Ast.e
     (* A clause names a condition *type*, which an import renames like any
        other, and binds a name for the condition inside its own body. *)
     | Ast.HandlerBind (clauses, body) ->
diff --git a/lib/parse.ml b/lib/parse.ml
index 483e091..5524c5d 100644
--- a/lib/parse.ml
+++ b/lib/parse.ml
@@ -220,9 +220,46 @@ and form f mk (head : Form.t) (args : Form.t list) : Ast.expr =
     in
     mk (Ast.HandlerBind (List.map clause clauses, body_of body))
 
+  (* (restart-case BODY (name [] BODY-1) ...) — spec-conditions.md §3.
+     The body and every clause have the same type, which is the form's.
+     Restarts take no parameters in this version; a clause that declares one is
+     rejected below rather than ignored. *)
+  | Sym "restart-case" ->
+    let body, clauses =
+      match args with
+      | body :: clauses when clauses <> [] -> (body, clauses)
+      | _ ->
+        fail f "restart-case is (restart-case body (name [] body ...) ...)"
+    in
+    let clause (c : Form.t) =
+      match c.Form.v with
+      | Form.List ({ v = Form.Sym n; _ } :: { v = Form.Vec ps; _ } :: cbody)
+        when cbody <> [] ->
+        if ps <> [] then
+          fail c
+            "a restart takes no parameters yet — spec-conditions.md §3 has              them, and they need argument marshalling and a runtime arity              check that this version does not do";
+        { Ast.rname = n; rbody = List.map expr cbody; rloc = c.Form.loc }
+      | _ -> fail c "a restart-case clause is (name [] body ...)"
+    in
+    mk (Ast.RestartCase (expr body, List.map clause clauses))
+
+  (* (invoke-restart 'name) : Never. The name is a quoted symbol — that is what
+     the reader's quote is for — and it is resolved on the restart stack at run
+     time, since restarts are dynamically scoped. *)
+  | Sym "invoke-restart" ->
+    (match args with
+     | [ { v = Form.List [ { v = Form.Sym "quote"; _ }; { v = Form.Sym n; _ } ]; _ } ] ->
+       mk (Ast.InvokeRestart n)
+     | [ _ ] ->
+       fail f
+         "invoke-restart takes a quoted restart name, as in           (invoke-restart 'use-placeholder)"
+     | _ ->
+       fail f
+         "a restart takes no arguments yet — spec-conditions.md §3 has them,           and they need argument marshalling and a runtime arity check that           this version does not do")
+
   (* Recognised, deliberately unimplemented. Rejected rather than left to fall
      through to Call, where they would parse and mean nothing. *)
-  | Sym ("handler-case" | "restart-case" | "invoke-restart"
+  | Sym ("handler-case"
         | "errdefer" | "with-allocator" | "loop" | "recur"
         | "defmacro" | "await" as name) ->
     fail f "%s is not implemented yet (see the build sequence in plan.org)" name
diff --git a/lib/session.ml b/lib/session.ml
index d4d6922..ec688fa 100644
--- a/lib/session.ml
+++ b/lib/session.ml
@@ -573,7 +573,7 @@ let eval_expr ?(origin = "<eval>") t src : change =
   t.thunks <- t.thunks + 1;
   let name = Printf.sprintf "eval/%d" t.thunks in
   let thunk : Tast.fn =
-    { Tast.name; params = []; ret = Types.Unit; body; floc = loc;
+    { Tast.name; params = []; ret = Types.Unit; body; fdefers = []; floc = loc;
       slots = Array.append base (Array.of_list (List.rev c.slots)) }
   in
   (* Built against the program but never spliced into it: an evaluation is not
diff --git a/lib/tast.ml b/lib/tast.ml
index 20fd6ff..e03bfba 100644
--- a/lib/tast.ml
+++ b/lib/tast.ml
@@ -69,6 +69,14 @@ and expr_kind =
      function by the checker, so what is left is the frame and the call. *)
   | Signal  of int * expr             (* type id, the condition value *)
   | Handled of hframe list * expr list
+  (* The transfer, spec-conditions.md §3–§6. [RestartCase] pushes one frame per
+     clause, runs its body, and pops them; if a transfer arrives naming one of
+     *its* frames it runs that clause instead, and the whole form yields either
+     way. [InvokeRestart] looks the name up on the restart stack, writes the
+     frame it found into the transfer channel and leaves — it has type Never,
+     so nothing follows it. *)
+  | RestartCase of rclause list * expr
+  | InvokeRestart of int * string * Loc.t   (* name id, name, where *)
 
 and place =
   | Plocal  of int
@@ -82,6 +90,11 @@ and place =
    that runs when one is signalled. *)
 and hframe = { htype : int; hfn : string }
 
+(* A restart clause. [rname_id] is what [invoke-restart] matches by name; the
+   body is a branch in the function that wrote it, because unlike a handler a
+   clause runs at the restart-case, which is where it was written. *)
+and rclause = { rname_id : int; rname : string; rbody : expr list }
+
 (* [binds] are the slots the pattern's fields are bound to, in field order. *)
 and arm = { acase : string option; binds : int list; abody : expr list }
 
@@ -99,6 +112,11 @@ type fn = {
   slots   : Types.t array;            (* the frame: one entry per slot *)
   ret     : Types.t;
   body    : expr list;
+  (* The defers again, innermost first. [body] already has them spliced onto
+     the normal exit path; this is the same list for the *transfer* exit path,
+     which leaves through a landing block the backend builds and no form in
+     [body] can reach. spec-conditions.md §5: they run, and errdefer does not. *)
+  fdefers : expr list;
   floc    : Loc.t;
 }
 
diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c
index 6c30f55..78c00f5 100644
--- a/runtime/flan_rt.c
+++ b/runtime/flan_rt.c
@@ -35,7 +35,7 @@
 typedef struct flan_handler {
   struct flan_handler *prev;
   uint32_t             type_id;
-  void               (*fn)(void *condition);
+  void               (*fn)(void *condition, void *xfer);
 } flan_handler;
 
 static flan_handler *handlers;
@@ -51,9 +51,48 @@ void flan_handler_pop(flan_handler *h) {
   handlers = h->prev;
 }
 
-void flan_signal(uint32_t type_id, void *condition) {
+/* [xfer] is the signalling function's own end of the transfer channel
+ * (spec-conditions.md §6), threaded through so that a handler invoking a
+ * restart can write its target into it. That makes this C frame transparent to
+ * a transfer, which it has to be: a handler is always reached through here, so
+ * the rule that a transfer cannot cross a foreign frame would otherwise make
+ * restart-case useless.
+ *
+ * A handler that transfers stops the walk. The remaining handlers are for a
+ * signal that is still looking for someone; this one has been answered. */
+void flan_signal(uint32_t type_id, void *condition, void *xfer) {
   for (flan_handler *h = handlers; h != NULL; h = h->prev)
-    if (h->type_id == type_id) h->fn(condition);
+    if (h->type_id == type_id) {
+      h->fn(condition, xfer);
+      if (*(void **)xfer != NULL) return;
+    }
+}
+
+/* A restart stack, the same shape and for the same reasons. What a transfer
+ * carries is the *address* of one of these frames, not a number: the frame is
+ * allocated by the restart-case that offers it, on its own stack, so the
+ * address is unique against every module a running program may later load and
+ * against every re-entry of the same restart-case. §4's "innermost frame
+ * offering the name" is then just the order of the walk. */
+
+typedef struct flan_restart {
+  struct flan_restart *prev;
+  uint32_t             name_id;
+} flan_restart;
+
+static flan_restart *restarts;
+
+void flan_restart_push(flan_restart *r) {
+  r->prev = restarts;
+  restarts = r;
+}
+
+void flan_restart_pop(flan_restart *r) { restarts = r->prev; }
+
+void *flan_find_restart(uint32_t name_id) {
+  for (flan_restart *r = restarts; r != NULL; r = r->prev)
+    if (r->name_id == name_id) return r;
+  return NULL;
 }
 
 /* [T] and string are both ptr+len — see Emit.ll. */
@@ -157,6 +196,31 @@ _Noreturn void flan_bounds_fail(const uint8_t *loc, int64_t loclen,
   rt_die();
 }
 
+/* Nothing on the restart stack offers the name. It is reported where the
+ * invoke was, because that is the only place that knows what was asked for;
+ * there is nowhere to resume, so there is nothing else to do. */
+_Noreturn void flan_restart_fail(const uint8_t *loc, int64_t loclen,
+                                 const uint8_t *name, int64_t namelen) {
+  fflush(stdout);
+  fprintf(stderr, "%.*s: no restart named %.*s is active\n",
+          (int)loclen, (const char *)loc, (int)namelen, (const char *)name);
+  rt_die();
+}
+
+/* Something a defer called invoked a restart. A defer is the cleanup a
+ * transfer runs on its way out (§5), so a transfer starting there would leave
+ * this frame's defers half run with two targets and no way to choose. The
+ * lexical case is refused by the checker; this is the one that reaches a
+ * function through a call, where nothing static could see it. */
+_Noreturn void flan_transfer_fail(const uint8_t *loc, int64_t loclen) {
+  fflush(stdout);
+  fprintf(stderr,
+          "%.*s: a defer invoked a restart, which a defer may not do — it is "
+          "the cleanup a transfer runs on its way out\n",
+          (int)loclen, (const char *)loc);
+  rt_die();
+}
+
 _Noreturn void flan_slice_fail(const uint8_t *loc, int64_t loclen,
                                int64_t lo, int64_t hi, int64_t len) {
   fflush(stdout);
diff --git a/test/programs/restarts.flan b/test/programs/restarts.flan
new file mode 100644
index 0000000..2d923d6
--- /dev/null
+++ b/test/programs/restarts.flan
@@ -0,0 +1,65 @@
+;;;; restart-case and invoke-restart — spec-conditions.md §3 to §6.
+;;;;
+;;;; The transfer. A handler runs where the signal was, decides, and control
+;;;; resumes at a restart-case further out: every function in between returns
+;;;; early with the target in the channel, running its defers on the way (§5).
+;;;; Restarts take no parameters in this version.
+(defstruct AssetMissing [id i32])
+
+(defvar log i64)
+
+;;; The signalling end. Two frames below the restart-case, so the transfer has
+;;; something to cross.
+(defn load [n i32] i32
+  (signal (AssetMissing {:id n}))
+  100)
+
+;;; §5: this defer runs whether the call below returns or transfers, and it
+;;; runs before the clause body starts.
+(defn middle [n i32] i32
+  (defer (set log (+ log 1)))
+  (+ (load n) 1))
+
+;;; The spec's load-texture shape (§1): a restart-case in value position, whose
+;;; fall-through has to produce the type too.
+(defn fetch [n i32] i32
+  (restart-case (middle n)
+    (use-placeholder [] -1)
+    (retry        [] 7)))
+
+;;; §4: an inner restart-case shadows an outer one offering the same name, and
+;;; the outer one is reached again once the inner has been left.
+(defn nested [n i32] i32
+  (restart-case
+    (+ (restart-case (middle n)
+         (use-placeholder [] 10))
+       1000)
+    (use-placeholder [] 20)))
+
+(defn main [] i32
+  ;; Nothing handles it, so signal is a no-op and the body's own value stands.
+  (print-i64 (i64 (fetch 1))) (newline)                   ; 101
+  (print-i64 log) (newline)                               ; 1
+
+  ;; A handler that transfers: the clause's value is the restart-case's.
+  (handler-bind [(AssetMissing [c] (invoke-restart 'use-placeholder))]
+    (print-i64 (i64 (fetch 2))) (newline))                ; -1
+  (print-i64 log) (newline)                               ; 2 — the defer ran
+
+  (handler-bind [(AssetMissing [c] (invoke-restart 'retry))]
+    (print-i64 (i64 (fetch 3))) (newline))                ; 7
+
+  ;; §4: the innermost frame offering the name wins, and the clause yields to
+  ;; *its* own continuation — so the +1000 written around the inner
+  ;; restart-case still runs, and the outer clause never does.
+  (handler-bind [(AssetMissing [c] (invoke-restart 'use-placeholder))]
+    (print-i64 (i64 (nested 4))) (newline))               ; 1010
+
+  ;; A handler that returns normally transfers nothing: §1's accumulation case
+  ;; still works, and the fall-through stands.
+  (handler-bind [(AssetMissing [c] (set log (+ log 100)))]
+    (print-i64 (i64 (fetch 5))) (newline))                ; 101
+  ;; The handler runs at the signal, which is inside the call the defer
+  ;; belongs to, so its +100 lands before that defer's +1.
+  (print-i64 log) (newline)                               ; 4 + 100 + 1 = 105
+  0)
diff --git a/test/reload_host.c b/test/reload_host.c
index 3e33a00..d04c28c 100644
--- a/test/reload_host.c
+++ b/test/reload_host.c
@@ -39,7 +39,11 @@
 /* The Flan symbols the executable itself defines. Flan names contain
  * characters C identifiers cannot, so each one is reached through its asm
  * label — the same name Emit spells. */
-extern int64_t flan_outer(void) __asm__("flan.outer");
+/* The trailing ptr is the transfer channel spec-conditions.md §6 puts in every
+ * Flan signature. This host never transfers, so it passes a slot of its own
+ * that stays null — but the parameter is not optional: getting it wrong reads
+ * garbage as the channel and fails nowhere near here. */
+extern int64_t flan_outer(void *xfer) __asm__("flan.outer");
 extern int64_t flan_counter __asm__("flan.counter");
 
 void flan_rt_init(int32_t argc, char **argv);
@@ -83,10 +87,11 @@ int main(int argc, char **argv) {
     fprintf(stderr, "usage: %s <module.so>...\n", argv[0]);
     return 2;
   }
-  printf("host %lld\n", (long long)flan_outer());
+  void *xfer = NULL;
+  printf("host %lld\n", (long long)flan_outer(&xfer));
   for (int i = 1; i < argc; i++) {
     if (!install(argv[i])) return 1;
-    printf("after%d %lld\n", i, (long long)flan_outer());
+    printf("after%d %lld\n", i, (long long)flan_outer(&xfer));
   }
   printf("counter %lld\n", (long long)flan_counter);
   return 0;
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 1e73a8d..d806a62 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -116,6 +116,17 @@ let () =
     outputs "conditions" "programs/conditions.flan" conditions_out;
     outputs ~opt:"-O0" "conditions, -O0" "programs/conditions.flan" conditions_out;
     outputs ~dev:true "conditions, dev" "programs/conditions.flan" conditions_out;
+    (* restart-case and invoke-restart, §3 to §6: the transfer itself. A
+       fall-through with nothing handling it, a clause reached from two frames
+       down, the defer in between running on the way out, an inner frame
+       shadowing an outer one of the same name, and a handler that returns
+       normally still transferring nothing. At -O0 as well, because the guard
+       after every call is control flow the optimiser would otherwise launder;
+       and as a dev build, where every one of those calls goes through a cell. *)
+    let restarts_out = "101\n1\n-1\n2\n7\n1010\n101\n105\n" in
+    outputs "restarts" "programs/restarts.flan" restarts_out;
+    outputs ~opt:"-O0" "restarts, -O0" "programs/restarts.flan" restarts_out;
+    outputs ~dev:true "restarts, dev" "programs/restarts.flan" restarts_out;
 
     (* The raylib FFI, headless. GetColor and the enums need no window, so the
        whole boundary is exercised without a display: a struct returned through
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 27d222a..c6fbed6 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -649,9 +649,51 @@ let () =
     "(defstruct C [id i32])\n\
      (defn f [] i32 (handler-bind [(C [c] (signal c))] (return 1)) 0)"
     ~needle:"return is not allowed inside handler-bind";
-  (* Everything the four operators do not yet cover still says so by name. *)
-  rejects_check "restart-case is still unimplemented"
-    "(defn f [] (restart-case 1 (skip [] 2)))" ~needle:"not implemented yet";
+  (* ── restart-case and invoke-restart, §3 to §6 ─────────────────── *)
+
+  accepts "restart-case with a clause that transfers into it"
+    "(defstruct C [id i32])\n\
+     (defn g [] i32 (signal (C {:id 1})) 0)\n\
+     (defn f [] i32 (restart-case (g) (skip [] 7)))\n\
+     (defn h [] i32 (handler-bind [(C [c] (invoke-restart 'skip))] (f)))";
+  (* §3: the body and every clause yield the whole form, so they have to agree
+     — which is also what makes the fall-through path visible in the source.
+     With a type expected from outside they are each checked against it; with
+     none, as in a let binding, the first one that produces a value sets it. *)
+  rejects_check "a clause that disagrees with the body"
+    "(defn f [] i32 (restart-case 1 (skip [] \"no\")))"
+    ~needle:"expected i32, found string";
+  rejects_check "two clauses that disagree, with nothing expected"
+    "(defn f [] i32 (let [x (restart-case (exit 1) (a [] 1) (b [] \"no\"))] 0))"
+    ~needle:"expected i32, found string";
+  (* §4 finds the first frame offering a name. Two of one name in one frame
+     would make that a choice nothing in the source shows. *)
+  rejects_check "one restart-case offering a name twice"
+    "(defn f [] i32 (restart-case 1 (skip [] 2) (skip [] 3)))"
+    ~needle:"offers skip twice";
+  (* Same rule as handler-bind: the restart frames are popped on the way out. *)
+  rejects_check "return inside restart-case"
+    "(defn f [] i32 (restart-case (return 1) (skip [] 2)))"
+    ~needle:"return is not allowed inside restart-case";
+  (* The two halves of §3 this version does not do, each refused by name with
+     the reason rather than parsed into something that means less. *)
+  rejects_check "a restart with parameters"
+    "(defn f [] i32 (restart-case 1 (skip [n i32] n)))"
+    ~needle:"a restart takes no parameters yet";
+  rejects_check "invoke-restart with arguments"
+    "(defn f [] (invoke-restart 'skip 1))"
+    ~needle:"a restart takes no arguments yet";
+  rejects_check "invoke-restart on an unquoted name"
+    "(defn f [] (invoke-restart skip))"
+    ~needle:"quoted restart name";
+  (* §5 runs the defers on the way out, so a defer is already the cleanup path
+     a transfer uses. One that starts its own transfer has no answer. *)
+  rejects_check "invoke-restart inside a defer"
+    "(defn f [] i32 (defer (invoke-restart 'skip)) 0)"
+    ~needle:"not allowed inside a defer";
+  (* Still unimplemented, and still says so by name. *)
+  rejects_check "handler-case is still unimplemented"
+    "(defn f [] (handler-case 1))" ~needle:"not implemented yet";
 
   (* ── The acceptance program checks end to end ──────────────────── *)
   accepts "calc-me.flan type checks"