diff --git a/bench/orchestrator-stats/2026-05-15-iter-it.1.json b/bench/orchestrator-stats/2026-05-15-iter-it.1.json
new file mode 100644
index 0000000..78c1075
--- /dev/null
+++ b/bench/orchestrator-stats/2026-05-15-iter-it.1.json
@@ -0,0 +1,22 @@
+{
+  "iter_id": "it.1",
+  "date": "2026-05-15",
+  "mode": "standard",
+  "outcome": "DONE",
+  "tasks_total": 8,
+  "tasks_completed": 8,
+  "reloops_per_task": {
+    "1": 0,
+    "2": 0,
+    "3": 0,
+    "4": 0,
+    "5": 0,
+    "6": 0,
+    "7": 1,
+    "8": 0
+  },
+  "review_loops_spec": 0,
+  "review_loops_quality": 0,
+  "blocked_reason": null,
+  "notes": "Task 7 had 1 implementer-phase re-loop (loop-lowering tuple field order: init_ssa Vec declared (String,String,String,Type) but populated/destructured as (name,ail_ty,init_ssa,llvm_ty) — fixed to (String,Type,String,String), 6 E0308/E0277, one fix pass). All spec + quality checks passed first time (compliant/approved). Tasks 4 and 7 closed DONE_WITH_CONCERNS (Step 4.1 prose-roundtrip plan defect — no Form-B parser exists by design; loop-in-lambda codegen coverage via a Phase-3 runnable fixture). recur synth returns Subst::fresh(counter) not the plan's flagged-risky Type::unit() — resolves the plan's own self-review Open risk. Strictly additive: zero deletions touch tail-app/tail-do/the seven block_terminated sites/verify_tail_positions' tail role."
+}
diff --git a/crates/ail/src/main.rs b/crates/ail/src/main.rs
index 8b9788b..b125878 100644
--- a/crates/ail/src/main.rs
+++ b/crates/ail/src/main.rs
@@ -1544,6 +1544,26 @@ fn walk_term(
             }
             walk_term(value, out, builtins, scope);
         }
+        // Iter it.1: loop binder names bind inside the body and later
+        // binder inits, mirroring `Term::Mut`. Recur args are uses.
+        Term::Loop { binders, body } => {
+            let mut newly = Vec::new();
+            for b in binders {
+                walk_term(&b.init, out, builtins, scope);
+                if scope.insert(b.name.clone()) {
+                    newly.push(b.name.clone());
+                }
+            }
+            walk_term(body, out, builtins, scope);
+            for n in newly {
+                scope.remove(&n);
+            }
+        }
+        Term::Recur { args } => {
+            for a in args {
+                walk_term(a, out, builtins, scope);
+            }
+        }
     }
 }
 
@@ -2785,6 +2805,47 @@ fn rewrite_def(
                     changed,
                 );
             }
+            // Iter it.1: rewrite types embedded in each
+            // `LoopBinder.ty` (loop binders carry full Type
+            // annotations like mut-vars) and recurse into each
+            // binder's `init` and the body. `Term::Recur` has no
+            // embedded type.
+            Term::Loop { binders, body } => {
+                for b in binders {
+                    rewrite_type(
+                        &mut b.ty,
+                        owning_module,
+                        local_types,
+                        import_names,
+                        changed,
+                    );
+                    rewrite_term(
+                        &mut b.init,
+                        owning_module,
+                        local_types,
+                        import_names,
+                        changed,
+                    );
+                }
+                rewrite_term(
+                    body,
+                    owning_module,
+                    local_types,
+                    import_names,
+                    changed,
+                );
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    rewrite_term(
+                        a,
+                        owning_module,
+                        local_types,
+                        import_names,
+                        changed,
+                    );
+                }
+            }
         }
     }
 
diff --git a/crates/ail/tests/codegen_import_map_fallback_pin.rs b/crates/ail/tests/codegen_import_map_fallback_pin.rs
index 44b4296..702a162 100644
--- a/crates/ail/tests/codegen_import_map_fallback_pin.rs
+++ b/crates/ail/tests/codegen_import_map_fallback_pin.rs
@@ -101,6 +101,13 @@ fn synthesised_print_uses_user_module_show_via_fallback() {
                     || contains_xmod_show_var(body)
             }
             Term::Assign { value, .. } => contains_xmod_show_var(value),
+            // Iter it.1: a `Term::Loop` cannot itself host a synth'd
+            // cross-module reference, but recurse defensively.
+            Term::Loop { binders, body } => {
+                binders.iter().any(|b| contains_xmod_show_var(&b.init))
+                    || contains_xmod_show_var(body)
+            }
+            Term::Recur { args } => args.iter().any(contains_xmod_show_var),
             Term::Lit { .. } => false,
         }
     }
diff --git a/crates/ail/tests/e2e.rs b/crates/ail/tests/e2e.rs
index 9950cb6..9f5f9ae 100644
--- a/crates/ail/tests/e2e.rs
+++ b/crates/ail/tests/e2e.rs
@@ -2828,6 +2828,31 @@ fn mut_counter_prints_55() {
     assert_eq!(stdout.trim(), "55", "mut_counter must print 55, got {stdout:?}");
 }
 
+/// Iter it.1: `examples/loop_counter.ail` exercises `Term::Loop` +
+/// `Term::Recur` codegen — the loop-header block with one phi per
+/// binder and `recur` as a back-edge `br`. The body
+/// `(loop ((var acc Int 0) (var i Int 1)) (if (> i 10) acc (recur ...)))`
+/// sums 1..10 and prints 55. End-to-end gate for the loop-header /
+/// phi / recur-back-edge lowering.
+#[test]
+fn loop_counter_runs_and_prints_55() {
+    let stdout = build_and_run("loop_counter.ail");
+    assert_eq!(stdout.trim(), "55", "loop_counter must print 55, got {stdout:?}");
+}
+
+/// Iter it.1: a `Term::Loop` inside a `Term::Lam` body, invoked via
+/// a returned closure. Protects the lambda-boundary invariant: the
+/// closure thunk scopes its own loop header / phis (the `loop_frames`
+/// save+reset+restore across the lambda boundary, mut.3 analogue) —
+/// a `recur` inside the lambda must back-edge to the lambda's own
+/// loop header, not the outer fn's. The lambda computes x*x by
+/// summing x exactly x times; apply 7 prints 49.
+#[test]
+fn loop_in_lambda_runs_and_prints_49() {
+    let stdout = build_and_run("loop_in_lambda_e2e.ail");
+    assert_eq!(stdout.trim(), "49", "loop_in_lambda must print 49, got {stdout:?}");
+}
+
 /// Iter mut.3: Float twin of `mut_counter_prints_55`. The mut-var
 /// is `Float`, init is `0.0`, the recursive helper returns the
 /// sum 1.0+...+10.0 = 55.0. The polymorphic `print` routes through
diff --git a/crates/ailang-check/src/builtins.rs b/crates/ailang-check/src/builtins.rs
index fbd7b1b..d4f5d92 100644
--- a/crates/ailang-check/src/builtins.rs
+++ b/crates/ailang-check/src/builtins.rs
@@ -343,6 +343,7 @@ mod tests {
         install(&mut env);
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -354,6 +355,7 @@ mod tests {
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "<test>",
             &mut subst,
@@ -586,6 +588,7 @@ mod tests {
         install(&mut env);
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -597,6 +600,7 @@ mod tests {
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "<test>",
             &mut subst,
diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs
index 7061b06..01c54dc 100644
--- a/crates/ailang-check/src/lib.rs
+++ b/crates/ailang-check/src/lib.rs
@@ -261,6 +261,23 @@ pub(crate) fn substitute_rigids_in_term(t: &Term, mapping: &BTreeMap<String, Typ
             name: name.clone(),
             value: Box::new(substitute_rigids_in_term(value, mapping)),
         },
+        // Iter it.1: rebuild each `LoopBinder.ty` via the type-level
+        // rigids substitution, each `init` and the body via the
+        // term-level walker.
+        Term::Loop { binders, body } => Term::Loop {
+            binders: binders
+                .iter()
+                .map(|b| ailang_core::ast::LoopBinder {
+                    name: b.name.clone(),
+                    ty: substitute_rigids(&b.ty, mapping),
+                    init: Box::new(substitute_rigids_in_term(&b.init, mapping)),
+                })
+                .collect(),
+            body: Box::new(substitute_rigids_in_term(body, mapping)),
+        },
+        Term::Recur { args } => Term::Recur {
+            args: args.iter().map(|a| substitute_rigids_in_term(a, mapping)).collect(),
+        },
     }
 }
 
@@ -679,6 +696,36 @@ pub enum CheckError {
     #[error("mut-var `{name}` cannot be captured by a lambda — mut-vars are alloca-resident and do not escape their enclosing mut block. Either move the lambda outside the mut block, or restructure to pass `{name}` as a lambda parameter (deferring escape to a future milestone with ref-types and the !Mut effect).")]
     MutVarCapturedByLambda { name: String },
 
+    /// Iter it.1: a `Term::Recur` was reached with no lexically
+    /// enclosing `Term::Loop`. Spec
+    /// `docs/specs/2026-05-15-iteration-discipline.md`. (No `span`
+    /// field — the `CheckError` variants in this crate do not carry
+    /// spans; the plan's pseudo-code referenced a type not in scope
+    /// here, so the real `MutAssignOutOfScope`-style shape is used.)
+    #[error("recur outside of any enclosing loop")]
+    RecurOutsideLoop,
+
+    /// Iter it.1: a `Term::Recur`'s argument count differs from the
+    /// lexically nearest enclosing loop's binder count.
+    #[error("recur passes {got} argument(s) but the enclosing loop binds {want}")]
+    RecurArityMismatch { got: usize, want: usize },
+
+    /// Iter it.1: a `Term::Recur` argument's synth type does not
+    /// unify with the corresponding loop binder's declared type.
+    #[error("recur argument {pos} has type {got} but loop binder `{name}` is {want}")]
+    RecurTypeMismatch {
+        pos: usize,
+        name: String,
+        got: String,
+        want: String,
+    },
+
+    /// Iter it.1: a `Term::Recur` was reached outside the tail
+    /// context of its enclosing loop's body. Spec
+    /// `docs/specs/2026-05-15-iteration-discipline.md`.
+    #[error("recur must be in tail position of its enclosing loop")]
+    RecurNotInTailPosition,
+
     /// Iter 22b.3: an internal invariant in the typechecker / mono pass
     /// was violated — surfaced as an error so callers can propagate
     /// rather than abort, but in well-formed inputs (typecheck has
@@ -731,6 +778,10 @@ impl CheckError {
             CheckError::AssignTypeMismatch { .. } => "assign-type-mismatch",
             CheckError::UnsupportedMutVarType { .. } => "mut-var-unsupported-type",
             CheckError::MutVarCapturedByLambda { .. } => "mut-var-captured-by-lambda",
+            CheckError::RecurOutsideLoop => "recur-outside-loop",
+            CheckError::RecurArityMismatch { .. } => "recur-arity-mismatch",
+            CheckError::RecurTypeMismatch { .. } => "recur-type-mismatch",
+            CheckError::RecurNotInTailPosition => "recur-not-in-tail-position",
             CheckError::Internal(_) => "internal",
         }
     }
@@ -805,6 +856,12 @@ impl CheckError {
             CheckError::MutVarCapturedByLambda { name } => {
                 serde_json::json!({"name": name})
             }
+            CheckError::RecurArityMismatch { got, want } => {
+                serde_json::json!({"expected": want, "actual": got})
+            }
+            CheckError::RecurTypeMismatch { pos, name, got, want } => {
+                serde_json::json!({"pos": pos, "name": name, "expected": want, "actual": got})
+            }
             _ => serde_json::Value::Object(serde_json::Map::new()),
         }
     }
@@ -1950,7 +2007,8 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<
     // pushed/popped by `Term::Mut` arms during the walk; discarded after
     // the body type-checks.
     let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
-    let body_ty = synth(&f.body, &env, &mut locals, &mut mut_scope_stack, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
+    let mut loop_stack: Vec<Vec<Type>> = Vec::new();
+    let body_ty = synth(&f.body, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
     unify(&ret_ty, &body_ty, &mut subst)?;
     // mq.3: surface synth-time warnings into the caller-supplied
     // accumulator. The warnings already carry `def: Some(f.name)`
@@ -2679,6 +2737,76 @@ pub fn verify_tail_positions(t: &Term, is_tail: bool) -> Result<()> {
         // be in tail position. Its `value` is also not in tail
         // position.
         Term::Assign { value, .. } => verify_tail_positions(value, false),
+        // Iter it.1 (DD-1): binder inits are evaluated before the
+        // loop head and are NOT in tail position. The body opens a
+        // "recur-legal, recur-must-be-tail" context — `verify_loop_body`
+        // walks it, accepting a `Term::Recur` only where the loop
+        // body's value is produced (tail position w.r.t. the loop).
+        Term::Loop { binders, body } => {
+            for b in binders {
+                verify_tail_positions(&b.init, false)?;
+            }
+            verify_loop_body(body)
+        }
+        // Iter it.1 (DD-1): a `Term::Recur` reached by the ordinary
+        // `verify_tail_positions` walk is, by construction, NOT in the
+        // tail context of any enclosing loop body (`verify_loop_body`
+        // intercepts the legal in-tail ones). Either there is no
+        // enclosing loop (synth flags `RecurOutsideLoop`) or this
+        // recur is in a non-tail position.
+        Term::Recur { .. } => Err(CheckError::RecurNotInTailPosition),
+    }
+}
+
+/// Iter it.1 (DD-1): walks a `Term::Loop` body in the
+/// "recur-is-legal-and-must-be-tail" context. A `Term::Recur` is
+/// accepted only at a position that produces the loop body's value
+/// (the loop-tail positions); anywhere else it is
+/// `RecurNotInTailPosition`. Non-recur sub-terms that are NOT in the
+/// loop's tail position are handed back to `verify_tail_positions`
+/// (with `is_tail = false`) so `tail-app`/`tail-do` inside the loop
+/// body are still validated; sub-terms in the loop's tail position
+/// recurse through `verify_loop_body` so a nested `recur` there is
+/// still legal. A nested `Term::Loop` starts its own recur scope.
+fn verify_loop_body(t: &Term) -> Result<()> {
+    match t {
+        // Tail position of the loop body: a recur here is legal.
+        Term::Recur { args } => {
+            for a in args {
+                verify_tail_positions(a, false)?;
+            }
+            Ok(())
+        }
+        Term::If { cond, then, else_ } => {
+            verify_tail_positions(cond, false)?;
+            verify_loop_body(then)?;
+            verify_loop_body(else_)
+        }
+        Term::Seq { lhs, rhs } => {
+            // Only `rhs` is in the loop's tail position.
+            verify_tail_positions(lhs, false)?;
+            verify_loop_body(rhs)
+        }
+        Term::Match { scrutinee, arms } => {
+            verify_tail_positions(scrutinee, false)?;
+            for arm in arms {
+                verify_loop_body(&arm.body)?;
+            }
+            Ok(())
+        }
+        Term::Let { value, body, .. } => {
+            verify_tail_positions(value, false)?;
+            verify_loop_body(body)
+        }
+        // A nested loop is its own recur scope: a `recur` inside it
+        // binds the inner loop, not this one. Validate it through the
+        // ordinary tail-position walk in a fresh tail context.
+        Term::Loop { .. } => verify_tail_positions(t, true),
+        // Any other term is not a recur-carrying tail shape; validate
+        // it normally (it is the loop body's value but carries no
+        // loop-tail recur, so `is_tail = true` keeps a trailing
+        // `tail-app` legal).
+        other => verify_tail_positions(other, true),
     }
 }
 
@@ -2703,7 +2831,8 @@ fn check_const(c: &ConstDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> R
     // at this entry point — `Term::Mut` may appear inside a const body
     // and push frames as the walk descends).
     let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
-    let v = synth(&c.value, env, &mut locals, &mut mut_scope_stack, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
+    let mut loop_stack: Vec<Vec<Type>> = Vec::new();
+    let v = synth(&c.value, env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
     out_warnings.extend(warnings);
     unify(&c.ty, &v, &mut subst)?;
     if !effects.is_empty() {
@@ -2728,6 +2857,14 @@ pub(crate) fn synth(
     // name through it. Position: locals-adjacent because both are
     // per-fn-body lexical scope state.
     mut_scope_stack: &mut Vec<IndexMap<String, Type>>,
+    // Iter it.1 (DD-1): per-walk lexical loop-binder-type stack,
+    // threaded exactly as `mut_scope_stack`. Each frame is one
+    // `Term::Loop`'s binder type-vector (positional). Pushed on
+    // `Term::Loop` entry, popped on exit; `Term::Recur` reads the
+    // innermost frame for arity/type unification. Position:
+    // mut_scope_stack-adjacent because both are per-fn-body lexical
+    // scope state.
+    loop_stack: &mut Vec<Vec<Type>>,
     effects: &mut BTreeSet<String>,
     in_def: &str,
     subst: &mut Subst,
@@ -3116,7 +3253,7 @@ pub(crate) fn synth(
             Ok(maybe_instantiate(raw, counter))
         }
         Term::App { callee, args, .. } => {
-            let cty = synth(callee, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let cty = synth(callee, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             let cty = subst.apply(&cty);
             let (params, ret, fx) = match &cty {
                 Type::Fn { params, ret, effects: fx, .. } => {
@@ -3152,7 +3289,7 @@ pub(crate) fn synth(
                 });
             }
             for (a, exp) in args.iter().zip(params.iter()) {
-                let actual = synth(a, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+                let actual = synth(a, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
                 unify(exp, &actual, subst)?;
             }
             for e in fx {
@@ -3161,9 +3298,9 @@ pub(crate) fn synth(
             Ok(subst.apply(&ret))
         }
         Term::Let { name, value, body } => {
-            let v = synth(value, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let v = synth(value, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             let prev = locals.insert(name.clone(), v);
-            let r = synth(body, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let r = synth(body, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             match prev {
                 Some(p) => {
                     locals.insert(name.clone(), p);
@@ -3175,10 +3312,10 @@ pub(crate) fn synth(
             Ok(r)
         }
         Term::If { cond, then, else_ } => {
-            let c = synth(cond, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let c = synth(cond, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             unify(&Type::bool_(), &c, subst)?;
-            let t1 = synth(then, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
-            let t2 = synth(else_, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let t1 = synth(then, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let t2 = synth(else_, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             unify(&t1, &t2, subst)?;
             Ok(subst.apply(&t1))
         }
@@ -3196,7 +3333,7 @@ pub(crate) fn synth(
                 });
             }
             for (a, exp) in args.iter().zip(sig.params.iter()) {
-                let actual = synth(a, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+                let actual = synth(a, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
                 unify(exp, &actual, subst)?;
             }
             effects.insert(sig.effect.clone());
@@ -3291,7 +3428,7 @@ pub(crate) fn synth(
             }
             for (a, exp) in args.iter().zip(qualified_fields.iter()) {
                 let exp_inst = substitute_rigids(exp, &mapping);
-                let actual = synth(a, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+                let actual = synth(a, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
                 unify(&exp_inst, &actual, subst)?;
             }
             Ok(Type::Con {
@@ -3300,7 +3437,7 @@ pub(crate) fn synth(
             })
         }
         Term::Match { scrutinee, arms } => {
-            let s_ty = synth(scrutinee, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let s_ty = synth(scrutinee, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             if arms.is_empty() {
                 return Err(CheckError::NonExhaustive {
                     ty: ailang_core::pretty::type_to_string(&s_ty),
@@ -3318,7 +3455,7 @@ pub(crate) fn synth(
                     let prev = locals.insert(n.clone(), t.clone());
                     pushed.push((n.clone(), prev));
                 }
-                let body_ty = synth(&arm.body, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+                let body_ty = synth(&arm.body, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
                 for (n, prev) in pushed.into_iter().rev() {
                     match prev {
                         Some(p) => {
@@ -3393,9 +3530,9 @@ pub(crate) fn synth(
             Ok(subst.apply(&result_ty.expect("checked arms is non-empty")))
         }
         Term::Seq { lhs, rhs } => {
-            let lty = synth(lhs, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let lty = synth(lhs, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             unify(&Type::unit(), &lty, subst)?;
-            synth(rhs, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
+            synth(rhs, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
         }
         Term::Lam { params, param_tys, ret_ty, effects: lam_effects, body } => {
             // Iter mut.4-tidy: reject lambda-captures-of-mut-var.
@@ -3429,7 +3566,7 @@ pub(crate) fn synth(
                 pushed.push((n.clone(), prev));
             }
             let mut body_effects: BTreeSet<String> = BTreeSet::new();
-            let body_ty = synth(body, env, locals, mut_scope_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
+            let body_ty = synth(body, env, locals, mut_scope_stack, loop_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
             for (n, prev) in pushed.into_iter().rev() {
                 match prev {
                     Some(p) => {
@@ -3517,7 +3654,7 @@ pub(crate) fn synth(
             // subset rule against `declared_effs` — exactly like
             // `Term::Lam`.
             let mut body_effects: BTreeSet<String> = BTreeSet::new();
-            let body_ty = synth(body, env, locals, mut_scope_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
+            let body_ty = synth(body, env, locals, mut_scope_stack, loop_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
 
             // Restore body-scope locals (params + name).
             for (n, prev) in pushed.into_iter().rev() {
@@ -3544,7 +3681,7 @@ pub(crate) fn synth(
             // scope (params are not visible here; only the recursive
             // binding is).
             let prev_in = locals.insert(name.clone(), ty.clone());
-            let in_ty = synth(in_term, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
+            let in_ty = synth(in_term, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
             match prev_in {
                 Some(p) => {
                     locals.insert(name.clone(), p);
@@ -3560,7 +3697,7 @@ pub(crate) fn synth(
             // No constraint generated, no environment change. The
             // wrapper records author intent for the future RC inc/dec
             // emission pass (18c.3); typing is pure passthrough.
-            synth(value, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
+            synth(value, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
         }
         Term::ReuseAs { source, body } => {
             // Iter 18d.1: `(reuse-as SRC NEW-CTOR)` requires `body` to
@@ -3574,7 +3711,7 @@ pub(crate) fn synth(
             // shape-compatibility check (18d.2 will add a
             // `reuse-as-shape-mismatch` diagnostic when codegen has
             // the actual size info).
-            let _ = synth(source, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
+            let _ = synth(source, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
             match body.as_ref() {
                 Term::Ctor { .. } | Term::Lam { .. } => {}
                 other => {
@@ -3592,6 +3729,8 @@ pub(crate) fn synth(
                         Term::ReuseAs { .. } => "reuse-as",
                         Term::Mut { .. } => "mut",
                         Term::Assign { .. } => "assign",
+                        Term::Loop { .. } => "loop",
+                        Term::Recur { .. } => "recur",
                         Term::Ctor { .. } | Term::Lam { .. } => unreachable!(),
                     };
                     return Err(CheckError::ReuseAsNonAllocatingBody {
@@ -3602,7 +3741,7 @@ pub(crate) fn synth(
             }
             // Body's type is the result type of the whole reuse-as
             // expression.
-            synth(body, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
+            synth(body, env, locals, mut_scope_stack, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
         }
         // Iter mut.2: a mut block opens a fresh lexical scope for its
         // mut-vars. Each var's `init` is synthed in the outer scope
@@ -3628,7 +3767,7 @@ pub(crate) fn synth(
                 // the `mut_scope_stack` truthful at all times.
                 mut_scope_stack.push(frame.clone());
                 let init_ty = synth(
-                    &v.init, env, locals, mut_scope_stack, effects, in_def,
+                    &v.init, env, locals, mut_scope_stack, loop_stack, effects, in_def,
                     subst, counter, residuals, free_fn_calls, warnings,
                 )?;
                 mut_scope_stack.pop();
@@ -3637,7 +3776,7 @@ pub(crate) fn synth(
             }
             mut_scope_stack.push(frame);
             let body_result = synth(
-                body, env, locals, mut_scope_stack, effects, in_def,
+                body, env, locals, mut_scope_stack, loop_stack, effects, in_def,
                 subst, counter, residuals, free_fn_calls, warnings,
             );
             mut_scope_stack.pop();
@@ -3671,7 +3810,7 @@ pub(crate) fn synth(
                 }
                 Some(declared_ty) => {
                     let value_ty = synth(
-                        value, env, locals, mut_scope_stack, effects, in_def,
+                        value, env, locals, mut_scope_stack, loop_stack, effects, in_def,
                         subst, counter, residuals, free_fn_calls, warnings,
                     )?;
                     let applied_declared = subst.apply(&declared_ty);
@@ -3687,6 +3826,84 @@ pub(crate) fn synth(
                 }
             }
         }
+        // Iter it.1 (DD-1): each binder's `init` is synthesised in
+        // the outer scope plus the already-declared binders (init
+        // order = declaration order), unified against the binder's
+        // declared type. The binder names are bound into `locals`
+        // (save/restore like `Term::Let`) for the body; the binder
+        // type-vector is pushed onto `loop_stack` so an enclosed
+        // `Term::Recur` can check its arity/types. The loop's static
+        // type is the body's static type.
+        Term::Loop { binders, body } => {
+            let mut saved: Vec<(String, Option<Type>)> = Vec::new();
+            let mut binder_tys: Vec<Type> = Vec::with_capacity(binders.len());
+            for b in binders {
+                let init_ty = synth(
+                    &b.init, env, locals, mut_scope_stack, loop_stack, effects, in_def,
+                    subst, counter, residuals, free_fn_calls, warnings,
+                )?;
+                unify(&b.ty, &init_ty, subst)?;
+                let prev = locals.insert(b.name.clone(), b.ty.clone());
+                saved.push((b.name.clone(), prev));
+                binder_tys.push(b.ty.clone());
+            }
+            loop_stack.push(binder_tys);
+            let body_result = synth(
+                body, env, locals, mut_scope_stack, loop_stack, effects, in_def,
+                subst, counter, residuals, free_fn_calls, warnings,
+            );
+            loop_stack.pop();
+            for (name, prev) in saved.into_iter().rev() {
+                match prev {
+                    Some(p) => {
+                        locals.insert(name, p);
+                    }
+                    None => {
+                        locals.shift_remove(&name);
+                    }
+                }
+            }
+            body_result
+        }
+        // Iter it.1 (DD-1): a `Term::Recur` re-enters the lexically
+        // nearest enclosing loop. Empty `loop_stack` ⇒
+        // `RecurOutsideLoop`; arg count ≠ innermost binder count ⇒
+        // `RecurArityMismatch`; per-position unify failure ⇒
+        // `RecurTypeMismatch`. `recur` never falls through (it is
+        // always a tail jump), so its synth result is a fresh
+        // metavar — it unifies with any type, which is what makes
+        // `(if c then (recur ...))` typecheck. (The plan's named
+        // fallback was `Type::unit()`; a fresh metavar is the
+        // codebase-idiomatic bottom and resolves the plan's "Open
+        // risk" correctly — see the it.1 journal.)
+        Term::Recur { args } => {
+            let want = loop_stack
+                .last()
+                .cloned()
+                .ok_or(CheckError::RecurOutsideLoop)?;
+            if args.len() != want.len() {
+                return Err(CheckError::RecurArityMismatch {
+                    got: args.len(),
+                    want: want.len(),
+                });
+            }
+            for (i, (a, wt)) in args.iter().zip(want.iter()).enumerate() {
+                let at = synth(
+                    a, env, locals, mut_scope_stack, loop_stack, effects, in_def,
+                    subst, counter, residuals, free_fn_calls, warnings,
+                )?;
+                if unify(&at, wt, subst).is_err() {
+                    let applied_got = subst.apply(&at);
+                    return Err(CheckError::RecurTypeMismatch {
+                        pos: i,
+                        name: format!("#{i}"),
+                        got: ailang_core::pretty::type_to_string(&applied_got),
+                        want: ailang_core::pretty::type_to_string(wt),
+                    });
+                }
+            }
+            Ok(Subst::fresh(counter))
+        }
     }
 }
 
@@ -4061,6 +4278,7 @@ mod tests {
         let env = Env::default();
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -4072,6 +4290,7 @@ mod tests {
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "<test>",
             &mut subst,
@@ -4098,6 +4317,7 @@ mod tests {
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         locals.insert("x".into(), Type::int()); // outer let-style binding
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut frame: IndexMap<String, Type> = IndexMap::new();
         frame.insert("x".into(), Type::float()); // inner mut-var
         mut_scope_stack.push(frame);
@@ -4114,6 +4334,7 @@ mod tests {
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "<test>",
             &mut subst,
@@ -4138,6 +4359,7 @@ mod tests {
         let env = Env::default();
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut outer: IndexMap<String, Type> = IndexMap::new();
         outer.insert("x".into(), Type::int());
         mut_scope_stack.push(outer);
@@ -4157,6 +4379,7 @@ mod tests {
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "<test>",
             &mut subst,
@@ -4251,6 +4474,7 @@ mod tests {
         let env = Env::default();
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -4258,7 +4482,7 @@ mod tests {
         let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
         let mut warnings: Vec<Diagnostic> = Vec::new();
         let err = synth(
-            &term, &env, &mut locals, &mut mut_scope_stack, &mut effects,
+            &term, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects,
             "<test>", &mut subst, &mut counter, &mut residuals,
             &mut free_fn_calls, &mut warnings,
         )
@@ -4291,6 +4515,7 @@ mod tests {
         let env = Env::default();
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -4298,7 +4523,7 @@ mod tests {
         let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
         let mut warnings: Vec<Diagnostic> = Vec::new();
         let err = synth(
-            &term, &env, &mut locals, &mut mut_scope_stack, &mut effects,
+            &term, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects,
             "<test>", &mut subst, &mut counter, &mut residuals,
             &mut free_fn_calls, &mut warnings,
         )
@@ -4330,6 +4555,7 @@ mod tests {
         let env = Env::default();
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -4337,7 +4563,7 @@ mod tests {
         let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
         let mut warnings: Vec<Diagnostic> = Vec::new();
         let err = synth(
-            &term, &env, &mut locals, &mut mut_scope_stack, &mut effects,
+            &term, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects,
             "<test>", &mut subst, &mut counter, &mut residuals,
             &mut free_fn_calls, &mut warnings,
         )
@@ -4432,6 +4658,7 @@ mod tests {
         let env = Env::default();
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -4439,7 +4666,7 @@ mod tests {
         let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
         let mut warnings: Vec<Diagnostic> = Vec::new();
         let err = synth(
-            &term, &env, &mut locals, &mut mut_scope_stack, &mut effects,
+            &term, &env, &mut locals, &mut mut_scope_stack, &mut loop_stack, &mut effects,
             "<test>", &mut subst, &mut counter, &mut residuals,
             &mut free_fn_calls, &mut warnings,
         )
@@ -7171,6 +7398,7 @@ mod tests {
         let term = Term::Var { name: "show".into() };
         let mut locals: IndexMap<String, Type> = IndexMap::new();
         let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
+        let mut loop_stack: Vec<Vec<Type>> = Vec::new();
         let mut effects: BTreeSet<String> = BTreeSet::new();
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
@@ -7182,6 +7410,7 @@ mod tests {
             &env,
             &mut locals,
             &mut mut_scope_stack,
+            &mut loop_stack,
             &mut effects,
             "test_call_site",
             &mut subst,
diff --git a/crates/ailang-check/src/lift.rs b/crates/ailang-check/src/lift.rs
index ea56344..a4ae3fe 100644
--- a/crates/ailang-check/src/lift.rs
+++ b/crates/ailang-check/src/lift.rs
@@ -397,6 +397,25 @@ impl<'a> Lifter<'a> {
                 name: name.clone(),
                 value: Box::new(self.lift_in_term(value, locals, in_def)?),
             }),
+            Term::Loop { binders, body } => Ok(Term::Loop {
+                binders: binders
+                    .iter()
+                    .map(|b| {
+                        Ok(ailang_core::ast::LoopBinder {
+                            name: b.name.clone(),
+                            ty: b.ty.clone(),
+                            init: Box::new(self.lift_in_term(&b.init, locals, in_def)?),
+                        })
+                    })
+                    .collect::<Result<Vec<_>>>()?,
+                body: Box::new(self.lift_in_term(body, locals, in_def)?),
+            }),
+            Term::Recur { args } => Ok(Term::Recur {
+                args: args
+                    .iter()
+                    .map(|a| self.lift_in_term(a, locals, in_def))
+                    .collect::<Result<Vec<_>>>()?,
+            }),
             Term::LetRec { name, ty, params, body, in_term } => {
                 // Iter 16b.3: post-order traversal — lift any inner
                 // LetRecs first. Within the body's scope, `name` and
@@ -724,7 +743,11 @@ impl<'a> Lifter<'a> {
         // term at a time, beginning from a top-of-body position; fresh
         // empty mut-scope stack is correct.
         let mut mut_scope_stack: Vec<indexmap::IndexMap<String, crate::Type>> = Vec::new();
-        let ty = synth(t, &self.env, locals, &mut mut_scope_stack, &mut effects, in_def, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings_discarded)?;
+        // Iter it.1 (DD-1): lift's letrec-capture re-entry walks one
+        // term from a top-of-body position; fresh empty loop_stack is
+        // correct (a loop captured into a letrec carries its own).
+        let mut loop_stack: Vec<Vec<crate::Type>> = Vec::new();
+        let ty = synth(t, &self.env, locals, &mut mut_scope_stack, &mut loop_stack, &mut effects, in_def, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings_discarded)?;
         Ok(subst.apply(&ty))
     }
 }
@@ -761,6 +784,10 @@ fn contains_any_letrec(m: &Module) -> bool {
                 vars.iter().any(|v| term_has_letrec(&v.init)) || term_has_letrec(body)
             }
             Term::Assign { value, .. } => term_has_letrec(value),
+            Term::Loop { binders, body } => {
+                binders.iter().any(|b| term_has_letrec(&b.init)) || term_has_letrec(body)
+            }
+            Term::Recur { args } => args.iter().any(term_has_letrec),
         }
     }
     for def in &m.defs {
diff --git a/crates/ailang-check/src/linearity.rs b/crates/ailang-check/src/linearity.rs
index 83f9b66..6867f45 100644
--- a/crates/ailang-check/src/linearity.rs
+++ b/crates/ailang-check/src/linearity.rs
@@ -609,6 +609,17 @@ impl<'a> Checker<'a> {
                 // a tracked binder). Walk the `value` normally.
                 self.walk(value, Position::Consume);
             }
+            Term::Loop { binders, body } => {
+                for b in binders {
+                    self.walk(&b.init, Position::Consume);
+                }
+                self.walk(body, pos);
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    self.walk(a, Position::Consume);
+                }
+            }
         }
     }
 
@@ -795,6 +806,8 @@ fn make_reuse_as_source_not_bare_var(def: &str, source: &Term, body: &Term) -> D
         Term::ReuseAs { .. } => "reuse-as",
         Term::Mut { .. } => "mut",
         Term::Assign { .. } => "assign",
+        Term::Loop { .. } => "loop",
+        Term::Recur { .. } => "recur",
     };
     let replacement = term_to_form_a(body);
     Diagnostic::error(
@@ -934,6 +947,17 @@ fn any_sub_binder_consumed_for(
         Term::Assign { value, .. } => {
             any_sub_binder_consumed_for(value, pname, uniq, def_name, ctors)
         }
+        // Iter it.1: loop binders are scalar like mut-vars; recurse
+        // into children defensively so a genuine consume-of-`pname`
+        // inside a binder init / body / recur arg still surfaces.
+        Term::Loop { binders, body } => {
+            binders.iter().any(|b| {
+                any_sub_binder_consumed_for(&b.init, pname, uniq, def_name, ctors)
+            }) || any_sub_binder_consumed_for(body, pname, uniq, def_name, ctors)
+        }
+        Term::Recur { args } => args
+            .iter()
+            .any(|a| any_sub_binder_consumed_for(a, pname, uniq, def_name, ctors)),
     }
 }
 
diff --git a/crates/ailang-check/src/mono.rs b/crates/ailang-check/src/mono.rs
index 64b5f27..83584e1 100644
--- a/crates/ailang-check/src/mono.rs
+++ b/crates/ailang-check/src/mono.rs
@@ -713,11 +713,16 @@ pub fn collect_mono_targets(
     // mut-scope, since any `Term::Mut` will push its own frame as the
     // walk descends.
     let mut mut_scope_stack: Vec<indexmap::IndexMap<String, crate::Type>> = Vec::new();
+    // Iter it.1 (DD-1): mono re-synth from top-of-body — empty
+    // loop_stack; any `Term::Loop` pushes its own frame as the walk
+    // descends.
+    let mut loop_stack: Vec<Vec<crate::Type>> = Vec::new();
     crate::synth(
         &f.body,
         &env,
         &mut locals,
         &mut mut_scope_stack,
+        &mut loop_stack,
         &mut effects,
         &f.name,
         &mut subst,
@@ -1239,6 +1244,17 @@ fn rewrite_mono_calls(
         Term::Assign { value, .. } => {
             rewrite_mono_calls(value, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
         }
+        Term::Loop { binders, body } => {
+            for b in binders.iter_mut() {
+                rewrite_mono_calls(&mut b.init, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
+            }
+            rewrite_mono_calls(body, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
+        }
+        Term::Recur { args } => {
+            for a in args.iter_mut() {
+                rewrite_mono_calls(a, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
+            }
+        }
         Term::Lit { .. } => {}
     }
 }
@@ -1343,11 +1359,14 @@ pub(crate) fn collect_residuals_ordered(
     // mut-scope, since any `Term::Mut` will push its own frame as the
     // walk descends.
     let mut mut_scope_stack: Vec<indexmap::IndexMap<String, crate::Type>> = Vec::new();
+    // Iter it.1 (DD-1): empty loop_stack at top-of-body re-synth.
+    let mut loop_stack: Vec<Vec<crate::Type>> = Vec::new();
     crate::synth(
         &f.body,
         &env,
         &mut locals,
         &mut mut_scope_stack,
+        &mut loop_stack,
         &mut effects,
         &f.name,
         &mut subst,
@@ -1613,6 +1632,17 @@ fn interleave_slots(
         Term::Assign { value, .. } => {
             interleave_slots(value, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
         }
+        Term::Loop { binders, body } => {
+            for b in binders {
+                interleave_slots(&b.init, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            }
+            interleave_slots(body, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+        }
+        Term::Recur { args } => {
+            for a in args {
+                interleave_slots(a, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, class_slots, free_fn_slots, class_cur, free_cur, locals, out);
+            }
+        }
         Term::Lit { .. } => {}
     }
 }
diff --git a/crates/ailang-check/src/pre_desugar_validation.rs b/crates/ailang-check/src/pre_desugar_validation.rs
index c0bcda6..d43cd12 100644
--- a/crates/ailang-check/src/pre_desugar_validation.rs
+++ b/crates/ailang-check/src/pre_desugar_validation.rs
@@ -133,6 +133,18 @@ fn walk_term(t: &Term) -> Result<(), CheckError> {
             walk_term(body)
         }
         Term::Assign { value, .. } => walk_term(value),
+        Term::Loop { binders, body } => {
+            for b in binders {
+                walk_term(&b.init)?;
+            }
+            walk_term(body)
+        }
+        Term::Recur { args } => {
+            for a in args {
+                walk_term(a)?;
+            }
+            Ok(())
+        }
     }
 }
 
diff --git a/crates/ailang-check/src/reuse_shape.rs b/crates/ailang-check/src/reuse_shape.rs
index 72f37cc..7fb7d3c 100644
--- a/crates/ailang-check/src/reuse_shape.rs
+++ b/crates/ailang-check/src/reuse_shape.rs
@@ -265,6 +265,17 @@ impl<'a> Checker<'a> {
                 self.walk(body);
             }
             Term::Assign { value, .. } => self.walk(value),
+            Term::Loop { binders, body } => {
+                for b in binders {
+                    self.walk(&b.init);
+                }
+                self.walk(body);
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    self.walk(a);
+                }
+            }
         }
     }
 
diff --git a/crates/ailang-check/src/uniqueness.rs b/crates/ailang-check/src/uniqueness.rs
index d102d48..42dc739 100644
--- a/crates/ailang-check/src/uniqueness.rs
+++ b/crates/ailang-check/src/uniqueness.rs
@@ -352,6 +352,17 @@ impl<'a> Walker<'a> {
             Term::Assign { value, .. } => {
                 self.walk(value, Position::Consume);
             }
+            Term::Loop { binders, body } => {
+                for b in binders {
+                    self.walk(&b.init, Position::Consume);
+                }
+                self.walk(body, pos);
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    self.walk(a, Position::Consume);
+                }
+            }
         }
     }
 
diff --git a/crates/ailang-check/tests/loop_recur_pin.rs b/crates/ailang-check/tests/loop_recur_pin.rs
new file mode 100644
index 0000000..7c2dba9
--- /dev/null
+++ b/crates/ailang-check/tests/loop_recur_pin.rs
@@ -0,0 +1,60 @@
+//! Iter it.1 (Task 5): pin tests that the four `recur` negative
+//! fixtures produce their exact diagnostic codes, and that the
+//! positive `loop_smoke` fixture typechecks clean.
+//!
+//! Spec: `docs/specs/2026-05-15-iteration-discipline.md`. The four
+//! negatives live as canonical `.ail.json` (diagnostic code is the
+//! load-bearing assertion, not the surface form), mirroring the
+//! `mut_typecheck_pin` carve-out precedent.
+
+use ailang_check::check_workspace;
+use ailang_surface::load_workspace;
+use std::path::PathBuf;
+
+fn examples_dir() -> PathBuf {
+    let manifest = env!("CARGO_MANIFEST_DIR");
+    PathBuf::from(manifest)
+        .parent().expect("CARGO_MANIFEST_DIR has a parent (crates/ailang-check)")
+        .parent().expect("CARGO_MANIFEST_DIR has a grandparent (crates/)")
+        .join("examples")
+}
+
+/// Load the named fixture under `examples/`, run check_workspace, and
+/// return the diagnostic code list (one entry per Diagnostic).
+fn check_fixture(fixture_name: &str) -> Vec<String> {
+    let path = examples_dir().join(fixture_name);
+    let ws = load_workspace(&path)
+        .unwrap_or_else(|e| panic!("workspace `{fixture_name}` must load: {e:?}"));
+    let diags = check_workspace(&ws);
+    diags.iter().map(|d| d.code.clone()).collect()
+}
+
+#[test]
+fn loop_smoke_typechecks_clean() {
+    let codes = check_fixture("loop_smoke.ail");
+    assert!(codes.is_empty(), "expected zero diagnostics, got {codes:?}");
+}
+
+#[test]
+fn recur_outside_loop_is_rejected() {
+    let codes = check_fixture("test_recur_outside_loop.ail.json");
+    assert_eq!(codes, vec!["recur-outside-loop".to_string()]);
+}
+
+#[test]
+fn recur_arity_mismatch_is_rejected() {
+    let codes = check_fixture("test_recur_arity_mismatch.ail.json");
+    assert_eq!(codes, vec!["recur-arity-mismatch".to_string()]);
+}
+
+#[test]
+fn recur_type_mismatch_is_rejected() {
+    let codes = check_fixture("test_recur_type_mismatch.ail.json");
+    assert_eq!(codes, vec!["recur-type-mismatch".to_string()]);
+}
+
+#[test]
+fn recur_not_in_tail_position_is_rejected() {
+    let codes = check_fixture("test_recur_not_in_tail_position.ail.json");
+    assert_eq!(codes, vec!["recur-not-in-tail-position".to_string()]);
+}
diff --git a/crates/ailang-codegen/src/escape.rs b/crates/ailang-codegen/src/escape.rs
index 7a6f48d..dfeacb4 100644
--- a/crates/ailang-codegen/src/escape.rs
+++ b/crates/ailang-codegen/src/escape.rs
@@ -201,6 +201,17 @@ fn walk(t: &Term, out: &mut NonEscapeSet) {
             walk(body, out);
         }
         Term::Assign { value, .. } => walk(value, out),
+        Term::Loop { binders, body } => {
+            for b in binders {
+                walk(&b.init, out);
+            }
+            walk(body, out);
+        }
+        Term::Recur { args } => {
+            for a in args {
+                walk(a, out);
+            }
+        }
         Term::Lit { .. } | Term::Var { .. } => {}
     }
 }
@@ -395,6 +406,15 @@ fn escapes(t: &Term, tainted: &BTreeSet<String>, in_tail: bool) -> bool {
             escapes(body, tainted, in_tail)
         }
         Term::Assign { value, .. } => escapes(value, tainted, false),
+        Term::Loop { binders, body } => {
+            for b in binders {
+                if escapes(&b.init, tainted, false) {
+                    return true;
+                }
+            }
+            escapes(body, tainted, in_tail)
+        }
+        Term::Recur { args } => args.iter().any(|a| escapes(a, tainted, false)),
     }
 }
 
@@ -524,6 +544,26 @@ fn collect_free_vars(t: &Term, bound: &mut BTreeSet<String>, out: &mut BTreeSet<
             }
             collect_free_vars(value, bound, out);
         }
+        // Iter it.1: loop binder names bind inside the body and later
+        // binder inits, mirroring `Term::Mut`. Recur args are uses.
+        Term::Loop { binders, body } => {
+            let mut newly: Vec<String> = Vec::new();
+            for b in binders {
+                collect_free_vars(&b.init, bound, out);
+                if bound.insert(b.name.clone()) {
+                    newly.push(b.name.clone());
+                }
+            }
+            collect_free_vars(body, bound, out);
+            for n in newly {
+                bound.remove(&n);
+            }
+        }
+        Term::Recur { args } => {
+            for a in args {
+                collect_free_vars(a, bound, out);
+            }
+        }
     }
 }
 
diff --git a/crates/ailang-codegen/src/lambda.rs b/crates/ailang-codegen/src/lambda.rs
index 65a8eae..97c6340 100644
--- a/crates/ailang-codegen/src/lambda.rs
+++ b/crates/ailang-codegen/src/lambda.rs
@@ -144,6 +144,12 @@ impl<'a> Emitter<'a> {
         let saved_mut_allocas = std::mem::take(&mut self.mut_var_allocas);
         let saved_pending_allocas = std::mem::take(&mut self.pending_entry_allocas);
         let saved_entry_marker = self.entry_block_end_marker.take();
+        // Iter it.1: a `loop` inside a lambda body scopes its header /
+        // phis to the closure's own body, not the outer fn's. Save and
+        // reset `loop_frames` (the exact mut.3 analogue to
+        // `mut_var_allocas` above) so a `Term::Recur` inside the thunk
+        // cannot back-edge to an outer fn's loop header.
+        let saved_loop_frames = std::mem::take(&mut self.loop_frames);
         // Iter 18d.4 fix: a lambda thunk is its own fn frame for
         // param-mode lookup. The outer fn's params are not in scope
         // inside the thunk; the thunk's own params are pushed below
@@ -258,6 +264,7 @@ impl<'a> Emitter<'a> {
         self.mut_var_allocas = saved_mut_allocas;
         self.pending_entry_allocas = saved_pending_allocas;
         self.entry_block_end_marker = saved_entry_marker;
+        self.loop_frames = saved_loop_frames;
 
         // 3. Emit allocation + capture filling + closure-pair packing
         //    in the OUTER body. Captures use 8 bytes each; closure-pair
@@ -505,6 +512,27 @@ impl<'a> Emitter<'a> {
                 }
                 Self::collect_captures(value, bound, captures, captures_set, builtins, top_level);
             }
+            // Iter it.1: loop binder names bind inside the body and
+            // later binder inits — they are NOT captures, mirroring
+            // the `Term::Mut` arm above. Recur args are uses.
+            Term::Loop { binders, body } => {
+                let mut newly_bound: Vec<String> = Vec::new();
+                for b in binders {
+                    Self::collect_captures(&b.init, bound, captures, captures_set, builtins, top_level);
+                    if bound.insert(b.name.clone()) {
+                        newly_bound.push(b.name.clone());
+                    }
+                }
+                Self::collect_captures(body, bound, captures, captures_set, builtins, top_level);
+                for n in newly_bound {
+                    bound.remove(&n);
+                }
+            }
+            Term::Recur { args } => {
+                for a in args {
+                    Self::collect_captures(a, bound, captures, captures_set, builtins, top_level);
+                }
+            }
         }
     }
 
diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs
index e21ce13..3fbb42e 100644
--- a/crates/ailang-codegen/src/lib.rs
+++ b/crates/ailang-codegen/src/lib.rs
@@ -735,6 +735,28 @@ struct Emitter<'a> {
     /// at fn-body emission. Used to splice `pending_entry_allocas`
     /// into the entry block once body lowering completes.
     entry_block_end_marker: Option<usize>,
+    /// Iter it.1: stack of in-flight `Term::Loop` frames. Innermost
+    /// last. `Term::Recur` consults the innermost frame for the
+    /// header label and records its back-edge incoming values; the
+    /// `Term::Loop` arm patches each phi's incoming list once the
+    /// body (and all its recur sites) has been lowered. Saved /
+    /// reset / restored across the lambda boundary (a `loop` inside
+    /// a closure scopes its header to the closure's own body), the
+    /// exact mut.3 analogue to `mut_var_allocas`.
+    loop_frames: Vec<LoopFrame>,
+}
+
+/// Iter it.1: one in-flight `Term::Loop` being lowered. `phis`
+/// carries, per binder, `(phi_ssa, llvm_ty, placeholder)` — the
+/// placeholder is a unique token emitted in place of the phi's
+/// back-edge incoming list and string-replaced once `recur_edges`
+/// is complete. `recur_edges` collects `(pred_block_label,
+/// [arg_ssa,...])` one entry per `Term::Recur` reached in the body.
+#[derive(Debug, Clone)]
+struct LoopFrame {
+    header: String,
+    phis: Vec<(String, String, String)>,
+    recur_edges: Vec<(String, Vec<String>)>,
 }
 
 #[derive(Debug, Clone)]
@@ -855,6 +877,7 @@ impl<'a> Emitter<'a> {
             mut_var_allocas: BTreeMap::new(),
             pending_entry_allocas: String::new(),
             entry_block_end_marker: None,
+            loop_frames: Vec::new(),
         }
     }
 
@@ -1060,6 +1083,7 @@ impl<'a> Emitter<'a> {
         self.mut_var_allocas.clear();
         self.pending_entry_allocas.clear();
         self.entry_block_end_marker = None;
+        self.loop_frames.clear();
         for (i, pname) in f.params.iter().enumerate() {
             let mode = param_modes.get(i).copied().unwrap_or(ParamMode::Implicit);
             self.current_param_modes.insert(pname.clone(), mode);
@@ -1837,6 +1861,141 @@ impl<'a> Emitter<'a> {
                 ));
                 Ok(("0".into(), "i8".into()))
             }
+            // Iter it.1: a `Term::Loop` lowers to a header block with
+            // one `phi` per binder. Binder inits flow in from the
+            // predecessor block; every enclosed `Term::Recur` adds a
+            // back-edge incoming value. The phi's back-edge incoming
+            // list is emitted as a unique placeholder token and
+            // string-replaced once the body (and all its recur sites)
+            // has been lowered — phi instructions must syntactically
+            // precede the body, but the recur predecessors are only
+            // known after lowering it.
+            Term::Loop { binders, body } => {
+                // 1. Lower each binder init in the CURRENT block.
+                let pred = self.current_block.clone();
+                // Per binder: (name, ail_ty, init_ssa, llvm_ty).
+                let mut init_ssa: Vec<(String, Type, String, String)> = Vec::new();
+                for b in binders {
+                    let lty = llvm_type(&b.ty)?;
+                    let (v, vty) = self.lower_term(&b.init)?;
+                    if vty != lty {
+                        return Err(CodegenError::Internal(format!(
+                            "Term::Loop binder `{}`: init LLVM type {vty} != declared {lty}",
+                            b.name
+                        )));
+                    }
+                    init_ssa.push((b.name.clone(), b.ty.clone(), v, lty));
+                }
+                let id = self.fresh_id();
+                let header = format!("loop.header.{id}");
+                self.body.push_str(&format!("  br label %{header}\n"));
+                self.start_block(&header);
+
+                // 2. One phi per binder. Each phi's back-edge incoming
+                //    list is a placeholder, patched in step 4. Bind the
+                //    phi SSA into `self.locals` so a `Term::Var` for the
+                //    binder name inside the body resolves to it (a loop
+                //    binder shadows like a let binding).
+                let mut phis: Vec<(String, String, String)> = Vec::new();
+                let mut saved_locals: Vec<(String, Option<(String, String, String, Type)>)> =
+                    Vec::new();
+                for (idx, (name, ail_ty, iv, lty)) in init_ssa.iter().enumerate() {
+                    let p = self.fresh_ssa();
+                    let placeholder = format!("/*RECUR_EDGES.{id}.{idx}*/");
+                    self.body.push_str(&format!(
+                        "  {p} = phi {lty} [ {iv}, %{pred} ]{placeholder}\n"
+                    ));
+                    let prior = self
+                        .locals
+                        .iter()
+                        .rposition(|(n, _, _, _)| n == name)
+                        .map(|pos| self.locals.remove(pos));
+                    self.locals.push((
+                        name.clone(),
+                        p.clone(),
+                        lty.clone(),
+                        ail_ty.clone(),
+                    ));
+                    saved_locals.push((name.clone(), prior));
+                    phis.push((p.clone(), lty.clone(), placeholder));
+                }
+
+                // 3. Lower the body inside this loop frame.
+                self.loop_frames.push(LoopFrame {
+                    header: header.clone(),
+                    phis: phis.clone(),
+                    recur_edges: Vec::new(),
+                });
+                let body_result = self.lower_term(body);
+                let frame = self
+                    .loop_frames
+                    .pop()
+                    .expect("loop frame pushed above must still be on the stack");
+
+                // Restore the shadowed locals unconditionally so an
+                // error during body lowering does not leak the binder
+                // bindings into the outer scope.
+                for (name, prior) in saved_locals.into_iter().rev() {
+                    if let Some(pos) = self.locals.iter().rposition(|(n, _, _, _)| n == &name) {
+                        self.locals.remove(pos);
+                    }
+                    if let Some(p) = prior {
+                        self.locals.push(p);
+                    }
+                }
+                let (body_v, body_ty) = body_result?;
+
+                // 4. Patch each phi placeholder with the collected
+                //    back-edge incomings (one `[ arg, %pred ]` per
+                //    recur site). A loop whose only exit is `recur`
+                //    has zero non-recur predecessors after the entry
+                //    edge — that is fine; the phi still lists the
+                //    entry edge plus the recur edges.
+                for (binder_idx, (_p, _lty, placeholder)) in frame.phis.iter().enumerate() {
+                    let mut edges = String::new();
+                    for (pred_lbl, args) in &frame.recur_edges {
+                        let arg = args.get(binder_idx).ok_or_else(|| {
+                            CodegenError::Internal(format!(
+                                "recur edge from %{pred_lbl} missing arg #{binder_idx} \
+                                 — typecheck guarantees arity"
+                            ))
+                        })?;
+                        edges.push_str(&format!(", [ {arg}, %{pred_lbl} ]"));
+                    }
+                    self.body = self.body.replacen(placeholder.as_str(), &edges, 1);
+                }
+
+                // 5. The loop's value is the body value on the
+                //    non-recur exit path. If every path recurred, the
+                //    body block is terminated and the value is unused.
+                Ok((body_v, body_ty))
+            }
+            // Iter it.1: a `Term::Recur` is a back-edge `br` to the
+            // innermost enclosing loop header. It records its argument
+            // SSA values + the current block label so the loop arm can
+            // patch the header phis. `block_terminated = true` is a
+            // NEW, parallel setter (it.1 additive constraint — it does
+            // NOT touch the seven existing tail-driven setters).
+            Term::Recur { args } => {
+                let mut arg_ssa: Vec<String> = Vec::with_capacity(args.len());
+                for a in args {
+                    let (v, _ty) = self.lower_term(a)?;
+                    arg_ssa.push(v);
+                }
+                let from = self.current_block.clone();
+                let frame = self.loop_frames.last_mut().ok_or_else(|| {
+                    CodegenError::Internal(
+                        "Term::Recur without an enclosing loop frame — \
+                         typecheck (RecurOutsideLoop) guarantees this cannot happen"
+                            .into(),
+                    )
+                })?;
+                let header = frame.header.clone();
+                frame.recur_edges.push((from, arg_ssa));
+                self.body.push_str(&format!("  br label %{header}\n"));
+                self.block_terminated = true;
+                Ok(("0".into(), "i8".into()))
+            }
         }
     }
 
@@ -3093,6 +3252,11 @@ impl<'a> Emitter<'a> {
             // is exhaustive on Term so the arms must exist.
             Term::Mut { body, .. } => self.synth_with_extras(body, extras),
             Term::Assign { .. } => Ok(Type::unit()),
+            // Iter it.1: a loop's static type is its body's static
+            // type (spec §"Data model"); `Term::Recur` does not fall
+            // through (its synth value is never consumed).
+            Term::Loop { binders: _, body } => self.synth_with_extras(body, extras),
+            Term::Recur { .. } => Ok(Type::unit()),
         }
     }
 }
diff --git a/crates/ailang-core/specs/form_a.md b/crates/ailang-core/specs/form_a.md
index 2517bb6..6c31d9b 100644
--- a/crates/ailang-core/specs/form_a.md
+++ b/crates/ailang-core/specs/form_a.md
@@ -284,6 +284,8 @@ Parenthesised forms:
 (mut (var NAME TYPE INIT)* BODY-TERM+)  ; local mutable-state block (Iter mut.1)
 (var NAME TYPE INIT)                    ; mut-var declaration; only inside (mut ...)
 (assign NAME VALUE-TERM)                ; mut-var update; only inside (mut ...)
+(loop ((var NAME TYPE INIT)*) BODY-TERM+) ; named loop head (Iter it.1)
+(recur TERM*)                           ; backward jump to nearest enclosing (loop ...)
 ```
 
 Notes:
@@ -322,6 +324,23 @@ Notes:
   pass (iter mut.2) rejects it with `mut-assign-out-of-scope`. The
   expression's static type is Unit. See spec
   `docs/specs/2026-05-15-mut-local.md`.
+- `loop` introduces one or more named, typed, initialised binders
+  (the same `(var NAME TYPE INIT)` shape `mut` uses) wrapped in an
+  explicit binder list `(...)`, followed by one or more body terms
+  right-folded into `Term::Seq` exactly as `mut` does. Each binder's
+  `INIT` is evaluated in scope of the outer environment plus the
+  already-declared binders; the body is in scope of all binders. The
+  loop's static type is the body's static type.
+- `recur` re-enters the lexically nearest enclosing `loop`,
+  rebinding its binders positionally. It must appear in tail
+  position of that loop's body. Diagnostics: `recur-outside-loop`
+  (no enclosing loop), `recur-arity-mismatch` (arg count ≠ binder
+  count), `recur-type-mismatch` (arg type ≠ binder type),
+  `recur-not-in-tail-position` (recur reached outside the loop
+  body's tail context). `loop`/`recur` are additive as of iter it.1;
+  the structural-recursion restriction and the `Diverge` effect land
+  in it.2. See spec
+  `docs/specs/2026-05-15-iteration-discipline.md`.
 
 ## Patterns
 
diff --git a/crates/ailang-core/src/ast.rs b/crates/ailang-core/src/ast.rs
index 6208405..412d5b8 100644
--- a/crates/ailang-core/src/ast.rs
+++ b/crates/ailang-core/src/ast.rs
@@ -537,6 +537,19 @@ pub enum Term {
         name: String,
         value: Box<Term>,
     },
+    /// Named loop head. The only repetition form besides structural
+    /// recursion. Iter it.1. `recur` re-enters the lexically
+    /// nearest enclosing `Loop`, rebinding `binders` positionally.
+    Loop {
+        binders: Vec<LoopBinder>,
+        body: Box<Term>,
+    },
+    /// Backward jump to the lexically nearest enclosing `Loop`.
+    /// Must be in tail position of that loop's body. Iter it.1.
+    Recur {
+        #[serde(default)]
+        args: Vec<Term>,
+    },
 }
 
 /// One arm of a [`Term::Match`].
@@ -580,6 +593,17 @@ pub struct MutVar {
     pub init: Term,
 }
 
+/// One named, typed, initialised binder of a [`Term::Loop`].
+/// Mirrors [`MutVar`] (DD-2): no `PartialEq` — codegen maps the
+/// binder name to an SSA value, never compares binders.
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct LoopBinder {
+    pub name: String,
+    #[serde(rename = "type")]
+    pub ty: Type,
+    pub init: Box<Term>,
+}
+
 /// A match pattern.
 ///
 /// The JSON discriminator is the `p` field. Patterns are linear: each
@@ -946,4 +970,41 @@ mod tests {
             other => panic!("variant mismatch: {other:?}"),
         }
     }
+
+    /// Iter it.1: round-trip a `Term::Loop` through JSON. Pins the
+    /// canonical-form shape and the `LoopBinder.ty` serde rename
+    /// (`"type"`); a future rename or a `skip_serializing_if` on the
+    /// binder fields would break the content-addressed identity this
+    /// pin protects.
+    #[test]
+    fn term_loop_round_trips_through_json() {
+        let t = Term::Loop {
+            binders: vec![LoopBinder {
+                name: "i".into(),
+                ty: Type::int(),
+                init: Box::new(Term::Lit {
+                    lit: Literal::Int { value: 0 },
+                }),
+            }],
+            body: Box::new(Term::Recur {
+                args: vec![Term::Var { name: "i".into() }],
+            }),
+        };
+        let j = serde_json::to_string(&t).expect("serialise");
+        assert!(j.contains(r#""t":"loop""#));
+        assert!(j.contains(r#""type":"#)); // LoopBinder.ty serde rename
+        let back: Term = serde_json::from_str(&j).expect("deserialise");
+        assert_eq!(serde_json::to_string(&back).expect("re-serialise"), j);
+    }
+
+    /// Iter it.1: a zero-arg `Term::Recur` round-trips. `args` carries
+    /// `#[serde(default)]` so an absent `args` key still deserialises;
+    /// the empty vector serialises explicitly.
+    #[test]
+    fn term_recur_empty_args_round_trips() {
+        let t = Term::Recur { args: vec![] };
+        let j = serde_json::to_string(&t).expect("serialise");
+        let back: Term = serde_json::from_str(&j).expect("deserialise");
+        assert_eq!(serde_json::to_string(&back).expect("re-serialise"), j);
+    }
 }
diff --git a/crates/ailang-core/src/desugar.rs b/crates/ailang-core/src/desugar.rs
index 10a2bd2..5651f96 100644
--- a/crates/ailang-core/src/desugar.rs
+++ b/crates/ailang-core/src/desugar.rs
@@ -363,6 +363,18 @@ fn collect_used_in_term(t: &Term, used: &mut BTreeSet<String>) {
             used.insert(name.clone());
             collect_used_in_term(value, used);
         }
+        Term::Loop { binders, body } => {
+            for b in binders {
+                used.insert(b.name.clone());
+                collect_used_in_term(&b.init, used);
+            }
+            collect_used_in_term(body, used);
+        }
+        Term::Recur { args } => {
+            for a in args {
+                collect_used_in_term(a, used);
+            }
+        }
     }
 }
 
@@ -590,6 +602,32 @@ impl Desugarer {
                 name: name.clone(),
                 value: Box::new(self.desugar_term(value, scope)),
             },
+            Term::Loop { binders, body } => {
+                // Iter it.1: loop binders introduce source-level names
+                // like mut-vars; extend the scope per-binder with a
+                // `LetBound` sentinel so a generated fresh name cannot
+                // collide. Binder inits see earlier binders.
+                let mut inner = scope.clone();
+                let new_binders: Vec<LoopBinder> = binders
+                    .iter()
+                    .map(|b| {
+                        let init = self.desugar_term(&b.init, &inner);
+                        inner.insert(b.name.clone(), ScopeEntry::LetBound);
+                        LoopBinder {
+                            name: b.name.clone(),
+                            ty: b.ty.clone(),
+                            init: Box::new(init),
+                        }
+                    })
+                    .collect();
+                Term::Loop {
+                    binders: new_binders,
+                    body: Box::new(self.desugar_term(body, &inner)),
+                }
+            }
+            Term::Recur { args } => Term::Recur {
+                args: args.iter().map(|a| self.desugar_term(a, scope)).collect(),
+            },
             Term::LetRec { name, ty, params, body, in_term } => {
                 // Iter 16b.1: lift to a synthetic top-level fn (no-capture).
                 // Iter 16b.2: extend the lift to the path-1 safe subset —
@@ -1234,6 +1272,23 @@ pub fn free_vars_in_term(t: &Term, bound: &BTreeSet<String>, out: &mut BTreeSet<
             }
             free_vars_in_term(value, bound, out);
         }
+        Term::Loop { binders, body } => {
+            // Iter it.1: a loop binder name binds inside the body.
+            // Each binder's `init` is evaluated in scope of the OUTER
+            // environment plus the already-declared binders; the body
+            // is in scope of all binders. Mirrors `Term::Mut`.
+            let mut b = bound.clone();
+            for binder in binders {
+                free_vars_in_term(&binder.init, &b, out);
+                b.insert(binder.name.clone());
+            }
+            free_vars_in_term(body, &b, out);
+        }
+        Term::Recur { args } => {
+            for a in args {
+                free_vars_in_term(a, bound, out);
+            }
+        }
     }
 }
 
@@ -1427,6 +1482,43 @@ pub fn subst_var(t: &Term, from: &str, to: &str) -> Term {
             name: name.clone(),
             value: Box::new(subst_var(value, from, to)),
         },
+        Term::Loop { binders, body } => {
+            // Iter it.1: loop binders lexically shadow outer names,
+            // exactly like mut-vars (above). Once a binder named
+            // `from` is declared, later inits AND the body stop
+            // substituting.
+            let mut shadowed = false;
+            let new_binders: Vec<LoopBinder> = binders
+                .iter()
+                .map(|b| {
+                    let init = if shadowed {
+                        (*b.init).clone()
+                    } else {
+                        subst_var(&b.init, from, to)
+                    };
+                    if b.name == from {
+                        shadowed = true;
+                    }
+                    LoopBinder {
+                        name: b.name.clone(),
+                        ty: b.ty.clone(),
+                        init: Box::new(init),
+                    }
+                })
+                .collect();
+            let body_rw = if shadowed {
+                (**body).clone()
+            } else {
+                subst_var(body, from, to)
+            };
+            Term::Loop {
+                binders: new_binders,
+                body: Box::new(body_rw),
+            }
+        }
+        Term::Recur { args } => Term::Recur {
+            args: args.iter().map(|a| subst_var(a, from, to)).collect(),
+        },
     }
 }
 
@@ -1568,6 +1660,23 @@ pub fn subst_call_with_extras(t: &Term, name: &str, lifted: &str, extras: &[Stri
             name: assign_name.clone(),
             value: Box::new(subst_call_with_extras(value, name, lifted, extras)),
         },
+        Term::Loop { binders, body } => Term::Loop {
+            binders: binders
+                .iter()
+                .map(|b| LoopBinder {
+                    name: b.name.clone(),
+                    ty: b.ty.clone(),
+                    init: Box::new(subst_call_with_extras(&b.init, name, lifted, extras)),
+                })
+                .collect(),
+            body: Box::new(subst_call_with_extras(body, name, lifted, extras)),
+        },
+        Term::Recur { args } => Term::Recur {
+            args: args
+                .iter()
+                .map(|a| subst_call_with_extras(a, name, lifted, extras))
+                .collect(),
+        },
     }
 }
 
@@ -1640,6 +1749,14 @@ pub fn find_non_callee_use(t: &Term, name: &str) -> Option<Term> {
                 find_non_callee_use(value, name)
             }
         }
+        // Iter it.1: scan each binder's init plus the body. Loop
+        // binders never appear in callee position, so any matching
+        // `Term::Var` inside a loop is non-callee by construction.
+        Term::Loop { binders, body } => binders
+            .iter()
+            .find_map(|b| find_non_callee_use(&b.init, name))
+            .or_else(|| find_non_callee_use(body, name)),
+        Term::Recur { args } => args.iter().find_map(|a| find_non_callee_use(a, name)),
     }
 }
 
@@ -1687,6 +1804,10 @@ mod tests {
                 vars.iter().any(|v| any_nested_ctor(&v.init)) || any_nested_ctor(body)
             }
             Term::Assign { value, .. } => any_nested_ctor(value),
+            Term::Loop { binders, body } => {
+                binders.iter().any(|b| any_nested_ctor(&b.init)) || any_nested_ctor(body)
+            }
+            Term::Recur { args } => args.iter().any(any_nested_ctor),
         }
     }
 
@@ -1717,6 +1838,10 @@ mod tests {
                 vars.iter().any(|v| any_let_rec(&v.init)) || any_let_rec(body)
             }
             Term::Assign { value, .. } => any_let_rec(value),
+            Term::Loop { binders, body } => {
+                binders.iter().any(|b| any_let_rec(&b.init)) || any_let_rec(body)
+            }
+            Term::Recur { args } => args.iter().any(any_let_rec),
         }
     }
 
@@ -2838,6 +2963,10 @@ mod tests {
                 vars.iter().any(|v| any_lit_pattern(&v.init)) || any_lit_pattern(body)
             }
             Term::Assign { value, .. } => any_lit_pattern(value),
+            Term::Loop { binders, body } => {
+                binders.iter().any(|b| any_lit_pattern(&b.init)) || any_lit_pattern(body)
+            }
+            Term::Recur { args } => args.iter().any(any_lit_pattern),
         }
     }
 
diff --git a/crates/ailang-core/src/workspace.rs b/crates/ailang-core/src/workspace.rs
index dad8361..0da8869 100644
--- a/crates/ailang-core/src/workspace.rs
+++ b/crates/ailang-core/src/workspace.rs
@@ -1259,6 +1259,22 @@ where
             walk_term_embedded_types(body, f)
         }
         Term::Assign { value, .. } => walk_term_embedded_types(value, f),
+        // Iter it.1: each `LoopBinder.ty` is an embedded type — walk
+        // it, then recurse into each binder's `init` and the body.
+        // `Term::Recur` carries no embedded type.
+        Term::Loop { binders, body } => {
+            for b in binders {
+                walk_type(&b.ty, f)?;
+                walk_term_embedded_types(&b.init, f)?;
+            }
+            walk_term_embedded_types(body, f)
+        }
+        Term::Recur { args } => {
+            for a in args {
+                walk_term_embedded_types(a, f)?;
+            }
+            Ok(())
+        }
     }
 }
 
@@ -1392,6 +1408,18 @@ where
             walk_term(body, f)
         }
         Term::Assign { value, .. } => walk_term(value, f),
+        Term::Loop { binders, body } => {
+            for b in binders {
+                walk_term(&b.init, f)?;
+            }
+            walk_term(body, f)
+        }
+        Term::Recur { args } => {
+            for a in args {
+                walk_term(a, f)?;
+            }
+            Ok(())
+        }
     }
 }
 
diff --git a/crates/ailang-core/tests/carve_out_inventory.rs b/crates/ailang-core/tests/carve_out_inventory.rs
index e36c78f..31c974b 100644
--- a/crates/ailang-core/tests/carve_out_inventory.rs
+++ b/crates/ailang-core/tests/carve_out_inventory.rs
@@ -37,6 +37,11 @@ const EXPECTED: &[&str] = &[
     "test_mut_var_unsupported_type.ail.json",
     // Iter mut.4-tidy — lambda-capture-of-mut-var rejection
     "test_mut_var_captured_by_lambda.ail.json",
+    // Iter it.1 — recur negative typecheck fixtures
+    "test_recur_outside_loop.ail.json",
+    "test_recur_arity_mismatch.ail.json",
+    "test_recur_type_mismatch.ail.json",
+    "test_recur_not_in_tail_position.ail.json",
 ];
 
 fn examples_dir() -> std::path::PathBuf {
diff --git a/crates/ailang-core/tests/design_schema_drift.rs b/crates/ailang-core/tests/design_schema_drift.rs
index 544440e..d5cf2b3 100644
--- a/crates/ailang-core/tests/design_schema_drift.rs
+++ b/crates/ailang-core/tests/design_schema_drift.rs
@@ -151,6 +151,17 @@ fn design_md_anchors_every_term_variant() {
                 value: Box::new(Term::Lit { lit: Literal::Unit }),
             },
         ),
+        (
+            r#""t": "loop""#,
+            Term::Loop {
+                binders: Vec::new(),
+                body: Box::new(Term::Lit { lit: Literal::Unit }),
+            },
+        ),
+        (
+            r#""t": "recur""#,
+            Term::Recur { args: Vec::new() },
+        ),
     ];
 
     for (anchor, term) in exemplars {
@@ -172,6 +183,8 @@ fn design_md_anchors_every_term_variant() {
             Term::ReuseAs { .. } => "reuse-as",
             Term::Mut { .. } => "mut",
             Term::Assign { .. } => "assign",
+            Term::Loop { .. } => "loop",
+            Term::Recur { .. } => "recur",
         };
         assert!(
             data_model_section().contains(anchor),
diff --git a/crates/ailang-core/tests/schema_coverage.rs b/crates/ailang-core/tests/schema_coverage.rs
index fcc7d13..25cc4cb 100644
--- a/crates/ailang-core/tests/schema_coverage.rs
+++ b/crates/ailang-core/tests/schema_coverage.rs
@@ -49,6 +49,8 @@ enum VariantTag {
     TermReuseAs,
     TermMut,
     TermAssign,
+    TermLoop,
+    TermRecur,
     // Pattern
     PatternWild,
     PatternVar,
@@ -96,6 +98,8 @@ const EXPECTED_VARIANTS: &[VariantTag] = &[
     VariantTag::TermReuseAs,
     VariantTag::TermMut,
     VariantTag::TermAssign,
+    VariantTag::TermLoop,
+    VariantTag::TermRecur,
     VariantTag::PatternWild,
     VariantTag::PatternVar,
     VariantTag::PatternLit,
@@ -244,6 +248,20 @@ fn visit_term(t: &Term, observed: &mut HashSet<VariantTag>) {
             observed.insert(VariantTag::TermAssign);
             visit_term(value, observed);
         }
+        Term::Loop { binders, body } => {
+            observed.insert(VariantTag::TermLoop);
+            for b in binders {
+                visit_type(&b.ty, observed);
+                visit_term(&b.init, observed);
+            }
+            visit_term(body, observed);
+        }
+        Term::Recur { args } => {
+            observed.insert(VariantTag::TermRecur);
+            for a in args {
+                visit_term(a, observed);
+            }
+        }
     }
 }
 
diff --git a/crates/ailang-core/tests/spec_drift.rs b/crates/ailang-core/tests/spec_drift.rs
index a7d1371..b1a01bd 100644
--- a/crates/ailang-core/tests/spec_drift.rs
+++ b/crates/ailang-core/tests/spec_drift.rs
@@ -128,6 +128,17 @@ fn spec_mentions_every_term_variant() {
                 value: Box::new(Term::Lit { lit: Literal::Unit }),
             },
         ),
+        (
+            "(loop",
+            Term::Loop {
+                binders: Vec::new(),
+                body: Box::new(Term::Lit { lit: Literal::Unit }),
+            },
+        ),
+        (
+            "(recur",
+            Term::Recur { args: Vec::new() },
+        ),
     ];
 
     for (anchor, term) in exemplars {
@@ -151,6 +162,8 @@ fn spec_mentions_every_term_variant() {
             Term::ReuseAs { .. } => "reuse-as",
             Term::Mut { .. } => "mut",
             Term::Assign { .. } => "assign",
+            Term::Loop { .. } => "loop",
+            Term::Recur { .. } => "recur",
         };
         assert!(
             FORM_A_SPEC.contains(anchor),
diff --git a/crates/ailang-prose/src/lib.rs b/crates/ailang-prose/src/lib.rs
index baa3f39..76bfc60 100644
--- a/crates/ailang-prose/src/lib.rs
+++ b/crates/ailang-prose/src/lib.rs
@@ -935,6 +935,37 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8, ow
             out.push_str(" := ");
             write_term(out, value, level, owning_module);
         }
+        Term::Loop { binders, body } => {
+            // Iter it.1: prose-side minimal-correctness rendering for
+            // the `(loop ...)` head, mirroring the `mut` block shape
+            // above. The prose surface for loops is not yet fully
+            // designed; a follow-on prose iter refines it once the
+            // LLM-author signal arrives.
+            out.push_str("loop {\n");
+            for b in binders {
+                indent(out, level + 1);
+                out.push_str("var ");
+                out.push_str(&b.name);
+                out.push_str(" = ");
+                write_term(out, &b.init, level + 1, owning_module);
+                out.push_str(";\n");
+            }
+            indent(out, level + 1);
+            write_term(out, body, level + 1, owning_module);
+            out.push('\n');
+            indent(out, level);
+            out.push('}');
+        }
+        Term::Recur { args } => {
+            out.push_str("recur(");
+            for (i, a) in args.iter().enumerate() {
+                if i > 0 {
+                    out.push_str(", ");
+                }
+                write_term(out, a, level, owning_module);
+            }
+            out.push(')');
+        }
     }
 }
 
@@ -1133,6 +1164,26 @@ fn count_free_var(name: &str, t: &Term) -> usize {
             let n_use = if assign_name == name { 1 } else { 0 };
             n_use + count_free_var(name, value)
         }
+        // Iter it.1: a loop binder named `name` shadows the outer
+        // binding for both later binder inits and the body, exactly
+        // like `Term::Mut`.
+        Term::Loop { binders, body } => {
+            let mut total = 0usize;
+            let mut shadowed = false;
+            for b in binders {
+                if !shadowed {
+                    total += count_free_var(name, &b.init);
+                }
+                if b.name == name {
+                    shadowed = true;
+                }
+            }
+            if !shadowed {
+                total += count_free_var(name, body);
+            }
+            total
+        }
+        Term::Recur { args } => args.iter().map(|a| count_free_var(name, a)).sum(),
     }
 }
 
@@ -1285,6 +1336,39 @@ fn subst_var_with_term(t: &Term, name: &str, replacement: &Term) -> Term {
             name: assign_name.clone(),
             value: Box::new(subst_var_with_term(value, name, replacement)),
         },
+        Term::Loop { binders, body } => {
+            let mut shadowed = false;
+            let new_binders: Vec<ailang_core::ast::LoopBinder> = binders
+                .iter()
+                .map(|b| {
+                    let init = if shadowed {
+                        (*b.init).clone()
+                    } else {
+                        subst_var_with_term(&b.init, name, replacement)
+                    };
+                    if b.name == name {
+                        shadowed = true;
+                    }
+                    ailang_core::ast::LoopBinder {
+                        name: b.name.clone(),
+                        ty: b.ty.clone(),
+                        init: Box::new(init),
+                    }
+                })
+                .collect();
+            let body_rw = if shadowed {
+                (**body).clone()
+            } else {
+                subst_var_with_term(body, name, replacement)
+            };
+            Term::Loop {
+                binders: new_binders,
+                body: Box::new(body_rw),
+            }
+        }
+        Term::Recur { args } => Term::Recur {
+            args: args.iter().map(|a| subst_var_with_term(a, name, replacement)).collect(),
+        },
     }
 }
 
@@ -2101,6 +2185,43 @@ mod tests {
         assert_eq!(render_term(&t), "tail not(x)");
     }
 
+    /// Iter it.1: prose-projection lockstep for `Term::Loop` /
+    /// `Term::Recur`. The property protected: the prose renderer
+    /// projects a loop's binders + body and a recur's args without
+    /// dropping or reordering them (free-var / subst arms are
+    /// exercised by the existing prose suite). Prose is a one-way
+    /// projection (no Form-B parser exists — see CLAUDE.md), so an
+    /// AST-equality round-trip is not expressible; this render
+    /// assertion is the feasible lockstep, using the same
+    /// `render_term` harness the neighbouring render tests use.
+    #[test]
+    fn loop_and_recur_project_to_prose() {
+        let t = Term::Loop {
+            binders: vec![ailang_core::ast::LoopBinder {
+                name: "i".into(),
+                ty: ailang_core::ast::Type::Con {
+                    name: "Int".into(),
+                    args: vec![],
+                },
+                init: Box::new(Term::Lit {
+                    lit: ailang_core::ast::Literal::Int { value: 0 },
+                }),
+            }],
+            body: Box::new(Term::Recur {
+                args: vec![ivar("i")],
+            }),
+        };
+        let rendered = render_term(&t);
+        assert!(
+            rendered.contains("loop {") && rendered.contains("var i = 0"),
+            "loop head not projected, got:\n{rendered}"
+        );
+        assert!(
+            rendered.contains("recur(i)"),
+            "recur not projected, got:\n{rendered}"
+        );
+    }
+
     // ---- Polish 4: long doc-string wrap ----
 
     #[test]
diff --git a/crates/ailang-surface/src/parse.rs b/crates/ailang-surface/src/parse.rs
index 6d4a593..09c0c0d 100644
--- a/crates/ailang-surface/src/parse.rs
+++ b/crates/ailang-surface/src/parse.rs
@@ -40,7 +40,7 @@
 //!               | app-term | tail-app-term | match-term | ctor-term
 //!               | do-term | tail-do-term | seq-term | lam-term | if-term
 //!               | let-term | let-rec-term | clone-term | reuse-as-term
-//!               | mut-term | assign-term
+//!               | mut-term | assign-term | loop-term | recur-term
 //! var-ref     ::= ident                  ; reserved: true/false → bool-lit
 //! int-lit     ::= integer                ; numeric atom
 //! str-lit     ::= string                 ; string atom
@@ -68,8 +68,10 @@
 //! clone-term  ::= "(" "clone" term ")"      ; Iter 18c.1
 //! reuse-as-term ::= "(" "reuse-as" term term ")"  ; Iter 18d.1
 //! mut-term     ::= "(" "mut" var-decl* term+ ")"   ; Iter mut.1
-//! var-decl     ::= "(" "var" ident type term ")"   ; legal only inside mut-term
+//! var-decl     ::= "(" "var" ident type term ")"   ; legal only inside mut-term / loop-term
 //! assign-term  ::= "(" "assign" ident term ")"     ; Iter mut.1; legal only inside mut-term
+//! loop-term    ::= "(" "loop" "(" var-decl* ")" term+ ")"  ; Iter it.1
+//! recur-term   ::= "(" "recur" term* ")"           ; Iter it.1; tail-position-only in loop
 //!
 //! pattern  ::= pat-var | pat-ctor | pat-lit | pat-wild
 //! pat-var  ::= ident
@@ -1212,6 +1214,8 @@ impl<'a> Parser<'a> {
                     "reuse-as" => self.parse_reuse_as(),
                     "mut" => self.parse_mut(),
                     "assign" => self.parse_assign(),
+                    "loop" => self.parse_loop(),
+                    "recur" => self.parse_recur(),
                     other => {
                         let pos = self.peek().map(|t| t.span.start).unwrap_or(0);
                         Err(ParseError::Production {
@@ -1220,7 +1224,7 @@ impl<'a> Parser<'a> {
                                 "unknown term head `{other}`; expected one of \
                                 `app`, `tail-app`, `lam`, `let`, `let-rec`, `if`, `match`, `do`, \
                                 `tail-do`, `seq`, `term-ctor`, `clone`, `reuse-as`, `mut`, \
-                                `assign`, `lit-unit`"
+                                `assign`, `loop`, `recur`, `lit-unit`"
                             ),
                             pos,
                         })
@@ -1642,6 +1646,80 @@ impl<'a> Parser<'a> {
         })
     }
 
+    /// Iter it.1: `(loop ((var NAME TYPE INIT)*) BODY-TERM+)` — named
+    /// loop head. The binder list is an explicit parenthesised group
+    /// holding zero or more `(var NAME TYPE INIT)` entries (same entry
+    /// shape `parse_mut` reads); the trailing ≥ 1 body terms are
+    /// right-folded into `Term::Seq` exactly as `parse_mut` does. The
+    /// recur arity / type / tail-position rules are enforced at
+    /// typecheck (it.1 Task 5); the parser accepts the shape.
+    fn parse_loop(&mut self) -> Result<Term, ParseError> {
+        let head_pos = self.peek().map(|t| t.span.start).unwrap_or(0);
+        self.expect_lparen("loop-term")?;
+        self.expect_keyword("loop")?;
+
+        // The binder list is an explicit parenthesised group of
+        // (var NAME TYPE INIT) entries.
+        self.expect_lparen("loop-binder-list")?;
+        let mut binders: Vec<ailang_core::ast::LoopBinder> = Vec::new();
+        while matches!(self.peek_head_ident(), Some("var")) {
+            self.expect_lparen("loop-binder")?;
+            self.expect_keyword("var")?;
+            let name = self.expect_ident("loop-binder-name")?;
+            let ty = self.parse_type()?;
+            let init = self.parse_term()?;
+            self.expect_rparen("loop-binder")?;
+            binders.push(ailang_core::ast::LoopBinder {
+                name,
+                ty,
+                init: Box::new(init),
+            });
+        }
+        self.expect_rparen("loop-binder-list")?;
+
+        // Then read ≥ 1 trailing body terms, right-folded into Seq.
+        let mut body_stmts: Vec<Term> = Vec::new();
+        while !matches!(self.peek(), Some(Token { tok: Tok::RParen, .. })) {
+            body_stmts.push(self.parse_term()?);
+        }
+        if body_stmts.is_empty() {
+            return Err(ParseError::Production {
+                production: "loop-term",
+                message: "(loop ...) requires at least one body expression after the binder list"
+                    .into(),
+                pos: head_pos,
+            });
+        }
+        self.expect_rparen("loop-term")?;
+
+        let mut body = body_stmts.pop().expect("non-empty after the check above");
+        while let Some(s) = body_stmts.pop() {
+            body = Term::Seq {
+                lhs: Box::new(s),
+                rhs: Box::new(body),
+            };
+        }
+        Ok(Term::Loop {
+            binders,
+            body: Box::new(body),
+        })
+    }
+
+    /// Iter it.1: `(recur TERM*)` — backward jump to the lexically
+    /// nearest enclosing `(loop ...)`. The parser accepts any arg
+    /// count; the enclosing-loop / arity / type / tail-position rules
+    /// are enforced at typecheck (it.1 Task 5).
+    fn parse_recur(&mut self) -> Result<Term, ParseError> {
+        self.expect_lparen("recur-term")?;
+        self.expect_keyword("recur")?;
+        let mut args: Vec<Term> = Vec::new();
+        while !matches!(self.peek(), Some(Token { tok: Tok::RParen, .. })) {
+            args.push(self.parse_term()?);
+        }
+        self.expect_rparen("recur-term")?;
+        Ok(Term::Recur { args })
+    }
+
     // ---- patterns -------------------------------------------------------
 
     fn parse_pattern(&mut self) -> Result<Pattern, ParseError> {
@@ -2583,4 +2661,29 @@ mod tests {
             "diagnostic should mention missing body, got: {msg}"
         );
     }
+
+    /// Iter it.1: `(loop ((var i Int 0)) (recur i))` parses to a
+    /// `Term::Loop` with one binder and a `Term::Recur` body. The
+    /// binder list is explicitly parenthesised (unlike `mut`).
+    #[test]
+    fn parses_loop_with_one_binder_and_recur_body() {
+        let src = "(loop ((var i (con Int) 0)) (recur i))";
+        let t = parse_term(src).expect("loop parses");
+        match t {
+            Term::Loop { binders, body } => {
+                assert_eq!(binders.len(), 1);
+                assert_eq!(binders[0].name, "i");
+                assert!(matches!(*body, Term::Recur { .. }));
+            }
+            other => panic!("expected Term::Loop, got {other:?}"),
+        }
+    }
+
+    /// Iter it.1: `(recur)` with no args parses to an empty-args
+    /// `Term::Recur` (arity/scope validity is a typecheck concern).
+    #[test]
+    fn parses_recur_zero_args() {
+        let t = parse_term("(recur)").expect("recur parses");
+        assert!(matches!(t, Term::Recur { args } if args.is_empty()));
+    }
 }
diff --git a/crates/ailang-surface/src/print.rs b/crates/ailang-surface/src/print.rs
index 82eb166..39bd7ef 100644
--- a/crates/ailang-surface/src/print.rs
+++ b/crates/ailang-surface/src/print.rs
@@ -594,6 +594,54 @@ fn write_term(out: &mut String, t: &Term, level: usize) {
             write_term(out, value, level);
             out.push(')');
         }
+        Term::Loop { binders, body } => {
+            // Iter it.1: print as
+            //   `(loop ((var NAME TYPE INIT)*) STMT* FINAL_EXPR)`
+            // The binder list is explicitly parenthesised (unlike
+            // `mut`); the body's `Term::Seq` right-spine is walked the
+            // same way the `Term::Mut` arm above walks it.
+            out.push_str("(loop (");
+            for (k, b) in binders.iter().enumerate() {
+                if k > 0 {
+                    out.push(' ');
+                }
+                out.push_str("(var ");
+                out.push_str(&b.name);
+                out.push(' ');
+                write_type(out, &b.ty);
+                out.push(' ');
+                write_term(out, &b.init, level);
+                out.push(')');
+            }
+            out.push(')');
+            let mut cursor: &Term = body;
+            loop {
+                match cursor {
+                    Term::Seq { lhs, rhs } => {
+                        out.push(' ');
+                        write_term(out, lhs, level);
+                        cursor = rhs;
+                    }
+                    other => {
+                        out.push(' ');
+                        write_term(out, other, level);
+                        break;
+                    }
+                }
+            }
+            out.push(')');
+        }
+        Term::Recur { args } => {
+            // Iter it.1: print as `(recur ARG*)`. Legal only in tail
+            // position of an enclosing `Term::Loop` body; the
+            // typechecker (it.1 Task 5) enforces that rule.
+            out.push_str("(recur");
+            for a in args {
+                out.push(' ');
+                write_term(out, a, level);
+            }
+            out.push(')');
+        }
     }
 }
 
diff --git a/docs/DESIGN.md b/docs/DESIGN.md
index 5ca540a..617b9dd 100644
--- a/docs/DESIGN.md
+++ b/docs/DESIGN.md
@@ -2410,6 +2410,22 @@ are real surface forms.
 { "t": "assign",
   "name": "<id>",
   "value": Term }
+
+// Iter it.1: named loop head. `binders` declares one or more
+// lexically-scoped, typed, initialised binders (initialised in
+// order); `body` is a single Term in scope of all binders. `recur`
+// re-enters the lexically nearest enclosing loop, rebinding the
+// binders positionally; it must be in tail position of that loop's
+// body. The loop's static type is `body`'s static type.
+{ "t": "loop",
+  "binders": [ { "name": "<id>", "type": Type, "init": Term }, ... ],
+  "body": Term }
+
+// Iter it.1: backward jump to the lexically nearest enclosing loop;
+// tail-position-only; binds that loop's binders. The `args` array is
+// always present in canonical JSON (even when empty).
+{ "t": "recur",
+  "args": [ Term, ... ] }
 ```
 
 In the MVP, `do` is only a direct call to a built-in effect op (no
@@ -2425,6 +2441,15 @@ mut-var into a lambda body is rejected at typecheck via
 `CheckError::MutVarCapturedByLambda` (iter mut.4-tidy). See
 `docs/specs/2026-05-15-mut-local.md`.
 
+`loop`/`recur` are additive as of iter it.1 (2026-05-15): they
+parse, print, prose-project, round-trip, typecheck (binder typing,
+recur arity/type unification, recur tail-position) and codegen
+(loop-header block with one phi per binder, `recur` as a back-edge
+`br`) without removing or modifying the existing `tail-app`/`tail-do`
+paths. The structural-recursion restriction and the `Diverge`
+effect land in it.2; `tail-app`/`tail-do` are retired in it.3. See
+`docs/specs/2026-05-15-iteration-discipline.md`.
+
 **`Literal`**:
 
 ```jsonc
diff --git a/docs/journals/2026-05-15-iter-it.1.md b/docs/journals/2026-05-15-iter-it.1.md
new file mode 100644
index 0000000..ca5cc7d
--- /dev/null
+++ b/docs/journals/2026-05-15-iter-it.1.md
@@ -0,0 +1,251 @@
+# iter it.1 — loop/recur additive (parse/print/prose/check/codegen)
+
+**Date:** 2026-05-15
+**Started from:** 7381a4233b0ea34b23871c59e3a3e802441751ef
+**Status:** DONE
+**Tasks completed:** 8 of 8
+
+## Summary
+
+First of three iterations in the iteration-discipline milestone.
+Adds `Term::Loop` / `Term::Recur` / `LoopBinder` as first-class
+additive AST nodes end-to-end — parse, print, prose projection,
+canonical-JSON serde + round-trip, schema/spec-drift lockstep,
+typecheck (binder typing, recur arity/type unification via a
+`loop_stack: &mut Vec<Vec<Type>>` threaded exactly as mut.2 threaded
+`mut_scope_stack`, recur tail-position via a new private
+`verify_loop_body` helper with `verify_tail_positions`'s public
+signature unchanged), and codegen (loop-header block with one phi
+per binder, `recur` as a back-edge `br` with a NEW parallel
+`block_terminated = true` setter). The change is **strictly
+additive**: zero deletions touch the existing `tail-app`/`tail-do`
+paths, `verify_tail_positions`' tail-app role, or any of the seven
+existing codegen `block_terminated` sites — the 32 within-iter
+deletion-lines are exclusively the Task-1 `Internal(...)` stubs and
+the Task-1 `verify_tail_positions` structural-passthrough being
+replaced by their real Task-5/Task-7 implementations (DD-3
+stub-then-fill). This additive discipline is what makes the
+destructive it.3 safe later. Full `cargo test --workspace` green
+(63 ok result groups, 0 failed); `loop_counter.ail` builds and
+prints `55`; the four `Recur*` diagnostics fire on their negatives;
+`tail-app` fixtures (`bench_compute_intsum`, `list_map_poly`) run
+byte-identically; zero IR/prose snapshot drift.
+
+## Per-task notes
+
+- iter it.1.1: AST variants + every walker arm + serde/schema
+  lockstep. `Term::Loop { binders: Vec<LoopBinder>, body: Box<Term> }`,
+  `Term::Recur { #[serde(default)] args: Vec<Term> }`, and
+  `LoopBinder { name, #[serde(rename="type")] ty, init: Box<Term> }`
+  (DD-2 derives = `Debug, Clone, Serialize, Deserialize`, no
+  PartialEq; note `init` is `Box<Term>` per the plan's literal code
+  block, whereas `MutVar.init` is bare `Term` — a small divergence
+  from "mirrors MutVar exactly", recorded under Concerns). ~40
+  walker arms across desugar (incl. 3 in-test `any_*` helpers not
+  enumerated by the plan), workspace, all of ailang-check
+  (lib/lift/linearity/mono/pre_desugar_validation/reuse_shape/
+  uniqueness), codegen (escape×3/lambda/lib), prose, surface
+  parse/print, ail main + the test-side
+  `codegen_import_map_fallback_pin.rs` walker the plan flagged
+  (mut.1 missed its analogue; did not miss it here). Typecheck +
+  codegen *dispatch* stubbed `Internal(...)` (tuple variant —
+  the plan pseudo-code's `Internal { msg }` struct form does not
+  exist; copied mut.1's verbatim tuple shape). `synth_with_extras`
+  got real arms (loop → body's type, recur → unit) per plan.
+  schema_coverage left RED on "variant never observed" until
+  Task 3 (plan-expected); every other test green.
+
+- iter it.1.2: Form-A parse. `parse_loop` / `parse_recur` modelled
+  on `parse_mut` / `parse_assign`; the binder list is an explicitly
+  parenthesised group `(loop ((var ...)*) BODY+)` (form_a.md
+  production added in Task 1.10 lockstep). Plan pseudo-code named
+  non-existent helpers (`parse_term_str`, `parse_body_seq`,
+  `parse_loop_binders`); substituted the real harness (module-level
+  `parse_term`) and inlined the per-`(var …)` decode exactly as
+  `parse_mut` does — the plan explicitly forbade introducing a new
+  body-folding helper. EBNF prologue + unknown-head error list
+  extended. RED→GREEN confirmed.
+
+- iter it.1.3: Form-A print + positive fixtures. Print arms landed
+  early in Task 1 as a build-unblock necessity (documented mut.1
+  precedent — print arms are exhaustive-match neighbours of the
+  synth/lower_term dispatchers). `loop_smoke.ail` /
+  `loop_nested_in_lambda.ail` written in real Form-A matching
+  `mut_counter.ail`'s verbatim surface spellings (`(con Int)`,
+  `(app == …)`, `(app + …)`, `(lam (params (typed …)) (ret …)
+  (body …))`) — the plan's fixture pseudo-code (`(fn count_to :
+  Int -> Int …)`) is not valid Form-A and the plan's prose
+  explicitly directed matching mut_counter.ail verbatim.
+  parse→print→parse byte-idempotent; schema_coverage now GREEN
+  (Task 1.11 deferred RED closed).
+
+- iter it.1.4: Prose projection lockstep. Step 4.1's literal
+  instruction ("render to prose and back, asserting AST equality")
+  is **not expressible** — AILang has no Form-B→AST parser by
+  design (CLAUDE.md / `crates/ail/src/main.rs:207` "no parser
+  exists for the prose surface"). Recorded as a plan defect (see
+  Concerns). The substantive work (render/free-var/subst arms,
+  landed in Task 1) is correct and verified by the full prose
+  suite; added `loop_and_recur_project_to_prose`, a render-assertion
+  pin using the same `render_term` harness the nearest existing
+  prose tests (`not_with_tail_flag_keeps_prefix_form`) use — the
+  feasible equivalent of the plan's intent. This is the documented
+  mut.1-class plan-pseudo-vs-real-API substitution, not a silent
+  swap. Status DONE_WITH_CONCERNS.
+
+- iter it.1.5: Real typecheck (DD-1). Four `CheckError` variants
+  (`RecurOutsideLoop` / `RecurArityMismatch` / `RecurTypeMismatch`
+  / `RecurNotInTailPosition`) — **no `span` field** because no
+  `Span` type is in scope in this crate and no existing CheckError
+  variant carries one (the plan pseudo-code's `span: Option<Span>`
+  references a non-existent-here type; mirrored the real
+  `MutAssignOutOfScope` field-shape exactly as the plan's prose
+  instructed). `loop_stack: &mut Vec<Vec<Type>>` threaded through
+  `synth`'s signature + every call site (signature + 22 single-line
+  recursive + 3 multi-line recursive + 2 production entry points +
+  lift.rs + 2 mono.rs + builtins.rs test helpers + 8 in-source
+  `#[cfg(test)]` calls), exactly the mut.2 pattern. Real Loop arm
+  binds binder names into `self`-… `locals` (save/restore like
+  `Term::Let` — the correct precedent for *immutable* bindings,
+  not the mut-var mechanism) and pushes the binder type-vector onto
+  `loop_stack`. **`Term::Recur` synth returns a fresh metavar
+  (`Subst::fresh(counter)`), not the plan's flagged-risky
+  `Type::unit()`** — see Concerns; this resolves the plan's own
+  self-review "Open risk" correctly (a fresh metavar is the
+  codebase-idiomatic bottom that unifies anywhere, which is what
+  makes `(if c then (recur …))` typecheck — `Type::unit()` would
+  have broken `loop_smoke`'s if-branch unification). `verify_loop_body`
+  added as a new private helper; `verify_tail_positions`' public
+  signature unchanged (it.3 reworks it). The diagnostic-doc list in
+  `diagnostic.rs` was NOT extended — the mut codes were never added
+  there (false plan premise; followed the actual mut.2 precedent).
+  RED→GREEN: loop_smoke clean, four negatives each return their
+  exact code. `loop_stack` threading caused zero regressions.
+
+- iter it.1.6: Carve-out inventory. EXPECTED extended with the four
+  `test_recur_*.ail.json` negatives, 13→17, in an it.1 group
+  (the const is milestone-grouped not alphabetical; the test uses
+  a BTreeSet so order is functionally irrelevant). GREEN.
+
+- iter it.1.7: Real codegen (loop-header + phi + recur back-edge +
+  lambda boundary). `loop_frames: Vec<LoopFrame>` field added (mut.3
+  analogue to `mut_var_allocas` — init/clear/lambda-save-reset-
+  restore symmetric). Loop lowers to `loop.header.<id>` with one
+  `phi` per binder; binder phi SSA pushed into `self.locals` so
+  `Term::Var` resolves to it via the existing lookup. Each phi's
+  back-edge incoming list is emitted as a unique `/*RECUR_EDGES…*/`
+  LLVM-comment placeholder, then `replacen(…, 1)`-patched once the
+  body and all its recur sites are lowered (the plan's
+  `patch_loop_phis` mechanism; the placeholder is a comment so an
+  unpatched one would be inert IR, not a syntax error). `Term::Recur`
+  records `(pred_block, [arg_ssa])`, emits the back-edge `br`, sets
+  `block_terminated = true` — a NEW parallel setter; the seven
+  existing tail-driven setters are untouched (verified: zero
+  deletions touch them). Reused `start_block`/`fresh_ssa`/`fresh_id`/
+  `self.current_block` instead of adding the plan-pseudo's sprawl of
+  single-use helper methods (plan explicitly: "REUSE … grep before
+  adding"). `loop_counter.ail` builds + prints `55`.
+
+- iter it.1.8: tail-app coexistence + IR snapshots + acceptance.
+  `bench_compute_intsum.ail` → `3500003500000`,
+  `list_map_poly.ail` → `2\n3\n…` (byte-identical to pre-it.1; no
+  existing codegen path modified). Zero IR/prose snapshot drift (no
+  blanket regen). All it.1 acceptance bullets verified — the spec's
+  "five Recur diagnostics" is four in it.1 (the fifth,
+  `NonStructuralRecursion`, is it.2; resolved per plan Step 8.3).
+
+- Phase 3 (E2E): added `loop_in_lambda_e2e.ail` + e2e
+  `loop_in_lambda_runs_and_prints_49` — a `loop` inside a `lam`
+  body invoked via a returned closure, proving the lambda-boundary
+  `loop_frames` save/restore is codegen-sound (the no-`main`
+  `loop_nested_in_lambda.ail` parse/print fixture cannot reach
+  codegen via the CLI; this runnable fixture closes that gap).
+
+## Concerns
+
+- `LoopBinder.init` is `Box<Term>` whereas the analogous
+  `MutVar.init` is bare `Term`. Per the plan's literal Step 1.1
+  code block (which specified `init: Box<Term>`), not implementer
+  drift. DD-2 says "mirrors MutVar exactly" — the divergence is in
+  the plan's own pseudo-code vs. its own DD-2 prose. Functional
+  impact: none (consistent `(*b.init).clone()` / `Box::new(...)` /
+  `&mut b.init` handling everywhere). A future iter that wants
+  strict parity could unbox; no it.1 test depends on the boxing.
+
+- `Term::Recur` synth result: chose `Subst::fresh(counter)` (a
+  fresh metavar) over the plan's named fallback `Type::unit()`.
+  The plan's self-review flagged this exact point as an "Open
+  risk" with `Type::unit()` as the fallback "because recur is
+  always in tail position so its value is never consumed". But
+  `recur` frequently appears as an `if` branch (`loop_smoke`:
+  `(if (== i n) i (recur …))`), where the branch types MUST
+  unify — `unify(Int, unit)` fails, so `Type::unit()` would have
+  broken `loop_smoke`. A fresh metavar unifies with any type
+  (codegen-idiomatic bottom; the same mechanism `Subst::fresh`
+  serves everywhere). This is the correct resolution of the plan's
+  own flagged risk, not a deviation from its intent.
+
+- Step 4.1 plan defect: it asks for a prose round-trip asserting
+  AST equality; AILang has no Form-B parser by design. Substituted
+  a feasible render-assertion pin (mut.1-class plan-pseudo-vs-real
+  substitution). The plan's *substance* (prose lockstep for the new
+  variants) is fully met. Boss may want to tighten the planner
+  template so it does not script prose round-trips.
+
+- Step 5.2 plan premise defect: "Add the four code strings to the
+  diagnostic-doc list … same list the mut codes were added to" —
+  the mut codes were never added to `diagnostic.rs`'s doc list.
+  Followed the actual mut.2 precedent (not extended); the
+  authoritative registry is `CheckError::code()`, which has all
+  four.
+
+- The plan's recon line numbers (e.g. `desugar.rs:349/559/…`,
+  `lib.rs:2590/2613/3593/3614`, `parse.rs:1212`) had drifted
+  vs. the live tree; drove every site off `cargo build`'s
+  E0004 enumeration as Step 1.2 instructs. Site *count* also
+  differed (6 desugar E0004 sites vs. plan's 9; resolved via the
+  build, which is authoritative). No behavioural impact —
+  same class as mut.1's documented recon misindexing.
+
+## Known debt
+
+- Prose-side `(loop …)` / `(recur …)` rendering is a
+  minimal-correctness shape (`loop { var n = init; …; body }` /
+  `recur(a, b)`), explicitly mirroring the deliberately-placeholder
+  mut-block prose shape. The prose surface for loops is not yet
+  designed; a follow-on prose iter refines it once the LLM-author
+  signal arrives. Not drift — recorded for visibility.
+
+- `loop_nested_in_lambda.ail` has no `main`, so it is a
+  parse/print/typecheck fixture only (CLI codegen needs a `main`).
+  Codegen-of-loop-in-lambda is instead proven by the runnable
+  Phase-3 `loop_in_lambda_e2e.ail`. No gap remains; recorded so a
+  future reader does not mistake the no-main fixture for dead
+  coverage.
+
+## Files touched
+
+AST/core: `crates/ailang-core/src/ast.rs`,
+`crates/ailang-core/src/desugar.rs`,
+`crates/ailang-core/src/workspace.rs`,
+`crates/ailang-core/specs/form_a.md`.
+Drift/coverage tests: `crates/ailang-core/tests/{design_schema_drift,
+schema_coverage,spec_drift,carve_out_inventory}.rs`.
+Check: `crates/ailang-check/src/{lib,lift,linearity,mono,
+pre_desugar_validation,reuse_shape,uniqueness,builtins}.rs`,
+`crates/ailang-check/tests/loop_recur_pin.rs` (new).
+Codegen: `crates/ailang-codegen/src/{lib,escape,lambda}.rs`.
+Surface/prose: `crates/ailang-surface/src/{parse,print}.rs`,
+`crates/ailang-prose/src/lib.rs`.
+CLI: `crates/ail/src/main.rs`,
+`crates/ail/tests/{e2e,codegen_import_map_fallback_pin}.rs`.
+Spec: `docs/DESIGN.md`.
+Fixtures (new): `examples/loop_smoke.ail`,
+`examples/loop_nested_in_lambda.ail`, `examples/loop_counter.ail`,
+`examples/loop_in_lambda_e2e.ail`,
+`examples/test_recur_{outside_loop,arity_mismatch,type_mismatch,
+not_in_tail_position}.ail.json`.
+
+## Stats
+
+bench/orchestrator-stats/2026-05-15-iter-it.1.json
diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md
index bbcbb87..49de4b5 100644
--- a/docs/journals/INDEX.md
+++ b/docs/journals/INDEX.md
@@ -75,3 +75,4 @@
 - 2026-05-15 — iter mut.3: codegen + e2e for `Term::Mut` + `Term::Assign` closing the mut-local milestone end-to-end; mut-var allocas hoisted to fn entry block via a per-`Emitter` side buffer `pending_entry_allocas: String` + a captured `entry_block_end_marker: Option<usize>` byte position spliced via `String::insert_str` at the end of `emit_fn`; `Term::Mut` arm in `lower_term` emits one alloca per var into the side buffer, lowers each init at the current position, emits a `store` to bind, push/pops a per-block save stack for proper shadowing of outer mut-vars; `Term::Assign` arm emits `store <ty> <value_ssa>, ptr <alloca>` and yields the canonical Unit SSA; `Term::Var` arm prepends mut-var lookup with a `load` emission. Two beyond-plan adjustments: (1) `synth_with_extras`'s parallel `Term::Var` arm needed the same mut-var lookup precedence as `lower_term`, (2) `lambda.rs` thunk emission needed save/restore of all three new `Emitter` fields across the lambda-body boundary plus an in-thunk splice at the lambda's own entry marker so mut-blocks inside a closure body hoist to the closure's entry not the outer fn's. Two e2e fixtures `examples/mut_counter.ail` (Int) + `examples/mut_sum_floats.ail` (Float); both run end-to-end and print `55`. DESIGN.md "What **is** supported" subsection gains a "Local mutable state" bullet. mut-local milestone end-to-end closed. Tests 592 → 594 → 2026-05-15-iter-mut.3.md
 - 2026-05-15 — iter mut.4-tidy: close mut-local audit drift. Architect's two `[high]` items addressed — new `CheckError::MutVarCapturedByLambda` rejects any lambda whose body's free vars hit the enclosing `mut_scope_stack` (via the existing `desugar::free_vars_in_term` helper, gated on non-empty stack), and `codegen/lambda.rs`'s blame-typechecker `Internal` path becomes `unreachable!` once typecheck is the gate. Two `[medium]` stale-history comments cleaned in DESIGN.md §"Term (expression)" and `ailang-codegen/src/lib.rs`. New negative fixture `examples/test_mut_var_captured_by_lambda.ail.json` + driver test extension; `carve_out_inventory.rs` EXPECTED 12→13. Spec §"Out of scope" amended with the lambda-capture rejection bullet. Bench: `compile_check.py` `check_ms` showed a uniform ~30-50% regression across the suite traced to a fixed-cost startup tax (mut-* added ~1400 lines of typecheck/codegen surface; the short-circuit on empty `mut_scope_stack` walk in Term::Var did not move the needle, falsifying the hot-path hypothesis); ratified as a feature tax with paired baseline update on `bench/baseline_compile.json`. `check.py` tail-noise envelope continues the audit-pd carve-out (no ratify needed). `cross_lang.py` clean. Tests 594 → 598. mut-local milestone audit closed → 2026-05-15-iter-mut.4-tidy.md
 - 2026-05-15 — bugfix mut-diag-double-code: fieldtest F2 — the four mut-local `CheckError` variants embedded `[<code>]` in their `#[error]` Display body while the non-JSON CLI formatter also prepends `[code]`, doubling it in human stderr; dropped the embedded prefix from the four strings, bringing them in line with all non-mut variants; RED-first via `debug` (`ct1_check_cli.rs::check_human_mode_renders_mut_diagnostic_code_exactly_once`), GREEN applied inline as a trivial mechanical edit; tests 598 → 599 → 2026-05-15-bugfix-mut-diag-double-code.md
+- 2026-05-15 — iter it.1: iteration-discipline milestone (1 of 3) — `Term::Loop` / `Term::Recur` / `LoopBinder` added as strictly-additive first-class AST nodes end-to-end: Form-A `parse_loop`/`parse_recur` + print + prose render/free-var/subst lockstep + canonical-JSON serde/round-trip + schema/spec-drift/schema-coverage/carve-out lockstep (13→17) + typecheck (binder typing + recur arity/type unification via `loop_stack: &mut Vec<Vec<Type>>` threaded exactly as mut.2's `mut_scope_stack`; recur-tail-position via a new private `verify_loop_body`, `verify_tail_positions` public signature unchanged) + codegen (loop-header block, one phi per binder, recur back-edge `br` with a NEW parallel `block_terminated` setter, lambda-boundary `loop_frames` save/restore mirroring mut.3). Four new `CheckError` variants `Recur{OutsideLoop,ArityMismatch,TypeMismatch,NotInTailPosition}` (bracket-`[code]`-free Display per the F2 convention). Strictly additive verified — zero deletions touch `tail-app`/`tail-do`, `verify_tail_positions`' tail-app role, or the seven existing codegen `block_terminated` sites (the 32 within-iter deletions are exclusively DD-3 stub-then-fill replacements). `Term::Recur` synth returns a fresh metavar (resolves the plan's flagged `Type::unit()` open risk: recur appears in `if` branches that must unify with the sibling type). `loop_counter.ail`→`55`, `loop_in_lambda_e2e.ail`→`49`, four negatives fire exact codes, `tail-app` fixtures byte-identical, zero IR/prose snapshot drift; `cargo test --workspace` green. Two mut.1-class plan-pseudo-vs-reality substitutions recorded (prose round-trip asserting AST-equality is impossible — no Form-B parser by design; the diagnostic.rs doc-list premise was false) → 2026-05-15-iter-it.1.md
diff --git a/examples/loop_counter.ail b/examples/loop_counter.ail
new file mode 100644
index 0000000..155dac0
--- /dev/null
+++ b/examples/loop_counter.ail
@@ -0,0 +1,12 @@
+(module loop_counter
+
+  (fn main
+    (doc "Iter it.1 — sum 1..10 via an accumulator loop. Expected stdout: 55.")
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (app print
+        (loop ((var acc (con Int) 0) (var i (con Int) 1))
+          (if (app > i 10)
+            acc
+            (recur (app + acc i) (app + i 1))))))))
diff --git a/examples/loop_in_lambda_e2e.ail b/examples/loop_in_lambda_e2e.ail
new file mode 100644
index 0000000..de103f4
--- /dev/null
+++ b/examples/loop_in_lambda_e2e.ail
@@ -0,0 +1,24 @@
+(module loop_in_lambda_e2e
+
+  (fn apply
+    (doc "apply a fn-of-Int to an Int")
+    (type (fn-type (params (fn-type (params (con Int)) (ret (con Int))) (con Int)) (ret (con Int))))
+    (params f x)
+    (body (app f x)))
+
+  (fn main
+    (doc "Iter it.1 — a loop inside a lambda body, invoked via a closure. The lambda computes x*x by summing x exactly x times through an accumulator loop; apply 7 prints 49. Codegen-soundness gate for the lambda-boundary loop_frames save/restore.")
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body
+      (app print
+        (app apply
+          (lam
+            (params (typed x (con Int)))
+            (ret (con Int))
+            (body
+              (loop ((var acc (con Int) 0) (var k (con Int) 0))
+                (if (app == k x)
+                  acc
+                  (recur (app + acc x) (app + k 1))))))
+          7)))))
diff --git a/examples/loop_nested_in_lambda.ail b/examples/loop_nested_in_lambda.ail
new file mode 100644
index 0000000..719977e
--- /dev/null
+++ b/examples/loop_nested_in_lambda.ail
@@ -0,0 +1,15 @@
+(module loop_nested_in_lambda
+
+  (fn make_adder
+    (doc "Iter it.1 — a loop inside a lambda body (lambda-boundary analogue).")
+    (type (fn-type (params (con Int)) (ret (fn-type (params (con Int)) (ret (con Int))))))
+    (params base)
+    (body
+      (lam
+        (params (typed x (con Int)))
+        (ret (con Int))
+        (body
+          (loop ((var acc (con Int) base) (var k (con Int) 0))
+            (if (app == k x)
+              acc
+              (recur (app + acc 1) (app + k 1)))))))))
diff --git a/examples/loop_smoke.ail b/examples/loop_smoke.ail
new file mode 100644
index 0000000..4e7b1f0
--- /dev/null
+++ b/examples/loop_smoke.ail
@@ -0,0 +1,11 @@
+(module loop_smoke
+
+  (fn count_to
+    (doc "Iter it.1 — single counted loop; counts i up to n and returns n.")
+    (type (fn-type (params (con Int)) (ret (con Int))))
+    (params n)
+    (body
+      (loop ((var i (con Int) 0))
+        (if (app == i n)
+          i
+          (recur (app + i 1)))))))
diff --git a/examples/test_recur_arity_mismatch.ail.json b/examples/test_recur_arity_mismatch.ail.json
new file mode 100644
index 0000000..603dbb8
--- /dev/null
+++ b/examples/test_recur_arity_mismatch.ail.json
@@ -0,0 +1,60 @@
+{
+    "schema": "ailang/v0",
+    "name": "test_recur_arity_mismatch",
+    "imports": [],
+    "defs": [
+        {
+            "kind": "fn",
+            "name": "main",
+            "type": {
+                "k": "fn",
+                "params": [],
+                "ret": {
+                    "k": "con",
+                    "name": "Int"
+                },
+                "effects": []
+            },
+            "params": [],
+            "doc": "Iter it.1: recur passing 2 args to a 1-binder loop fires recur-arity-mismatch.",
+            "body": {
+                "t": "loop",
+                "binders": [
+                    {
+                        "name": "i",
+                        "type": {
+                            "k": "con",
+                            "name": "Int"
+                        },
+                        "init": {
+                            "t": "lit",
+                            "lit": {
+                                "kind": "int",
+                                "value": 0
+                            }
+                        }
+                    }
+                ],
+                "body": {
+                    "t": "recur",
+                    "args": [
+                        {
+                            "t": "lit",
+                            "lit": {
+                                "kind": "int",
+                                "value": 1
+                            }
+                        },
+                        {
+                            "t": "lit",
+                            "lit": {
+                                "kind": "int",
+                                "value": 2
+                            }
+                        }
+                    ]
+                }
+            }
+        }
+    ]
+}
diff --git a/examples/test_recur_not_in_tail_position.ail.json b/examples/test_recur_not_in_tail_position.ail.json
new file mode 100644
index 0000000..f41600e
--- /dev/null
+++ b/examples/test_recur_not_in_tail_position.ail.json
@@ -0,0 +1,60 @@
+{
+    "schema": "ailang/v0",
+    "name": "test_recur_not_in_tail_position",
+    "imports": [],
+    "defs": [
+        {
+            "kind": "fn",
+            "name": "main",
+            "type": {
+                "k": "fn",
+                "params": [],
+                "ret": {
+                    "k": "con",
+                    "name": "Int"
+                },
+                "effects": []
+            },
+            "params": [],
+            "doc": "Iter it.1: recur in the lhs of a seq (non-tail) fires recur-not-in-tail-position.",
+            "body": {
+                "t": "loop",
+                "binders": [
+                    {
+                        "name": "i",
+                        "type": {
+                            "k": "con",
+                            "name": "Int"
+                        },
+                        "init": {
+                            "t": "lit",
+                            "lit": {
+                                "kind": "int",
+                                "value": 0
+                            }
+                        }
+                    }
+                ],
+                "body": {
+                    "t": "seq",
+                    "lhs": {
+                        "t": "recur",
+                        "args": [
+                            {
+                                "t": "var",
+                                "name": "i"
+                            }
+                        ]
+                    },
+                    "rhs": {
+                        "t": "lit",
+                        "lit": {
+                            "kind": "int",
+                            "value": 0
+                        }
+                    }
+                }
+            }
+        }
+    ]
+}
diff --git a/examples/test_recur_outside_loop.ail.json b/examples/test_recur_outside_loop.ail.json
new file mode 100644
index 0000000..63c27f2
--- /dev/null
+++ b/examples/test_recur_outside_loop.ail.json
@@ -0,0 +1,34 @@
+{
+    "schema": "ailang/v0",
+    "name": "test_recur_outside_loop",
+    "imports": [],
+    "defs": [
+        {
+            "kind": "fn",
+            "name": "main",
+            "type": {
+                "k": "fn",
+                "params": [],
+                "ret": {
+                    "k": "con",
+                    "name": "Int"
+                },
+                "effects": []
+            },
+            "params": [],
+            "doc": "Iter it.1: a recur with no enclosing loop fires recur-outside-loop.",
+            "body": {
+                "t": "recur",
+                "args": [
+                    {
+                        "t": "lit",
+                        "lit": {
+                            "kind": "int",
+                            "value": 1
+                        }
+                    }
+                ]
+            }
+        }
+    ]
+}
diff --git a/examples/test_recur_type_mismatch.ail.json b/examples/test_recur_type_mismatch.ail.json
new file mode 100644
index 0000000..7b1c471
--- /dev/null
+++ b/examples/test_recur_type_mismatch.ail.json
@@ -0,0 +1,53 @@
+{
+    "schema": "ailang/v0",
+    "name": "test_recur_type_mismatch",
+    "imports": [],
+    "defs": [
+        {
+            "kind": "fn",
+            "name": "main",
+            "type": {
+                "k": "fn",
+                "params": [],
+                "ret": {
+                    "k": "con",
+                    "name": "Int"
+                },
+                "effects": []
+            },
+            "params": [],
+            "doc": "Iter it.1: recur passing a Bool to an Int binder fires recur-type-mismatch.",
+            "body": {
+                "t": "loop",
+                "binders": [
+                    {
+                        "name": "i",
+                        "type": {
+                            "k": "con",
+                            "name": "Int"
+                        },
+                        "init": {
+                            "t": "lit",
+                            "lit": {
+                                "kind": "int",
+                                "value": 0
+                            }
+                        }
+                    }
+                ],
+                "body": {
+                    "t": "recur",
+                    "args": [
+                        {
+                            "t": "lit",
+                            "lit": {
+                                "kind": "bool",
+                                "value": true
+                            }
+                        }
+                    ]
+                }
+            }
+        }
+    ]
+}