diff --git a/Strata/DL/Imperative/ExitProperties.lean b/Strata/DL/Imperative/ExitProperties.lean
new file mode 100644
index 0000000000..bc4a48c4ac
--- /dev/null
+++ b/Strata/DL/Imperative/ExitProperties.lean
@@ -0,0 +1,120 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.DL.Imperative.StmtSemantics
+
+/-!
+# Exit Semantics: Per-Transition Named Lemmas
+
+Thin wrappers over `StepStmt` constructors that give each exit-related
+transition a descriptive name, so downstream proofs can cite the
+transition by intent rather than by constructor tag.
+
+See `docs/design/exit-semantics/spec.md` §4.1 and §4.2.
+-/
+
+namespace Imperative
+
+section ExitProperties
+
+variable {P : PureExpr} {CmdT : Type} {EvalCmd : EvalCmdParam P CmdT}
+  {extendEval : ExtendEval P}
+  [HasBool P] [HasNot P]
+
+/-- An `exit` statement steps to `.exiting` carrying the same environment.
+    Realizes spec §4.1 row 1. -/
+public theorem exit_preserves_env (label : Option String) (md : MetaData P) (ρ : Env P) :
+    StepStmt P EvalCmd extendEval
+      (.stmt (.exit label md) ρ)
+      (.exiting label ρ) :=
+  .step_exit
+
+/-- When a `seq` configuration's inner part has become `.exiting`,
+    the remaining statements do not execute — the seq as a whole
+    steps directly to `.exiting`.
+    Realizes spec §4.1 row 2. -/
+public theorem exit_skips_remaining (label : Option String) (ρ' : Env P)
+    (ss : List (Stmt P CmdT)) :
+    StepStmt P EvalCmd extendEval
+      (.seq (.exiting label ρ') ss)
+      (.exiting label ρ') :=
+  .step_seq_exit
+
+/-- A labeled block whose body has reached `.exiting (some L)`
+    where `L` matches the block's label steps to `.terminal`,
+    consuming the exit.
+    Realizes spec §4.1 row 3. -/
+public theorem matching_block_consumes (L : String) (ρ' : Env P) :
+    StepStmt P EvalCmd extendEval
+      (.block (.some L) (.exiting (.some L) ρ'))
+      (.terminal ρ') :=
+  .step_block_exit_match rfl
+
+/-- A labeled block whose body has reached `.exiting (some M)`
+    where the block's label does not equal `some M`
+    propagates the exit unchanged.
+    Realizes spec §4.1 row 4. -/
+public theorem nonmatching_exit_propagates
+    (blockLabel : Option String) (M : String) (ρ' : Env P)
+    (Hne : blockLabel ≠ .some M) :
+    StepStmt P EvalCmd extendEval
+      (.block blockLabel (.exiting (.some M) ρ'))
+      (.exiting (.some M) ρ') :=
+  .step_block_exit_mismatch Hne
+
+/-- A block whose body has reached `.terminal`
+    steps to `.terminal`.
+    Realizes spec §4.1 row 5. -/
+public theorem normal_block_completion (label : Option String) (ρ' : Env P) :
+    StepStmt P EvalCmd extendEval
+      (.block label (.terminal ρ'))
+      (.terminal ρ') :=
+  .step_block_done
+
+/-- A block whose body has reached `.exiting none`
+    steps to `.terminal`. An unlabeled exit is consumed by any
+    enclosing block regardless of the block's own label.
+    Realizes spec §4.1 row 6. -/
+public theorem unlabeled_exit_consumed (label : Option String) (ρ' : Env P) :
+    StepStmt P EvalCmd extendEval
+      (.block label (.exiting .none ρ'))
+      (.terminal ρ') :=
+  .step_block_exit_none
+
+/-- A block context propagates inner steps.
+    Realizes spec §4.1 row 7. -/
+public theorem block_body_steps (label : Option String)
+    (inner inner' : Config P CmdT)
+    (H : StepStmt P EvalCmd extendEval inner inner') :
+    StepStmt P EvalCmd extendEval
+      (.block label inner)
+      (.block label inner') :=
+  .step_block_body H
+
+/-! ### Multi-step companions
+
+Reflexive-transitive closure variants used when composing with
+downstream proofs that track `StepStmtStar` rather than single steps.
+-/
+
+/-- `.stmt (.exit label md) ρ  →*  .exiting label ρ` -/
+public theorem exit_eval (label : Option String) (md : MetaData P) (ρ : Env P) :
+    StepStmtStar P EvalCmd extendEval
+      (.stmt (.exit label md) ρ)
+      (.exiting label ρ) :=
+  .step _ _ _ .step_exit (.refl _)
+
+/-- `.block (some L) (.exiting (some L) ρ')  →*  .terminal ρ'` -/
+public theorem matching_block_eval (L : String) (ρ' : Env P) :
+    StepStmtStar P EvalCmd extendEval
+      (.block (.some L) (.exiting (.some L) ρ'))
+      (.terminal ρ') :=
+  .step _ _ _ (.step_block_exit_match rfl) (.refl _)
+
+end ExitProperties
+
+end Imperative
diff --git a/Strata/DL/Imperative/ExitWellFormedness.lean b/Strata/DL/Imperative/ExitWellFormedness.lean
new file mode 100644
index 0000000000..c5bfcca15d
--- /dev/null
+++ b/Strata/DL/Imperative/ExitWellFormedness.lean
@@ -0,0 +1,52 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.DL.Imperative.Stmt
+
+/-!
+# Exit Semantics: Structural Properties of Well-Formedness
+
+Thin wrappers over `Stmt.exitsCoveredByBlocks` that give the structural
+consequences of well-formedness descriptive names,
+so downstream proofs can cite them directly.
+
+See `docs/design/exit-semantics/spec.md` §4.2.
+-/
+
+namespace Imperative
+
+section WellFormedness
+
+variable {P : PureExpr} {CmdT : Type}
+
+/-- Under well-formedness,
+    every `exit (some L)` sub-statement has its label
+    present in the enclosing label list.
+
+    This follows directly from the definition of
+    `Stmt.exitsCoveredByBlocks` —
+    the `.exit (some l) _` case reduces to `some l ∈ labels`.
+
+    Realizes spec §4.2. -/
+public theorem exit_target_in_labels
+    {labels : List (Option String)} {L : String} {md : MetaData P}
+    (hwf : @Stmt.exitsCoveredByBlocks P CmdT labels (.exit (.some L) md)) :
+    .some L ∈ labels := hwf
+
+/-- Under well-formedness,
+    every `exit none` sub-statement has a non-empty enclosing label list.
+
+    Like `exit_target_in_labels`, this follows directly from the
+    definition of `Stmt.exitsCoveredByBlocks`. -/
+public theorem exit_none_has_enclosing
+    {labels : List (Option String)} {md : MetaData P}
+    (hwf : @Stmt.exitsCoveredByBlocks P CmdT labels (.exit .none md)) :
+    labels.length > 0 := hwf
+
+end WellFormedness
+
+end Imperative
diff --git a/Strata/DL/Imperative/StmtSemantics.lean b/Strata/DL/Imperative/StmtSemantics.lean
index 3b9da68ab7..f310623906 100644
--- a/Strata/DL/Imperative/StmtSemantics.lean
+++ b/Strata/DL/Imperative/StmtSemantics.lean
@@ -818,7 +818,7 @@ theorem smallStep_hasFailure_irrel
 /-! ## Well-paired exits: preservation and no-escape -/
 
 /-- A single step preserves `Config.exitsCoveredByBlocks`. -/
-private theorem step_preserves_exitsCoveredByBlocks
+public theorem step_preserves_exitsCoveredByBlocks
     (labels : List (Option String))
     (c₁ c₂ : Config P CmdT)
     (hstep : StepStmt P EvalCmd extendEval c₁ c₂)
diff --git a/docs/design/exit-semantics/README.md b/docs/design/exit-semantics/README.md
new file mode 100644
index 0000000000..bfdde4f4c9
--- /dev/null
+++ b/docs/design/exit-semantics/README.md
@@ -0,0 +1,18 @@
+# Exit Semantics
+
+Design documentation for `exit` and labeled-block semantics
+in Strata's Imperative dialect.
+
+- [`spec.md`](./spec.md) —
+  formal specification with RFC 2119 normative statements
+  and pointers to the existing Lean theorems that discharge them.
+- [`decisions.md`](./decisions.md) —
+  the design decisions made,
+  the options considered,
+  and the tradeoffs.
+
+This contribution adds documentation only —
+all cited theorems already exist in upstream main.
+
+Tracked as
+[#993](https://github.com/strata-org/Strata/issues/993).
diff --git a/docs/design/exit-semantics/decisions.md b/docs/design/exit-semantics/decisions.md
new file mode 100644
index 0000000000..6f712e8816
--- /dev/null
+++ b/docs/design/exit-semantics/decisions.md
@@ -0,0 +1,290 @@
+# Exit Semantics: Design Decisions
+
+**Date:** 2026-04-22
+**Status:** Proposed
+
+## Decision 1: Where is exit state represented?
+
+**Context.**
+The formal semantics needs to record
+whether a configuration is currently "propagating an exit."
+That information has to live somewhere.
+
+**Options.**
+- (A) A dedicated `Config` constructor, `.exiting (label) (env)`,
+  alongside `.stmt`, `.stmts`, `.terminal`, `.block`, `.seq`.
+- (B) A flag on `Env` (parallel to the existing `.error` flag).
+- (C) A separate `BlockResult` inductive that accompanies each relation,
+  as used in some big-step formalisms.
+
+**Tradeoffs.**
+(A) keeps exit as a first-class control-flow state,
+distinct from the data carried by the store and the evaluator.
+The semantics pattern-matches on the `Config` shape
+to decide which step rule applies,
+and `.exiting` is one of those shapes.
+
+(B) would make step rules shorter
+(no extra `Config` case)
+but couples control flow to data.
+Properties like "exit does not modify the store"
+become statements about the flag,
+not about the shape of the configuration.
+
+(C) was the form in an earlier big-step draft.
+It disappeared when upstream removed big-step (#806).
+Returning to it would require re-introducing a relation layer
+that the project has deliberately left behind.
+
+**Decision.**
+(A) —
+exit state is a `Config` constructor.
+
+The small-step semantics already uses this shape,
+and #869's review converged on reusing `CoreConfig`
+(the Core-level instantiation of this `Config`)
+rather than introducing a parallel `StepResult`.
+Our proofs build directly on it.
+
+Moving exit state onto `Env` is a possible future refactor
+but is out of scope here.
+
+## Decision 2: Exit inside loops propagates out
+
+**Context.**
+The type checker permits `exit` inside a loop body.
+A loop body is not itself a labeled block,
+so an exit reaching the loop body's end has nowhere to be consumed
+by the loop itself.
+
+**Options.**
+- (A) The loop terminates immediately
+  and propagates the exit outward.
+- (B) Reject programs with `exit` inside loops.
+
+**Tradeoffs.**
+(A) matches the operational evaluator
+and matches source-language semantics
+(Java `break` / `continue` desugar to `exit`;
+early `return` inside a loop desugars to `exit $body`).
+
+(B) would break Python `try`/`except` and every language
+that depends on control flow escaping loops.
+
+**Decision.**
+(A) —
+an exit reaching a loop body's boundary propagates out of the loop.
+
+The small-step relation already realizes this
+via `step_loop_exit` and `step_loop_nondet_exit`.
+No new step rules are needed for this decision.
+
+## Decision 3: Well-formedness is `exitsCoveredByBlocks`
+
+**Context.**
+The theorems about exit need a predicate characterizing
+"programs where every exit has a matching enclosing block."
+
+Upstream `Stmt.lean` and `StmtSemantics.lean` already define
+`Stmt.exitsCoveredByBlocks : List String → Stmt P CmdT → Prop`
+and its `Config.exitsCoveredByBlocks` lift,
+along with helper theorems
+`step_preserves_exitsCoveredByBlocks`
+and `exitsCoveredByBlocks_noEscape`.
+
+An earlier draft of this proposal introduced a new inductive
+`WFLabels` with the same coverage semantics
+plus an additional no-shadowing constraint.
+
+**Options.**
+- (A) Use upstream's `exitsCoveredByBlocks` as the well-formedness predicate.
+- (B) Introduce a new inductive `WFLabels` with the same coverage semantics.
+- (C) Introduce `WFLabels` as a strictly stronger predicate
+  (adding no-shadowing on top of coverage).
+
+**Tradeoffs.**
+(A) reuses proven machinery, avoids duplication,
+and keeps this contribution aligned with the rest of the codebase.
+A downside is that `exitsCoveredByBlocks` is a recursive function,
+which is sometimes less ergonomic for structural induction
+than an inductive predicate.
+
+(B) would duplicate upstream code
+and invite drift between the two predicates.
+No new guarantees are produced.
+
+(C) separates concerns cleanly
+(coverage vs shadowing)
+but adds a predicate whose only consumer at the moment
+would be the no-shadowing lemma itself.
+No current downstream consumer requires no-shadowing
+to reason about its programs.
+
+**Decision.**
+(A) —
+use upstream's `exitsCoveredByBlocks`.
+
+No-shadowing is not required by any consumer today.
+If a downstream proof needs it,
+a focused `NoLabelShadowing` predicate can be added later
+without affecting the properties documented here.
+
+## Decision 4: Theorem naming uses descriptive names only
+
+**Context.**
+An earlier draft used identifiers like "E1" through "E9"
+both as theorem names and as cross-references in design docs.
+
+**Options.**
+- (A) Descriptive snake_case names
+  (`matching_block_consumes`, `nonmatching_exit_propagates`, …).
+- (B) E-numbered names
+  (`E1_preserves_env`, `E3_matching_block_consumes`, …).
+- (C) Descriptive names in code,
+  E-numbers preserved in docstrings and design docs
+  as stable handles.
+
+**Tradeoffs.**
+(A) reads naturally in Lean code
+and matches CONTRIBUTING.md's snake_case convention.
+
+(B) makes cross-referencing trivial
+but turns Lean code into number soup.
+
+(C) duplicates information
+and creates a drift risk
+between doc numbers and code names.
+
+**Decision.**
+(A) —
+descriptive names only.
+
+Reviewer feedback on #993 explicitly preferred this.
+Cross-references in docs cite theorem names directly.
+
+## Decision 5: No new proof files are required for this contribution
+
+**Context.**
+The initial proposal planned three new files under
+`Strata/DL/Imperative/`:
+`ExitProperties.lean`,
+`ExitWellFormedness.lean`,
+and a new `ExitCompleteness.lean`
+for the no-escape theorem.
+
+On examination,
+upstream `StmtSemantics.lean` already contains
+`step_preserves_exitsCoveredByBlocks`
+and `exitsCoveredByBlocks_noEscape`
+(plus `block_exitsCoveredByBlocks_noEscape` for statement lists),
+along with the per-transition step rules
+that the proposed `ExitProperties.lean` theorems
+would simply restate as named lemmas.
+
+**Options.**
+- (A) Ship this contribution as documentation only,
+  citing the upstream theorems by their existing names.
+- (B) Add a thin file of renamed aliases
+  (`matching_block_consumes := step_block_exit_match` etc.)
+  for ergonomic downstream use.
+- (C) Write and land the three proof files as originally proposed,
+  duplicating upstream.
+
+**Tradeoffs.**
+(A) is the smallest possible change
+and acknowledges that the proofs we intended to write already exist.
+
+(B) adds a layer of indirection.
+Some downstream consumers may prefer descriptive names,
+but introducing aliases without a consumer asking for them
+is premature.
+
+(C) duplicates existing code
+and contradicts Decision 3.
+
+**Decision.**
+(B) —
+add thin named-wrapper files.
+
+The wrappers (`exit_preserves_env`, `matching_block_consumes`,
+`nonmatching_exit_propagates`, and so on)
+live in `Strata/DL/Imperative/ExitProperties.lean` and
+`Strata/DL/Imperative/ExitWellFormedness.lean`.
+Each is a one-line proof over the corresponding `StepStmt` constructor
+or `Stmt.exitsCoveredByBlocks` definitional equation.
+
+The contribution additionally promotes
+`step_preserves_exitsCoveredByBlocks` from private to public,
+so §4.3's requirement cites a public symbol.
+
+## Decision 6: Global completeness is preservation, not liveness
+
+**Context.**
+An informal claim appears in multiple places:
+*"an exit never escapes the procedure body in a well-formed program."*
+The claim can be made formal in more than one way.
+
+**Options.**
+- (A) Preservation (safety).
+  No reachable configuration from a well-formed procedure body
+  is outer-`.exiting`.
+- (B) Progress (liveness).
+  Every `.exiting` reached inside the body is eventually consumed,
+  leading to `.terminal`.
+- (C) Both, as paired lemmas.
+
+**Tradeoffs.**
+(A) is what reviewers literally asked
+and what #869's concrete interpreter needs
+to justify treating escaped exits as unreachable.
+
+(B) is stronger
+but requires a termination argument orthogonal to exit semantics.
+It is a substantially larger undertaking
+and is not needed by any known downstream consumer.
+
+(C) combines the burden of (B) with the value of (A).
+Useful eventually,
+not worth blocking this work on.
+
+**Decision.**
+(A) —
+use preservation.
+
+Upstream's `exitsCoveredByBlocks_noEscape`
+already proves preservation
+for a starting `Stmt`,
+and `block_exitsCoveredByBlocks_noEscape` does the same
+for a starting `.stmts`.
+This contribution points at those theorems
+rather than introducing a new one.
+
+Liveness can be added later as a separate theorem
+if a downstream consumer requires it.
+The spec's "future work" section
+notes that liveness is deliberately out of scope.
+
+## Future work
+
+The following are deliberately out of scope for this work
+and are recorded here for future reference.
+
+- **Liveness** (Decision 6, option B).
+  A consumer that needs to know every exit *eventually* reaches
+  a matching block
+  will need a companion theorem
+  and a termination argument.
+
+- **Exit state on `Env`** (Decision 1, option B).
+  If the Core interpreter (#869)
+  or a later refactor
+  wants exit state to live on `Env`,
+  that is a larger change
+  that would revisit every step rule
+  and every proof in the affected files.
+
+- **No-label-shadowing predicate** (Decision 3, option C).
+  If a downstream consumer needs to reason about programs
+  in which inner block labels cannot shadow outer ones,
+  a `NoLabelShadowing` predicate can be added
+  alongside `exitsCoveredByBlocks`.
diff --git a/docs/design/exit-semantics/spec.md b/docs/design/exit-semantics/spec.md
new file mode 100644
index 0000000000..1dcafeedb1
--- /dev/null
+++ b/docs/design/exit-semantics/spec.md
@@ -0,0 +1,235 @@
+# Exit Semantics: Formal Specification
+
+**Date:** 2026-04-22
+**Status:** Proposed
+
+The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT",
+"SHOULD", "SHOULD NOT", "RECOMMENDED", "MAY", and "OPTIONAL"
+in this document are to be interpreted as described in RFC 2119.
+
+## 1. Context
+
+The small-step operational semantics
+in `Strata/DL/Imperative/StmtSemantics.lean`
+implements `exit` and labeled blocks
+through a dedicated `Config.exiting` constructor
+and a family of step rules
+(`step_exit`, `step_block_exit_*`, `step_seq_exit`, `step_block_body`, …).
+
+This specification documents that behavior
+and lists the properties the semantics satisfies.
+It makes the existing semantics
+explicit and citable
+so contributors and downstream features
+can build on a proven foundation
+rather than re-deriving control-flow facts.
+
+## 2. Definitions
+
+### 2.1 Configurations
+
+A configuration is one of:
+
+| Shape | Meaning |
+|---|---|
+| `.stmt s env` | about to execute statement `s` |
+| `.stmts ss env` | about to execute the first statement of list `ss` |
+| `.seq inner ss` | executing `inner`; when it terminates, continue with `ss` |
+| `.block L inner` | executing `inner` inside a block labeled `L` |
+| `.terminal env` | done, normally |
+| `.exiting label env` | propagating `exit label` outward |
+
+A configuration's execution is modelled by the small-step transitions listed in §3.
+
+### 2.2 Labels
+
+An exit label is `Option String`.
+`none` denotes an unlabeled exit
+that is consumed by any enclosing labeled block.
+`some L` denotes a labeled exit
+that is consumed only by an enclosing block whose label equals `L`.
+
+### 2.3 Well-formedness (`exitsCoveredByBlocks`)
+
+A statement is well-formed with respect to exit
+if every `exit` inside it
+resolves to an enclosing labeled block.
+
+Formally,
+`Stmt.exitsCoveredByBlocks : List (Option String) → Stmt P CmdT → Prop`
+(defined in `Stmt.lean`)
+holds when:
+
+- Every `exit (some L)` sub-statement satisfies `.some L ∈ labels`.
+- Every `exit none` sub-statement has a non-empty `labels` list.
+- Every `block L body` sub-statement
+  has `body` well-formed under `L :: labels`
+  (where `L : Option String`,
+  since labels on blocks may be anonymous).
+
+A program is well-formed
+if its top-level statement is well-formed under the empty label list.
+
+The predicate is lifted to configurations by
+`Config.exitsCoveredByBlocks`
+(in `StmtSemantics.lean`),
+which extends well-formedness to the small-step configuration shapes.
+
+## 3. Small-Step Transitions
+
+The step rules that define the behavior of exit and labeled blocks
+are given in `StmtSemantics.lean`
+as constructors of the inductive relation `StepStmt`.
+`StepStmtStar` is its reflexive-transitive closure.
+
+See §4.1 for the transitions and their realizing constructors.
+
+## 4. Correctness Properties
+
+This section states the properties
+that the small-step exit semantics satisfies.
+Each property is given in English
+followed by its formal statement.
+Each requirement cites the existing Lean construct that discharges it.
+
+### 4.1 Per-transition behavior
+
+The following transitions describe how exit and labeled-block
+configurations evolve under a single step of `StepStmt`.
+Each is realized directly by a constructor of the inductive relation
+and does not require a separate theorem.
+The named wrappers in `ExitProperties.lean`
+give each transition a descriptive identifier for citation.
+
+| Transition | Realized by | Named wrapper |
+|---|---|---|
+| `.stmt (.exit label md) ρ ⟶ .exiting label ρ` | `StepStmt.step_exit` | `exit_preserves_env` |
+| `.seq (.exiting label ρ) ss ⟶ .exiting label ρ` | `StepStmt.step_seq_exit` | `exit_skips_remaining` |
+| `.block (some L) (.exiting (some L) ρ) ⟶ .terminal ρ` | `StepStmt.step_block_exit_match` | `matching_block_consumes` |
+| `bl ≠ some M → .block bl (.exiting (some M) ρ) ⟶ .exiting (some M) ρ` | `StepStmt.step_block_exit_mismatch` | `nonmatching_exit_propagates` |
+| `.block label (.terminal ρ) ⟶ .terminal ρ` | `StepStmt.step_block_done` | `normal_block_completion` |
+| `.block label (.exiting none ρ) ⟶ .terminal ρ` | `StepStmt.step_block_exit_none` | `unlabeled_exit_consumed` |
+| `inner ⟶ inner' → .block label inner ⟶ .block label inner'` | `StepStmt.step_block_body` | `block_body_steps` |
+
+Two observations follow from the shape of the relation
+and require no separate proof:
+
+- An `exit` statement leaves the environment unchanged
+  (the result-side `ρ` of `step_exit` is syntactically identical to its input `ρ`).
+  The store, evaluator, and cumulative failure flag are likewise unchanged.
+- Exit propagation through `if` / `else` is not handled by a dedicated rule.
+  The generic seq and block-context rules
+  (`step_seq_exit`, `step_block_body`)
+  carry inner-configuration exits outward,
+  so no conditional-specific step rule is needed.
+
+### 4.2 Structural property of well-formedness
+
+Under well-formedness,
+every `exit (some L)` sub-statement has its label
+present in the enclosing label list:
+
+```
+Stmt.exitsCoveredByBlocks labels (.exit (some L) md)  →  .some L ∈ labels
+```
+
+This follows directly from the definition of
+`Stmt.exitsCoveredByBlocks`
+(the `.exit (some l) _` case reduces to `.some l ∈ labels`).
+Named wrapper: `exit_target_in_labels` in `ExitWellFormedness.lean`.
+
+### 4.3 Preservation of well-formedness
+
+If a configuration is well-formed under some label context,
+any single step MUST lead to a configuration
+that is still well-formed under the same label context.
+
+```
+StepStmt EvalCmd extendEval c₁ c₂  →
+Config.exitsCoveredByBlocks labels c₁  →
+Config.exitsCoveredByBlocks labels c₂
+```
+
+Realized by `step_preserves_exitsCoveredByBlocks`
+in `StmtSemantics.lean`.
+
+### 4.4 No-escape (preservation)
+
+Exit MUST NOT escape a well-formed procedure body.
+For any reachable configuration
+starting from the initial configuration of a well-formed procedure body,
+the reachable configuration MUST NOT be `.exiting`.
+
+```
+Stmt.exitsCoveredByBlocks [] s  →
+∀ ρ lbl ρ',
+  ¬ StepStmtStar EvalCmd extendEval (.stmt s ρ) (.exiting lbl ρ')
+```
+
+Realized by `exitsCoveredByBlocks_noEscape`
+in `StmtSemantics.lean`.
+A companion theorem
+`block_exitsCoveredByBlocks_noEscape`
+states the same property
+for an execution starting from `.stmts ss ρ`.
+
+Liveness —
+the claim that every `.exiting` eventually reaches a consuming block —
+is deliberately out of scope.
+See `decisions.md` Decision 6.
+
+## 5. File Layout
+
+The underlying definitions and theorems exist in upstream main.
+This contribution adds two thin files of named wrappers
+plus one `private → public` promotion
+so the spec's requirements cite descriptive, public symbols.
+
+| File | Relevant contents |
+|---|---|
+| `Strata/DL/Imperative/Stmt.lean` | `Stmt.exitsCoveredByBlocks`, `block_exitsCoveredByBlocks_append`, `exitsCoveredByBlocks_weaken` |
+| `Strata/DL/Imperative/StmtSemantics.lean` | `Config`, `StepStmt`, `StepStmtStar`, `Config.exitsCoveredByBlocks`, `step_preserves_exitsCoveredByBlocks` (public), `exitsCoveredByBlocks_noEscape`, `block_exitsCoveredByBlocks_noEscape` |
+| `Strata/DL/Imperative/ExitProperties.lean` | Seven per-transition named wrappers and two multi-step companions (§4.1) |
+| `Strata/DL/Imperative/ExitWellFormedness.lean` | `exit_target_in_labels`, `exit_none_has_enclosing` (§4.2) |
+
+## 6. Dependents
+
+The following in-tree feature currently depends on exit semantics:
+
+- **Python `return`, `break`, and `continue`**
+  in `Strata/Languages/Python/PythonToCore.lean`.
+  The translator emits `.exit (some jmp_target)` to desugar each of these
+  control-flow constructs into labeled blocks plus exit.
+
+- **Core concrete interpreter** (landed in #869).
+  The interpreter handles exit state at the procedure boundary.
+  `exitsCoveredByBlocks_noEscape`
+  and the newly-public `step_preserves_exitsCoveredByBlocks`
+  justify treating escaped exits as unreachable there.
+
+Other dependents
+(Laurel `throw` / `try` / `catch` / `finally`,
+JVerify's Java→Laurel frontend,
+downstream formal-verification projects)
+live on forks not yet merged to upstream
+and are out of scope for this document.
+
+## 7. Future Work
+
+These items are deliberately out of scope for this work.
+
+- **Liveness** (§4.4).
+  See Decision 6.
+- **No-label-shadowing**.
+  `exitsCoveredByBlocks` allows a block to re-use a label
+  that is already in scope.
+  A future `NoLabelShadowing` predicate could rule that out
+  if a downstream consumer needs it.
+- **`break` / `continue`** for loops.
+  Once added at source level,
+  they desugar to `exit` against an inserted labeled block.
+  No new semantics are required.
+- **Exit state on `Env`**.
+  See Decision 1, option B.
+  A larger refactor that would revisit every step rule
+  and every existing proof in the files listed in §5.