diff --git a/FIX.org b/FIX.org
index 21105ed..7d1b2c0 100644
--- a/FIX.org
+++ b/FIX.org
@@ -520,6 +520,31 @@ answers the same question at a fraction of the wall clock. The consequence to
 accept is that a lane is reviewed on its code rather than on sweep numbers it
 no longer produces, which is what the review before a merge is for.
 
+* handler-case, decided 2026-09-19
+Built, both backends, and it needed no backend work at all: it is a
+handler-bind whose clause invokes a restart the form established around
+itself, which is spec-conditions.md's one open question about the operator
+answered in the affirmative. The shape is (handler-case BODY [(T [c] ...)]),
+body first and clauses after, the opposite of handler-bind's order because a
+handler-bind reads as something put around a body and this one reads as a body
+with answers hung off it.
+
+Everything the unwinding form needs it inherits. Defers and the
+with-allocator restore run on the way out because a transfer already runs them
+for every frame it leaves. The body and every clause agree on one type because
+§3 already says a restart-case's do, and a clause that disagrees is refused
+with the same message an if with disagreeing arms gets. A condition no clause
+lists installs no matching frame and carries on outward untouched. A clause
+runs at the form, so it sees the establishing function's locals, which a
+handler-bind clause cannot — that is the whole difference, and it falls out of
+where a restart clause runs rather than being arranged for.
+
+The one wart, noted and left: the restart the form makes up for itself is on
+the restart stack like any other, so a break loop entered underneath one lists
+it. Choosing it there is refused loudly rather than answered wrongly, and
+hiding it would mean a new field in a frame layout written out in emit.ml, in
+x86.ml and in flan_rt.c.
+
 * Surface syntax discussion, 2026-09-19
 The author wants an F#-ish indentation-based ML surface living side by side
 with s-expressions, not replacing them. The languages that disappear for the
diff --git a/docs/PORTING.md b/docs/PORTING.md
index f4f643a..d47f29d 100644
--- a/docs/PORTING.md
+++ b/docs/PORTING.md
@@ -186,10 +186,23 @@ Neither implementation returns errors as values. Both use the host's exception o
 condition system throughout. Porting this game exercises `signal`/`error`/`restart-case`
 and never wants a `Result`.
 
-### `handler-case` — one site, and `handler-bind` already covers it
+### `handler-case` — one site, and it is now the natural spelling of it
 
-`engine.clj`'s `reload-config!` is `(try … (catch Exception e (println e)))`. That is
-"log it and carry on", which is what a `handler-bind` clause returning normally does.
+`engine.clj`'s `reload-config!` is `(try … (catch Exception e (println e)))`. The ranking
+below was written when the operator did not exist, and said `handler-bind` covers it,
+which it does: "log it and carry on" is what a clause returning normally does. It is no
+longer the closer translation. `handler-case` landed on 2026-09-19 and is Clojure's
+try/catch by construction, so that site ports across as itself:
+
+```
+(handler-case (read-config path)
+  [(FileError [c] (do (println (.path c)) default-config))])
+```
+
+The difference that decides it is not spelling. A `handler-bind` clause is lifted into a
+function of its own and cannot see `reload-config!`'s locals; a `handler-case` clause runs
+at the form and can, which is what a catch block is assumed to do everywhere it is
+written.
 
 ### `Handle` and pools — nothing to pool
 
@@ -642,9 +655,11 @@ not compete for the same slot.
 
 **Not ranked, because this game does not need them:** escaping closures and capture (one
 site, fixed by one parameter), `Handle` and pools (nothing to pool), `Result`/`try`
-(neither host uses that discipline), `handler-case` (one site, `handler-bind` covers it),
-`loop`/`recur` and tail calls (nothing recurses), user-written allocators, structural
-typing.
+(neither host uses that discipline), `loop`/`recur` and tail calls (nothing recurses),
+user-written allocators, structural typing. `handler-case` was on this list for the same
+reason and has since been built anyway — it cost one function in the checker and nothing
+in either backend, being a `handler-bind` whose clause invokes a restart the form
+established around itself.
 
 ---
 
diff --git a/emacs/flan-mode.el b/emacs/flan-mode.el
index c1c8d3d..00905c7 100644
--- a/emacs/flan-mode.el
+++ b/emacs/flan-mode.el
@@ -292,6 +292,10 @@ line is off screen."
     ("dotimes" . 1)
     ;; The clause vector, then the protected body.  Same shape as `let'.
     ("handler-bind" . 1)
+    ;; `handler-case' is the other way round — the body first and the clause
+    ;; vector after it — but the entry is the same number, because what it
+    ;; says is that one argument is special and the rest indent as a body,
+    ;; and that is true of both orders.
     ("handler-case" . 1)
     ;; Test first, body after.
     ("if" . 1)
diff --git a/lib/ast.ml b/lib/ast.ml
index 63e6fa1..80c50c5 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -86,6 +86,13 @@ and expr_kind =
   (* (handler-bind [(Type [c] body ...) ...] body ...) — spec-conditions.md.
      A clause binds a name for the condition, so this cannot be a call. *)
   | HandlerBind of hclause list * expr list
+  (* (handler-case BODY [(Type [c] body ...) ...]) — the other half of
+     spec-conditions.md's pair. Where a handler-bind clause runs at the signal
+     with the stack below it intact, a handler-case clause runs *here*, after
+     that stack has gone, and its value is the value of the whole form. The
+     clauses share [hclause] with handler-bind because the syntax is the same
+     one; what differs is entirely where the body runs. *)
+  | HandlerCase of expr * hclause list
   | Signal  of sigkind * expr                 (* (signal c) / (error c)        *)
   (* (restart-case body (name [p T] body ...) ...) and
      (invoke-restart 'name arg ...). Both alter control flow, so neither can be
@@ -271,6 +278,7 @@ let map_children f (e : expr) : expr =
     | Defer es -> Defer (List.map ex es)
     | Unwrap (u, x) -> Unwrap (u, ex x)
     | HandlerBind (cs, es) -> HandlerBind (List.map hcl cs, List.map ex es)
+    | HandlerCase (b, cs) -> HandlerCase (ex b, List.map hcl cs)
     | Signal (k, x) -> Signal (k, ex x)
     | RestartCase (b, cs) -> RestartCase (ex b, List.map rcl cs)
     | InvokeRestart (n, args) -> InvokeRestart (n, List.map ex args)
diff --git a/lib/check.ml b/lib/check.ml
index 46fe24a..adfb863 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -2059,6 +2059,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
     expect loc ~want (mk loc ty (Tast.Signal (kind, type_id name, c)))
 
   | Ast.HandlerBind (clauses, body) -> check_handler_bind ctx ?want loc clauses body
+  | Ast.HandlerCase (body, clauses) -> check_handler_case ctx ?want loc body clauses
 
   (* 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
@@ -2404,9 +2405,15 @@ and check_fn ctx ~want loc (params : string list) body =
    The body may not [return] either. The frames are pushed and popped around
    it, and an early exit would leave them on the stack pointing into a function
    that has gone. *)
-and check_handler_bind ctx ?want loc clauses body =
+and check_handler_bind ctx ?want ?(what = "handler-bind") loc clauses body =
   let frames =
-    List.map
+    (* Left to right, and not [List.map], whose order is unspecified: each of
+       these calls lifts a function onto [ctx.env.lifted] and names it after
+       the count already there, so an order nobody chose would number the
+       clauses of one handler-bind differently between builds. The names go in
+       a redefinition module, which is where that would be noticed — see the
+       argument in [check_fn]. *)
+    map_lr
       (fun (c : Ast.hclause) ->
          let ty = resolve ctx.env c.Ast.hty in
          let name =
@@ -2471,16 +2478,20 @@ and check_handler_bind ctx ?want loc clauses body =
      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";
+  (* [what] is the form the reader wrote. A handler-case establishes its
+     frames through this function, so a [return] under one has to be refused
+     naming handler-case rather than naming the machinery underneath it. *)
+  ctx.in_frames <- Some what;
   (* The body's last form is the form's value, which is [with-allocator]'s
      shape and for the same reason: both wrap a body in something established
      around it and taken off after, and neither is a reason for the body to
      stop being an expression. §3 needs it — a [restart-case] whose body is a
      [handler-bind] has to agree in type with its clauses, which is how all
      four of this repository's crossing probes are written — and it is what
-     [handler-case] will *not* be: that one's value is the handler's, which is
-     the whole difference between the two and is why it is still refused by
-     name in [parse.ml].
+     [handler-case] is *not*: that one's value is its clause's, which is the
+     whole difference between the two. [check_handler_case] below builds one
+     out of this form and a [restart-case], so both spellings run through
+     here and only the clause's landing place differs.
 
      This used to be [ignore want] and a flat [Types.Unit], and nothing
      complained, because a unit in value position is only caught where the
@@ -2489,7 +2500,7 @@ and check_handler_bind ctx ?want loc clauses body =
      machine whatever the body's last form had left in the slot. Neither was a
      value; one of them merely looked like one. *)
   let body, ty =
-    barrier ctx "a handler-bind" (fun () ->
+    barrier ctx ("a " ^ what) (fun () ->
       let rec go = function
         | [] -> [ unit_at loc ], Types.Unit
         | [ last ] -> let l = check ctx ?want last in [ l ], l.Tast.ty
@@ -2520,6 +2531,13 @@ and check_restart_case ctx ?want loc body clauses =
   ctx.in_frames <- Some "restart-case";
   let tbody = barrier ctx "a restart-case" (fun () -> check ctx ?want body) in
   ctx.in_frames <- saved;
+  restart_clauses ctx ?want ~what:"restart-case" loc tbody clauses
+
+(* The clauses of a [restart-case], checked against a body that has already
+   been checked. Separate from the form above because [handler-case] supplies
+   its own body — a [handler-bind] it built — and has to name itself in the
+   refusals rather than naming the machinery it is made of. *)
+and restart_clauses ctx ?want ~what loc (tbody : Tast.expr) clauses =
   (* 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. *)
@@ -2537,7 +2555,7 @@ and check_restart_case ctx ?want loc body clauses =
             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;
+           fail c.Ast.rloc "this %s offers %s twice" what c.Ast.rname;
          seen := c.Ast.rname :: !seen;
          (* §3's parameters. They are slots in *this* function — a clause runs
             here, not where the invoke was — and the invoker stores into a
@@ -2567,7 +2585,7 @@ and check_restart_case ctx ?want loc body clauses =
               (* The same barrier the body gets, and for the same reason: a
                  clause runs after a transfer landed at this restart-case, with
                  its frames still to be popped. *)
-              barrier ctx "a restart-case"
+              barrier ctx ("a " ^ what)
                 (fun () -> 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;
@@ -2579,6 +2597,119 @@ and check_restart_case ctx ?want loc body clauses =
   let ty = match !ty with Some t -> t | None -> Types.Never in
   mk loc ty (Tast.RestartCase (clauses, tbody))
 
+(* (handler-case BODY [(Type [c] BODY-1) ...]) — the unwinding handler, and
+   spec-conditions.md's one remaining open question about it, answered: it *is*
+   a handler-bind plus a transfer, built here rather than given nodes and
+   backends of its own.
+
+       (handler-case B [(T [c] A)])
+    == (restart-case (handler-bind [(T [c] (invoke-restart 'R c))] B)
+         (R [c T] A))
+
+   That is Common Lisp's own definition of the operator, and every property
+   this form is supposed to have falls out of the two it is made of rather
+   than being re-implemented beside them.
+
+   - The clause runs *here*, at the handler-case, because a restart clause
+     does; so it sees this function's locals, which a handler clause cannot,
+     and its value is the whole form's, because a restart-case's clause value
+     is the whole restart-case's.
+   - The stack below is gone by then. §5's defers, and the allocator a
+     [with-allocator] rebound, are honoured on the way out because that is
+     what a transfer already does for every frame it leaves.
+   - A condition matching no clause installs no frame, so nothing here sees
+     it and it keeps going outward exactly as it would have.
+   - The body and every clause agree on one type, because §3 already says a
+     restart-case's body and clauses do. A clause that disagrees is refused
+     where it is written, like an [if] whose arms disagree.
+
+   The condition crosses as a restart argument, which means by value into a
+   buffer this frame owns — which is the only thing that can work, since §5
+   kills the signalling frame the condition was living on the moment the
+   transfer starts.
+
+   The restart the two halves meet over is named after this function and
+   numbered within it, and the number is the count of handler clauses already
+   lifted out of this function. That count never goes down, and every
+   handler-case lifts at least one clause before the next one can read it, so
+   within a name's own bucket the numbers are strictly increasing and no two
+   forms can mint the same name. A clause body written inside another handler
+   clause counts against the [<none>] bucket rather than against a function's,
+   which is the same argument again and not a hole: that bucket is one list
+   for the whole program and it only grows.
+
+   Uniqueness is the requirement rather than a nicety. Two handler-cases
+   sharing a name, one inside the other's extent, would have the inner frame
+   shadow the outer one (§4), which lands a condition at the wrong form —
+   and, because the two would be expecting different condition types, lands it
+   as a run-time signature refusal rather than as a wrong answer. *)
+and check_handler_case ctx ?want loc body clauses =
+  let what = "handler-case" in
+  (* Resolved once here, for the refusal below; [check_handler_bind] resolves
+     them again for the frames, which is cheap and keeps that function whole. *)
+  let names =
+    List.map
+      (fun (c : Ast.hclause) ->
+         match resolve ctx.env c.Ast.hty with
+         | Types.Named n -> n
+         | t ->
+           fail c.Ast.hloc
+             "a handler matches a struct type, not %s" (Types.to_string t))
+      clauses
+  in
+  (* Two clauses for one condition type: the first would take every one of
+     them and the second could never run, and nothing in the source says which
+     the reader meant. The same refusal a duplicate restart name gets, and for
+     the same reason. *)
+  let seen = ref [] in
+  List.iter2
+    (fun (c : Ast.hclause) n ->
+       if List.mem n !seen then
+         fail c.Ast.hloc "this handler-case handles %s twice" n;
+       seen := n :: !seen)
+    clauses names;
+  let k =
+    List.length
+      (List.filter
+         (fun (l : Tast.fn) ->
+            l.Tast.fparent = Some ctx.owner
+            && String.length l.Tast.name >= 8
+            && String.sub l.Tast.name 0 8 = "handler/")
+         ctx.env.lifted)
+  in
+  let rnames =
+    List.map (Printf.sprintf "handler-case/%s/%d/%s" ctx.owner k) names
+  in
+  (* The handler half: one clause per arm, whose whole body is the transfer.
+     It is lifted into a function of its own like any handler clause, and the
+     condition it was handed is copied into the restart frame's buffer on its
+     way out. *)
+  let handlers =
+    List.map2
+      (fun (c : Ast.hclause) r ->
+         { c with
+           Ast.hbody =
+             [ { Ast.e =
+                   Ast.InvokeRestart
+                     (r, [ { Ast.e = Ast.Var c.Ast.hname; loc = c.Ast.hloc } ]);
+                 loc = c.Ast.hloc } ] })
+      clauses rnames
+  in
+  (* The landing half: one restart clause per arm, taking the condition as its
+     single parameter and running what the reader actually wrote. *)
+  let landings =
+    List.map2
+      (fun (c : Ast.hclause) r ->
+         { Ast.rname = r;
+           rparams =
+             [ { Ast.fname = c.Ast.hname; fty = c.Ast.hty;
+                 floc = c.Ast.hloc } ];
+           rbody = c.Ast.hbody; rloc = c.Ast.hloc })
+      clauses rnames
+  in
+  let tbody = check_handler_bind ctx ?want ~what loc handlers [ body ] in
+  restart_clauses ctx ?want ~what loc tbody landings
+
 (* The forms of a [defer], checked in place and hung on the function. It emits
    nothing where it stands, so what is left behind is [unit]. *)
 and register_defer ctx loc forms =
diff --git a/lib/load.ml b/lib/load.ml
index c6c88ce..7766635 100644
--- a/lib/load.ml
+++ b/lib/load.ml
@@ -316,6 +316,19 @@ let rec rename_expr owned alias bound (e : Ast.expr) : Ast.expr =
                     c.Ast.hbody })
            clauses,
          gos body)
+    (* The same clause shape, and the same rewrite — the difference between the
+       two forms is where a clause runs, which an import does not see. *)
+    | Ast.HandlerCase (body, clauses) ->
+      Ast.HandlerCase
+        (go body,
+         List.map
+           (fun (c : Ast.hclause) ->
+              { c with
+                Ast.hty = rename_texpr owned alias c.Ast.hty;
+                hbody =
+                  List.map (rename_expr owned alias (c.Ast.hname :: bound))
+                    c.Ast.hbody })
+           clauses)
   in
   { e with Ast.e = k }
 
@@ -680,6 +693,11 @@ let rec expr_uses acc (e : Ast.expr) =
       (fun (c : Ast.hclause) -> texpr_uses acc c.Ast.hty; gos c.Ast.hbody)
       clauses;
     gos body
+  | Ast.HandlerCase (body, clauses) ->
+    go body;
+    List.iter
+      (fun (c : Ast.hclause) -> texpr_uses acc c.Ast.hty; gos c.Ast.hbody)
+      clauses
 
 (* A place carries no location of its own, so it borrows the [set] form's. *)
 and place_uses acc loc (p : Ast.place) =
diff --git a/lib/parse.ml b/lib/parse.ml
index 5ab0133..68b6aa3 100644
--- a/lib/parse.ml
+++ b/lib/parse.ml
@@ -420,6 +420,35 @@ and form f mk (head : Form.t) (args : Form.t list) : Ast.expr =
     in
     mk (Ast.HandlerBind (List.map clause clauses, body_of body))
 
+  (* (handler-case BODY [(Type [c] body ...) ...]) — spec-conditions.md, the
+     unwinding half of the pair.
+
+     The body comes first and the clauses after it, which is the opposite of
+     handler-bind's order and is deliberate: a handler-bind is read as
+     something established *around* a body, and a handler-case is read as a
+     body with answers hung off the end of it. A clause is spelled exactly as
+     handler-bind spells one, because it names the same thing — a condition
+     type and a name to bind it to. At least one clause, since a handler-case
+     with none would be its body and nothing else. *)
+  | Sym "handler-case" ->
+    let body, clauses =
+      match args with
+      | [ body; { v = Vec clauses; _ } ] when clauses <> [] -> (body, clauses)
+      | _ ->
+        fail f
+          "handler-case is (handler-case body [(Type [name] body ...) ...]) \
+           with at least one clause"
+    in
+    let clause (c : Form.t) =
+      match c.Form.v with
+      | Form.List (ty :: { v = Form.Vec [ { v = Form.Sym n; _ } ]; _ } :: cbody)
+        when cbody <> [] ->
+        { Ast.hty = texpr ty; hname = n; hbody = List.map expr cbody;
+          hloc = c.Form.loc }
+      | _ -> fail c "a handler-case clause is (Type [name] body ...)"
+    in
+    mk (Ast.HandlerCase (expr body, List.map clause clauses))
+
   (* (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
@@ -499,12 +528,9 @@ and form f mk (head : Form.t) (args : Form.t list) : Ast.expr =
 
   (* Recognised, deliberately unimplemented. Rejected rather than left to fall
      through to Call, where they would parse and mean nothing. *)
-  | Sym ("handler-case"
-        (* Named in the spec and not written yet, so each says so rather than
-           falling through to Call and coming back as an unknown name:
-           [find-restart] and [compute-restarts] are §4's two ways to look at
-           the restart stack without committing to one. *)
-        | "find-restart" | "compute-restarts"
+  (* [find-restart] and [compute-restarts] are §4's two ways to look at the
+     restart stack without committing to one. *)
+  | Sym ("find-restart" | "compute-restarts"
         | "errdefer"
         | "await" as name) ->
     fail f "%s is not implemented yet (see the build sequence in plan.org)" name
diff --git a/lib/tast.ml b/lib/tast.ml
index 5b996d7..679aaa6 100644
--- a/lib/tast.ml
+++ b/lib/tast.ml
@@ -179,7 +179,14 @@ and expr_kind =
      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. *)
+     nothing static can see.
+
+     Not every one of these was written as a [restart-case]. A [handler-case]
+     is a [Handled] whose clause invokes a restart, wrapped in one of these to
+     catch it — see [Check.check_handler_case] — so the unwinding handler
+     reaches a backend as this node and needs nothing of its own. A clause
+     whose name begins with [handler-case/] is one the checker made up for
+     that. *)
   | RestartCase of rclause list * expr
   (* (with-allocator A BODY...) — spec-memory.md. It rebinds the current
      allocator for its dynamic extent and releases nothing. Its own node
diff --git a/spec-conditions.md b/spec-conditions.md
index 8b0e45a..e923d9b 100644
--- a/spec-conditions.md
+++ b/spec-conditions.md
@@ -219,6 +219,34 @@ per-frame slot nests correctly with no threads involved.
 
 ## What this does not settle
 
-Condition inheritance/predicate-matching details, the break-loop UI, restart
-interaction with threads, and whether `handler-case` should be a macro over
-`handler-bind` + a transfer. None of these block milestone 5.
+Condition inheritance/predicate-matching details, the break-loop UI, and restart
+interaction with threads. None of these block milestone 5.
+
+`handler-case` **is** a `handler-bind` plus a transfer, decided 2026-09-19 and
+built that way. `(handler-case B [(T [c] A)])` is
+
+```
+(restart-case (handler-bind [(T [c] (invoke-restart 'R c))] B)
+  (R [c T] A))
+```
+
+with `R` a name the form makes up for itself, which is Common Lisp's own
+definition of the operator. Everything the unwinding form needs it inherits
+rather than re-implements: §5's defers and the `with-allocator` restore,
+because a transfer already runs both for every frame it leaves; §3's rule that
+the body and every clause share one type; §4's shadowing, which is why the name
+has to be unique per form; and both backends, which needed no new node. The
+clause runs at the `handler-case` and therefore sees the establishing
+function's locals, which a `handler-bind` clause cannot — that is the whole of
+the difference between the two, and it is a consequence of where a restart
+clause runs rather than something arranged for it.
+
+The condition crosses as the restart's single argument, which means by value
+into a buffer the form owns. §5 requires it: the signalling frame the condition
+was living on dies the moment the transfer starts.
+
+The visible cost is that the made-up restart is on the restart stack like any
+other, so a break loop entered under a `handler-case` lists it. Taking it from
+there is refused loudly — nothing filled its argument buffer in — rather than
+answered wrongly, and hiding it would mean a field in a frame layout spelled
+out in three places. Left as it is.
diff --git a/test/programs/handler-case.flan b/test/programs/handler-case.flan
new file mode 100644
index 0000000..b469b99
--- /dev/null
+++ b/test/programs/handler-case.flan
@@ -0,0 +1,231 @@
+;;;; handler-case — the unwinding handler, spec-conditions.md.
+;;;;
+;;;; handler-bind runs its clause at the signal, with everything below still
+;;;; standing, and carries on from there. This one is the other half: a listed
+;;;; condition unwinds the stack back to the form, the clause runs *here*, and
+;;;; its value is the value of the whole handler-case. Clojure's try/catch and
+;;;; Common Lisp's handler-case, and built out of the two operators that were
+;;;; already here — a handler-bind whose clause invokes a restart the form
+;;;; established around itself.
+;;;;
+;;;; What this program pins is the list of things that only an unwind can get
+;;;; wrong: the defers between the signal and the form, a condition nobody
+;;;; listed carrying on outward untouched, the two nestings against
+;;;; handler-bind, and a clause that signals — which must not be caught by the
+;;;; handler-case it belongs to, because by the time it runs that form's frames
+;;;; are off the stack.
+;;;;
+;;;; [log] is a digit trace rather than a running sum, which is cleanup.flan's
+;;;; device and is here for cleanup.flan's reason: a sum commutes, so a backend
+;;;; that ran the defers outermost-first would print exactly the same total as
+;;;; one that got them right. A shift records the *order* and a wrong order is
+;;;; a different number.
+(defstruct Missing [id i32])
+(defstruct Corrupt [id i32])
+(defstruct Late    [id i32])
+
+(defvar log i64)
+(defvar frame Allocator)
+
+(defn note [n i64] () (set log (+ (* log 10) n)))
+
+;;; Two frames below any handler-case here, each with a defer, so an unwind has
+;;; something to cross and leaves a mark saying it crossed it — and says in
+;;; which order it crossed them (§5: innermost first).
+(defn inner [n i32] i32
+  (defer (note 1))
+  (error (Missing {.id n}))
+  0)
+
+(defn middle [n i32] i32
+  (defer (note 2))
+  (+ (inner n) 1))
+
+;;; Nothing signals: the body's own value stands, which is the case a form that
+;;; only ever answers its clauses would quietly get wrong.
+(defn quiet [n i32] i32
+  (handler-case (+ n 1)
+    [(Missing [c] -1)]))
+
+;;; Caught, and the clause reads a local of the function that established the
+;;; form. That is the whole difference from handler-bind, whose clause is
+;;; lifted into a function of its own and can see no such thing.
+(defn caught [n i32] i32
+  (let [bonus 100]
+    (handler-case (middle n)
+      [(Missing [c] (+ bonus (.id c)))])))
+
+;;; Two clauses, and the one whose type was signalled is the one that runs.
+(defn raise [k i32] i32
+  (cond
+    (= k 0) (error (Missing {.id 1}))
+    (= k 1) (error (Corrupt {.id 2}))
+    :else   (error (Late    {.id 3}))))
+
+(defn two [k i32] i32
+  (handler-case (raise k)
+    [(Missing [c] (+ 100 (.id c)))
+     (Corrupt [c] (+ 200 (.id c)))]))
+
+;;; A condition no clause lists installs no frame that matches it, so this form
+;;; never sees it and it goes on outward unchanged. The outer handler-bind is
+;;; what proves it arrived, and the 7 is what proves signal still returned ()
+;;; and the body carried on from where it was.
+(defn unmatched [n i32] i32
+  (handler-case
+    (do (signal (Corrupt {.id n}))
+        7)
+    [(Missing [c] -1)]))
+
+;;; A handler-case inside a handler-bind. The Corrupt goes out to the
+;;; handler-bind, which returns normally, so the body carries on; the Missing
+;;; that follows unwinds to the handler-case in between.
+(defn hc-in-hb [n i32] i32
+  (handler-bind [(Corrupt [c] (note 4))]
+    (handler-case
+      (do (signal (Corrupt {.id n}))
+          (error (Missing {.id n}))
+          0)
+      [(Missing [c] (.id c))])))
+
+;;; And the other way round. The inner handler-bind is on the path the unwind
+;;; takes, so its frame has to come off as the transfer passes through it —
+;;; which is the same landing pad a restart transfer already uses.
+(defn hb-in-hc [n i32] i32
+  (handler-case
+    (handler-bind [(Corrupt [c] (note 5))]
+      (do (signal (Corrupt {.id n}))
+          (error (Missing {.id n}))
+          0))
+    [(Missing [c] (* 2 (.id c)))]))
+
+;;; A clause that signals. It runs with its own handler-case's frames already
+;;; off the stack, so this Missing must not be caught here — that would be an
+;;; unbounded loop rather than a wrong number. It has to leave this function,
+;;; running the defer below on the way, and land further out.
+(defn arm-signals [n i32] i32
+  (defer (note 3))
+  (handler-case (middle n)
+    [(Missing [c] (do (signal (Missing {.id 99}))
+                      (.id c)))]))
+
+(defn arm-caught-outside [n i32] i32
+  (handler-case (arm-signals n)
+    [(Missing [c] (+ 5000 (.id c)))]))
+
+;;; A clause that returns. A clause runs at the form, in the function that
+;;; wrote it, so a [return] there is an ordinary return from *this* function —
+;;; not the refusal the body gets, where the frames are still standing. It has
+;;; to run this function's own defer on the way out, after the two the unwind
+;;; already ran, and it has to leave nothing on the handler stack: main signals
+;;; once more afterwards with nothing listening, which would be a call into a
+;;; frame that has gone if anything leaked.
+(defn return-from-clause [n i32] i32
+  (defer (note 9))
+  (handler-case (middle n)
+    [(Missing [c] (return (+ 700 (.id c))))])
+  0)
+
+;;; A handler-case inside a defer. A defer is itself the cleanup an unwind
+;;; runs, so establishing frames in one has to work like establishing them
+;;; anywhere — what a defer may not do is start a transfer that leaves it, and
+;;; this one begins and ends inside. Two defers, so the order is pinned here
+;;; too: the handler-case one is innermost and notes first.
+(defn hc-in-defer [n i32] i32
+  (defer (note 8))
+  (defer (note (i64 (handler-case (error (Corrupt {.id n}))
+                      [(Corrupt [d] (.id d))]))))
+  n)
+
+;;; Two handler-cases written inside handler-bind clauses. Such a clause is
+;;; lifted into a function of its own, so both of these mint their made-up
+;;; restart name out of one shared bucket rather than out of a function's —
+;;; which is exactly where two forms landing on the same name would show, the
+;;; inner shadowing the outer wherever their extents overlapped. Each notes the
+;;; id of the condition *it* caught, so the trace says they are two names.
+(defn in-clause-a [] ()
+  (handler-bind
+    [(Late [c]
+       (note (i64 (handler-case (error (Corrupt {.id 6}))
+                    [(Corrupt [d] (.id d))]))))]
+    (signal (Late {.id 0}))))
+
+(defn in-clause-b [] ()
+  (handler-bind
+    [(Late [c]
+       (note (i64 (handler-case (error (Corrupt {.id 7}))
+                    [(Corrupt [d] (.id d))]))))]
+    (signal (Late {.id 0}))))
+
+;;; A with-allocator on the way out. It rebinds the context allocator for its
+;;; extent and the transfer passes straight through it, so the restore has to
+;;; happen on that path as well as on the normal one — otherwise the clause,
+;;; and everything after the whole form, would be allocating out of a region
+;;; nobody else knows about. main destroys the arena before it allocates
+;;; again, so a context left pointing at it would not be a wrong number.
+(defn scoped [n i32] i32
+  (handler-case
+    (with-allocator frame
+      (let [v (vec-new i32)]
+        (push v 1)
+        (error (Missing {.id n}))
+        (i32 (len v))))
+    [(Missing [c] (+ 20 (.id c)))]))
+
+(defn main [] i32
+  ;; Normal completion.
+  (print (quiet 41)) (println "")
+  (print log) (println "")
+
+  ;; Caught, with both defers between the signal and the form having run, and
+  ;; the trace saying inner's ran before middle's.
+  (print (caught 5)) (println "")
+  (print log) (println "")
+
+  ;; The arm that matches is the arm that runs.
+  (print (two 0)) (println "")
+  (print (two 1)) (println "")
+
+  ;; Unmatched: past this form and out to a handler-bind around it, and the
+  ;; body's own value still stands.
+  (handler-bind [(Corrupt [c] (note 6))]
+    (print (unmatched 3)) (println ""))
+  (print log) (println "")
+
+  ;; The two nestings. Neither signals from under [middle], so what each adds
+  ;; to the trace is its own handler-bind's clause and nothing else.
+  (print (hc-in-hb 6)) (println "")
+  (print (hb-in-hc 8)) (println "")
+  (print log) (println "")
+
+  ;; A clause that signals, caught by the handler-case outside it. Two unwinds,
+  ;; so both defers under [middle] run and then the one in [arm-signals] does.
+  (print (arm-caught-outside 4)) (println "")
+  (print log) (println "")
+
+  ;; A clause that returns, and then a signal nothing is listening for. The
+  ;; second is the leak check: it must be the no-op §2 says it is.
+  (print (return-from-clause 5)) (println "")
+  (print log) (println "")
+  (signal (Missing {.id 0}))
+  (print log) (println "")
+
+  ;; A handler-case established inside a defer.
+  (print (hc-in-defer 4)) (println "")
+  (print log) (println "")
+
+  ;; Two forms out of the one bucket of made-up names, each answering its own.
+  (in-clause-a)
+  (in-clause-b)
+  (print log) (println "")
+
+  ;; And the allocator scope. The arena is destroyed straight after, so the
+  ;; heap allocation below is only possible if the context was put back.
+  (set frame (arena-new 4096))
+  (print (scoped 3)) (println "")
+  (arena-destroy frame)
+  (let [h (vec-new i32)]
+    (push h 9)
+    (print (len h)) (println "")
+    (free h))
+  0)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 3301263..15470a0 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -448,6 +448,37 @@ let () =
     in
     restart_mismatch ();
     restart_mismatch ~opt:"-O0" ();
+    (* handler-case, the unwinding half of the pair. It is a handler-bind whose
+       clause invokes a restart the form established around itself, so what
+       these rows are really asserting is that the composition holds together
+       at the places an unwind can come apart: the defers between the signal
+       and the form, a condition nobody listed carrying on outward with the
+       body still running after it, a handler-bind on the path out having its
+       frame taken off as the transfer passes through, and a clause that
+       signals landing outside the form it belongs to rather than back in it.
+       A clause that returns, which is an ordinary return from the function
+       that wrote the form and must leave the handler stack empty behind it.
+       And two of them written inside handler-bind clauses, which is where the
+       made-up restart names come out of one shared bucket and where two forms
+       minting the same one would show.
+       At -O0 as well, because the guard after every call is control flow the
+       optimiser would otherwise launder, and under --x86, where the transfer
+       exit and the with-allocator restore share one epilogue and there is no
+       second copy to forget.
+
+       The long numbers are cleanup.flan's digit trace and not a running sum,
+       which is what makes them worth comparing: a sum commutes, so defers run
+       outermost-first would total the same, and a trace that says 12 where the
+       order is wrong says 21. *)
+    let handler_case_out =
+      "42\n0\n105\n12\n101\n202\n7\n126\n6\n16\n12645\n5099\n12645123\n705\n\
+       12645123129\n12645123129\n4\n1264512312948\n126451231294867\n23\n1\n"
+    in
+    outputs "handler-case" "programs/handler-case.flan" handler_case_out;
+    outputs ~opt:"-O0" "handler-case, -O0" "programs/handler-case.flan"
+      handler_case_out;
+    outputs ~x86:true "handler-case, --x86" "programs/handler-case.flan"
+      handler_case_out;
     (* 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
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 0d334e2..7bf416d 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -1653,10 +1653,94 @@ let () =
     (fun (name, src) ->
        rejects_check (name ^ " is still unimplemented") src
          ~needle:"not implemented yet")
-    [ "handler-case",     "(defn f [] () (handler-case 1))";
-      "find-restart",     "(defn f [] () (find-restart 'skip))";
+    [ "find-restart",     "(defn f [] () (find-restart 'skip))";
       "compute-restarts", "(defn f [] () (compute-restarts))" ];
 
+  (* ── handler-case ──────────────────────────────────────────────── *)
+
+  (* The unwinding handler. It is built out of a handler-bind and a
+     restart-case, so most of what could go wrong is already pinned where
+     those two are; what is asserted here is the surface it puts in front of
+     them and the one rule that is its own — every clause and the body agree
+     on a type, which is the type of the whole form. *)
+  let boom =
+    "(defstruct Boom [id i32])\n(defstruct Dud [id i32])\n"
+  in
+  accepts "handler-case"
+    (boom ^ "(defn f [] i32 (handler-case 1 [(Boom [c] (.id c))]))");
+  accepts "handler-case with several clauses"
+    (boom ^ "(defn f [] i32 (handler-case 1 [(Boom [c] (.id c)) \
+             (Dud [c] (+ 1 (.id c)))]))");
+  (* The whole difference from handler-bind: a clause runs at the form, in the
+     function that wrote it, so it sees that function's locals. The same body
+     under a handler-bind is refused by name. *)
+  accepts "a handler-case clause sees the establishing function's locals"
+    (boom ^ "(defn f [] i32 (let [n 1] (handler-case 0 [(Boom [c] n)])))");
+  rejects_check "a handler-bind clause still cannot"
+    (boom ^ "(defn f [] i32 (let [n 1] (handler-bind [(Boom [c] (set n 2))] 0)))")
+    ~needle:"a handler cannot see n: it is a local of the enclosing function";
+  (* Nothing static refuses a condition no clause lists: it installs no frame
+     that matches, so it goes past untouched and the body carries on. *)
+  accepts "a condition no clause lists"
+    (boom ^ "(defn f [] i32 (handler-case (do (signal (Dud {.id 1})) 7) \
+             [(Boom [c] 0)]))");
+  (* The typing rule, and it fails where an [if] with disagreeing arms fails:
+     at the form that does not fit, saying what was wanted and what was
+     found. *)
+  rejects_check "a handler-case clause that disagrees with the body"
+    (boom ^ "(defn f [] i32 (handler-case 1 [(Boom [c] \"no\")]))")
+    ~needle:"expected i32, found string";
+  rejects_check "two handler-case clauses that disagree"
+    (boom ^ "(defn f [] () (println (handler-case 1 [(Boom [c] 2) \
+             (Dud [c] \"no\")])))")
+    ~needle:"expected i32, found string";
+  (* Two clauses for one condition type: the first would take every one of
+     them and the second could never run. *)
+  rejects_check "one condition type twice"
+    (boom ^ "(defn f [] i32 (handler-case 1 [(Boom [c] 2) (Boom [c] 3)]))")
+    ~needle:"handles Boom twice";
+  rejects_check "a handler-case clause on something that is not a struct"
+    "(defn f [] i32 (handler-case 1 [(i32 [c] 2)]))"
+    ~needle:"a handler matches a struct type";
+  (* The frames are established around the body and taken off after it, so an
+     early exit out of the middle would leave them on the stack — and the
+     refusal names the form the reader wrote rather than the handler-bind
+     underneath it. *)
+  rejects_check "return inside a handler-case body"
+    (boom ^ "(defn f [] i32 (handler-case (return 1) [(Boom [c] 2)]))")
+    ~needle:"not allowed inside handler-case";
+  (* A clause is the other side of that rule and not an exception to it. It
+     runs at the form, in the function that wrote it, with the frames already
+     off the stack — so a [return] there is an ordinary return and there is
+     nothing left for it to strand. *)
+  accepts "return inside a handler-case clause"
+    (boom ^ "(defn f [] i32 (handler-case 1 [(Boom [c] (return 2))]))");
+  (* A defer is not, though, and for the reason every nested form is refused
+     one: it is copied onto every exit path of the *function*, so a defer
+     written where it looks scoped to the clause would run whether the clause
+     did or not. The same answer a restart-case clause gets. *)
+  rejects_check "defer inside a handler-case clause"
+    (boom ^ "(defn f [] i32 (handler-case 1 [(Boom [c] (defer (println \"\")) 2)]))")
+    ~needle:"defer is not allowed inside a nested form";
+  (* The other way round works. A defer is the cleanup an unwind runs, so
+     establishing frames inside one is ordinary — what a defer may not do is
+     start a transfer that leaves it, and a handler-case begins and ends its
+     own. *)
+  accepts "handler-case inside a defer"
+    (boom ^ "(defn f [] i32 (defer (println (handler-case 1 [(Boom [c] 2)]))) 0)");
+  (* The shape. The clauses go in a vector after the body, which is the
+     opposite of handler-bind's order, so a form written the other way round
+     has to say so rather than parse as something else. *)
+  rejects_check "handler-case with no clauses"
+    (boom ^ "(defn f [] i32 (handler-case 1 []))")
+    ~needle:"at least one clause";
+  rejects_check "handler-case written the handler-bind way round"
+    (boom ^ "(defn f [] i32 (handler-case [(Boom [c] 2)] 1))")
+    ~needle:"handler-case is (handler-case body";
+  rejects_check "a handler-case clause that binds nothing"
+    (boom ^ "(defn f [] i32 (handler-case 1 [(Boom [] 2)]))")
+    ~needle:"a handler-case clause is (Type [name] body ...)";
+
   (* ── Destructuring ─────────────────────────────────────────────── *)
 
   (* A pattern is desugared in [Parse] into the bindings and field accesses that
diff --git a/test/test_sanitize.ml b/test/test_sanitize.ml
index 8fbdca5..d180cc9 100644
--- a/test/test_sanitize.ml
+++ b/test/test_sanitize.ml
@@ -141,6 +141,14 @@ let corpus =
        same directory; the new C here is three more path buffers, which is
        exactly what this tool is for. *)
     "programs/files.flan", [];
+    (* The unwinding handler, and here for the frames rather than for the heap:
+       every path it takes leaves a function through the transfer exit, where
+       a handler frame or a restart frame left on its stack is a pointer into
+       an alloca that has gone. An output comparison cannot see that until
+       something later calls through it; ASan sees it at the store. The
+       with-allocator case is the one that reaches the heap — the region it
+       rebound is released after the unwind has carried a value out of it. *)
+    "programs/handler-case.flan", [];
     (* The JSON reader, which is the corpus's densest allocator: every string
        in the document is a (Vec u8) grown a byte at a time and then handed
        out as a view of its own block, and the block is never freed because
diff --git a/web/index.html b/web/index.html
index 4607389..1458723 100644
--- a/web/index.html
+++ b/web/index.html
@@ -2013,7 +2013,6 @@ name, with the milestone it belongs to, and the tests assert on the reason.</p>
 <tr><td>a bare lowercase type name</td><td>generic code over the type variable a is not implemented yet — milestone 5 (see plan.org)</td></tr>
 <tr><td><code>errdefer</code></td><td>errdefer is not implemented yet (see the build sequence in plan.org)</td></tr>
 <tr><td><code>await</code></td><td>await is not implemented yet (see the build sequence in plan.org)</td></tr>
-<tr><td><code>handler-case</code></td><td>handler-case is not implemented yet (see the build sequence in plan.org)</td></tr>
 <tr><td><code>find-restart</code>, <code>compute-restarts</code></td><td>… is not implemented yet (see the build sequence in plan.org)</td></tr>
 <tr><td>a union as a <code>declare</code> parameter</td><td>a parameter of g is U, which cannot cross to C directly — pass (Ptr U) and let the shim read it</td></tr>
 <tr><td>a user-written allocator</td><td>a user-written allocator is not implemented yet, and a defn's name in that position …</td></tr>