diff --git a/lib/ast.ml b/lib/ast.ml
index 3edf084..c37147e 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -57,10 +57,11 @@ 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 sigkind * expr                 (* (signal c) / (error c)        *)
-  (* (restart-case body (name [] body ...) ...) and (invoke-restart 'name).
-     Both alter control flow, so neither can be a call. *)
+  (* (restart-case body (name [p T] body ...) ...) and
+     (invoke-restart 'name arg ...). Both alter control flow, so neither can be
+     a call, and a clause binds its parameters — §3. *)
   | RestartCase of expr * rclause list
-  | InvokeRestart of string
+  | InvokeRestart of string * expr list
 
 (* Two ways to signal, because they are two different things — §1 and §2.
    [signal] returns Unit whatever it finds; [error] has type Never and, with
@@ -68,7 +69,16 @@ and expr_kind =
 and sigkind = Ssignal | Serror
 
 and hclause = { hty : texpr; hname : string; hbody : expr list; hloc : Loc.t }
-and rclause = { rname : string; rbody : expr list; rloc : Loc.t }
+(* [rparams] are §3's inline annotations, the same name/type pairs a [defn]
+   takes. They are bound in the clause body and filled in by whatever invoked
+   the restart, which is why their count and types are checked at run time
+   (§3): a restart is found by name on a dynamic stack. *)
+and rclause =
+  { rname : string; rparams : field list; rbody : expr list; rloc : Loc.t }
+
+(* Inline name/type pairs, as in [defn], [let] and [defstruct]. Here because a
+   restart clause's parameters are one, and a clause is part of an expression. *)
+and field = { fname : string; fty : texpr; floc : Loc.t }
 
 (* Two unwrap operators, because they are two different things — plan.org. *)
 and unwrap = Usome | Utry
@@ -90,8 +100,6 @@ and pattern =
 
 (* ── Declarations ──────────────────────────────────────────────────── *)
 
-type field = { fname : string; fty : texpr; floc : Loc.t }
-
 type fn = {
   name    : string;
   params  : field list;
diff --git a/lib/check.ml b/lib/check.ml
index e85f043..931e09c 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -338,6 +338,21 @@ let type_id name =
     name;
   !h
 
+(* How a restart's parameter list is spelled, and with it what the two ends of
+   an [invoke-restart] compare — spec-conditions.md §3's run-time check. A
+   restart is found by name on a dynamic stack, so neither end can see the
+   other and nothing static can be checked: what is compared at run time is
+   this string's hash, alongside the count, and the string itself is carried so
+   that a mismatch can say what was wanted and what was given.
+
+   Comparing a 32-bit hash means two different parameter lists could in
+   principle collide. The count is checked separately, which rules out every
+   practical case (a collision would have to be between two lists of the same
+   length), and the types are parenthesised so that [(Option i32)] cannot read
+   as two parameters. *)
+let restart_sig tys =
+  "(" ^ String.concat " " (List.map Types.to_string tys) ^ ")"
+
 let expect loc ~want (got : Tast.expr) =
   match want with
   | None -> got
@@ -489,18 +504,48 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
      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 ->
+  | Ast.InvokeRestart (name, args) ->
     (* 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. *)
+       dynamically scoped and named — §4 — and so, for the same reason, is the
+       check that these arguments are the ones the clause takes (§3). *)
     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)))
+    let args = map_lr (fun a -> check ctx a) args in
+    List.iter
+      (fun (a : Tast.expr) ->
+         match a.Tast.ty with
+         | Types.Unit | Types.Never ->
+           fail a.Tast.loc
+             "a restart argument must be a value, and this one is %s"
+             (Types.to_string a.Tast.ty)
+         | _ -> ())
+      args;
+    let sg = restart_sig (List.map (fun (a : Tast.expr) -> a.Tast.ty) args) in
+    (* Evaluated into slots first, so that an argument which transfers on its
+       own is guarded before this form aims the channel, and so that a call
+       written in an argument is on the ordinary walk rather than hidden
+       inside a node that [Reach] and [Load] treat as a leaf. *)
+    let binds =
+      List.map (fun (a : Tast.expr) -> (fresh_slot ctx a.Tast.ty, a)) args
+    in
+    let locals =
+      List.map
+        (fun (s, (a : Tast.expr)) -> mk a.Tast.loc a.Tast.ty (Tast.Local s))
+        binds
+    in
+    let invoke =
+      mk loc Types.Never
+        (Tast.InvokeRestart (type_id name, name, locals, sg, type_id sg, loc))
+    in
+    expect loc ~want
+      (if binds = [] then invoke
+       else mk loc Types.Never (Tast.Let (binds, [ invoke ])))
 
   | Ast.Defer _ ->
     (* Registered by [check_fn], which is the only place that sees a form's
@@ -703,13 +748,36 @@ and check_restart_case ctx ?want loc body clauses =
          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;
-         (* Each is checked against what the form has settled on so far, so a
-            clause that disagrees fails where it is written. The first one to
-            produce a value is what settles it when nothing outside did. *)
-         let b = block ctx ?want:!ty c.Ast.rloc c.Ast.rbody in
+         (* §3's parameters. They are slots in *this* function — a clause runs
+            here, not where the invoke was — and the invoker stores into a
+            buffer this frame owns, because its own frame is gone by the time
+            the clause body starts (§5). Bound like a function's parameters:
+            visible only in the clause, and not assignable. *)
+         let params, b =
+           scoped ctx (fun () ->
+             let params =
+               List.map
+                 (fun (p : Ast.field) ->
+                    let ty = resolve ctx.env p.Ast.fty in
+                    (match ty with
+                     | Types.Unit | Types.Never ->
+                       fail p.Ast.floc
+                         "%s would be a restart parameter of type %s, which is \
+                          not a value" p.Ast.fname (Types.to_string ty)
+                     | _ -> ());
+                    (bind ctx p.Ast.fname ty ~assignable:false, ty))
+                 c.Ast.rparams
+             in
+             (* Each is checked against what the form has settled on so far, so
+                a clause that disagrees fails where it is written. The first one
+                to produce a value is what settles it when nothing outside
+                did. *)
+             (params, block ctx ?want:!ty c.Ast.rloc c.Ast.rbody))
+         in
          if !ty = None && b.Tast.ty <> Types.Never then ty := Some b.Tast.ty;
+         let sg = restart_sig (List.map snd params) in
          { Tast.rname_id = type_id c.Ast.rname; rname = c.Ast.rname;
-           rbody = [ b ] })
+           rparams = params; rsig = sg; rsig_id = type_id sg; rbody = [ b ] })
       clauses
   in
   let ty = match !ty with Some t -> t | None -> Types.Never in
diff --git a/lib/emit.ml b/lib/emit.ml
index 44f2dd7..d13093a 100644
--- a/lib/emit.ml
+++ b/lib/emit.ml
@@ -638,7 +638,11 @@ and value_at f (e : Tast.expr) : string =
   (* §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) ->
+  | Tast.InvokeRestart (id, name, args, sg, sg_id, rloc) ->
+    (* The arguments are already in slots — the checker put them there, so an
+       argument that transferred on its own has been guarded before anything
+       here runs. *)
+    let vals = List.map (fun a -> (value f a, a.Tast.ty)) args in
     let t = fresh f in
     ins f "%s = call ptr @flan_find_restart(i32 %d)" t id;
     let ok = fresh f in
@@ -649,6 +653,52 @@ and value_at f (e : Tast.expr) : string =
       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);
+    (* §3's run-time check. A restart is found by name on a dynamic stack, so
+       what it takes is not knowable here: the frame carries its parameter
+       count and the hash of how they are spelled, and both are compared.
+       The count is not redundant with the hash — it is what makes a 32-bit
+       collision between two different signatures harmless in practice — and
+       it is also the cheaper half. *)
+    let arity = fresh f in
+    ins f "%s = load i32, ptr %s" arity (restart_field f t 5);
+    let a_ok = fresh f in
+    ins f "%s = icmp eq i32 %s, %d" a_ok arity (List.length args);
+    let want = fresh f in
+    ins f "%s = load i32, ptr %s" want (restart_field f t 6);
+    let s_ok = fresh f in
+    ins f "%s = icmp eq i32 %s, %d" s_ok want sg_id;
+    let both = fresh f in
+    ins f "%s = and i1 %s, %s" both a_ok s_ok;
+    fail_block f rloc both (fun id n ->
+      let nid, nn = string_bytes f.md name in
+      (* What the frame says it takes is read off the frame, because only the
+         frame knows; what was given is this call site's own spelling. *)
+      let wp = fresh f in
+      ins f "%s = load ptr, ptr %s" wp (restart_field f t 8);
+      let wl = fresh f in
+      ins f "%s = load i64, ptr %s" wl (restart_field f t 9);
+      let gid, gn = string_bytes f.md sg in
+      ins f
+        "call void @flan_restart_args_fail(ptr %s, i64 %d, ptr %s, i64 %d, \
+         ptr %s, i64 %s, ptr %s, i64 %d)" id n nid nn wp wl gid gn);
+    (* Into the buffer the target frame owns, field by field: this frame is
+       about to go, and the clause runs after it has. The layout is the one the
+       signature just agreed on. *)
+    if vals <> [] then begin
+      let buf = fresh f in
+      ins f "%s = load ptr, ptr %s" buf (restart_field f t 4);
+      let sty =
+        "{ " ^ String.concat ", " (List.map (fun (_, ty) -> ll ty) vals) ^ " }"
+      in
+      List.iteri
+        (fun i (v, ty) ->
+           let p = fresh f in
+           ins f "%s = getelementptr inbounds %s, ptr %s, i32 0, i32 %d"
+             p sty buf i;
+           ins f "store %s %s, ptr %s" (ll ty) v p)
+        vals;
+      ins f "store i32 1, ptr %s" (restart_field f t 7)
+    end;
     ins f "store ptr %s, ptr %s" t xfer_param;
     term f "br label %%%s" (current_pad f);
     "zeroinitializer"
@@ -898,7 +948,19 @@ and emit_handled f frames body =
   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.
+(* A clause's parameters, as one LLVM struct: what the invoker stores into and
+   what the clause loads out of. The two ends never see each other, so the
+   layout is agreed by the signature hash they compare first — same types in
+   the same order is the same struct. *)
+and args_type (c : Tast.rclause) =
+  "{ " ^ String.concat ", " (List.map (fun (_, t) -> ll t) c.Tast.rparams) ^ " }"
+
+and restart_field f slot i =
+  let p = fresh f in
+  ins f "%s = getelementptr inbounds %%restart, ptr %s, i32 0, i32 %d" p slot i;
+  p
+
+(* (restart-case BODY (name [p T] 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
@@ -909,33 +971,55 @@ and emit_handled f frames body =
 
    §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. *)
+   frames off, copy §3's parameters out of the buffer the invoker filled, and
+   start the clause.
+
+   The parameters live in a buffer this frame owns, not the invoker's: by the
+   time a clause runs, every frame between the two has returned, so anything on
+   the invoking side is gone. The invoker stores into it while both are alive,
+   which is the one moment they are. *)
 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 "store i32 %d, ptr %s" c.Tast.rname_id (restart_field f slot 1);
          (* The name itself, beside the hash. A hash is all that matching
             needs, but a break loop has to *show* someone their choices, and
             nothing at run time can turn a hash back into a name. *)
          let sid, slen = string_bytes f.md c.Tast.rname in
-         let np = fresh f in
-         ins f "%s = getelementptr inbounds %%restart, ptr %s, i32 0, i32 2"
-           np slot;
-         ins f "store ptr %s, ptr %s" sid np;
-         let nl = fresh f in
-         ins f "%s = getelementptr inbounds %%restart, ptr %s, i32 0, i32 3"
-           nl slot;
-         ins f "store i64 %d, ptr %s" slen nl;
+         ins f "store ptr %s, ptr %s" sid (restart_field f slot 2);
+         ins f "store i64 %d, ptr %s" slen (restart_field f slot 3);
+         (* §3's signature, which every frame carries whether it takes
+            parameters or not: an [invoke-restart] compares against whatever
+            frame the name found, and a clause taking none has to be able to
+            refuse arguments as loudly as one taking two of the wrong type. *)
+         ins f "store i32 %d, ptr %s"
+           (List.length c.Tast.rparams) (restart_field f slot 5);
+         ins f "store i32 %d, ptr %s" c.Tast.rsig_id (restart_field f slot 6);
+         let gid, glen = string_bytes f.md c.Tast.rsig in
+         ins f "store ptr %s, ptr %s" gid (restart_field f slot 8);
+         ins f "store i64 %d, ptr %s" glen (restart_field f slot 9);
+         let args =
+           if c.Tast.rparams = [] then None
+           else begin
+             let buf = alloca_raw f (args_type c) in
+             ins f "store ptr %s, ptr %s" buf (restart_field f slot 4);
+             (* Nothing has filled it in yet. Whoever aims a transfer at this
+                frame without going through an [invoke-restart] — the break
+                loop, today — leaves this zero, and the clause traps rather
+                than running on values no one supplied. *)
+             ins f "store i32 0, ptr %s" (restart_field f slot 7);
+             Some buf
+           end
+         in
          ins f "call void @flan_restart_push(ptr %s)" slot;
-         slot)
+         (slot, args))
       clauses
   in
+  let args_of slot = List.assoc slot frames in
+  let frames = List.map fst frames in
   let pop () =
     List.iter
       (fun slot -> ins f "call void @flan_restart_pop(ptr %s)" slot)
@@ -966,6 +1050,37 @@ and emit_restart_case f ty clauses body =
      guarded like any other; it must not start with the channel still set. *)
   ins f "store ptr null, ptr %s" xfer_param;
   pop ();
+  (* §3's parameters, copied out of the frame's buffer into the clause's own
+     slots before its body starts. The frame is still addressable — it is an
+     alloca of *this* function — and the buffer is whatever the invoker left
+     there. *)
+  let bind_params slot (c : Tast.rclause) =
+    match args_of slot with
+    | None -> ()
+    | Some buf ->
+      let armed = fresh f in
+      ins f "%s = load i32, ptr %s" armed (restart_field f slot 7);
+      let ok = fresh f in
+      ins f "%s = icmp ne i32 %s, 0" ok armed;
+      (* Aimed here by something that supplied no arguments — there is no such
+         path from an [invoke-restart], so this is the break loop taking a
+         restart it cannot yet fill in. Refused with the reason, rather than
+         running the clause on a buffer nobody wrote. *)
+      fail_block f (List.hd c.Tast.rbody).Tast.loc ok (fun id n ->
+        let nid, nn = string_bytes f.md c.Tast.rname in
+        let gid, gn = string_bytes f.md c.Tast.rsig in
+        ins f
+          "call void @flan_restart_unarmed(ptr %s, i64 %d, ptr %s, i64 %d, \
+           ptr %s, i64 %d)" id n nid nn gid gn);
+      List.iteri
+        (fun i (slot_i, ty) ->
+           let p = fresh f in
+           ins f "%s = getelementptr inbounds %s, ptr %s, i32 0, i32 %d"
+             p (args_type c) buf i;
+           let v = load f p ty in
+           ins f "store %s %s, ptr %s" (ll ty) v f.slots.(slot_i))
+        c.Tast.rparams
+  in
   let rec dispatch = function
     | [] ->
       ins f "store ptr %s, ptr %s" tgt xfer_param;
@@ -976,6 +1091,7 @@ and emit_restart_case f ty clauses body =
       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;
+      bind_params slot c;
       yield (block f c.Tast.rbody);
       label f next;
       dispatch rest
@@ -1545,7 +1661,14 @@ let header = {|; Generated by flan. The layout is C's: no object headers anywher
 ; 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, ptr, i64 }
+;
+; Then §3's parameters: the buffer the clause reads them out of — owned by the
+; restart-case, because the invoker's frame is gone by the time a clause runs —
+; how many there are, the hash of how they are spelled, whether anything has
+; filled the buffer in, and that spelling itself for the message when the two
+; ends disagree. The first four fields are what the runtime's own
+; [flan_restart] declares and their offsets do not move.
+%restart = type { ptr, i32, ptr, i64, ptr, i32, i32, i32, ptr, i64 }
 
 declare void @flan_rt_init(i32, ptr)
 declare void @flan_argv(ptr)
@@ -1565,6 +1688,8 @@ 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_restart_args_fail(ptr, i64, ptr, i64, ptr, i64, ptr, i64) noreturn cold
+declare void @flan_restart_unarmed(ptr, i64, 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
diff --git a/lib/load.ml b/lib/load.ml
index a1e1a3d..5514be6 100644
--- a/lib/load.ml
+++ b/lib/load.ml
@@ -202,15 +202,29 @@ let rec rename_expr owned alias bound (e : Ast.expr) : Ast.expr =
     | Ast.Unwrap (u, v) -> Ast.Unwrap (u, go v)
     | Ast.Signal (k, c) -> Ast.Signal (k, 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. *)
+       stack, not in the environment — so an import does not qualify it. The
+       bodies are rewritten, and so are a clause's parameter types, which name
+       types like any other annotation; the parameters themselves bind inside
+       the clause and shadow a package name there. *)
     | Ast.RestartCase (body, clauses) ->
       Ast.RestartCase
         (go body,
          List.map
-           (fun (c : Ast.rclause) -> { c with Ast.rbody = gos c.Ast.rbody })
+           (fun (c : Ast.rclause) ->
+              let ps =
+                List.map
+                  (fun (p : Ast.field) ->
+                     { p with Ast.fty = rename_texpr owned alias p.Ast.fty })
+                  c.Ast.rparams
+              in
+              let bound =
+                List.map (fun (p : Ast.field) -> p.Ast.fname) ps @ bound
+              in
+              { c with
+                Ast.rparams = ps;
+                rbody = List.map (rename_expr owned alias bound) c.Ast.rbody })
            clauses)
-    | Ast.InvokeRestart _ -> e.Ast.e
+    | Ast.InvokeRestart (n, args) -> Ast.InvokeRestart (n, gos args)
     (* 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) ->
@@ -336,8 +350,11 @@ let rec expr_uses acc (e : Ast.expr) =
   let go = expr_uses acc in
   let gos = List.iter go in
   match e.Ast.e with
-  | Ast.Int _ | Ast.Float _ | Ast.Byte _ | Ast.Str _ | Ast.Kw _ | Ast.Quote _
-  | Ast.InvokeRestart _ -> ()
+  | Ast.Int _ | Ast.Float _ | Ast.Byte _ | Ast.Str _ | Ast.Kw _ | Ast.Quote _ ->
+    ()
+  (* The name is not one an import can supply, but the arguments are ordinary
+     expressions and may well use one. *)
+  | Ast.InvokeRestart (_, args) -> gos args
   | Ast.Var n -> acc := (n, e.Ast.loc) :: !acc
   | Ast.Do body -> gos body
   | Ast.Let (bs, body) ->
@@ -365,7 +382,11 @@ let rec expr_uses acc (e : Ast.expr) =
   | Ast.Signal (_, c) -> go c
   | Ast.RestartCase (body, clauses) ->
     go body;
-    List.iter (fun (c : Ast.rclause) -> gos c.Ast.rbody) clauses
+    List.iter
+      (fun (c : Ast.rclause) ->
+         List.iter (fun (p : Ast.field) -> texpr_uses acc p.Ast.fty) c.Ast.rparams;
+         gos c.Ast.rbody)
+      clauses
   | Ast.HandlerBind (clauses, body) ->
     List.iter
       (fun (c : Ast.hclause) -> texpr_uses acc c.Ast.hty; gos c.Ast.hbody)
diff --git a/lib/parse.ml b/lib/parse.ml
index ef25878..8b708e3 100644
--- a/lib/parse.ml
+++ b/lib/parse.ml
@@ -256,47 +256,41 @@ 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. *)
+  (* (restart-case BODY (name [p T ...] BODY-1) ...) — spec-conditions.md §3.
+     The body and every clause have the same type, which is the form's. A
+     clause's parameters are inline name/type pairs, like any other binding
+     form; what fills them in is the [invoke-restart] that chose the clause. *)
   | 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 ...) ...)"
+        fail f "restart-case is (restart-case body (name [p T] 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 ...)"
+        { Ast.rname = n; rparams = fields c ps;
+          rbody = List.map expr cbody; rloc = c.Form.loc }
+      | _ -> fail c "a restart-case clause is (name [p T] 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. *)
+  (* (invoke-restart 'name arg ...) : 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. The arguments
+     fill in the clause's parameters, and how many there are and what they are
+     is settled at run time too, against the frame the name found (§3). *)
   | 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)"
+     | { v = Form.List [ { v = Form.Sym "quote"; _ }; { v = Form.Sym n; _ } ]; _ }
+       :: rest ->
+       mk (Ast.InvokeRestart (n, List.map expr rest))
      | _ ->
        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")
+         "invoke-restart takes a quoted restart name and then its arguments, \
+          as in (invoke-restart 'use-value 42)")
 
   (* ── macros ────────────────────────────────────────────────────── *)
   (* The reader now produces these three, so they arrive here as ordinary heads
diff --git a/lib/tast.ml b/lib/tast.ml
index 0e17f01..5b99033 100644
--- a/lib/tast.ml
+++ b/lib/tast.ml
@@ -81,9 +81,20 @@ and expr_kind =
      *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. *)
+     so nothing follows it.
+
+     [InvokeRestart]'s arguments are already evaluated: the checker binds each
+     to a slot and wraps the node in a [Let], so what is left here is a list of
+     locals to copy into the frame. Two reasons, and both matter. An argument
+     that transfers on its own must be guarded before this one aims the
+     channel; and a call written in an argument has to be on the walk [Reach]
+     and [Load] already do, which a list hanging off a node they treat as a
+     leaf would not be. [rsig] is the argument types as written, and [rsig_id]
+     their hash — §3's run-time check, since the name is resolved on a stack
+     nothing static can see. *)
   | RestartCase of rclause list * expr
-  | InvokeRestart of int * string * Loc.t   (* name id, name, where *)
+  (* name id, name, arguments, their spelling, its hash, where *)
+  | InvokeRestart of int * string * expr list * string * int * Loc.t
 
 (* [Serror] is §2's diverging variant: the same lookup, type Never, and with
    nothing transferring the program stops rather than carrying on. *)
@@ -102,8 +113,15 @@ 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 }
+   clause runs at the restart-case, which is where it was written.
+
+   [rparams] are the slots §3's parameters are bound to, in order, with their
+   types; the invoker stores into a buffer this frame owns and the clause loads
+   them from it. [rsig] is how those types are spelled and [rsig_id] its hash:
+   what the two ends compare, since neither can see the other. *)
+and rclause =
+  { rname_id : int; rname : string; rparams : (int * Types.t) list;
+    rsig : string; rsig_id : int; 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 }
diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c
index c649104..3b8fb33 100644
--- a/runtime/flan_rt.c
+++ b/runtime/flan_rt.c
@@ -398,6 +398,40 @@ _Noreturn void flan_restart_fail(const uint8_t *loc, int64_t loclen,
   rt_die();
 }
 
+/* The frame the name found does not take these arguments — spec-conditions.md
+ * §3's run-time check. It has to be at run time: a restart is resolved on a
+ * dynamic stack, so the invoke site cannot see what it will find, and the
+ * frame cannot see who will find it. What each end knows is its own parameter
+ * list, so the message is both of them side by side. */
+_Noreturn void flan_restart_args_fail(const uint8_t *loc, int64_t loclen,
+                                      const uint8_t *name, int64_t namelen,
+                                      const uint8_t *want, int64_t wantlen,
+                                      const uint8_t *got, int64_t gotlen) {
+  fflush(stdout);
+  fprintf(stderr, "%.*s: restart %.*s takes %.*s, given %.*s\n",
+          (int)loclen, (const char *)loc, (int)namelen, (const char *)name,
+          (int)wantlen, (const char *)want, (int)gotlen, (const char *)got);
+  rt_die();
+}
+
+/* A clause with parameters was reached by a transfer that filled none of them
+ * in. No [invoke-restart] can do that — it writes the arguments before it aims
+ * the channel — so this is the other way a transfer starts: the break loop,
+ * which today takes a restart by position and has no way to supply a value.
+ * Refused at the clause rather than run on a buffer nobody wrote. */
+_Noreturn void flan_restart_unarmed(const uint8_t *loc, int64_t loclen,
+                                    const uint8_t *name, int64_t namelen,
+                                    const uint8_t *want, int64_t wantlen) {
+  fflush(stdout);
+  fprintf(stderr,
+          "%.*s: restart %.*s takes %.*s, and whatever took it supplied no "
+          "arguments — a restart with parameters cannot be taken from the "
+          "break loop yet\n",
+          (int)loclen, (const char *)loc, (int)namelen, (const char *)name,
+          (int)wantlen, (const char *)want);
+  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
diff --git a/test/programs/restarts.flan b/test/programs/restarts.flan
index 1515e5b..d38baf2 100644
--- a/test/programs/restarts.flan
+++ b/test/programs/restarts.flan
@@ -3,7 +3,12 @@
 ;;;; 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.
+;;;;
+;;;; §3's parameters are here too, along with the run-time check they need: the
+;;;; supply-a-value half of the vocabulary, which is the half whose answer comes
+;;;; from outside the program. With no argument this program is the exit-0 case
+;;;; the table pins; with one it selects a mismatch, which traps and is asserted
+;;;; on its reason.
 (defstruct AssetMissing [id i32])
 
 (defvar log i64)
@@ -46,7 +51,53 @@
         0)
     (use-placeholder [] -2)))
 
-(defn main [] i32
+;;; Called from nowhere but inside an [invoke-restart]'s argument list.
+(defn half [x i32] i32 (/ x 2))
+
+;;; §3: a clause with parameters. The value comes from the handler, which is
+;;; the whole point — [use-value] and [store-value] are the two restarts whose
+;;; answer is not in the program. The parameters are slots of *this* function
+;;; and the invoker fills a buffer this frame owns, because by the time the
+;;; clause runs the invoking frame has gone (§5).
+(defn supplied [n i32] i32
+  (restart-case (middle n)
+    (use-value [v i32] (* v 2))
+    (use-pair  [a i32 b i32] (+ a b))
+    (retry     [] 7)))
+
+;;; Parameters of more than one type, and one that is not a machine word: a
+;;; string is ptr+len and crosses the transfer as the two of them.
+(defn labelled [n i32] i32
+  (restart-case (middle n)
+    (use-labelled [label string v i32]
+      (do (print label) (println "") v))))
+
+;;; The mismatch cases. Each is selected by the argument, because each stops
+;;; the program: what a restart takes is not knowable where it is invoked, so
+;;; §3 checks it at run time and this is what that check refuses.
+(defn mismatched [n i32] i32
+  (handler-bind [(AssetMissing [c] (invoke-restart 'use-value))]
+    (supplied n)))
+
+(defn mistyped [n i32] i32
+  (handler-bind [(AssetMissing [c] (invoke-restart 'use-value "forty-one"))]
+    (supplied n)))
+
+(defn overfull [n i32] i32
+  (handler-bind [(AssetMissing [c] (invoke-restart 'retry 1))]
+    (supplied n)))
+
+(defn main [args [string]] i32
+  ;; One argument selects a trap; none runs the table's case.
+  (if (> (len args) 1)
+    (let [k (i32 (bytes->i64 (bytes (at args 1))))]
+      (cond
+        (= k 1) (print (mismatched 90))
+        (= k 2) (print (mistyped 91))
+        (= k 3) (print (overfull 92))
+        :else (println "?"))
+      (return 0)))
+
   ;; Nothing handles it, so signal is a no-op and the body's own value stands.
   (print (fetch 1)) (println "")                          ; 101
   (print log) (println "")                                ; 1
@@ -77,4 +128,27 @@
   ;; the trap case in the acceptance table rather than a line here.
   (handler-bind [(AssetMissing [c] (invoke-restart 'use-placeholder))]
     (print (strict 6)) (println ""))                        ; -2
+
+  ;; §3: the handler supplies the value, and the clause computes with it —
+  ;; the arithmetic is in the clause so that a transfer which forgot to copy
+  ;; the argument could not pass by returning what it was given.
+  (handler-bind [(AssetMissing [c] (invoke-restart 'use-value 21))]
+    (print (supplied 7)) (println ""))                      ; 42
+  ;; Two parameters, so their order is pinned: 1 and 2 would sum the same
+  ;; whichever way round they landed.
+  (handler-bind [(AssetMissing [c] (invoke-restart 'use-pair 30 4))]
+    (print (supplied 8)) (println ""))                      ; 34
+  ;; A clause with no parameters is still reachable from a restart-case that
+  ;; has some, and an invoke with no arguments still matches it.
+  (handler-bind [(AssetMissing [c] (invoke-restart 'retry))]
+    (print (supplied 9)) (println ""))                      ; 7
+  ;; A string and an integer together: two different widths, and the string is
+  ;; ptr+len rather than a machine word.
+  (handler-bind [(AssetMissing [c] (invoke-restart 'use-labelled "supplied" 5))]
+    (print (labelled 10)) (println ""))                     ; supplied / 5
+  ;; The argument is an ordinary expression, evaluated where the invoke is —
+  ;; here a call, and [half] is reached from nowhere else, so a walk that did
+  ;; not look inside an invoke-restart would drop it and fail to link.
+  (handler-bind [(AssetMissing [c] (invoke-restart 'use-value (half 42)))]
+    (print (supplied 12)) (println ""))                     ; 21 * 2
   0)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 05b46a2..eac002a 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -256,11 +256,100 @@ let () =
        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-2\n" in
+       and as a dev build, where every one of those calls goes through a cell.
+
+       Then §3's parameters: one, two of them in an order a sum would not pin,
+       a string beside an integer, a clause taking none in the same form as
+       clauses taking some, and an argument that is a call to a function
+       reached from nowhere else. The last one is the reachability claim — an
+       invoke-restart whose arguments were not walked would drop [half] and
+       fail to link, which is why the arguments are evaluated into slots before
+       the node rather than hanging off it. *)
+    let restarts_out =
+      "101\n1\n-1\n2\n7\n1010\n101\n105\n-2\n42\n34\n7\nsupplied\n5\n42\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;
+    (* §3's run-time check, which is the price of a restart being found by name
+       on a dynamic stack: neither end of an invoke can see the other, so what
+       a clause takes against what was given is settled where the transfer
+       starts. Each of these stops the program, so each is asserted on its
+       reason rather than on the exit status alone — too few arguments, the
+       right count of the wrong type, and arguments handed to a clause that
+       takes none. *)
+    let restart_mismatch ?opt () =
+      let exe = compile ?opt "programs/restarts.flan" in
+      let refuses name arg reason =
+        let code, text = run exe (Some arg) in
+        if code <> 134
+           || not (contains text "programs/restarts.flan:")
+           || not (contains text reason)
+        then begin
+          incr failures;
+          Printf.printf
+            "FAIL  %s\n        got: %S (exit %d)\n     wanted: %S (exit 134)\n"
+            name text code reason
+        end
+      in
+      refuses "a restart invoked with too few arguments" "1"
+        "restart use-value takes (i32), given ()";
+      refuses "a restart invoked with the wrong type" "2"
+        "restart use-value takes (i32), given (string)";
+      refuses "arguments given to a restart that takes none" "3"
+        "restart retry takes (), given (i32)";
+      (try Sys.remove exe with Sys_error _ -> ())
+    in
+    restart_mismatch ();
+    restart_mismatch ~opt:"-O0" ();
+    (* The other way a transfer starts is the break loop, which chooses a
+       restart by position and has nothing to fill parameters in with. It
+       reaches the clause through the same channel an invoke-restart writes, so
+       nothing downstream could tell the two apart — except that the clause's
+       buffer is still the zero the frame was pushed with. Asserted on the IR,
+       because driving it needs a stopped program and a socket, and what is
+       being claimed is that the guard exists at all. *)
+    let p =
+      Reader.read_file "programs/restarts.flan" |> Parse.program |> Check.program
+    in
+    if not (contains (Emit.program p) "call void @flan_restart_unarmed(") then begin
+      incr failures;
+      print_endline
+        "FAIL  a clause with parameters has no guard against being taken \
+         without any"
+    end;
+    (* What is refused before anything runs, and why. Not everything about a
+       restart's arguments waits for run time: the shape of the form and
+       whether an argument is a value at all are here, and each is asserted on
+       its reason. *)
+    let refuses_src name src needle =
+      match Check.program (Parse.program (Reader.read_all ~file:"<restarts>" src)) with
+      | _ ->
+        incr failures;
+        Printf.printf "FAIL  %s\n        it was accepted\n" name
+      | exception Loc.Error (_, m) ->
+        if not (contains m needle) then begin
+          incr failures;
+          Printf.printf "FAIL  %s\n        said: %S\n     wanted: %S in it\n"
+            name m needle
+        end
+    in
+    (* The name is still a quoted symbol, and now it is the *first* of several
+       things, so an unquoted one has to say what the form is rather than read
+       as a call with a spare argument. *)
+    refuses_src "invoke-restart without a quoted name"
+      "(defn main [] i32 (invoke-restart use-value 1) 0)"
+      "a quoted restart name and then its arguments";
+    (* A clause parameter is a binding, so it needs something to hold. *)
+    refuses_src "a restart parameter that is not a value"
+      "(defn main [] i32 (restart-case 0 (use-value [v Unit] 1)))"
+      "which is not a value";
+    (* And so does an argument: a [println] is Unit, and there would be nothing
+       to store into the clause's buffer. *)
+    refuses_src "a restart argument that is not a value"
+      "(defn main [] i32 (restart-case 0 (use-value [v i32] v))\n\
+      \  (invoke-restart 'use-value (println \"\")) 0)"
+      "a restart argument must be a value";
     (* §2's other half, which cannot be an [outputs] case because it does not
        exit 0: a handler runs, returns normally, and has still not answered the
        error, so the program stops and names the condition. *)
@@ -1512,10 +1601,11 @@ ERR@7 unexpected token: not the kind the caller was reading
          (defn fetch [n i32] i32\n\
         \  (restart-case\n\
         \    (do (error (Missing {:id n})) 0)\n\
+        \    (use-value [v i32  s string] (do (print s) v))\n\
         \    (use-placeholder [] -1)))\n\
          (defn run [] i32\n\
         \  (defer (set seen (+ seen 1)))\n\
-        \  (handler-bind [(Missing [m] (invoke-restart 'use-placeholder))]\n\
+        \  (handler-bind [(Missing [m] (invoke-restart 'use-value 4 \"\"))]\n\
         \    (fetch 3)))\n\
          (defn main [] i32\n\
         \  (set (at arr 2) 9)\n\
diff --git a/test/test_flan.ml b/test/test_flan.ml
index ff84835..be11e1e 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -811,17 +811,22 @@ let () =
   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";
+  (* §3's parameters. A clause binds them like a function's, so the body sees
+     them and nothing outside does; what they are is checked against the
+     invoke at run time, because the two ends meet on a dynamic stack. *)
+  accepts "a restart with parameters"
+    "(defn f [] i32 (restart-case 1 (skip [n i32] n)))";
+  accepts "invoke-restart with arguments"
+    "(defn f [] (invoke-restart 'skip 1))";
+  rejects_check "a restart parameter outside its clause"
+    "(defn f [] i32 (+ (restart-case 1 (skip [n i32] n)) n))"
+    ~needle:"unknown name n";
+  rejects_check "a restart argument that is not a value"
+    "(defn f [] (invoke-restart 'skip (println \"\")))"
+    ~needle:"a restart argument must be a value";
   rejects_check "invoke-restart on an unquoted name"
     "(defn f [] (invoke-restart skip))"
-    ~needle:"quoted restart name";
+    ~needle:"a quoted restart name and then its arguments";
   (* §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"