diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
index f3e0117..07c89b6 100644
--- a/.machine_readable/6a2/STATE.a2ml
+++ b/.machine_readable/6a2/STATE.a2ml
@@ -6,9 +6,9 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Layer-10 cross-handler named residues: residue-binding grammar syntax (let undo = reversible {…}; reverse undo) carried through agent state — Harvard-guarded grammar change, own rung; then continue parser gap fill (types, imports, locales, choreographies)"
-last_action: "Phase-2 echo-residue landed: residue is now Linear<Echo<T>> (affine capability, linear consumption — double-reverse rejected, un-reversed residue not an error); Idris2 EchoResidueLinear.idr (reverseLinear (1 e), ResidueCell Holding/Spent, idris2 --check clean, zero believe_me); 3 new typechecker tests (883 oo7-core passing); spec §11b.4/§11.4 + CHANGELOG + integration doc updated in lockstep. estate-standardization-20260607 reconciled into main (PR #40 merged). Prior: Layer 10 phase-1 (PR #34), CI gates greened (PR #38), 6a2/ecosystem refresh (PR #39)"
-updated: 2026-06-14T02:00:00Z
+next_action: "Layer-10 rung 3b: cross-handler residues through agent state — residue cell in agent state + evaluator runtime Holding/Spent (ResidueCell, takeForReverse:Maybe) + EchoResidueLinear bridge lemma; then continue parser gap fill (types, imports, locales, choreographies)"
+last_action: "Phase-3 rung-3a landed: NAMED residues within a body — new syntax `reversible as <name> {…}` / `reverse <name>` (anonymous forms unchanged). Additive AST ReversibleAs/ReverseNamed; grammar.pest+grammar.ebnf; typechecker named_residues map (Holding/Spent, static mirror of ResidueCell) with per-function/handler isolation; eval/codegen/formatter/dual_ast/metainterpreter/CFG/oracle threaded. Affine/linear discipline: double-reverse rejected, un-reversed ok, no cross-body leak. 2 parser + 5 typechecker tests (890 oo7-core passing; fmt clean, clippy -D warnings 0). Spec §11b.5 + CHANGELOG + integration doc in lockstep. Prior: phase-2 Linear<Echo<T>> (PR #41 merged), phase-1 (PR #34), CI gates (PR #38), 6a2 (PR #39), estate reconcile (PR #40)"
+updated: 2026-06-15T17:00:00Z
 
 @blockers:
 - id: proof-debt
diff --git a/.machine_readable/session-log.txt b/.machine_readable/session-log.txt
index ff210a1..13bdb43 100644
--- a/.machine_readable/session-log.txt
+++ b/.machine_readable/session-log.txt
@@ -29,3 +29,5 @@
 
 
 [2026-06-14 01:25:37] Session ended (continuation): item-2 estate-standardization reconcile MERGED (PR #40) → main is one reconciled line. Then resumed ORIGINAL WORK = Layer-10 PHASE 2 (residue as a linear undo-capability). (a) Idris2: proofs/idris2/EchoResidueLinear.idr (NEW, %default total, zero believe_me, idris2 --check clean) — reverseLinear consumes (1 e : Echo f y) (Idris2 quantity 1 = "consumed exactly once" proof, mirroring 007's planned Linear<Echo<T>>); reverseLinearCorrect (recovered input maps back to y, intrinsic via the dependent pair); ResidueCell Holding/Spent = the residue carried as agent STATE between handlers; takeForReverse (later handler consumes the cell; Spent→Nothing); holdingReverses/spentDoesNotReverse (cross-handler reversal succeeds iff a residue was retained); cellMode bridges a cell back to the phase-1 Reversibility mode. (b) Rust typechecker.rs: residue stack now carries Linear<Echo<T>> (push_echo_residue wraps Type::Echo in Type::Linear) — the consumed-once discipline is explicit in the carried type; the single linear use is the take_echo_residue pop in a later reverse. +3 typechecker_tests (l10_phase2_residue_type_is_linear_echo / _double_reverse_of_single_residue_is_error / _retained_residue_is_not_an_error) → 883 oo7-core lib tests passing. CI gates verified LOCALLY: cargo check --offline 0, full oo7-core test suite 922 ok 0 fail, fmt --check 0, clippy (CI-equivalent, no --all-targets) -D warnings exit 0. (c) DESIGN DECISION flagged to user (a plus/interesting): the residue is an AFFINE capability consumed LINEARLY — replaying one log twice is rejected (linear use; structural in the stack), but a reversible block need NOT be paired with a reverse (un-reversed residue is NOT an error; reversibility is a capability, usually unused). The opposite (strict must-reverse / LinearNotConsumed) was deliberately REJECTED as semantically wrong + poor agent ergonomics; the 3 tests lock the affine-drop in so it can't be silently tightened. (d) Docs in lockstep: TYPE-SYSTEM-SPEC §11b.4 + OPERATIONAL-SEMANTICS §11.4 (planned→landed), CHANGELOG phase-2 bullet, docs/echo-residue-integration.adoc (phase-2 section + design-decision subsection + "still open" cross-handler rung), 6a2 STATE.a2ml last/next_action + cleared estate-standardization-unmerged blocker. (e) NOTE — canonical-proof-suite MANIFEST.a2ml NOT touched: phase-1 EchoResidue.idr is not a manifest entry either, so EchoResidueLinear.idr stays alongside it (checked by idris2 --check, not the curated S/E/M suite); the proof-suite workflow ignores unlisted .idr files (no CI risk). STILL OPEN (next rung): cross-handler NAMED residues need residue-binding grammar syntax (let undo = reversible {…}; reverse undo) — Harvard-guarded grammar change, kept as its own rung; formal model (ResidueCell) already in place, only surface syntax missing. Phase-2 work pushed to branch claude/echo-residue-phase2-linear → draft PR. Billing blocker may still gate CI (account-owner action).
+
+[2026-06-15 17:39:22] Session continued: Layer-10 PHASE 3 RUNG 3a landed (named residues within a body) on branch claude/echo-residue-phase3-named off main. User chose syntax `reversible as undo {…}` / `reverse undo` (the `as`-binder, agent-ergonomic) and scope "static core first" (within-body, fully static; cross-handler 3b deferred). (a) Grammar: grammar.pest + spec/grammar.ebnf — reversible_block gains optional ("as" ~ ident); new reverse_named = "reverse" ~ ident; Harvard-safe (control rules ref the shared ident token; Harvard guard PASS). (b) AST: ADDITIVE variants ReversibleAs{binding,body} + ReverseNamed{target} — existing Reversible/Irreversible/Reverse untouched, so the 9 exhaustive ControlStmt matches were compiler-enumerated + mirrored (codegen_cranelift/elixir/native, dual_ast, eval, formatter, metainterpreter, semantic_analyser/control_flow, typechecker check_stmt) + oracle check.rs + the two combined typechecker passes (effects, collect_linear_lets). (c) Typechecker: per-body named_residues: HashMap<String,NamedResidueState{Holding(Type)|Spent}> — the static mirror of ResidueCell; bind_named_residue (reversible as → Holding(Linear<Echo<T>>)); take_named_residue (reverse → Holding→Spent, else Err); per-function + per-handler mem::take isolation (no cross-body leak). Affine/linear: double reverse <name> rejected (Spent), un-reversed bound name NOT an error, reverse of unknown/spent name = L10_REVERSE_WITHOUT_RESIDUE. (d) Parser: build_reversible_block detects optional ident → ReversibleAs vs Reversible; build_reverse_named. (e) Tests: 2 parser (reversible_as_binds_named_residue, reverse_named_parses) + 5 typechecker (named-reverse-ok, reverse-unknown-errs, double-reverse-errs, unreversed-ok-affine, no-cross-function-leak) → 890 oo7-core lib tests pass; full workspace cargo test 0 failures; cargo fmt --check clean; cargo clippy --offline -D warnings exit 0 (CI-equivalent). (f) Docs in lockstep: TYPE-SYSTEM-SPEC §11b.5 (new), docs/echo-residue-integration.adoc (phase-3 section + rung-3b still-open), CHANGELOG, 6a2 STATE. NO new Idris needed — ResidueCell/reverseLinear already model rung 3a. STILL OPEN rung 3b: cross-handler residues via agent state — irreducibly partly RUNTIME (no static knowledge whether the earlier handler fired; Idris takeForReverse returns Maybe), so it adds a residue cell in agent state + evaluator Holding/Spent + bridge lemma. Pushed to claude/echo-residue-phase3-named → draft PR. Billing may still gate CI (account-owner action); verified locally.
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 09e5176..675dbe6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -8,6 +8,7 @@ All notable changes to this project will be documented in this file.
 ### Added
 - **Layer 10 — Reversibility (Echo residue): echo-types integrated into the type system.** `reversible`/`irreversible`/`reverse` are no longer checked identically: `Type::Echo<T>` residues are tracked per body (`reversible` retains one, `irreversible` discards it, `reverse` consumes one), and a `reverse` with no residue is `ReverseWithoutResidue` — enforcing OPERATIONAL-SEMANTICS §11.3, previously unenforced. Grounded in echo-types' keystone `A ≃ Σ B (Echo f)` and mechanised in `proofs/idris2/EchoResidue.idr` (`encodeDecode`, `reverseAfterIrreversibleIllTyped`, `collapseHasNoSection`; `%default total`, zero `believe_me`). Surfaced to agents via `agent_api` code `L10_REVERSE_WITHOUT_RESIDUE` (+`mark_reversible`/`retain_echo` remediations). 4 new typechecker tests. Spec: TYPE-SYSTEM-SPEC §"Layer 10", OPERATIONAL-SEMANTICS §11.4; design note `docs/echo-residue-integration.adoc`.
 - **Layer 10 phase 2 — the residue is a linear undo-capability.** The checker's residue stack now carries `Linear<Echo<T>>` (was a bare `Echo<T>`), making the consumed-once discipline explicit in the type. Discipline: *affine capability, linear consumption* — a given reversal log is consumed at most once (a double `reverse` of one residue is rejected) yet a `reversible` block need not be paired with a `reverse` (an un-reversed residue is **not** an error; reversibility is a capability, usually unused). Mechanised in `proofs/idris2/EchoResidueLinear.idr` (`reverseLinear` consumes `(1 e : Echo f y)`; `ResidueCell` Holding/Spent = the residue as agent state; `holdingReverses`/`spentDoesNotReverse`; `%default total`, zero `believe_me`, `idris2 --check` clean). 3 new typechecker tests (883 `oo7-core` lib tests passing). Remaining rung: cross-handler *named* residues (residue-binding grammar syntax, Harvard-guarded — kept separate). Spec/docs updated in lockstep.
+- **Layer 10 phase 3 (rung 3a) — named residues within a body.** New surface syntax `reversible as <name> { … }` binds the echo residue to a name; `reverse <name>` replays it (anonymous `reversible {…}`/`reverse {…}` unchanged). The named residue is tracked per body as a `Holding(Linear<Echo<T>>)` cell that `reverse` transitions to `Spent` — the static mirror of `ResidueCell` (Holding/Spent) in `EchoResidueLinear.idr`. Same affine/linear discipline: double `reverse <name>` is rejected (cell already `Spent`); a never-replayed binding is **not** an error; named residues are scoped per body (no cross-body leak). Additive AST variants `ReversibleAs`/`ReverseNamed` (existing variants untouched); grammar (`grammar.pest` + `spec/grammar.ebnf`), parser, typechecker (`named_residues` map + per-function/handler isolation), and the eval/codegen/formatter/dual-ast/metainterpreter/CFG/oracle pipeline all threaded. 2 parser + 5 typechecker tests (890 `oo7-core` lib tests passing; fmt clean, clippy `-D warnings` exit 0). Remaining rung 3b: cross-handler residues through agent state (irreducibly partly runtime — `takeForReverse : Maybe`). Spec: TYPE-SYSTEM-SPEC §11b.5; docs `docs/echo-residue-integration.adoc`.
 - **752 tests** (up from 207 at 0.5.0). CRG-C achieved 2026-04-04 for `oo7-core`.
 - **31 multi-language backends** via `mk2_bridge::create_backend_registry()`. Real dispatch to `elixir`, `idris2`, `gleam`, `rescript`, `nickel`, `guile`, `psql`, etc. Tier-5 coprocessor backends (CUDA/Vulkan/Metal/OpenCL/FPGA/TPU/DSP) do phase-1 device discovery with documented "kernel launch is future work" status.
 - **Metainterpreter** (`metainterpreter.rs`, ~3,075 LOC): reify/reflect/step/replay, four modes, 40 inline tests, 18 benches.
diff --git a/crates/oo7-core/src/ast.rs b/crates/oo7-core/src/ast.rs
index 378438e..341c8db 100644
--- a/crates/oo7-core/src/ast.rs
+++ b/crates/oo7-core/src/ast.rs
@@ -346,6 +346,19 @@ pub enum ControlStmt {
     Irreversible(Vec<ControlStmt>),
     /// `reverse { ... }` — executes the reverse of a previous reversible block
     Reverse(Vec<ControlStmt>),
+    /// `reversible as undo { ... }` — a reversible block that BINDS its echo
+    /// residue to a name (`undo`), so a later `reverse undo` can replay it.
+    /// L10 phase 3 (rung 3a): the named residue is a `Linear<Echo<T>>` tracked
+    /// per-body; it is an affine capability consumed linearly (replay at most
+    /// once; never replaying is not an error).
+    ReversibleAs {
+        binding: String,
+        body: Vec<ControlStmt>,
+    },
+    /// `reverse undo` — replays the named echo residue `undo` bound by an
+    /// earlier `reversible as undo { ... }`. Consumes the residue: a second
+    /// `reverse undo` is the L10 reverse-without-residue error.
+    ReverseNamed { target: String },
     /// `enter discourse name { ... }` — execute within a discourse's interpretation rules.
     /// Branch strategy and evidence weights change within the block.
     EnterDiscourse {
diff --git a/crates/oo7-core/src/codegen_cranelift.rs b/crates/oo7-core/src/codegen_cranelift.rs
index 79abbb1..51bceb2 100644
--- a/crates/oo7-core/src/codegen_cranelift.rs
+++ b/crates/oo7-core/src/codegen_cranelift.rs
@@ -372,6 +372,16 @@ pub fn gen_body(
             ControlStmt::Reverse(body) => {
                 last = gen_body(body, builder, var_map, next_var, ptr_type);
             }
+            ControlStmt::ReversibleAs { body, .. } => {
+                // A named reversible block compiles its body directly; the
+                // residue binding is a type-level (L10) concern.
+                last = gen_body(body, builder, var_map, next_var, ptr_type);
+            }
+            ControlStmt::ReverseNamed { .. } => {
+                // `reverse <name>` replays a named residue — a runtime concern
+                // (rung 3b); nothing to emit at rung 3a.
+                last = builder.ins().iconst(cranelift_codegen::ir::types::I64, 0);
+            }
             ControlStmt::EnterDiscourse { body, .. } => {
                 // Discourse is a runtime semantic concern — compile the body.
                 last = gen_body(body, builder, var_map, next_var, ptr_type);
diff --git a/crates/oo7-core/src/codegen_elixir.rs b/crates/oo7-core/src/codegen_elixir.rs
index 6fcb44c..06f4a8d 100644
--- a/crates/oo7-core/src/codegen_elixir.rs
+++ b/crates/oo7-core/src/codegen_elixir.rs
@@ -819,6 +819,18 @@ pub fn gen_control_stmt(stmt: &ControlStmt, ctx: &GenContext, indent: usize) ->
             out.push_str(&gen_stmts(body, ctx, indent));
             out
         }
+        ControlStmt::ReversibleAs { binding, body } => {
+            let mut out = format!("{}# reversible as {}\n{}try do\n", ind, binding, ind);
+            out.push_str(&gen_stmts(body, ctx, indent + 1));
+            out.push_str(&format!(
+                "\n{}rescue\n{}  e -> {{:error, e}}\n{}end",
+                ind, ind, ind
+            ));
+            out
+        }
+        ControlStmt::ReverseNamed { target } => {
+            format!("{}# reverse {}", ind, target)
+        }
         ControlStmt::EnterDiscourse { discourse, body } => {
             // Discourse context — emit a comment and execute the body.
             // Runtime discourse semantics are a future extension.
diff --git a/crates/oo7-core/src/codegen_native.rs b/crates/oo7-core/src/codegen_native.rs
index 65ce08e..26ddc47 100644
--- a/crates/oo7-core/src/codegen_native.rs
+++ b/crates/oo7-core/src/codegen_native.rs
@@ -381,6 +381,16 @@ fn gen_stmt_zig(stmt: &ControlStmt, depth: usize) -> String {
             }
             out
         }
+        ControlStmt::ReversibleAs { binding, body } => {
+            let mut out = format!("// reversible as {}\n", binding);
+            for s in body {
+                out.push_str(&format!("{}{};\n", indent, gen_stmt_zig(s, depth)));
+            }
+            out
+        }
+        ControlStmt::ReverseNamed { target } => {
+            format!("// reverse {}\n", target)
+        }
         ControlStmt::EnterDiscourse { discourse, body } => {
             let mut out = format!("// enter discourse {}\n", discourse);
             for s in body {
diff --git a/crates/oo7-core/src/dual_ast.rs b/crates/oo7-core/src/dual_ast.rs
index b6a4d75..891ce85 100644
--- a/crates/oo7-core/src/dual_ast.rs
+++ b/crates/oo7-core/src/dual_ast.rs
@@ -978,12 +978,16 @@ fn lower_control_stmt(
         ControlStmt::Continue => control.alloc(ControlNode::Continue),
         ControlStmt::Reversible(stmts)
         | ControlStmt::Irreversible(stmts)
-        | ControlStmt::Reverse(stmts) => {
+        | ControlStmt::Reverse(stmts)
+        | ControlStmt::ReversibleAs { body: stmts, .. } => {
             for s in stmts {
                 lower_control_stmt(s, control, data);
             }
             control.alloc(ControlNode::Var("reversible-block".to_string()))
         }
+        ControlStmt::ReverseNamed { .. } => {
+            control.alloc(ControlNode::Var("reverse-named".to_string()))
+        }
         ControlStmt::EnterDiscourse { discourse, body } => {
             let body_ids: Vec<ControlNodeId> = body
                 .iter()
diff --git a/crates/oo7-core/src/eval.rs b/crates/oo7-core/src/eval.rs
index 3177a30..9c1526e 100644
--- a/crates/oo7-core/src/eval.rs
+++ b/crates/oo7-core/src/eval.rs
@@ -1926,12 +1926,18 @@ impl Evaluator {
             // handled by the type checker.
             ControlStmt::Reversible(body)
             | ControlStmt::Irreversible(body)
-            | ControlStmt::Reverse(body) => {
+            | ControlStmt::Reverse(body)
+            | ControlStmt::ReversibleAs { body, .. } => {
                 env.push_scope();
                 let r = self.eval_stmts(body, env);
                 env.pop_scope();
                 r
             }
+            ControlStmt::ReverseNamed { .. } => {
+                // Rung 3a: `reverse <name>` is statically checked; runtime
+                // replay of a named residue is the cross-handler rung (3b).
+                RtValue::Unit
+            }
 
             ControlStmt::EnterDiscourse { discourse, body } => {
                 // Enter a discourse context — swap the branch strategy to the
diff --git a/crates/oo7-core/src/formatter.rs b/crates/oo7-core/src/formatter.rs
index b3c62ff..a789c75 100644
--- a/crates/oo7-core/src/formatter.rs
+++ b/crates/oo7-core/src/formatter.rs
@@ -771,6 +771,15 @@ fn format_stmt(stmt: &ControlStmt, depth: usize) -> String {
             out.push_str(&format!("{}}}", indent));
             out
         }
+        ControlStmt::ReversibleAs { binding, body } => {
+            let mut out = format!("reversible as {} {{\n", binding);
+            for s in body {
+                out.push_str(&format!("{}{}\n", inner, format_stmt(s, depth + 1)));
+            }
+            out.push_str(&format!("{}}}", indent));
+            out
+        }
+        ControlStmt::ReverseNamed { target } => format!("reverse {}", target),
         ControlStmt::EnterDiscourse { discourse, body } => {
             let mut out = format!("enter discourse {} {{\n", discourse);
             for s in body {
diff --git a/crates/oo7-core/src/grammar.pest b/crates/oo7-core/src/grammar.pest
index 79d116d..e28d2d9 100644
--- a/crates/oo7-core/src/grammar.pest
+++ b/crates/oo7-core/src/grammar.pest
@@ -192,6 +192,7 @@ control_stmt = {
     | return_stmt
     | reversible_block
     | irreversible_block
+    | reverse_named
     | reverse_block
     | enter_discourse_stmt
     | control_expr ~ ";"?
@@ -645,10 +646,15 @@ enum_variant = { upper_ident ~ ("(" ~ typed_fields ~ ")")? }
 // Reversibility Blocks
 // ============================================================
 
-reversible_block = { "reversible" ~ "{" ~ control_stmt* ~ "}" }
+// `reversible { ... }` is anonymous; `reversible as <name> { ... }` BINDS the
+// echo residue to <name> so a later `reverse <name>` can replay it (L10 phase 3).
+reversible_block = { "reversible" ~ ("as" ~ ident)? ~ "{" ~ control_stmt* ~ "}" }
 
 reverse_block = { "reverse" ~ "{" ~ control_stmt* ~ "}" }
 
+// `reverse <name>` replays the named residue bound by `reversible as <name>`.
+reverse_named = { "reverse" ~ ident }
+
 irreversible_block = { "irreversible" ~ "{" ~ control_stmt* ~ "}" }
 
 // ============================================================
diff --git a/crates/oo7-core/src/metainterpreter.rs b/crates/oo7-core/src/metainterpreter.rs
index bc0be7a..582a071 100644
--- a/crates/oo7-core/src/metainterpreter.rs
+++ b/crates/oo7-core/src/metainterpreter.rs
@@ -782,6 +782,20 @@ pub fn reify_control_stmt(stmt: &ControlStmt) -> RtValue {
                 vec![("body".to_string(), RtValue::List(stmts))],
             )
         }
+        ControlStmt::ReversibleAs { binding, body } => {
+            let stmts: Vec<RtValue> = body.iter().map(reify_control_stmt).collect();
+            meta_record(
+                "ControlStmt::ReversibleAs",
+                vec![
+                    ("binding".to_string(), RtValue::String(binding.clone())),
+                    ("body".to_string(), RtValue::List(stmts)),
+                ],
+            )
+        }
+        ControlStmt::ReverseNamed { target } => meta_record(
+            "ControlStmt::ReverseNamed",
+            vec![("target".to_string(), RtValue::String(target.clone()))],
+        ),
         ControlStmt::EnterDiscourse { discourse, body } => {
             let stmts: Vec<RtValue> = body.iter().map(reify_control_stmt).collect();
             meta_record(
diff --git a/crates/oo7-core/src/parser.rs b/crates/oo7-core/src/parser.rs
index 5df9698..ad12289 100644
--- a/crates/oo7-core/src/parser.rs
+++ b/crates/oo7-core/src/parser.rs
@@ -417,6 +417,7 @@ fn build_control_stmt(pair: pest::iterators::Pair<Rule>) -> ControlStmt {
         Rule::reversible_block => build_reversible_block(inner),
         Rule::irreversible_block => build_irreversible_block(inner),
         Rule::reverse_block => build_reverse_block(inner),
+        Rule::reverse_named => build_reverse_named(inner),
         Rule::enter_discourse_stmt => build_enter_discourse_stmt(inner),
         Rule::control_expr => ControlStmt::Expr(build_control_expr(inner)),
         _ => ControlStmt::Expr(ControlExpr::Var(inner.as_str().to_string())),
@@ -609,10 +610,33 @@ fn build_return_stmt(pair: pest::iterators::Pair<Rule>) -> ControlStmt {
     ControlStmt::Return(expr)
 }
 
-/// Build a `reversible { ... }` block.
+/// Build a `reversible { ... }` block, or `reversible as <name> { ... }` which
+/// BINDS the echo residue to <name> (L10 phase 3). `build_control_stmts`
+/// filter-skips the optional `ident` pair, so it yields the body either way.
 fn build_reversible_block(pair: pest::iterators::Pair<Rule>) -> ControlStmt {
+    let binding = pair
+        .clone()
+        .into_inner()
+        .find(|p| p.as_rule() == Rule::ident)
+        .map(|p| p.as_str().to_string());
     let body = build_control_stmts(pair.into_inner());
-    ControlStmt::Reversible(body)
+    match binding {
+        Some(name) => ControlStmt::ReversibleAs {
+            binding: name,
+            body,
+        },
+        None => ControlStmt::Reversible(body),
+    }
+}
+
+/// Build a `reverse <name>` statement — replays the named residue.
+fn build_reverse_named(pair: pest::iterators::Pair<Rule>) -> ControlStmt {
+    let target = pair
+        .into_inner()
+        .find(|p| p.as_rule() == Rule::ident)
+        .map(|p| p.as_str().to_string())
+        .unwrap_or_default();
+    ControlStmt::ReverseNamed { target }
 }
 
 /// Build an `irreversible { ... }` block.
diff --git a/crates/oo7-core/src/parser_tests.rs b/crates/oo7-core/src/parser_tests.rs
index d3cfa49..ec13904 100644
--- a/crates/oo7-core/src/parser_tests.rs
+++ b/crates/oo7-core/src/parser_tests.rs
@@ -1073,6 +1073,51 @@ mod tests {
         assert!(matches!(&f.body[0], ControlStmt::Reverse(_)));
     }
 
+    #[test]
+    fn reversible_as_binds_named_residue() {
+        // `reversible as <name> { ... }` parses to ReversibleAs with the name.
+        let decl = first_decl(
+            r#"@impure fn example() {
+                reversible as undo {
+                    let x = do_something()
+                }
+            }"#,
+        );
+        let TopLevelDecl::Function(f) = decl else {
+            panic!("Expected Function")
+        };
+        match &f.body[0] {
+            ControlStmt::ReversibleAs { binding, body } => {
+                assert_eq!(binding, "undo");
+                assert_eq!(body.len(), 1);
+            }
+            other => panic!("Expected ReversibleAs, got {other:?}"),
+        }
+    }
+
+    #[test]
+    fn reverse_named_parses() {
+        // `reverse <name>` parses to ReverseNamed; the anonymous `reverse { }`
+        // form is unaffected (covered by `reverse_block`). Guards the PEG
+        // ordering of `reverse_named` vs `reverse_block`.
+        let decl = first_decl(
+            r#"@impure fn example() {
+                reversible as undo {
+                    let x = do_something()
+                }
+                reverse undo
+            }"#,
+        );
+        let TopLevelDecl::Function(f) = decl else {
+            panic!("Expected Function")
+        };
+        assert!(matches!(&f.body[0], ControlStmt::ReversibleAs { .. }));
+        match &f.body[1] {
+            ControlStmt::ReverseNamed { target } => assert_eq!(target, "undo"),
+            other => panic!("Expected ReverseNamed, got {other:?}"),
+        }
+    }
+
     // ================================================================
     // COMMENTS
     // ================================================================
diff --git a/crates/oo7-core/src/semantic_analyser/control_flow.rs b/crates/oo7-core/src/semantic_analyser/control_flow.rs
index d2ffa84..f3cd4ff 100644
--- a/crates/oo7-core/src/semantic_analyser/control_flow.rs
+++ b/crates/oo7-core/src/semantic_analyser/control_flow.rs
@@ -260,7 +260,14 @@ impl CfgBuilder {
             }
             ControlStmt::Reversible(body)
             | ControlStmt::Irreversible(body)
-            | ControlStmt::Reverse(body) => self.build_stmts(body, prev),
+            | ControlStmt::Reverse(body)
+            | ControlStmt::ReversibleAs { body, .. } => self.build_stmts(body, prev),
+            ControlStmt::ReverseNamed { .. } => {
+                let id = self.fresh_id("reverse");
+                self.add_node(&id, CFGNodeType::Assignment);
+                self.add_edge(prev, &id);
+                id
+            }
             ControlStmt::EnterDiscourse { discourse, body } => {
                 let d_entry = self.fresh_id(&format!("enter_discourse_{}", discourse));
                 self.add_node(&d_entry, CFGNodeType::DiscourseEntry);
diff --git a/crates/oo7-core/src/typechecker.rs b/crates/oo7-core/src/typechecker.rs
index 307aa64..87ee454 100644
--- a/crates/oo7-core/src/typechecker.rs
+++ b/crates/oo7-core/src/typechecker.rs
@@ -520,6 +520,27 @@ pub struct TypeEnv {
     /// and consumed by a later handler — is the next rung and needs residue
     /// binding syntax in the grammar (cf. `ResidueCell` in the Idris proof).
     echo_residues: Vec<Type>,
+    /// L10 phase 3 (rung 3a): NAMED echo residues bound by `reversible as
+    /// <name> { … }` and replayed by `reverse <name>` within the same body.
+    /// Each name maps to a `Holding(Linear<Echo<T>>)` cell that a `reverse`
+    /// transitions to `Spent` — the static mirror of `ResidueCell` in
+    /// proofs/idris2/EchoResidueLinear.idr. Affine: a name left `Holding` at a
+    /// body boundary is dropped, not flagged (an unexercised undo capability
+    /// is not an error); a `reverse` of a `Spent` (or absent) name is the
+    /// reverse-without-residue error. Like `echo_residues`, this map is scoped
+    /// per body (isolated at function/handler boundaries); cross-body carry
+    /// through agent state is the next rung (rung 3b).
+    named_residues: HashMap<String, NamedResidueState>,
+}
+
+/// The static state of a named echo residue — the checker-side shadow of the
+/// `ResidueCell` GADT (`Holding` / `Spent`) in EchoResidueLinear.idr.
+#[derive(Debug, Clone)]
+enum NamedResidueState {
+    /// The named residue is live: a `Linear<Echo<T>>` available to `reverse`.
+    Holding(Type),
+    /// The named residue has already been replayed (consumed exactly once).
+    Spent,
 }
 
 impl TypeEnv {
@@ -540,6 +561,7 @@ impl TypeEnv {
             constants: HashMap::new(),
             nonzero_witnesses: HashSet::new(),
             echo_residues: Vec::new(),
+            named_residues: HashMap::new(),
         }
     }
 
@@ -571,6 +593,40 @@ impl TypeEnv {
         self.echo_residues.pop()
     }
 
+    /// Bind a NAMED echo residue (`reversible as <name> { … }`): record `name`
+    /// as `Holding` a `Linear<Echo<T>>`. Re-binding an existing name overwrites
+    /// it (the previous, unreplayed residue is simply dropped — affine).
+    fn bind_named_residue(&mut self, name: String, inner: Type) {
+        self.named_residues.insert(
+            name,
+            NamedResidueState::Holding(Type::Linear(Box::new(Type::Echo(Box::new(inner))))),
+        );
+    }
+
+    /// Consume a NAMED echo residue (`reverse <name>`): transition `Holding` →
+    /// `Spent` (the single linear use). Returns `Err(reason)` when the name is
+    /// not live — either it was never bound, or it has already been replayed
+    /// (double-`reverse`) — which the caller raises as ReverseWithoutResidue.
+    fn take_named_residue(&mut self, name: &str) -> Result<(), String> {
+        match self.named_residues.get_mut(name) {
+            Some(slot) => match slot {
+                NamedResidueState::Holding(_) => {
+                    *slot = NamedResidueState::Spent;
+                    Ok(())
+                }
+                NamedResidueState::Spent => Err(format!(
+                    "the residue named `{name}` has already been reversed — a \
+                     residue is a linear undo-capability, replayable at most once"
+                )),
+            },
+            None => Err(format!(
+                "no live residue named `{name}` is in scope: there is no preceding \
+                 `reversible as {name} {{ … }}` in this body whose reversal log it \
+                 can replay"
+            )),
+        }
+    }
+
     // -- Scope management --
 
     /// Push a new scope onto the scope stack.
@@ -1676,7 +1732,8 @@ fn check_stmt_effects(
         }
         ControlStmt::Reversible(body)
         | ControlStmt::Irreversible(body)
-        | ControlStmt::Reverse(body) => {
+        | ControlStmt::Reverse(body)
+        | ControlStmt::ReversibleAs { body, .. } => {
             for s in body {
                 check_stmt_effects(s, context_purity, fn_name, env);
             }
@@ -1822,10 +1879,12 @@ fn check_function_decl(fd: &FunctionDecl, env: &mut TypeEnv) {
     // reversal carries a residue by name through agent state; that named
     // binding is the next rung (cf. `ResidueCell` in EchoResidueLinear.idr).
     let saved_residues = std::mem::take(&mut env.echo_residues);
+    let saved_named = std::mem::take(&mut env.named_residues);
     for stmt in &fd.body {
         check_stmt(stmt, &ret_type, env);
     }
     env.echo_residues = saved_residues;
+    env.named_residues = saved_named;
 
     env.pop_scope();
     env.current_purity = old_purity;
@@ -1870,10 +1929,12 @@ fn check_agent_decl(ad: &AgentDecl, env: &mut TypeEnv) {
         // EchoResidueLinear.idr). Residues outstanding at the handler boundary
         // are dropped: an unexercised undo capability is not an error.
         let saved_residues = std::mem::take(&mut env.echo_residues);
+        let saved_named = std::mem::take(&mut env.named_residues);
         for stmt in &handler.body {
             check_stmt(stmt, &Type::Unit, env);
         }
         env.echo_residues = saved_residues;
+        env.named_residues = saved_named;
         env.pop_scope();
     }
 
@@ -3463,6 +3524,34 @@ fn check_stmt(stmt: &ControlStmt, expected_ret: &Type, env: &mut TypeEnv) {
             env.pop_scope();
         }
 
+        ControlStmt::ReversibleAs { binding, body } => {
+            // Like `reversible`, but the residue is BOUND to `binding` so a
+            // later `reverse <binding>` in the same body can replay it. The
+            // named residue is a `Linear<Echo<T>>` tracked per body (rung 3a);
+            // cross-body carry through agent state is the next rung (3b).
+            env.push_scope();
+            for s in body {
+                check_stmt(s, expected_ret, env);
+            }
+            env.pop_scope();
+            env.bind_named_residue(binding.clone(), Type::Unit);
+        }
+
+        ControlStmt::ReverseNamed { target } => {
+            // `reverse <target>` consumes the named residue exactly once. It is
+            // ill-typed if no live residue of that name is in scope — either it
+            // was never bound, or it has already been replayed (double-reverse,
+            // the named analogue of the §11.3 reverse-without-residue error).
+            if let Err(reason) = env.take_named_residue(target) {
+                env.error(
+                    TypeErrorKind::ReverseWithoutResidue {
+                        detail: reason.clone(),
+                    },
+                    format!("cannot `reverse {target}`: {reason} (spec §11.3)"),
+                );
+            }
+        }
+
         ControlStmt::Expr(e) => {
             let _ty = infer_control(e, env);
         }
@@ -4941,7 +5030,8 @@ fn collect_linear_lets(stmt: &ControlStmt, out: &mut Vec<(String, String)>) {
         }
         ControlStmt::Reversible(body)
         | ControlStmt::Irreversible(body)
-        | ControlStmt::Reverse(body) => {
+        | ControlStmt::Reverse(body)
+        | ControlStmt::ReversibleAs { body, .. } => {
             for s in body {
                 collect_linear_lets(s, out);
             }
diff --git a/crates/oo7-core/src/typechecker_tests.rs b/crates/oo7-core/src/typechecker_tests.rs
index 770ce5c..011028c 100644
--- a/crates/oo7-core/src/typechecker_tests.rs
+++ b/crates/oo7-core/src/typechecker_tests.rs
@@ -1883,3 +1883,103 @@ fn l10_phase2_retained_residue_is_not_an_error() {
         );
     }
 }
+
+// ── Phase 3 (rung 3a): named residues within a body ──────────────────
+//
+// `reversible as <name> { … }` binds the echo residue to <name>; a later
+// `reverse <name>` in the SAME body replays it. The named residue is the
+// static mirror of `ResidueCell` (Holding/Spent) in EchoResidueLinear.idr:
+// affine (replay at most once; never replaying is fine) and scoped per body
+// (cross-body carry through agent state is the next rung, 3b).
+
+#[test]
+fn l10_phase3_named_reverse_after_reversible_as_ok() {
+    // `reverse undo` matched by a preceding `reversible as undo { … }` in the
+    // same body is well-typed.
+    let src = r#"@impure fn f() {
+        reversible as undo {
+            let x = 1
+        }
+        reverse undo
+    }"#;
+    if let Err(errs) = parse_and_check(src) {
+        assert!(
+            !has_reverse_without_residue(&errs),
+            "reverse of a bound named residue must NOT raise ReverseWithoutResidue, got: {:?}",
+            errs
+        );
+    }
+}
+
+#[test]
+fn l10_phase3_reverse_unknown_name_is_error() {
+    // `reverse undo` with no `reversible as undo` in scope is the named
+    // analogue of reverse-without-residue.
+    let src = r#"@impure fn f() {
+        reverse undo
+    }"#;
+    let errs = parse_and_check(src).expect_err("expected reverse of unknown residue to error");
+    assert!(
+        has_reverse_without_residue(&errs),
+        "reverse of an unbound name must raise ReverseWithoutResidue, got: {:?}",
+        errs
+    );
+}
+
+#[test]
+fn l10_phase3_double_reverse_named_is_error() {
+    // The named residue is consumed linearly: replaying it twice is rejected
+    // (the second `reverse undo` finds it already Spent).
+    let src = r#"@impure fn f() {
+        reversible as undo {
+            let x = 1
+        }
+        reverse undo
+        reverse undo
+    }"#;
+    let errs = parse_and_check(src).expect_err("expected the second `reverse undo` to error");
+    assert!(
+        has_reverse_without_residue(&errs),
+        "double `reverse undo` must raise ReverseWithoutResidue (linear use-at-most-once), got: {:?}",
+        errs
+    );
+}
+
+#[test]
+fn l10_phase3_unreversed_named_residue_is_not_an_error() {
+    // Affine: a named residue that is bound but never reversed is dropped at
+    // the body boundary, not flagged.
+    let src = r#"@impure fn f() {
+        reversible as undo {
+            let x = 1
+        }
+    }"#;
+    if let Err(errs) = parse_and_check(src) {
+        assert!(
+            !has_reverse_without_residue(&errs),
+            "a bound-but-unused named residue must NOT raise a reversibility error, got: {:?}",
+            errs
+        );
+    }
+}
+
+#[test]
+fn l10_phase3_named_residue_does_not_leak_across_functions() {
+    // A `reversible as undo` in one function must not license a `reverse undo`
+    // in another — named residues are scoped per body (cross-body carry is the
+    // next rung). The static-soundness guard for rung 3a.
+    let src = r#"@impure fn a() {
+        reversible as undo {
+            let x = 1
+        }
+    }
+    @impure fn b() {
+        reverse undo
+    }"#;
+    let errs = parse_and_check(src).expect_err("expected cross-function `reverse undo` to error");
+    assert!(
+        has_reverse_without_residue(&errs),
+        "named residue must not leak across functions; expected ReverseWithoutResidue, got: {:?}",
+        errs
+    );
+}
diff --git a/crates/oo7-typechecker-oracle/src/check.rs b/crates/oo7-typechecker-oracle/src/check.rs
index ad0db3c..fc06af4 100644
--- a/crates/oo7-typechecker-oracle/src/check.rs
+++ b/crates/oo7-typechecker-oracle/src/check.rs
@@ -538,7 +538,11 @@ fn check_stmt(env: &mut OracleEnv, stmt: &ControlStmt) -> OracleType {
             parity::skip(env, "break-continue");
             OracleType::Error
         }
-        ControlStmt::Reversible(_) | ControlStmt::Irreversible(_) | ControlStmt::Reverse(_) => {
+        ControlStmt::Reversible(_)
+        | ControlStmt::Irreversible(_)
+        | ControlStmt::Reverse(_)
+        | ControlStmt::ReversibleAs { .. }
+        | ControlStmt::ReverseNamed { .. } => {
             parity::skip(env, "reversible");
             OracleType::Error
         }
diff --git a/docs/echo-residue-integration.adoc b/docs/echo-residue-integration.adoc
index dccac9a..81adb12 100644
--- a/docs/echo-residue-integration.adoc
+++ b/docs/echo-residue-integration.adoc
@@ -143,23 +143,73 @@ linear strand (`EchoLinear.agda`) with 007's linear handles (`Type::Linear`,
 already carrying `LinearUsedTwice` / `LinearNotConsumed`), and matches agent
 ergonomics (agents already reason in linear handles).
 
-=== Still open → the next rung (cross-handler *named* residues)
-
-The type-level linearisation above is the foundation; the remaining work is
-to let a residue cross a *body boundary* by name. `examples/reversibility.007`
-performs `reversible` in an `on receive` handler and `reverse` in a separate
-`on error` handler — **cross-handler** reversal. The residue is agent
-*state*, so it must be *bound to a name* and stored, then consumed by the
-later handler. The formal model is already done (`ResidueCell` above); what
-is missing is **surface syntax**: a way to write `let undo = reversible {…}`
-and later `reverse undo`. Once the grammar carries a residue binding, the
-existing `LinearStatus::Linear` machinery enforces consume-exactly-once for
-free (`LinearUsedTwice` on double-reverse; the binding lives in agent state
-rather than a block-local scope). Because the grammar is Harvard-guarded
-(CI checks grammar changes), that binding syntax is its own carefully-scoped
-rung and is intentionally **not** bundled here. Until then, cross-handler
-reversal is conservatively rejected by the per-body isolation (sound, if
-incomplete).
+== What landed (phase 3 rung 3a — named residues, within a body)
+
+The phase-2 linearisation gave the residue a type; phase 3 gives it a *name*.
+Surface syntax now binds a residue and replays it by name:
+
+[source]
+----
+reversible as undo {        // bind this block's residue to `undo`
+  apply(m)
+}
+reverse undo                // replay it — consumes the residue exactly once
+----
+
+`reversible as <name> { … }` and `reverse <name>` are new control statements
+(the anonymous `reversible {…}` / `reverse {…}` forms are unchanged). The
+named residue is tracked per body as a `Holding(Linear<Echo<T>>)` cell that a
+`reverse` transitions to `Spent` — the static mirror of `ResidueCell`
+(`Holding`/`Spent`) in `EchoResidueLinear.idr`. The discipline is the same
+affine-capability / linear-consumption rule as phase 2:
+
+* **Linear consumption** — a second `reverse undo` finds the cell `Spent` and
+  is the reverse-without-residue error (replay at most once).
+* **Affine retention** — a `reversible as undo { … }` never followed by a
+  `reverse undo` is *not* an error; the cell is dropped at the body boundary.
+* **No leak** — named residues are scoped per body (isolated at function and
+  handler boundaries), so a `reverse undo` cannot reference a `reversible as
+  undo` in a *different* body. That is the soundness guard for rung 3a and the
+  seam where rung 3b takes over.
+
+[cols="1,3",options="header"]
+|===
+| Artefact | What
+
+| `crates/oo7-core/src/grammar.pest`, `spec/grammar.ebnf`
+| `reversible as <ident>` (optional binder) and `reverse_named = "reverse"
+  ident`. Harvard-safe (control rules referencing the shared `ident` token).
+
+| `crates/oo7-core/src/ast.rs`
+| Additive variants `ReversibleAs { binding, body }` and `ReverseNamed
+  { target }` (existing `Reversible`/`Reverse` untouched).
+
+| `crates/oo7-core/src/typechecker.rs`
+| Per-body `named_residues: HashMap<String, NamedResidueState>` with
+  `Holding(Type)`/`Spent`; `bind_named_residue` / `take_named_residue`;
+  the two `check_stmt` arms; per-function and per-handler isolation.
+
+| `crates/oo7-core/src/{parser,eval,formatter,dual_ast,metainterpreter,
+  codegen_*}.rs`, `semantic_analyser/control_flow.rs`, oracle `check.rs`
+| Parser builders + the additive match arms across the pipeline.
+
+| tests
+| 2 parser tests + 5 typechecker tests (bind+reverse ok; reverse-unknown errs;
+  double-reverse errs; un-reversed ok; no cross-function leak).
+|===
+
+=== Still open → rung 3b (cross-handler residues through agent state)
+
+Rung 3a is within a single body. The remaining work is to let a named residue
+cross a *body boundary* through agent **state** — the motivating case in
+`examples/reversibility.007`, where a `reversible` in `on receive` is replayed
+by a `reverse` in `on error`. This is irreducibly partly *runtime*: no static
+analysis knows whether `on receive` fired before `on error`, so the residue
+cell is checked at run time (the Idris `takeForReverse` returns `Maybe` —
+`Spent` reverses to `Nothing`). Rung 3b therefore adds: a residue cell in
+agent state, evaluator support for `reverse <name>` (runtime `Holding`/`Spent`
+matching `ResidueCell`), and the bridge lemma. The static name-resolution and
+affine discipline from rung 3a carry straight over.
 
 == Cross-repo bridge (echo-types)
 
diff --git a/spec/TYPE-SYSTEM-SPEC.adoc b/spec/TYPE-SYSTEM-SPEC.adoc
index 65bb9ab..c452891 100644
--- a/spec/TYPE-SYSTEM-SPEC.adoc
+++ b/spec/TYPE-SYSTEM-SPEC.adoc
@@ -736,12 +736,31 @@ residue is *not* an error). This is mechanised in
 `proofs/idris2/EchoResidueLinear.idr` (`reverseLinear` consumes
 `(1 e : Echo f y)`; `ResidueCell`'s `Spent` reverses to `Nothing`).
 
-The remaining rung is *cross-handler naming*: letting a residue cross a body
-boundary as a named value in agent state (`let undo = reversible {…}` … later
-`reverse undo`), so a `reverse` in one handler can replay a `reversible` in
-another. The formal model is in place (`ResidueCell`); only surface syntax is
-missing, and because grammar changes are Harvard-guarded it is a separate
-rung. See `docs/echo-residue-integration.adoc`.
+=== 11b.5 Named residues (phase 3, rung 3a)
+
+A residue may be *named* and replayed by name, within a body:
+
+[source]
+----
+reversible as undo { … }    // bind this block's residue to `undo`
+reverse undo                // replay it — consumes the residue exactly once
+----
+
+`reversible as <name> { … }` and `reverse <name>` are control statements (the
+anonymous forms are unchanged). The named residue is tracked per body as a
+`Holding(Linear<Echo<T>>)` cell that `reverse` transitions to `Spent` — the
+static mirror of `ResidueCell` in `EchoResidueLinear.idr`. The discipline is
+the same affine/linear rule: a second `reverse undo` (the cell is `Spent`) is
+the reverse-without-residue error; a never-replayed `reversible as undo` is
+*not* an error; and named residues are scoped per body, so a `reverse undo`
+cannot reach a `reversible as undo` in another body (the soundness guard).
+
+The remaining rung (3b) is *cross-handler* residues: carrying a named residue
+across a body boundary through agent **state**, so a `reverse` in one handler
+replays a `reversible` in another. That step is irreducibly partly run time
+(whether the earlier handler fired is not statically known — the Idris
+`takeForReverse` returns `Maybe`), so it adds evaluator support for runtime
+`Holding`/`Spent`. See `docs/echo-residue-integration.adoc`.
 
 == 12. The Layers in Concert
 
diff --git a/spec/grammar.ebnf b/spec/grammar.ebnf
index c122fc0..04204a5 100644
--- a/spec/grammar.ebnf
+++ b/spec/grammar.ebnf
@@ -143,6 +143,7 @@ control_stmt = let_binding
              | return_stmt
              | reversible_block
              | irreversible_block
+             | reverse_named
              | reverse_block
              | control_expr , ";" ;
 
@@ -469,10 +470,15 @@ capability = ident
 (* 13. REVERSIBILITY                                         *)
 (* ========================================================= *)
 
-reversible_block = "reversible" , "{" , { control_stmt } , "}" ;
+(* `reversible as <name> { ... }` binds the echo residue to <name> so a later
+   `reverse <name>` can replay it (L10 phase 3). Anonymous form unchanged. *)
+reversible_block = "reversible" , [ "as" , ident ] , "{" , { control_stmt } , "}" ;
 
 reverse_block = "reverse" , "{" , { control_stmt } , "}" ;
 
+(* `reverse <name>` replays the named residue bound by `reversible as <name>`. *)
+reverse_named = "reverse" , ident ;
+
 irreversible_block = "irreversible" , "{" , { control_stmt } , "}" ;
 
 (* ========================================================= *)