iter mut.1: AST extension + Form A surface for local mutable state

First iteration of the mut-local milestone (foundation step on the
Stateful-islands roadmap path). Lands the schema + surface tier:
Term::Mut, Term::Assign, and the nested MutVar struct become
first-class AST nodes that round-trip cleanly through Form A.
Typecheck and codegen recognition are deferred to mut.2 and mut.3
per the spec's out-of-iteration boundary; reaching either dispatch
entry point with these variants produces CheckError::Internal /
CodegenError::Internal with a 'deferred to iter mut.{2,3}' message.

Concretely:

- crates/ailang-core/src/ast.rs: two new Term variants behind
  #[serde(tag = 't')]; pub struct MutVar { name, ty, init } adjacent
  to Arm. Two canonical-bytes pin tests for the explicit-empty-vars
  serialisation and the assign round-trip.

- ~25 substantive Term-walker arms across ailang-core/desugar,
  ailang-core/workspace, ailang-check (lib + lift + linearity + mono
  + pre_desugar_validation + reuse_shape + uniqueness),
  ailang-codegen (escape + lambda + lib), ailang-prose, and
  crates/ail/src/main.rs. Universal policy: substantive recurse-into-
  children at every site; only the two dispatch entry points
  (synth in ailang-check, lower_term in ailang-codegen) stub with
  Internal-error. One test-side walker arm in
  crates/ail/tests/codegen_import_map_fallback_pin.rs not
  enumerated by the plan was added as well (defensive recursion).

- ailang-surface: parse_mut + parse_assign helpers; Term::Mut
  body desugared from a flat statement sequence into a right-folded
  Term::Seq chain inside the JSON-AST. Print arms in print.rs match
  the parser convention. EBNF prologue + crates/ailang-core/specs/
  form_a.md productions updated. Four new parser pin tests cover
  the empty-mut, single-var, body-required, and vars-only-no-body
  cases.

- Drift + coverage tests extended: design_schema_drift.rs adds two
  exemplars + match arms; schema_coverage.rs adds two VariantTag
  entries + EXPECTED_VARIANTS + visit_term arms; spec_drift.rs adds
  two exemplars + match arms. DESIGN.md §'Term (expression)' gets
  jsonc-blocked schemas for the two new variants.

- examples/mut.ail: six-fn round-trip fixture exercising empty mut,
  single-var, two-var, nested-shadow, and the four supported scalar
  return types (Int, Float, Bool, Unit). The round_trip auto-glob
  and schema_coverage corpus walker both pick it up.

Plan deviation: the plan named lib.rs:2572 as the typecheck
dispatch stub site, but that line is actually verify_tail_positions
(substantive walker). The real dispatch is synth (3403-area, stub
at 3489); the orchestrator routed correctly.

Tests: 564 → 579 green; cargo build green; round-trip green for
the new fixture; all drift + coverage tests green.

Journal: docs/journals/2026-05-15-iter-mut.1.md.

Refs: docs/specs/2026-05-15-mut-local.md, docs/plans/2026-05-15-iter-mut.1.md.

crates/ail/src/main.rs

@@ -1513,6 +1513,37 @@ fn walk_term(
             walk_term(source, out, builtins, scope);
             walk_term(body, out, builtins, scope);
         }
+        // Iter mut.1: each `var` introduces a new lexical binding;
+        // its `init` is in the outer scope plus already-declared
+        // vars; the body sees all of them. Mirrors `Term::Lam`'s
+        // newly-bound roll-back convention.
+        Term::Mut { vars, body } => {
+            let mut newly = Vec::new();
+            for v in vars {
+                walk_term(&v.init, out, builtins, scope);
+                if scope.insert(v.name.clone()) {
+                    newly.push(v.name.clone());
+                }
+            }
+            walk_term(body, out, builtins, scope);
+            for n in newly {
+                scope.remove(&n);
+            }
+        }
+        // Iter mut.1: the `value` is walked; the assigned `name` is
+        // a use of an in-scope mut-var. If the user wrote an
+        // out-of-scope assign, it surfaces as an unknown identifier
+        // in the dep walk, which is acceptable for the CLI's
+        // dependency view (typecheck would already have rejected).
+        Term::Assign { name, value } => {
+            if !name.contains('.')
+                && !scope.contains(name)
+                && !builtins.contains(name.as_str())
+            {
+                out.insert(name.clone());
+            }
+            walk_term(value, out, builtins, scope);
+        }
     }
 }
 
@@ -2716,6 +2747,44 @@ fn rewrite_def(
                     changed,
                 );
             }
+            // Iter mut.1: rewrite types embedded in each `MutVar.ty`
+            // (via `rewrite_type` — mut-vars carry full Type
+            // annotations) and recurse into each var's `init` and
+            // the block's body. `Term::Assign` has no embedded type.
+            Term::Mut { vars, body } => {
+                for v in vars {
+                    rewrite_type(
+                        &mut v.ty,
+                        owning_module,
+                        local_types,
+                        import_names,
+                        changed,
+                    );
+                    rewrite_term(
+                        &mut v.init,
+                        owning_module,
+                        local_types,
+                        import_names,
+                        changed,
+                    );
+                }
+                rewrite_term(
+                    body,
+                    owning_module,
+                    local_types,
+                    import_names,
+                    changed,
+                );
+            }
+            Term::Assign { value, .. } => {
+                rewrite_term(
+                    value,
+                    owning_module,
+                    local_types,
+                    import_names,
+                    changed,
+                );
+            }
         }
     }
 

crates/ail/tests/codegen_import_map_fallback_pin.rs

@@ -91,6 +91,16 @@ fn synthesised_print_uses_user_module_show_via_fallback() {
             Term::ReuseAs { source, body } => {
                 contains_xmod_show_var(source) || contains_xmod_show_var(body)
             }
+            // Iter mut.1: a `Term::Mut` cannot itself host a
+            // `show_user_adt.show__<T>` reference (its body is a
+            // mut-block, not a synthesised polymorphic call), but
+            // recurse defensively so any nested reference inside a
+            // var init / body / assign-value still surfaces.
+            Term::Mut { vars, body } => {
+                vars.iter().any(|v| contains_xmod_show_var(&v.init))
+                    || contains_xmod_show_var(body)
+            }
+            Term::Assign { value, .. } => contains_xmod_show_var(value),
             Term::Lit { .. } => false,
         }
     }

crates/ailang-check/src/lib.rs

@@ -243,6 +243,24 @@ pub(crate) fn substitute_rigids_in_term(t: &Term, mapping: &BTreeMap<String, Typ
             source: Box::new(substitute_rigids_in_term(source, mapping)),
             body: Box::new(substitute_rigids_in_term(body, mapping)),
         },
+        // Iter mut.1: rebuild each `MutVar.ty` via the type-level
+        // rigids substitution, each `init` via the term-level
+        // walker, and the body via the term-level walker.
+        Term::Mut { vars, body } => Term::Mut {
+            vars: vars
+                .iter()
+                .map(|v| ailang_core::ast::MutVar {
+                    name: v.name.clone(),
+                    ty: substitute_rigids(&v.ty, mapping),
+                    init: substitute_rigids_in_term(&v.init, mapping),
+                })
+                .collect(),
+            body: Box::new(substitute_rigids_in_term(body, mapping)),
+        },
+        Term::Assign { name, value } => Term::Assign {
+            name: name.clone(),
+            value: Box::new(substitute_rigids_in_term(value, mapping)),
+        },
     }
 }
 
@@ -2577,6 +2595,22 @@ pub fn verify_tail_positions(t: &Term, is_tail: bool) -> Result<()> {
             verify_tail_positions(source, false)?;
             verify_tail_positions(body, is_tail)
         }
+        // Iter mut.1: var inits are evaluated for side-effect before
+        // the body and are NOT in tail position. The body is the
+        // value of the whole block and inherits the enclosing tail
+        // position (a `(tail-app ...)` as the final expression of a
+        // `(mut ...)` block is itself in tail position because the
+        // block's value is the call's value).
+        Term::Mut { vars, body } => {
+            for v in vars {
+                verify_tail_positions(&v.init, false)?;
+            }
+            verify_tail_positions(body, is_tail)
+        }
+        // Iter mut.1: `Term::Assign` has static type Unit and cannot
+        // be in tail position. Its `value` is also not in tail
+        // position.
+        Term::Assign { value, .. } => verify_tail_positions(value, false),
     }
 }
 
@@ -3428,6 +3462,8 @@ pub(crate) fn synth(
                         Term::Seq { .. } => "seq",
                         Term::Clone { .. } => "clone",
                         Term::ReuseAs { .. } => "reuse-as",
+                        Term::Mut { .. } => "mut",
+                        Term::Assign { .. } => "assign",
                         Term::Ctor { .. } | Term::Lam { .. } => unreachable!(),
                     };
                     return Err(CheckError::ReuseAsNonAllocatingBody {
@@ -3440,6 +3476,25 @@ pub(crate) fn synth(
             // expression.
             synth(body, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
         }
+        // Iter mut.1: typecheck recognition of `Term::Mut` and
+        // `Term::Assign` is deferred to iter mut.2 (see
+        // `docs/specs/2026-05-15-mut-local.md` §"Iteration mut.1"
+        // out-of-iteration boundary). The dispatch entry here stubs
+        // with `CheckError::Internal` so that a well-formed mut block
+        // reaching this point in mut.1 fails fast with a
+        // human-readable message — the Form-A surface parses these
+        // shapes and the AST round-trips them, but no fn body is
+        // expected to *use* them yet.
+        Term::Mut { .. } => {
+            Err(CheckError::Internal(
+                "Term::Mut not yet supported in typecheck (deferred to iter mut.2)".into(),
+            ))
+        }
+        Term::Assign { .. } => {
+            Err(CheckError::Internal(
+                "Term::Assign not yet supported in typecheck (deferred to iter mut.2)".into(),
+            ))
+        }
     }
 }
 

crates/ailang-check/src/lift.rs

@@ -375,6 +375,28 @@ impl<'a> Lifter<'a> {
                 source: Box::new(self.lift_in_term(source, locals, in_def)?),
                 body: Box::new(self.lift_in_term(body, locals, in_def)?),
             }),
+            // Iter mut.1: lift letrecs out of each var's init and the
+            // body. Mut-vars cannot themselves participate in a
+            // letrec capture set (letrec bodies are fn-typed and
+            // mut-vars are scalar values), so the var bindings do
+            // not extend `locals` for the lift walk.
+            Term::Mut { vars, body } => Ok(Term::Mut {
+                vars: vars
+                    .iter()
+                    .map(|v| {
+                        Ok(ailang_core::ast::MutVar {
+                            name: v.name.clone(),
+                            ty: v.ty.clone(),
+                            init: self.lift_in_term(&v.init, locals, in_def)?,
+                        })
+                    })
+                    .collect::<Result<Vec<_>>>()?,
+                body: Box::new(self.lift_in_term(body, locals, in_def)?),
+            }),
+            Term::Assign { name, value } => Ok(Term::Assign {
+                name: name.clone(),
+                value: Box::new(self.lift_in_term(value, locals, in_def)?),
+            }),
             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
@@ -729,6 +751,12 @@ fn contains_any_letrec(m: &Module) -> bool {
             Term::Clone { value } => term_has_letrec(value),
             // Iter 18d.1: structural recursion through both children.
             Term::ReuseAs { source, body } => term_has_letrec(source) || term_has_letrec(body),
+            // Iter mut.1: any var init or the body can contain a
+            // letrec; the assign's value can too.
+            Term::Mut { vars, body } => {
+                vars.iter().any(|v| term_has_letrec(&v.init)) || term_has_letrec(body)
+            }
+            Term::Assign { value, .. } => term_has_letrec(value),
         }
     }
     for def in &m.defs {

crates/ailang-check/src/linearity.rs

@@ -592,6 +592,23 @@ impl<'a> Checker<'a> {
                 // standard position rules.
                 self.walk(body, pos);
             }
+            // Iter mut.1: mut-vars are alloca-resident scalars (Int /
+            // Float / Bool / Unit per spec §"Iteration mut.1") — they
+            // are not RC-managed and do not participate in the
+            // linearity analysis. Walk children defensively so any
+            // RC-managed value referenced inside an init or the body
+            // is still tracked.
+            Term::Mut { vars, body } => {
+                for v in vars {
+                    self.walk(&v.init, Position::Consume);
+                }
+                self.walk(body, pos);
+            }
+            Term::Assign { value, .. } => {
+                // The assigned `name` is a mut-var (alloca slot, not
+                // a tracked binder). Walk the `value` normally.
+                self.walk(value, Position::Consume);
+            }
         }
     }
 
@@ -776,6 +793,8 @@ fn make_reuse_as_source_not_bare_var(def: &str, source: &Term, body: &Term) -> D
         Term::Seq { .. } => "seq",
         Term::Clone { .. } => "clone",
         Term::ReuseAs { .. } => "reuse-as",
+        Term::Mut { .. } => "mut",
+        Term::Assign { .. } => "assign",
     };
     let replacement = term_to_form_a(body);
     Diagnostic::error(
@@ -901,6 +920,20 @@ fn any_sub_binder_consumed_for(
             any_sub_binder_consumed_for(source, pname, uniq, def_name, ctors)
                 || any_sub_binder_consumed_for(body, pname, uniq, def_name, ctors)
         }
+        // Iter mut.1: mut-vars are scalar (Int/Float/Bool/Unit) and
+        // do not participate in the consume-tracking heuristic; the
+        // surrounding analysis only cares about heap-typed param
+        // consumption. Recurse into children defensively so any
+        // genuine consume-of-`pname` inside a var init / body /
+        // assign value still surfaces.
+        Term::Mut { vars, body } => {
+            vars.iter().any(|v| {
+                any_sub_binder_consumed_for(&v.init, pname, uniq, def_name, ctors)
+            }) || any_sub_binder_consumed_for(body, pname, uniq, def_name, ctors)
+        }
+        Term::Assign { value, .. } => {
+            any_sub_binder_consumed_for(value, pname, uniq, def_name, ctors)
+        }
     }
 }
 

crates/ailang-check/src/mono.rs

@@ -1221,6 +1221,19 @@ fn rewrite_mono_calls(
             rewrite_mono_calls(source, 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);
         }
+        // Iter mut.1: visitor-shape recurse with mutable access.
+        // Mut-vars do not declare class-method or poly-fn names; the
+        // var inits, the body, and assign values can though, so walk
+        // them in place.
+        Term::Mut { vars, body } => {
+            for v in vars.iter_mut() {
+                rewrite_mono_calls(&mut v.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::Assign { value, .. } => {
+            rewrite_mono_calls(value, method_to_candidate_classes, poly_free_fns, poly_free_fn_ccounts, caller_module, ordered_targets, cursor, locals);
+        }
         Term::Lit { .. } => {}
     }
 }
@@ -1577,6 +1590,19 @@ fn interleave_slots(
             interleave_slots(source, 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);
         }
+        // Iter mut.1: visitor-shape recurse, symmetric to
+        // `rewrite_mono_calls` above. Mut-vars themselves do not
+        // contribute slots; their init and body terms (and assign
+        // values) can.
+        Term::Mut { vars, body } => {
+            for v in vars {
+                interleave_slots(&v.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::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::Lit { .. } => {}
     }
 }

crates/ailang-check/src/pre_desugar_validation.rs

@@ -120,6 +120,19 @@ fn walk_term(t: &Term) -> Result<(), CheckError> {
             walk_term(source)?;
             walk_term(body)
         }
+        // Iter mut.1: pre-desugar validation has nothing specific to
+        // assert about mut blocks (the only invariant this pass
+        // enforces today is "no Float in literal patterns" — mut
+        // var inits are Terms, but they can hold any literal, and
+        // patterns inside a body are visited via the normal
+        // `Term::Match` arm). Recurse into children.
+        Term::Mut { vars, body } => {
+            for v in vars {
+                walk_term(&v.init)?;
+            }
+            walk_term(body)
+        }
+        Term::Assign { value, .. } => walk_term(value),
     }
 }
 

crates/ailang-check/src/reuse_shape.rs

@@ -253,6 +253,18 @@ impl<'a> Checker<'a> {
                 self.walk(body);
                 self.check_reuse_as(source, body);
             }
+            // Iter mut.1: mut-vars are scalar (Int/Float/Bool/Unit)
+            // and cannot host an allocating ctor body, so the
+            // reuse-as path-ctor analysis has nothing to refine here.
+            // Recurse defensively into children so any reuse-as
+            // nested inside a var init or the body is still checked.
+            Term::Mut { vars, body } => {
+                for v in vars {
+                    self.walk(&v.init);
+                }
+                self.walk(body);
+            }
+            Term::Assign { value, .. } => self.walk(value),
         }
     }
 

crates/ailang-check/src/uniqueness.rs

@@ -336,6 +336,22 @@ impl<'a> Walker<'a> {
                 self.walk(source, Position::Consume);
                 self.walk(body, pos);
             }
+            // Iter mut.1: mut-vars are alloca-resident scalars and
+            // are NOT RC-tracked binders. They do not contribute to
+            // uniqueness counts (the alloca slot is the per-fn
+            // storage, not a heap allocation). Walk children
+            // defensively so any RC-managed value passed through a
+            // var init / body / assign-value still updates the
+            // appropriate uniqueness counts.
+            Term::Mut { vars, body } => {
+                for v in vars {
+                    self.walk(&v.init, Position::Consume);
+                }
+                self.walk(body, pos);
+            }
+            Term::Assign { value, .. } => {
+                self.walk(value, Position::Consume);
+            }
         }
     }
 

crates/ailang-codegen/src/escape.rs

@@ -190,6 +190,17 @@ fn walk(t: &Term, out: &mut NonEscapeSet) {
             walk(source, out);
             walk(body, out);
         }
+        // Iter mut.1: mut-vars are alloca-resident scalars (Int /
+        // Float / Bool / Unit) and never participate in heap escape.
+        // Their `init` and `body` and assign `value` terms may still
+        // contain Let-allocation candidates, so walk through.
+        Term::Mut { vars, body } => {
+            for v in vars {
+                walk(&v.init, out);
+            }
+            walk(body, out);
+        }
+        Term::Assign { value, .. } => walk(value, out),
         Term::Lit { .. } | Term::Var { .. } => {}
     }
 }
@@ -367,6 +378,23 @@ fn escapes(t: &Term, tainted: &BTreeSet<String>, in_tail: bool) -> bool {
             }
             escapes(body, tainted, in_tail)
         }
+        // Iter mut.1: mut-vars are alloca-resident scalars and do
+        // not themselves contribute to heap escape. Var inits are
+        // evaluated for side-effect (their values are stored into
+        // allocas, not used as the block's value), so they are
+        // walked in non-tail mode. The body IS the block's value,
+        // so it inherits `in_tail`. An assign's value is stored
+        // into an alloca, not used as a tail value — walk
+        // non-tail.
+        Term::Mut { vars, body } => {
+            for v in vars {
+                if escapes(&v.init, tainted, false) {
+                    return true;
+                }
+            }
+            escapes(body, tainted, in_tail)
+        }
+        Term::Assign { value, .. } => escapes(value, tainted, false),
     }
 }
 
@@ -471,6 +499,31 @@ fn collect_free_vars(t: &Term, bound: &mut BTreeSet<String>, out: &mut BTreeSet<
             collect_free_vars(source, bound, out);
             collect_free_vars(body, bound, out);
         }
+        // Iter mut.1: a mut-var name binds inside the block. Var
+        // inits before the binding see the outer scope; later inits
+        // and the body see the var as bound. Mirrors `Term::Let`'s
+        // add-then-walk-then-remove pattern, extended over N vars.
+        Term::Mut { vars, body } => {
+            let mut newly: Vec<String> = Vec::new();
+            for v in vars {
+                collect_free_vars(&v.init, bound, out);
+                if bound.insert(v.name.clone()) {
+                    newly.push(v.name.clone());
+                }
+            }
+            collect_free_vars(body, bound, out);
+            for n in newly {
+                bound.remove(&n);
+            }
+        }
+        // Iter mut.1: the assigned `name` is a free var unless
+        // bound by an enclosing `Term::Mut`.
+        Term::Assign { name, value } => {
+            if !bound.contains(name) {
+                out.insert(name.clone());
+            }
+            collect_free_vars(value, bound, out);
+        }
     }
 }
 

crates/ailang-codegen/src/lambda.rs

@@ -430,6 +430,43 @@ impl<'a> Emitter<'a> {
                 Self::collect_captures(source, bound, captures, captures_set, builtins, top_level);
                 Self::collect_captures(body, bound, captures, captures_set, builtins, top_level);
             }
+            // Iter mut.1: a mut-var name binds inside the block. Var
+            // inits before the binding see the outer scope; later
+            // inits and the body see the var as bound. Mut-vars
+            // cannot be captured by an inner lambda in mut.1 (the
+            // typecheck pass at mut.2 will enforce this); for the
+            // capture-collection scan the var bindings are tracked
+            // identically to let-bound names.
+            Term::Mut { vars, body } => {
+                let mut newly_bound: Vec<String> = Vec::new();
+                for v in vars {
+                    Self::collect_captures(&v.init, bound, captures, captures_set, builtins, top_level);
+                    if bound.insert(v.name.clone()) {
+                        newly_bound.push(v.name.clone());
+                    }
+                }
+                Self::collect_captures(body, bound, captures, captures_set, builtins, top_level);
+                for n in newly_bound {
+                    bound.remove(&n);
+                }
+            }
+            Term::Assign { name, value, .. } => {
+                // The assigned `name` is a use of a mut-var binding.
+                // If it is bound in scope (it should be, by spec), it
+                // is not a capture. Otherwise — well-formed inputs do
+                // not produce this case (the typecheck pass at mut.2
+                // rejects it via `MutAssignOutOfScope`); we
+                // conservatively treat it as a possible capture so an
+                // ill-formed input still flows through codegen.
+                if !bound.contains(name)
+                    && !builtins.contains(name.as_str())
+                    && !top_level.contains(name)
+                    && captures_set.insert(name.clone())
+                {
+                    captures.push(name.clone());
+                }
+                Self::collect_captures(value, bound, captures, captures_set, builtins, top_level);
+            }
         }
     }
 

crates/ailang-codegen/src/lib.rs

@@ -1669,6 +1669,26 @@ impl<'a> Emitter<'a> {
                 };
                 self.lower_reuse_as_rc(source, body_type_name, body_ctor, body_args)
             }
+            // Iter mut.1: codegen recognition of `Term::Mut` and
+            // `Term::Assign` is deferred to iter mut.3 (see
+            // `docs/specs/2026-05-15-mut-local.md` §"Iteration mut.1"
+            // out-of-iteration boundary). The dispatch entry here
+            // stubs with `CodegenError::Internal` so a well-formed
+            // mut block reaching codegen in mut.1 fails fast with a
+            // human-readable message. The typecheck pass also stubs
+            // at `synth` (iter mut.1, same spec subsection), so the
+            // codegen stub is a defense-in-depth — under normal
+            // flow, typecheck has already rejected.
+            Term::Mut { .. } => {
+                Err(CodegenError::Internal(
+                    "Term::Mut not yet supported in codegen (deferred to iter mut.3)".into(),
+                ))
+            }
+            Term::Assign { .. } => {
+                Err(CodegenError::Internal(
+                    "Term::Assign not yet supported in codegen (deferred to iter mut.3)".into(),
+                ))
+            }
         }
     }
 
@@ -2911,6 +2931,14 @@ impl<'a> Emitter<'a> {
                 // type. The source is dropped at codegen.
                 self.synth_with_extras(body, extras)
             }
+            // Iter mut.1: `Term::Mut`'s static type is the body's
+            // static type (spec §"JSON-AST schema"). `Term::Assign`'s
+            // is Unit (spec §"Form A surface"). These won't be hit
+            // along the shipping codegen path because the dispatcher
+            // at `lower_term` stubs both — but `synth_with_extras`
+            // is exhaustive on Term so the arms must exist.
+            Term::Mut { body, .. } => self.synth_with_extras(body, extras),
+            Term::Assign { .. } => Ok(Type::unit()),
         }
     }
 }

crates/ailang-core/specs/form_a.md

@@ -281,6 +281,9 @@ Parenthesised forms:
 (seq EFFECTFUL-TERM RESULT-TERM)        ; sequence; lhs evaluated for effect
 (clone TERM)                            ; explicit RC clone (Iter 18c.1)
 (reuse-as SOURCE-TERM BODY-TERM)        ; explicit reuse hint (Iter 18d.1)
+(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 ...)
 ```
 
 Notes:
@@ -298,6 +301,27 @@ Notes:
 - `reuse-as` requires `SOURCE-TERM` to be a bare variable reference
   (a `NAME` in the term grammar). Anything else fails the linearity
   check with `reuse-as-source-not-bare-var`.
+- `mut` opens a lexically-scoped block of mutable bindings. The
+  body is a flat sequence of zero or more Unit-typed statements
+  followed by exactly one final expression of any supported type;
+  the parser right-folds this trailing sequence into `Term::Seq`
+  inside `Term::Mut.body`, so the canonical JSON-AST always sees a
+  single `body: Term`. The `vars` array stays present in canonical
+  JSON even when empty (a `(mut EXPR)` form with no vars is legal
+  and round-trips uniformly). A `(mut)` form with neither vars nor
+  body is rejected at parse. Mut-var element types are restricted
+  to the stack-resident primitives Int / Float / Bool / Unit in
+  this milestone; the typecheck pass (iter mut.2) rejects other
+  types with `mut-var-unsupported-type`.
+- `(var NAME TYPE INIT)` is only legal as a leading entry inside a
+  `(mut ...)` block. Outside the parser rejects `var` as an
+  unknown term head.
+- `(assign NAME VALUE-TERM)` is only legal as a sub-term inside a
+  `(mut ...)` block whose `vars` includes a var with the matching
+  `NAME`. Outside the parser accepts the shape but the typecheck
+  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`.
 
 ## Patterns
 

crates/ailang-core/src/ast.rs

@@ -510,6 +510,33 @@ pub enum Term {
         source: Box<Term>,
         body: Box<Term>,
     },
+    /// Iter mut.1: local mutable-state block. `vars` declares zero or
+    /// more lexically-scoped mutable bindings (initialised in order);
+    /// `body` is a single Term evaluated in scope of all vars. The
+    /// block's static type is `body`'s static type. `vars` stays
+    /// present in canonical JSON even when empty (no
+    /// `skip_serializing_if` — the field is part of the shape).
+    ///
+    /// Typecheck and codegen recognition land in iters mut.2 / mut.3;
+    /// in iter mut.1 the dispatch entry points (`synth` in
+    /// `ailang-check`, `lower_term` in `ailang-codegen`) stub these
+    /// variants with `CheckError::Internal` / `CodegenError::Internal`
+    /// respectively per spec `docs/specs/2026-05-15-mut-local.md`
+    /// §"Iteration mut.1".
+    Mut {
+        vars: Vec<MutVar>,
+        body: Box<Term>,
+    },
+    /// Iter mut.1: in-block update of a mut-var. Only legal as a
+    /// sub-term of a `Term::Mut` whose `vars` includes a var with the
+    /// same `name`. Static type is Unit. The lexical-scope invariant
+    /// is enforced at typecheck (iter mut.2,
+    /// `CheckError::MutAssignOutOfScope`); codegen relies on it (iter
+    /// mut.3).
+    Assign {
+        name: String,
+        value: Box<Term>,
+    },
 }
 
 /// One arm of a [`Term::Match`].
@@ -524,6 +551,35 @@ pub struct Arm {
     pub body: Term,
 }
 
+/// Iter mut.1: a mutable binding inside [`Term::Mut`]. Lives as a
+/// nested field of `Term::Mut`, not as a standalone `Term` variant —
+/// mut-vars are not first-class values (they cannot escape the
+/// enclosing `Term::Mut` scope; see
+/// `docs/specs/2026-05-15-mut-local.md` §"Why three AST nodes, not
+/// one fused construct").
+///
+/// The JSON field for `ty` is `"type"`, mirroring the spec's schema
+/// (`{ "name": "<id>", "type": Type, "init": Term }`). Derives match
+/// [`Arm`]'s for cross-tree consistency.
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct MutVar {
+    /// The mut-var's lexical name. Within the enclosing `Term::Mut`,
+    /// a `Term::Var { name }` resolves to this binding (innermost-wins
+    /// shadowing per spec §"Term::Var resolution"); a
+    /// `Term::Assign { name, .. }` updates it.
+    pub name: String,
+    /// The mut-var's declared type. Restricted to
+    /// `{ Int, Float, Bool, Unit }` in this milestone — the typecheck
+    /// pass (iter mut.2) rejects other choices with
+    /// `CheckError::UnsupportedMutVarType`.
+    #[serde(rename = "type")]
+    pub ty: Type,
+    /// Initial value. Evaluated in the outer scope plus the
+    /// already-declared vars of the same `Term::Mut` (vars are
+    /// initialised in declaration order).
+    pub init: Term,
+}
+
 /// A match pattern.
 ///
 /// The JSON discriminator is the `p` field. Patterns are linear: each
@@ -834,3 +890,60 @@ impl Eq for Type {}
 fn is_false(b: &bool) -> bool {
     !*b
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    /// Iter mut.1: pin the canonical-bytes shape of an empty-`vars`
+    /// `Term::Mut`. Spec `docs/specs/2026-05-15-mut-local.md`
+    /// §"Canonical-form invariants" requires the `vars` array to stay
+    /// present in canonical JSON rather than being omitted; a future
+    /// addition of `skip_serializing_if = "Vec::is_empty"` to the
+    /// field would silently break this property and is the failure
+    /// mode this pin protects against.
+    #[test]
+    fn term_mut_empty_vars_serialises_with_explicit_vars_field() {
+        let t = Term::Mut {
+            vars: Vec::new(),
+            body: Box::new(Term::Lit {
+                lit: Literal::Int { value: 0 },
+            }),
+        };
+        let bytes = serde_json::to_string(&t).expect("serialise");
+        assert_eq!(
+            bytes,
+            r#"{"t":"mut","vars":[],"body":{"t":"lit","lit":{"kind":"int","value":0}}}"#,
+        );
+    }
+
+    /// Iter mut.1: round-trip a `Term::Assign` through JSON.
+    /// Pins the canonical-form shape `{ "t": "assign", "name": ..., "value": ... }`.
+    #[test]
+    fn term_assign_round_trips_through_json() {
+        let t = Term::Assign {
+            name: "x".into(),
+            value: Box::new(Term::Lit {
+                lit: Literal::Int { value: 42 },
+            }),
+        };
+        let bytes = serde_json::to_string(&t).expect("serialise");
+        assert_eq!(
+            bytes,
+            r#"{"t":"assign","name":"x","value":{"t":"lit","lit":{"kind":"int","value":42}}}"#,
+        );
+        let back: Term = serde_json::from_str(&bytes).expect("deserialise");
+        match back {
+            Term::Assign { name, value } => {
+                assert_eq!(name, "x");
+                match *value {
+                    Term::Lit {
+                        lit: Literal::Int { value: 42 },
+                    } => {}
+                    other => panic!("inner literal mismatch: {other:?}"),
+                }
+            }
+            other => panic!("variant mismatch: {other:?}"),
+        }
+    }
+}

crates/ailang-core/src/desugar.rs

@@ -346,6 +346,23 @@ fn collect_used_in_term(t: &Term, used: &mut BTreeSet<String>) {
             collect_used_in_term(source, used);
             collect_used_in_term(body, used);
         }
+        Term::Mut { vars, body } => {
+            // Iter mut.1: mut-var declarations introduce source-level
+            // names — track them so a generated fresh-name cannot
+            // accidentally collide with one. Then recurse into each
+            // var's `init` and the block's body.
+            for v in vars {
+                used.insert(v.name.clone());
+                collect_used_in_term(&v.init, used);
+            }
+            collect_used_in_term(body, used);
+        }
+        Term::Assign { name, value } => {
+            // Iter mut.1: the assigned `name` is a *use* of the
+            // mut-var; record it and recurse into `value`.
+            used.insert(name.clone());
+            collect_used_in_term(value, used);
+        }
     }
 }
 
@@ -539,6 +556,40 @@ impl Desugarer {
                 source: Box::new(self.desugar_term(source, scope)),
                 body: Box::new(self.desugar_term(body, scope)),
             },
+            Term::Mut { vars, body } => {
+                // Iter mut.1: structural recursion. Each `var`'s `init`
+                // is evaluated in scope of the outer environment plus
+                // the *already-declared* vars of the same `Term::Mut`
+                // (spec §"Iteration mut.2" — first-class scoping
+                // formally lands at typecheck). For desugar's purposes
+                // we extend the scope per-var with a `LetBound`
+                // sentinel so a generated fresh name does not collide
+                // with mut-var names; the LetRec lifter does not
+                // consult mut-vars (mut-vars cannot appear in let-rec
+                // capture sets — letrec lifting happens before
+                // typecheck of the mut body).
+                let mut inner = scope.clone();
+                let new_vars: Vec<MutVar> = vars
+                    .iter()
+                    .map(|v| {
+                        let init = self.desugar_term(&v.init, &inner);
+                        inner.insert(v.name.clone(), ScopeEntry::LetBound);
+                        MutVar {
+                            name: v.name.clone(),
+                            ty: v.ty.clone(),
+                            init,
+                        }
+                    })
+                    .collect();
+                Term::Mut {
+                    vars: new_vars,
+                    body: Box::new(self.desugar_term(body, &inner)),
+                }
+            }
+            Term::Assign { name, value } => Term::Assign {
+                name: name.clone(),
+                value: Box::new(self.desugar_term(value, scope)),
+            },
             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 —
@@ -1160,6 +1211,29 @@ pub fn free_vars_in_term(t: &Term, bound: &BTreeSet<String>, out: &mut BTreeSet<
             free_vars_in_term(source, bound, out);
             free_vars_in_term(body, bound, out);
         }
+        Term::Mut { vars, body } => {
+            // Iter mut.1: a mut-var name binds inside the block. Each
+            // `var`'s `init` is evaluated in scope of the OUTER
+            // environment plus the already-declared vars (init order
+            // matches declaration order); the body is in scope of all
+            // vars. Mirrors the `Term::Let` pattern but generalised
+            // across N vars.
+            let mut b = bound.clone();
+            for v in vars {
+                free_vars_in_term(&v.init, &b, out);
+                b.insert(v.name.clone());
+            }
+            free_vars_in_term(body, &b, out);
+        }
+        Term::Assign { name, value } => {
+            // Iter mut.1: the assigned `name` is a free var unless
+            // bound by an enclosing `Term::Mut`. The value is walked
+            // as usual.
+            if !bound.contains(name) {
+                out.insert(name.clone());
+            }
+            free_vars_in_term(value, bound, out);
+        }
     }
 }
 
@@ -1304,6 +1378,55 @@ pub fn subst_var(t: &Term, from: &str, to: &str) -> Term {
             source: Box::new(subst_var(source, from, to)),
             body: Box::new(subst_var(body, from, to)),
         },
+        Term::Mut { vars, body } => {
+            // Iter mut.1: mut-vars lexically shadow outer names. Walk
+            // each var's `init` substituting only if no earlier var in
+            // the same block already shadows `from`; once a var named
+            // `from` is declared, subsequent inits AND the body see
+            // that var, so substitution must stop.
+            let mut shadowed = false;
+            let new_vars: Vec<MutVar> = vars
+                .iter()
+                .map(|v| {
+                    let init = if shadowed {
+                        v.init.clone()
+                    } else {
+                        subst_var(&v.init, from, to)
+                    };
+                    if v.name == from {
+                        shadowed = true;
+                    }
+                    MutVar {
+                        name: v.name.clone(),
+                        ty: v.ty.clone(),
+                        init,
+                    }
+                })
+                .collect();
+            let body_rw = if shadowed {
+                (**body).clone()
+            } else {
+                subst_var(body, from, to)
+            };
+            Term::Mut {
+                vars: new_vars,
+                body: Box::new(body_rw),
+            }
+        }
+        Term::Assign { name, value } => Term::Assign {
+            // Iter mut.1: substitute inside `value`; the `name` field
+            // refers to a mut-var declared by an enclosing
+            // `Term::Mut`. Renaming it here without renaming the
+            // declaration would break the scope link. The desugar
+            // pass's `subst_var` is used only to rewrite let-rec
+            // captures (KnownType / LetBound / MatchArm — never
+            // mut-vars), so leaving the `name` untouched is
+            // semantically correct: any `from` that matches the
+            // assigned `name` is in a different namespace by
+            // construction.
+            name: name.clone(),
+            value: Box::new(subst_var(value, from, to)),
+        },
     }
 }
 
@@ -1425,6 +1548,26 @@ pub fn subst_call_with_extras(t: &Term, name: &str, lifted: &str, extras: &[Stri
             source: Box::new(subst_call_with_extras(source, name, lifted, extras)),
             body: Box::new(subst_call_with_extras(body, name, lifted, extras)),
         },
+        Term::Mut { vars, body } => Term::Mut {
+            // Iter mut.1: structural recursion through each var's
+            // `init` and the block's body. Mut-var declarations
+            // cannot shadow a top-level fn name (mut-vars are
+            // first-order scalars, fns are not assignable), so the
+            // call-substitution sees through the block uniformly.
+            vars: vars
+                .iter()
+                .map(|v| MutVar {
+                    name: v.name.clone(),
+                    ty: v.ty.clone(),
+                    init: subst_call_with_extras(&v.init, name, lifted, extras),
+                })
+                .collect(),
+            body: Box::new(subst_call_with_extras(body, name, lifted, extras)),
+        },
+        Term::Assign { name: assign_name, value } => Term::Assign {
+            name: assign_name.clone(),
+            value: Box::new(subst_call_with_extras(value, name, lifted, extras)),
+        },
     }
 }
 
@@ -1479,6 +1622,24 @@ pub fn find_non_callee_use(t: &Term, name: &str) -> Option<Term> {
         Term::ReuseAs { source, body } => {
             find_non_callee_use(source, name).or_else(|| find_non_callee_use(body, name))
         }
+        // Iter mut.1: scan each var's init plus the body. Mut-vars
+        // are first-order scalars and never appear in callee position,
+        // so any matching `Term::Var` inside a mut block is non-callee
+        // by construction.
+        Term::Mut { vars, body } => vars
+            .iter()
+            .find_map(|v| find_non_callee_use(&v.init, name))
+            .or_else(|| find_non_callee_use(body, name)),
+        // Iter mut.1: the assigned `name` is a non-callee *use* of
+        // the mut-var; if it matches the searched name, surface the
+        // node itself. Otherwise recurse into the value.
+        Term::Assign { name: assign_name, value } => {
+            if assign_name == name {
+                Some(t.clone())
+            } else {
+                find_non_callee_use(value, name)
+            }
+        }
     }
 }
 
@@ -1521,6 +1682,11 @@ mod tests {
             }
             Term::Clone { value } => any_nested_ctor(value),
             Term::ReuseAs { source, body } => any_nested_ctor(source) || any_nested_ctor(body),
+            // Iter mut.1: scan each var's init plus the body.
+            Term::Mut { vars, body } => {
+                vars.iter().any(|v| any_nested_ctor(&v.init)) || any_nested_ctor(body)
+            }
+            Term::Assign { value, .. } => any_nested_ctor(value),
         }
     }
 
@@ -1546,6 +1712,11 @@ mod tests {
             Term::LetRec { .. } => true,
             Term::Clone { value } => any_let_rec(value),
             Term::ReuseAs { source, body } => any_let_rec(source) || any_let_rec(body),
+            // Iter mut.1: scan each var's init plus the body.
+            Term::Mut { vars, body } => {
+                vars.iter().any(|v| any_let_rec(&v.init)) || any_let_rec(body)
+            }
+            Term::Assign { value, .. } => any_let_rec(value),
         }
     }
 
@@ -2662,6 +2833,11 @@ mod tests {
             }
             Term::Clone { value } => any_lit_pattern(value),
             Term::ReuseAs { source, body } => any_lit_pattern(source) || any_lit_pattern(body),
+            // Iter mut.1: scan each var's init plus the body.
+            Term::Mut { vars, body } => {
+                vars.iter().any(|v| any_lit_pattern(&v.init)) || any_lit_pattern(body)
+            }
+            Term::Assign { value, .. } => any_lit_pattern(value),
         }
     }
 

crates/ailang-core/src/workspace.rs

@@ -1247,6 +1247,18 @@ where
             walk_term_embedded_types(source, f)?;
             walk_term_embedded_types(body, f)
         }
+        // Iter mut.1: each `MutVar.ty` is an embedded type — walk
+        // it. Then recurse into each var's `init` and the block's
+        // body. `Term::Assign` carries no embedded type; recurse
+        // into its `value` only.
+        Term::Mut { vars, body } => {
+            for v in vars {
+                walk_type(&v.ty, f)?;
+                walk_term_embedded_types(&v.init, f)?;
+            }
+            walk_term_embedded_types(body, f)
+        }
+        Term::Assign { value, .. } => walk_term_embedded_types(value, f),
     }
 }
 
@@ -1369,6 +1381,17 @@ where
             walk_term(source, f)?;
             walk_term(body, f)
         }
+        // Iter mut.1: `Term::Ctor.type_name` is the only string this
+        // walker reports — mut-vars carry no Ctor-type strings. Just
+        // recurse into each var's `init` and the body, and into
+        // assign's `value`.
+        Term::Mut { vars, body } => {
+            for v in vars {
+                walk_term(&v.init, f)?;
+            }
+            walk_term(body, f)
+        }
+        Term::Assign { value, .. } => walk_term(value, f),
     }
 }
 

crates/ailang-core/tests/design_schema_drift.rs

@@ -137,6 +137,20 @@ fn design_md_anchors_every_term_variant() {
                 body: Box::new(Term::Var { name: "y".into() }),
             },
         ),
+        (
+            r#""t": "mut""#,
+            Term::Mut {
+                vars: Vec::new(),
+                body: Box::new(Term::Lit { lit: Literal::Unit }),
+            },
+        ),
+        (
+            r#""t": "assign""#,
+            Term::Assign {
+                name: "x".into(),
+                value: Box::new(Term::Lit { lit: Literal::Unit }),
+            },
+        ),
     ];
 
     for (anchor, term) in exemplars {
@@ -156,6 +170,8 @@ fn design_md_anchors_every_term_variant() {
             Term::Seq { .. } => "seq",
             Term::Clone { .. } => "clone",
             Term::ReuseAs { .. } => "reuse-as",
+            Term::Mut { .. } => "mut",
+            Term::Assign { .. } => "assign",
         };
         assert!(
             data_model_section().contains(anchor),

crates/ailang-core/tests/schema_coverage.rs

@@ -47,6 +47,8 @@ enum VariantTag {
     TermSeq,
     TermClone,
     TermReuseAs,
+    TermMut,
+    TermAssign,
     // Pattern
     PatternWild,
     PatternVar,
@@ -92,6 +94,8 @@ const EXPECTED_VARIANTS: &[VariantTag] = &[
     VariantTag::TermSeq,
     VariantTag::TermClone,
     VariantTag::TermReuseAs,
+    VariantTag::TermMut,
+    VariantTag::TermAssign,
     VariantTag::PatternWild,
     VariantTag::PatternVar,
     VariantTag::PatternLit,
@@ -228,6 +232,18 @@ fn visit_term(t: &Term, observed: &mut HashSet<VariantTag>) {
             visit_term(source, observed);
             visit_term(body, observed);
         }
+        Term::Mut { vars, body } => {
+            observed.insert(VariantTag::TermMut);
+            for v in vars {
+                visit_type(&v.ty, observed);
+                visit_term(&v.init, observed);
+            }
+            visit_term(body, observed);
+        }
+        Term::Assign { value, .. } => {
+            observed.insert(VariantTag::TermAssign);
+            visit_term(value, observed);
+        }
     }
 }
 

crates/ailang-core/tests/spec_drift.rs

@@ -114,6 +114,20 @@ fn spec_mentions_every_term_variant() {
                 body: Box::new(Term::Var { name: "y".into() }),
             },
         ),
+        (
+            "(mut",
+            Term::Mut {
+                vars: Vec::new(),
+                body: Box::new(Term::Lit { lit: Literal::Unit }),
+            },
+        ),
+        (
+            "(assign",
+            Term::Assign {
+                name: "x".into(),
+                value: Box::new(Term::Lit { lit: Literal::Unit }),
+            },
+        ),
     ];
 
     for (anchor, term) in exemplars {
@@ -135,6 +149,8 @@ fn spec_mentions_every_term_variant() {
             Term::Seq { .. } => "seq",
             Term::Clone { .. } => "clone",
             Term::ReuseAs { .. } => "reuse-as",
+            Term::Mut { .. } => "mut",
+            Term::Assign { .. } => "assign",
         };
         assert!(
             FORM_A_SPEC.contains(anchor),

crates/ailang-prose/src/lib.rs

@@ -906,6 +906,35 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8, ow
                 out.push_str(&body_buf);
             }
         }
+        Term::Mut { vars, body } => {
+            // Iter mut.1: prose-side minimal-correctness rendering for
+            // the `(mut ...)` block. The prose-form for mut blocks is
+            // not yet fully designed (the prose surface predates this
+            // milestone); render the block as `mut { var <name>: <ty>
+            // = <init>; ...; <body> }` so a reader can see the shape
+            // without overcommitting to a final prose syntax. Refined
+            // in a follow-on prose iter once the LLM-author signal
+            // arrives.
+            out.push_str("mut {\n");
+            for v in vars {
+                indent(out, level + 1);
+                out.push_str("var ");
+                out.push_str(&v.name);
+                out.push_str(" = ");
+                write_term(out, &v.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::Assign { name, value } => {
+            out.push_str(name);
+            out.push_str(" := ");
+            write_term(out, value, level, owning_module);
+        }
     }
 }
 
@@ -1077,6 +1106,33 @@ fn count_free_var(name: &str, t: &Term) -> usize {
         }
         Term::Clone { value } => count_free_var(name, value),
         Term::ReuseAs { source, body } => count_free_var(name, source) + count_free_var(name, body),
+        // Iter mut.1: a `Term::Mut` whose `vars` includes a name
+        // matching `name` shadows the outer binding for both later
+        // var inits and the body. Var inits before the shadowing one
+        // still see the outer `name`.
+        Term::Mut { vars, body } => {
+            let mut total = 0usize;
+            let mut shadowed = false;
+            for v in vars {
+                if !shadowed {
+                    total += count_free_var(name, &v.init);
+                }
+                if v.name == name {
+                    shadowed = true;
+                }
+            }
+            if !shadowed {
+                total += count_free_var(name, body);
+            }
+            total
+        }
+        // Iter mut.1: the assigned `name` field is a use of the
+        // mut-var binding (which may or may not be `name`); the
+        // value is recursed.
+        Term::Assign { name: assign_name, value } => {
+            let n_use = if assign_name == name { 1 } else { 0 };
+            n_use + count_free_var(name, value)
+        }
     }
 }
 
@@ -1188,6 +1244,47 @@ fn subst_var_with_term(t: &Term, name: &str, replacement: &Term) -> Term {
             source: Box::new(subst_var_with_term(source, name, replacement)),
             body: Box::new(subst_var_with_term(body, name, replacement)),
         },
+        // Iter mut.1: lexical-shadow semantics for mut-vars symmetric
+        // to `count_free_var` above: once a var named `name` is
+        // declared, neither later inits nor the body should be
+        // rewritten.
+        Term::Mut { vars, body } => {
+            let mut shadowed = false;
+            let new_vars: Vec<ailang_core::ast::MutVar> = vars
+                .iter()
+                .map(|v| {
+                    let init = if shadowed {
+                        v.init.clone()
+                    } else {
+                        subst_var_with_term(&v.init, name, replacement)
+                    };
+                    if v.name == name {
+                        shadowed = true;
+                    }
+                    ailang_core::ast::MutVar {
+                        name: v.name.clone(),
+                        ty: v.ty.clone(),
+                        init,
+                    }
+                })
+                .collect();
+            let body_rw = if shadowed {
+                (**body).clone()
+            } else {
+                subst_var_with_term(body, name, replacement)
+            };
+            Term::Mut {
+                vars: new_vars,
+                body: Box::new(body_rw),
+            }
+        }
+        // Iter mut.1: substitute only inside `value`. The `name`
+        // field is a binding reference (cf. the desugar.rs
+        // `subst_var` arm).
+        Term::Assign { name: assign_name, value } => Term::Assign {
+            name: assign_name.clone(),
+            value: Box::new(subst_var_with_term(value, name, replacement)),
+        },
     }
 }
 

crates/ailang-surface/src/parse.rs

@@ -39,7 +39,8 @@
 //! term        ::= var-ref | int-lit | str-lit | bool-lit | unit-lit
 //!               | 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
+//!               | let-term | let-rec-term | clone-term | reuse-as-term
+//!               | mut-term | assign-term
 //! var-ref     ::= ident                  ; reserved: true/false → bool-lit
 //! int-lit     ::= integer                ; numeric atom
 //! str-lit     ::= string                 ; string atom
@@ -66,6 +67,9 @@
 //!                      "(" "in" term ")" ")"
 //! 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
+//! assign-term  ::= "(" "assign" ident term ")"     ; Iter mut.1; legal only inside mut-term
 //!
 //! pattern  ::= pat-var | pat-ctor | pat-lit | pat-wild
 //! pat-var  ::= ident
@@ -1206,6 +1210,8 @@ impl<'a> Parser<'a> {
                     "let-rec" => self.parse_let_rec(),
                     "clone" => self.parse_clone(),
                     "reuse-as" => self.parse_reuse_as(),
+                    "mut" => self.parse_mut(),
+                    "assign" => self.parse_assign(),
                     other => {
                         let pos = self.peek().map(|t| t.span.start).unwrap_or(0);
                         Err(ParseError::Production {
@@ -1213,7 +1219,8 @@ impl<'a> Parser<'a> {
                             message: format!(
                                 "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`, `lit-unit`"
+                                `tail-do`, `seq`, `term-ctor`, `clone`, `reuse-as`, `mut`, \
+                                `assign`, `lit-unit`"
                             ),
                             pos,
                         })
@@ -1565,6 +1572,76 @@ impl<'a> Parser<'a> {
         })
     }
 
+    /// Iter mut.1: `(mut (var NAME TYPE INIT)* BODY_TERM+)` — local
+    /// mutable-state block. Reads zero or more `(var ...)` entries
+    /// off the front of the body, then ≥ 1 trailing terms. The
+    /// trailing sequence is right-folded into `Term::Seq` with the
+    /// final term as the seed (so the JSON-AST always sees a single
+    /// `body: Term`). Spec `docs/specs/2026-05-15-mut-local.md`
+    /// §"Form A surface" + §"Canonical-form invariants".
+    fn parse_mut(&mut self) -> Result<Term, ParseError> {
+        let head_pos = self.peek().map(|t| t.span.start).unwrap_or(0);
+        self.expect_lparen("mut-term")?;
+        self.expect_keyword("mut")?;
+
+        // Pull off all leading (var NAME TYPE INIT) entries.
+        let mut vars: Vec<ailang_core::ast::MutVar> = Vec::new();
+        while matches!(self.peek_head_ident(), Some("var")) {
+            self.expect_lparen("mut-var")?;
+            self.expect_keyword("var")?;
+            let name = self.expect_ident("mut-var-name")?;
+            let ty = self.parse_type()?;
+            let init = self.parse_term()?;
+            self.expect_rparen("mut-var")?;
+            vars.push(ailang_core::ast::MutVar { name, ty, init });
+        }
+
+        // Then read ≥ 1 trailing body terms. Right-fold into Seq
+        // with the final term as the seed.
+        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: "mut-term",
+                message: "(mut ...) requires at least one body expression after vars".into(),
+                pos: head_pos,
+            });
+        }
+        self.expect_rparen("mut-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::Mut {
+            vars,
+            body: Box::new(body),
+        })
+    }
+
+    /// Iter mut.1: `(assign NAME VALUE)` — in-block update of a
+    /// mut-var. Positional shape: name then value. The lexical-scope
+    /// rule ("legal only inside a `(mut ...)` whose `vars` includes
+    /// a var with the same `name`") is enforced at typecheck
+    /// (mut.2, `CheckError::MutAssignOutOfScope`); the parser
+    /// accepts the shape unconditionally.
+    fn parse_assign(&mut self) -> Result<Term, ParseError> {
+        self.expect_lparen("assign-term")?;
+        self.expect_keyword("assign")?;
+        let name = self.expect_ident("assign-name")?;
+        let value = self.parse_term()?;
+        self.expect_rparen("assign-term")?;
+        Ok(Term::Assign {
+            name,
+            value: Box::new(value),
+        })
+    }
+
     // ---- patterns -------------------------------------------------------
 
     fn parse_pattern(&mut self) -> Result<Pattern, ParseError> {
@@ -2423,4 +2500,87 @@ mod tests {
             other => panic!("expected Term::Lit::Float, got {other:?}"),
         }
     }
+
+    /// Iter mut.1: `(mut 0)` parses as a `Term::Mut` with empty `vars`
+    /// and an `Int 0` body. Spec
+    /// `docs/specs/2026-05-15-mut-local.md` §"Canonical-form
+    /// invariants" — the empty-vars form is a legal degenerate case
+    /// the schema accepts uniformly.
+    #[test]
+    fn parses_empty_mut_with_int_body() {
+        let t = parse_term("(mut 0)").expect("parse");
+        match t {
+            Term::Mut { vars, body } => {
+                assert!(vars.is_empty(), "vars should be empty, got {vars:?}");
+                match *body {
+                    Term::Lit { lit: Literal::Int { value: 0 } } => {}
+                    other => panic!("expected Lit Int 0, got {other:?}"),
+                }
+            }
+            other => panic!("expected Term::Mut, got {other:?}"),
+        }
+    }
+
+    /// Iter mut.1: `(mut (var x ...) (assign x ...) x)` parses with
+    /// the trailing statement-and-final-expression sequence right-
+    /// folded into a `Term::Seq`. The schema's `Term::Mut.body` is
+    /// always a single Term; multi-statement bodies are folded
+    /// through `Seq` at parse time.
+    #[test]
+    fn parses_mut_with_one_var_and_one_assign_and_final() {
+        let src = "(mut (var x (con Int) 0) (assign x (app + x 1)) x)";
+        let t = parse_term(src).expect("parse");
+        match t {
+            Term::Mut { vars, body } => {
+                assert_eq!(vars.len(), 1, "expected exactly one var");
+                assert_eq!(vars[0].name, "x");
+                match *body {
+                    Term::Seq { lhs, rhs } => {
+                        match *lhs {
+                            Term::Assign { name, .. } => assert_eq!(name, "x"),
+                            other => panic!("expected Assign as Seq.lhs, got {other:?}"),
+                        }
+                        match *rhs {
+                            Term::Var { name } => assert_eq!(name, "x"),
+                            other => panic!("expected Var x as Seq.rhs, got {other:?}"),
+                        }
+                    }
+                    other => panic!("expected Seq as Mut.body, got {other:?}"),
+                }
+            }
+            other => panic!("expected Term::Mut, got {other:?}"),
+        }
+    }
+
+    /// Iter mut.1: `(mut)` with neither vars nor body is rejected at
+    /// parse — the spec's §"Canonical-form invariants" mandates at
+    /// least one body expression after the `var` entries.
+    #[test]
+    fn rejects_mut_with_no_body() {
+        let err = parse_term("(mut)").expect_err("must reject empty mut");
+        let msg = format!("{err}");
+        assert!(
+            msg.contains("mut"),
+            "diagnostic should mention `mut`, got: {msg}"
+        );
+        assert!(
+            msg.contains("body") || msg.contains("expression"),
+            "diagnostic should mention the missing body, got: {msg}"
+        );
+    }
+
+    /// Iter mut.1: `(mut (var x ...))` declares a var but has no
+    /// trailing body expression — also rejected (the rule is "≥ 0
+    /// vars followed by ≥ 1 body terms"; zero body terms is the
+    /// rejection trigger).
+    #[test]
+    fn rejects_mut_with_only_vars_no_final_expression() {
+        let err = parse_term("(mut (var x (con Int) 0))")
+            .expect_err("must reject vars-only mut");
+        let msg = format!("{err}");
+        assert!(
+            msg.contains("body") || msg.contains("expression"),
+            "diagnostic should mention missing body, got: {msg}"
+        );
+    }
 }

crates/ailang-surface/src/print.rs

@@ -548,6 +548,52 @@ fn write_term(out: &mut String, t: &Term, level: usize) {
             write_term(out, body, level);
             out.push(')');
         }
+        Term::Mut { vars, body } => {
+            // Iter mut.1: print as
+            //   `(mut (var NAME TYPE INIT)* STMT* FINAL_EXPR)`
+            // where the body's right-spine of `Term::Seq` is walked
+            // and each lhs is printed as a top-level statement; the
+            // terminal expression (the rightmost non-Seq term) is the
+            // block's value. This is the inverse of the parser's
+            // right-fold over the trailing sequence.
+            out.push_str("(mut");
+            for v in vars {
+                out.push_str(" (var ");
+                out.push_str(&v.name);
+                out.push(' ');
+                write_type(out, &v.ty);
+                out.push(' ');
+                write_term(out, &v.init, level);
+                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::Assign { name, value } => {
+            // Iter mut.1: print as `(assign NAME VALUE)`. Legal only
+            // inside a `Term::Mut.body`; the parser enforces the
+            // structural rule, the typechecker (mut.2) enforces the
+            // scope rule.
+            out.push_str("(assign ");
+            out.push_str(name);
+            out.push(' ');
+            write_term(out, value, level);
+            out.push(')');
+        }
     }
 }