diff --git a/examples/1011-errors-value-failable.sx b/examples/1011-errors-value-failable.sx
index f410fea..621f946 100644
--- a/examples/1011-errors-value-failable.sx
+++ b/examples/1011-errors-value-failable.sx
@@ -19,9 +19,10 @@ parse :: (n: s32) -> (s32, !E) {
 main :: () -> s32 {
     r : s32 = 0;
 
+    // The value slot is live only where the error is proven absent (ERR E1.8):
+    // read `v1` under an `if !e1` guard, not after a bare tag-compare.
     v1, e1 := parse(5);                  // success → v1 = 50, e1 = no error
-    if e1 == error.Bad { r = r + 1000; }  // false
-    r = r + v1;                           // +50
+    if !e1 { r = r + v1; }                // success → +50
 
     v2, e2 := parse(-1);                 // Bad
     if e2 == error.Bad   { r = r + 7; }   // true  → +7
diff --git a/examples/1012-errors-value-failable-consume.sx b/examples/1012-errors-value-failable-consume.sx
index a5d4b23..3f3f56b 100644
--- a/examples/1012-errors-value-failable-consume.sx
+++ b/examples/1012-errors-value-failable-consume.sx
@@ -46,8 +46,7 @@ classify :: (n: s32) -> s32 {
 main :: () -> s32 {
     r : s32 = 0;
     a, ea := inc(5);                      // parse(5)=10 → v=10 → 11
-    if ea == error.Bad { r = r + 100; }   // false
-    r = r + a;                             // +11
+    if !ea { r = r + a; }                  // success → +11 (value live only when proven ok)
     b, eb := inc(-1);                      // parse(-1)=Bad → propagate {undef, Bad}
     if eb == error.Bad { r = r + 4; }      // true → +4
     er := relay(3);                        // parse(3)=6 ok → relay ok
diff --git a/examples/1018-errors-multi-value-failable.sx b/examples/1018-errors-multi-value-failable.sx
index 15d0b73..94adbc1 100644
--- a/examples/1018-errors-multi-value-failable.sx
+++ b/examples/1018-errors-multi-value-failable.sx
@@ -52,15 +52,13 @@ main :: () -> s32 {
     // Destructure binds EVERY slot including the error tag (e1 / e2 / e3) —
     // the error is treated, never dropped.
     v1, b1, e1 := parse(5);          // success → (10, 6, no-error)
-    if e1 == error.Bad { r = r + 1000; }  // false
-    r = r + v1 + b1;                 // +16
+    if !e1 { r = r + v1 + b1; }      // success → +16 (slots live only when proven ok)
 
     v2, b2, e2 := parse(-1);         // Bad → {undef, undef, Bad}
     if e2 == error.Bad { r = r + 4; }   // +4
 
     a, c, ea := inc(5);              // parse(5)=(10,6) → (11, 7, no-error)
-    if ea == error.Bad { r = r + 2000; }  // false
-    r = r + a + c;                   // +18
+    if !ea { r = r + a + c; }        // success → +18
 
     a2, c2, e3 := inc(-1);           // try parse(-1)=Bad → propagate {undef, undef, Bad}
     if e3 == error.Bad { r = r + 5; }   // +5
diff --git a/examples/1044-errors-generic-failable-composition.sx b/examples/1044-errors-generic-failable-composition.sx
index a107a4e..59e5b24 100644
--- a/examples/1044-errors-generic-failable-composition.sx
+++ b/examples/1044-errors-generic-failable-composition.sx
@@ -15,10 +15,10 @@ main :: () -> s32 {
     // success, consumed by catch
     print("catch={}\n", wrap(s32, closure(() -> (s32, !E) { return 7; })) catch e -1);   // 7
 
-    // success, consumed by destructure (binds value + error slot)
+    // success, consumed by destructure (binds value + error slot); the value
+    // slot is read only under an `if !err` guard (ERR E1.8 path-sensitivity)
     r, err := wrap(s32, closure(() -> (s32, !E) { return 9; }));
-    no_err := if err == error.Bad then false else true;
-    print("destr={} ok={}\n", r, no_err);                                                 // destr=9 ok=true
+    if !err { print("destr={} ok=true\n", r); }                                           // destr=9 ok=true
 
     // failure path: the raised tag propagates through the generic `try`
     print("fail={}\n", wrap(s32, closure(() -> (s32, !E) { raise error.Bad; }) ) catch e -1); // -1
diff --git a/examples/1046-errors-value-slot-liveness.sx b/examples/1046-errors-value-slot-liveness.sx
new file mode 100644
index 0000000..4aa1a35
--- /dev/null
+++ b/examples/1046-errors-value-slot-liveness.sx
@@ -0,0 +1,60 @@
+// Path-sensitive value-slot liveness (ERR step E1.8). After `v, err := f()`, the
+// value slot `v` is "live only where `err` is proven absent". Every read of `v`
+// below sits on a path where the compiler can prove `err == null`:
+//
+//   • `if !err { … v … }`            — proven inside the guard
+//   • `if err { return } … v …`      — proven on the fall-through
+//   • `if err { raise } … v …`       — fall-through in a failable function
+//   • `if err { … } else { … v … }`  — proven in the else branch
+//   • `!err and <reads v>`          — short-circuit keeps the proof
+//
+// A bare tag-compare (`if err == error.X`) proves NOTHING about absence — see the
+// rejection regression in 1047. (Regression for the E1.8 path-sensitive slice.)
+
+#import "modules/std.sx";
+
+E :: error { Bad, Empty }
+
+parse :: (n: s32) -> (s32, !E) {
+    if n < 0  { raise error.Bad; }
+    if n == 0 { raise error.Empty; }
+    return n * 10;
+}
+
+// Early-return guard: the fall-through proves `err` absent.
+guarded :: (n: s32) -> s32 {
+    v, err := parse(n);
+    if err { return -1; }
+    return v;                              // err proven absent here
+}
+
+// `if err { raise }` in a failable function: same fall-through proof.
+relay :: (n: s32) -> (s32, !E) {
+    v, err := parse(n);
+    if err { raise err; }
+    return v + 1;                          // err proven absent here
+}
+
+main :: () -> s32 {
+    total : s32 = 0;
+
+    // (1) proven inside `if !err`
+    v1, e1 := parse(5);
+    if !e1 { total = total + v1; }          // +50
+
+    // (2) proven in the else branch
+    v2, e2 := parse(7);
+    if e2 { total = total + 1; } else { total = total + v2; }  // +70
+
+    // (3) short-circuit `&&` keeps the proof for the rhs
+    v3, e3 := parse(3);
+    if !e3 and v3 > 0 { total = total + v3; }  // +30
+
+    // (4) early-return / raise helpers
+    total = total + guarded(4);             // +40
+    total = total + guarded(-1);            // -1
+    total = total + (relay(2) catch e 0);   // parse(2)=20 → +1 = 21
+
+    print("liveness total: {}\n", total);   // 50+70+30+40-1+21 = 210
+    return total;
+}
diff --git a/examples/1047-errors-value-slot-liveness-reject.sx b/examples/1047-errors-value-slot-liveness-reject.sx
new file mode 100644
index 0000000..bc1cfb9
--- /dev/null
+++ b/examples/1047-errors-value-slot-liveness-reject.sx
@@ -0,0 +1,35 @@
+// Rejection counterpart to 1046 (ERR step E1.8). Reading a failable's value slot
+// where its error is NOT proven absent is a compile error. Two unproven shapes:
+//
+//   (A) reading the value inside the `if err { … }` error path itself
+//   (B) reading the value after a bare tag-compare (`if err == error.X`), which
+//       narrows the tag but proves nothing about absence
+//
+// Each read is rejected with the E1.8 diagnostic; the program never runs (exit 1).
+
+#import "modules/std.sx";
+
+E :: error { Bad }
+
+parse :: (n: s32) -> (s32, !E) {
+    if n < 0 { raise error.Bad; }
+    return n * 10;
+}
+
+// (A) the read sits on the error path — `err` is present here, not absent.
+bad_a :: () -> s32 {
+    v, err := parse(5);
+    if err { return v; }                  // REJECTED: err present on this path
+    return 0;
+}
+
+// (B) a tag-compare narrows which error, but does not prove there is none.
+bad_b :: () -> s32 {
+    v, err := parse(5);
+    if err == error.Bad { return 1; }
+    return v;                             // REJECTED: err not proven absent
+}
+
+main :: () -> s32 {
+    return bad_a() + bad_b();
+}
diff --git a/examples/expected/1046-errors-value-slot-liveness.exit b/examples/expected/1046-errors-value-slot-liveness.exit
new file mode 100644
index 0000000..cd7da05
--- /dev/null
+++ b/examples/expected/1046-errors-value-slot-liveness.exit
@@ -0,0 +1 @@
+210
diff --git a/examples/expected/1046-errors-value-slot-liveness.stderr b/examples/expected/1046-errors-value-slot-liveness.stderr
new file mode 100644
index 0000000..8b13789
--- /dev/null
+++ b/examples/expected/1046-errors-value-slot-liveness.stderr
@@ -0,0 +1 @@
+
diff --git a/examples/expected/1046-errors-value-slot-liveness.stdout b/examples/expected/1046-errors-value-slot-liveness.stdout
new file mode 100644
index 0000000..1d50bce
--- /dev/null
+++ b/examples/expected/1046-errors-value-slot-liveness.stdout
@@ -0,0 +1 @@
+liveness total: 210
diff --git a/examples/expected/1047-errors-value-slot-liveness-reject.exit b/examples/expected/1047-errors-value-slot-liveness-reject.exit
new file mode 100644
index 0000000..d00491f
--- /dev/null
+++ b/examples/expected/1047-errors-value-slot-liveness-reject.exit
@@ -0,0 +1 @@
+1
diff --git a/examples/expected/1047-errors-value-slot-liveness-reject.stderr b/examples/expected/1047-errors-value-slot-liveness-reject.stderr
new file mode 100644
index 0000000..bdf7a17
--- /dev/null
+++ b/examples/expected/1047-errors-value-slot-liveness-reject.stderr
@@ -0,0 +1,11 @@
+error: value `v` from a failable can be used only where its error `err` is proven absent — guard the use with `if !err { … }`, or return early with `if err { return; }` before reading `v`
+  --> /Users/agra/projects/sx/examples/1047-errors-value-slot-liveness-reject.sx:22:21
+   |
+22 |     if err { return v; }                  // REJECTED: err present on this path
+   |                     ^
+
+error: value `v` from a failable can be used only where its error `err` is proven absent — guard the use with `if !err { … }`, or return early with `if err { return; }` before reading `v`
+  --> /Users/agra/projects/sx/examples/1047-errors-value-slot-liveness-reject.sx:30:12
+   |
+30 |     return v;                             // REJECTED: err not proven absent
+   |            ^
diff --git a/examples/expected/1047-errors-value-slot-liveness-reject.stdout b/examples/expected/1047-errors-value-slot-liveness-reject.stdout
new file mode 100644
index 0000000..8b13789
--- /dev/null
+++ b/examples/expected/1047-errors-value-slot-liveness-reject.stdout
@@ -0,0 +1 @@
+
diff --git a/src/ir/lower.zig b/src/ir/lower.zig
index cc0e090..c28d786 100644
--- a/src/ir/lower.zig
+++ b/src/ir/lower.zig
@@ -361,6 +361,12 @@ pub const Lowering = struct {
         // top-level sets; before body lowering so `try slot(x)` widening sees
         // the full per-shape union.
         self.convergeClosureShapeSets();
+        // Pass 1e: error-flow checks (ERR E1.8 value-slot liveness + E1.7
+        // cleanup-body absorption) over the main file's functions. Runs after
+        // the error-set convergence passes (so failable callees resolve) and
+        // before body lowering — purely a diagnostic pass; `core.zig` halts on
+        // any error before codegen.
+        self.checkErrorFlow(decls);
         // Pass 2: lower main (and comptime side-effects)
         self.lowerMainAndComptime(decls);
         // Pass 3: lower deferred functions (any_to_string etc.) now that all types are registered
@@ -440,6 +446,355 @@ pub const Lowering = struct {
         }
     }
 
+    // ── ERR E1.7 / E1.8 — error-flow analysis ───────────────────────────────
+    //
+    // One structured, path-sensitive walk over each MAIN-file function body
+    // (imported modules are trusted) drives two checks:
+    //
+    //  • E1.8 (value-slot liveness): a `v, err := failable()` destructure binds
+    //    `v` "live only where `err` is proven absent". A read of `v` is legal
+    //    iff `err` is proven null on the current path — established by
+    //    `if !err { … }` (proven inside) or `if err { return/raise }` (proven on
+    //    the fall-through). Error-set `==`/tag-compares do NOT prove absence.
+    //
+    //  • E1.7 (cleanup absorption): a bare failable call in a `defer`/`onfail`
+    //    body (with no `catch` / `or value`) is rejected — its error has nowhere
+    //    to propagate (the block is already exiting). See `checkCleanupBody`.
+
+    /// Per-function registration state for the flow walk. `bindings` maps each
+    /// failable value-slot variable to its partner error variable; `err_vars`
+    /// is the set of those error variables (so conditions over them refine the
+    /// proven-null set). Both are monotonic — entries are added as destructures
+    /// are encountered, never removed (out-of-scope names simply stop being read).
+    const FlowCtx = struct {
+        bindings: std.StringHashMap([]const u8),
+        err_vars: std.StringHashMap(void),
+    };
+
+    /// The proven-null set: error-variable names known to be absent on the
+    /// current path. Threaded by value-clone across branches; the join after an
+    /// `if` is the intersection of the reachable branches' sets.
+    const ProvenSet = std.ArrayList([]const u8);
+
+    fn provenHas(set: ProvenSet, name: []const u8) bool {
+        for (set.items) |n| if (std.mem.eql(u8, n, name)) return true;
+        return false;
+    }
+
+    fn provenAdd(self: *Lowering, set: *ProvenSet, name: []const u8) void {
+        if (!provenHas(set.*, name)) set.append(self.alloc, name) catch {};
+    }
+
+    fn provenClone(self: *Lowering, set: ProvenSet) ProvenSet {
+        var out = ProvenSet.empty;
+        out.appendSlice(self.alloc, set.items) catch {};
+        return out;
+    }
+
+    fn provenIntersect(self: *Lowering, a: ProvenSet, b: ProvenSet) ProvenSet {
+        var out = ProvenSet.empty;
+        for (a.items) |n| if (provenHas(b, n)) (out.append(self.alloc, n) catch {});
+        return out;
+    }
+
+    /// Pass 1e: run the error-flow checks over every function defined in the
+    /// main file. Library modules are assumed well-formed (and may use patterns
+    /// this conservative check would over-reject), so they are skipped.
+    fn checkErrorFlow(self: *Lowering, decls: []const *const Node) void {
+        if (self.diagnostics == null) return;
+        for (decls) |decl| {
+            if (self.main_file) |mf| {
+                if (decl.source_file) |sf| {
+                    if (!std.mem.eql(u8, sf, mf)) continue;
+                }
+            }
+            switch (decl.data) {
+                .fn_decl => |fd| self.analyzeFnBody(fd.body),
+                .const_decl => |cd| {
+                    if (cd.value.data == .fn_decl) self.analyzeFnBody(cd.value.data.fn_decl.body);
+                },
+                else => {},
+            }
+        }
+    }
+
+    /// Analyze one function (or lambda) body as its own boundary — a fresh
+    /// binding context and an empty proven set.
+    fn analyzeFnBody(self: *Lowering, body: *const Node) void {
+        var ctx = FlowCtx{
+            .bindings = std.StringHashMap([]const u8).init(self.alloc),
+            .err_vars = std.StringHashMap(void).init(self.alloc),
+        };
+        var proven = ProvenSet.empty;
+        _ = self.flowWalk(body, &ctx, &proven);
+    }
+
+    /// Walk a block or single statement. Returns whether control always
+    /// diverges (every path ends in return/raise/break/continue) — used by the
+    /// caller to mark code after a branch unreachable.
+    fn flowWalk(self: *Lowering, node: *const Node, ctx: *FlowCtx, proven: *ProvenSet) bool {
+        switch (node.data) {
+            .block => |b| {
+                for (b.stmts) |s| if (self.flowStmt(s, ctx, proven)) return true;
+                return false;
+            },
+            else => return self.flowStmt(node, ctx, proven),
+        }
+    }
+
+    fn flowStmt(self: *Lowering, node: *const Node, ctx: *FlowCtx, proven: *ProvenSet) bool {
+        switch (node.data) {
+            .destructure_decl => |dd| {
+                self.flowExpr(dd.value, ctx, proven.*);
+                self.registerFailableDestructure(&dd, ctx);
+                return false;
+            },
+            .var_decl => |vd| {
+                if (vd.value) |v| self.flowExpr(v, ctx, proven.*);
+                return false;
+            },
+            .const_decl => |cd| {
+                self.flowExpr(cd.value, ctx, proven.*);
+                return false;
+            },
+            .assignment => |a| {
+                self.flowExpr(a.value, ctx, proven.*);
+                self.flowExpr(a.target, ctx, proven.*);
+                return false;
+            },
+            .multi_assign => |ma| {
+                for (ma.values) |v| self.flowExpr(v, ctx, proven.*);
+                return false;
+            },
+            .return_stmt => |r| {
+                if (r.value) |v| self.flowExpr(v, ctx, proven.*);
+                return true;
+            },
+            .raise_stmt => |rs| {
+                self.flowExpr(rs.tag, ctx, proven.*);
+                return true;
+            },
+            .break_expr, .continue_expr => return true,
+            .if_expr => |ie| return self.flowIf(&ie, ctx, proven),
+            .while_expr => |we| {
+                self.flowExpr(we.condition, ctx, proven.*);
+                var loop_proven = self.provenClone(proven.*);
+                _ = self.flowWalk(we.body, ctx, &loop_proven);
+                return false;
+            },
+            .for_expr => |fe| {
+                self.flowExpr(fe.iterable, ctx, proven.*);
+                if (fe.range_end) |re| self.flowExpr(re, ctx, proven.*);
+                var loop_proven = self.provenClone(proven.*);
+                _ = self.flowWalk(fe.body, ctx, &loop_proven);
+                return false;
+            },
+            .match_expr => |me| return self.flowMatch(&me, ctx, proven),
+            .push_stmt => |ps| {
+                self.flowExpr(ps.context_expr, ctx, proven.*);
+                var inner = self.provenClone(proven.*);
+                _ = self.flowWalk(ps.body, ctx, &inner);
+                return false;
+            },
+            .defer_stmt => |ds| {
+                self.checkCleanupBody(ds.expr, "defer");
+                self.flowExpr(ds.expr, ctx, proven.*);
+                return false;
+            },
+            .onfail_stmt => |os| {
+                self.checkCleanupBody(os.body, "onfail");
+                self.flowExpr(os.body, ctx, proven.*);
+                return false;
+            },
+            else => {
+                self.flowExpr(node, ctx, proven.*);
+                return false;
+            },
+        }
+    }
+
+    /// Path-sensitive `if`: refine the proven set on each branch, recurse, and
+    /// join the reachable fall-through states by intersection.
+    fn flowIf(self: *Lowering, ie: *const ast.IfExpr, ctx: *FlowCtx, proven: *ProvenSet) bool {
+        self.flowExpr(ie.condition, ctx, proven.*);
+        var then_proven = self.provenClone(proven.*);
+        var else_proven = self.provenClone(proven.*);
+        self.applyRefinement(ie.condition, true, ctx, &then_proven);
+        self.applyRefinement(ie.condition, false, ctx, &else_proven);
+
+        const then_div = self.flowWalk(ie.then_branch, ctx, &then_proven);
+        var else_div = false;
+        if (ie.else_branch) |eb| else_div = self.flowWalk(eb, ctx, &else_proven);
+
+        // Reachable fall-through contributors: a branch that doesn't diverge,
+        // plus the implicit (empty) else when there is no `else`.
+        var contributors = std.ArrayList(ProvenSet).empty;
+        if (!then_div) contributors.append(self.alloc, then_proven) catch {};
+        if (ie.else_branch != null) {
+            if (!else_div) contributors.append(self.alloc, else_proven) catch {};
+        } else {
+            contributors.append(self.alloc, else_proven) catch {};
+        }
+        if (contributors.items.len == 0) return true; // both branches diverge
+
+        var result = self.provenClone(contributors.items[0]);
+        for (contributors.items[1..]) |c| result = self.provenIntersect(result, c);
+        proven.* = result;
+        return false;
+    }
+
+    /// Refine the proven-null set for a branch taken when `cond` is `want_true`.
+    /// A bare error-variable is truthy when it HOLDS an error, so its falsy edge
+    /// proves absence; `!`, `&&`, `||` compose. Tag/equality compares prove
+    /// nothing (error-set `==` compares tags, not presence).
+    fn applyRefinement(self: *Lowering, cond: *const Node, want_true: bool, ctx: *FlowCtx, set: *ProvenSet) void {
+        switch (cond.data) {
+            .identifier => |id| {
+                if (ctx.err_vars.contains(id.name) and !want_true) self.provenAdd(set, id.name);
+            },
+            .unary_op => |uop| {
+                if (uop.op == .not) self.applyRefinement(uop.operand, !want_true, ctx, set);
+            },
+            .binary_op => |bop| {
+                if (bop.op == .and_op and want_true) {
+                    self.applyRefinement(bop.lhs, true, ctx, set);
+                    self.applyRefinement(bop.rhs, true, ctx, set);
+                } else if (bop.op == .or_op and !want_true) {
+                    self.applyRefinement(bop.lhs, false, ctx, set);
+                    self.applyRefinement(bop.rhs, false, ctx, set);
+                }
+            },
+            else => {},
+        }
+    }
+
+    fn flowMatch(self: *Lowering, me: *const ast.MatchExpr, ctx: *FlowCtx, proven: *ProvenSet) bool {
+        self.flowExpr(me.subject, ctx, proven.*);
+        for (me.arms) |arm| {
+            var arm_proven = self.provenClone(proven.*);
+            _ = self.flowWalk(arm.body, ctx, &arm_proven);
+        }
+        return false;
+    }
+
+    /// Check an expression for reads of a still-tainted value-slot variable and
+    /// recurse into nested lambdas as their own boundaries. `proven` is by value
+    /// — sub-expressions never publish proven-null facts back to the statement.
+    fn flowExpr(self: *Lowering, node: *const Node, ctx: *FlowCtx, proven: ProvenSet) void {
+        switch (node.data) {
+            .identifier => |id| {
+                if (ctx.bindings.get(id.name)) |err_var| {
+                    if (!provenHas(proven, err_var)) {
+                        if (self.diagnostics) |d| d.addFmt(.err, node.span, "value `{s}` from a failable can be used only where its error `{s}` is proven absent — guard the use with `if !{s} {{ … }}`, or return early with `if {s} {{ return; }}` before reading `{s}`", .{ id.name, err_var, err_var, err_var, id.name });
+                    }
+                }
+            },
+            .lambda => |lam| self.analyzeFnBody(lam.body),
+            .binary_op => |b| {
+                self.flowExpr(b.lhs, ctx, proven);
+                // Short-circuit: the rhs of `&&` runs only when the lhs is true
+                // (and `||`'s rhs only when the lhs is false), so refine the
+                // proven-null set accordingly before checking it. This is what
+                // makes `if !err && use(v)` legal.
+                if (b.op == .and_op or b.op == .or_op) {
+                    var rp = self.provenClone(proven);
+                    self.applyRefinement(b.lhs, b.op == .and_op, ctx, &rp);
+                    self.flowExpr(b.rhs, ctx, rp);
+                } else {
+                    self.flowExpr(b.rhs, ctx, proven);
+                }
+            },
+            .chained_comparison => |cc| {
+                for (cc.operands) |op| self.flowExpr(op, ctx, proven);
+            },
+            .unary_op => |u| self.flowExpr(u.operand, ctx, proven),
+            .call => |c| {
+                self.flowExpr(c.callee, ctx, proven);
+                for (c.args) |a| self.flowExpr(a, ctx, proven);
+            },
+            .field_access => |fa| self.flowExpr(fa.object, ctx, proven),
+            .index_expr => |ix| {
+                self.flowExpr(ix.object, ctx, proven);
+                self.flowExpr(ix.index, ctx, proven);
+            },
+            .slice_expr => |se| {
+                self.flowExpr(se.object, ctx, proven);
+                if (se.start) |s| self.flowExpr(s, ctx, proven);
+                if (se.end) |e| self.flowExpr(e, ctx, proven);
+            },
+            .try_expr => |te| self.flowExpr(te.operand, ctx, proven),
+            .catch_expr => |ce| {
+                self.flowExpr(ce.operand, ctx, proven);
+                self.flowExpr(ce.body, ctx, proven);
+            },
+            .force_unwrap => |fu| self.flowExpr(fu.operand, ctx, proven),
+            .null_coalesce => |nc| {
+                self.flowExpr(nc.lhs, ctx, proven);
+                self.flowExpr(nc.rhs, ctx, proven);
+            },
+            .deref_expr => |de| self.flowExpr(de.operand, ctx, proven),
+            .comptime_expr => |ce| self.flowExpr(ce.expr, ctx, proven),
+            .insert_expr => |ie| self.flowExpr(ie.expr, ctx, proven),
+            .spread_expr => |se| self.flowExpr(se.operand, ctx, proven),
+            .struct_literal => |sl| {
+                for (sl.field_inits) |fi| self.flowExpr(fi.value, ctx, proven);
+            },
+            .array_literal => |al| {
+                for (al.elements) |el| self.flowExpr(el, ctx, proven);
+            },
+            .tuple_literal => |tl| {
+                for (tl.elements) |el| self.flowExpr(el.value, ctx, proven);
+            },
+            .if_expr => |ie| {
+                var tmp = self.provenClone(proven);
+                _ = self.flowIf(&ie, ctx, &tmp);
+            },
+            .match_expr => |me| {
+                var tmp = self.provenClone(proven);
+                _ = self.flowMatch(&me, ctx, &tmp);
+            },
+            .block => |b| {
+                var tmp = self.provenClone(proven);
+                for (b.stmts) |s| if (self.flowStmt(s, ctx, &tmp)) break;
+            },
+            else => {},
+        }
+    }
+
+    /// Register a `v…, err := failable()` destructure. Only a complete bare
+    /// destructure (every slot bound, error slot a real name) creates taint —
+    /// an omitted or `_`-bound error slot is already rejected by the discard
+    /// check in `lowerDestructureDecl`, so it produces no proof obligation here.
+    fn registerFailableDestructure(self: *Lowering, dd: *const ast.DestructureDecl, ctx: *FlowCtx) void {
+        const ty = self.inferExprType(dd.value);
+        if (self.errorChannelOf(ty) == null) return;
+        if (ty.isBuiltin()) return;
+        const ti = self.module.types.get(ty);
+        if (ti != .tuple) return;
+        const fields = ti.tuple.fields;
+        if (dd.names.len != fields.len) return;
+        const err_name = dd.names[fields.len - 1];
+        if (std.mem.eql(u8, err_name, "_")) return;
+        ctx.err_vars.put(err_name, {}) catch {};
+        var i: usize = 0;
+        while (i + 1 < dd.names.len) : (i += 1) {
+            const vn = dd.names[i];
+            if (std.mem.eql(u8, vn, "_")) continue;
+            ctx.bindings.put(vn, err_name) catch {};
+        }
+    }
+
+    /// E1.7: a `defer`/`onfail` body runs while the block is already exiting, so
+    /// a bare failable call has nowhere to send its error. Reject any failable
+    /// expression-statement that isn't absorbed locally by `catch` / `or value`
+    /// / a destructure binding. (Parser already bans `try`/`raise`/`return`/
+    /// `break`/`continue` here.) Stub until slice B.
+    fn checkCleanupBody(self: *Lowering, body: *const Node, kind: []const u8) void {
+        _ = self;
+        _ = body;
+        _ = kind;
+    }
+
     /// On Android, the OS loads the .so via a Java-side Activity declared
     /// with `#jni_main #jni_class("...")`. The Java class drives the
     /// lifecycle (onCreate / onPause / etc.) and sx provides the native