diff --git a/docs/roadmap.md b/docs/roadmap.md
index 2553d5d..be99145 100644
--- a/docs/roadmap.md
+++ b/docs/roadmap.md
@@ -35,6 +35,20 @@ work progresses.
 
 ## P0 — In flight
 
+- [~] **\[milestone\]** Prose `loop` binders — projection redesign.
+  Form-B prose currently renders loop binders as `name = init;`
+  statements *inside* the `loop { … }` body, which misreads as
+  C/Rust re-init-every-iteration semantics. Move them to a
+  parenthesised init-list on the keyword — `loop(acc = 0, i = 1)
+  { … }` — positionally isomorphic to `recur(...)`. Projection-only:
+  one `ailang-prose` `write_term` `Term::Loop` arm + 2 snapshot
+  fixtures/tests; loop/recur AST, Form A, JSON-AST, typecheck,
+  codegen, and the Form-A↔JSON round-trip invariant all unchanged.
+  Spec'd + approved 2026-05-18; Step-7.5 grounding-check PASS. Plan
+  next.
+  - context: `docs/specs/2026-05-18-prose-loop-binders.md`;
+    surfaced from the loop/recur prose review (2026-05-18 chat).
+
 - [x] **\[milestone\]** Standalone `loop` / `recur` — CLOSED 2026-05-18.
   Strictly-additive strict-iteration surface, `recur` tail-position-only,
   no totality claim. Shipped: iter 1 `a179ec3` (additive AST nodes),
diff --git a/docs/specs/2026-05-18-prose-loop-binders.md b/docs/specs/2026-05-18-prose-loop-binders.md
new file mode 100644
index 0000000..b123991
--- /dev/null
+++ b/docs/specs/2026-05-18-prose-loop-binders.md
@@ -0,0 +1,341 @@
+# Prose `loop` binders — projection redesign — Design Spec
+
+**Date:** 2026-05-18
+**Status:** Draft — awaiting user spec review
+**Authors:** Brummel (orchestrator) + Claude
+
+## Goal
+
+The Form-B prose projection of `Term::Loop` currently renders the
+binder-with-initial-value list as bare `name = init;` statements
+*inside* the `loop { … }` body block:
+
+```rust
+loop {
+  acc = 0;
+  i = 1;
+  if i > n { acc } else { recur(acc + i, i + 1) }
+}
+```
+
+A reader (LLM or human) decodes `loop { x = 0; … }` with the
+C/Rust mental model: *re-assign `x = 0` on every iteration, then run
+the rest*. That reading is wrong. The binders are **loop entry
+state**, bound once on entry and thereafter re-bound **only** by
+`recur`; they are not body statements and do not re-run per iteration.
+
+Prose exists as the reading/diffing surface. AILang's load-bearing
+doctrine is "the signature tells the truth without reading the body";
+the dual obligation is that *when the body is read, the projection
+must not lie about it*. The current projection lies. This milestone
+replaces it.
+
+The fix is a single change to one render arm in `ailang-prose`.
+The `loop`-recur AST, Form-A surface, canonical JSON-AST, typechecker
+and codegen are **unchanged**. This is a projection-only milestone,
+one iteration.
+
+## Architecture
+
+`ailang-prose` is a one-way, deliberately lossy projection
+(`docs/PROSE_ROUNDTRIP.md`). There is **no Form-B parser**: edited
+prose is re-integrated by an LLM mediator (`ail merge-prose`), and
+that mediator is fed `ailang_surface::print` (Form-A) as the original
+module — *not* the prose. Consequently the `loop` prose rendering
+feeds nothing back: it is read by humans/LLMs in step 2 of the
+prose cycle and nowhere else.
+
+The byte-isomorphic round-trip invariant in this project is
+**Form-A ↔ JSON-AST** (surface crate, gated by the cross-form-identity
+preflight). Prose is not on that path. This milestone therefore has
+**zero** interaction with the round-trip invariant — stated explicitly
+here so milestone-close audit does not chase a phantom risk.
+
+The only contract the change must preserve is *projection
+determinism* (same module → same prose bytes), which any pure printer
+change preserves trivially, plus the snapshot-test discipline in
+`crates/ailang-prose/tests/snapshot.rs` (a renderer change requires a
+deliberate, diff-visible snapshot update — exactly the RED→GREEN of
+this milestone).
+
+The chosen rendering is a parenthesised init-list on the `loop`
+keyword, positionally isomorphic to `recur`'s argument list:
+
+```rust
+loop(acc = 0, i = 1) {
+  if i > n { acc } else { recur(acc + i, i + 1) }
+}
+```
+
+Rationale (semantic, not effort):
+- The body block `{ … }` now contains exactly the loop body — the
+  binders are physically outside it, killing the "re-init every
+  iteration" misreading at the syntax level.
+- `loop(acc = 0, i = 1)` and `recur(acc + i, i + 1)` are the same
+  positional shape. The binder list *is* the parameter list that
+  `recur` re-supplies; making them visually isomorphic teaches the
+  correct model ("`recur` re-binds these, positionally") instead of
+  obscuring it.
+- Types are stripped (`acc = 0`, not `acc: Int = 0`), consistent
+  with the standing prose rule that `(con T)` is dropped everywhere
+  — `let`, `mut`/`var`, and fn parameters all render type-free in
+  prose because the type is re-derivable.
+
+Rejected alternatives:
+- **`loop with acc = 0, i = 1 { … }`** — `with` already denotes the
+  effect set in prose (`fn main() -> Unit with IO`). Overloading one
+  token with two unrelated meanings reduces readability; rejected on
+  the token-collision ground, not on effort.
+- **`loop { initially acc = 0, i = 1; <body> }`** — stays inside the
+  braces (still visually conflated) and invents an `initially`
+  keyword; weaker than the chosen form on the exact axis at issue.
+
+## Concrete code shapes
+
+### The AILang program (primary — clause-1 evidence)
+
+This milestone changes **no** authoring surface, so there is no new
+construct an LLM author reaches for. The clause-1 artefact is the
+existing, unchanged Form-A program and its projection. The program
+(`examples/loop_sum_to_run.ail`, verbatim, unchanged by this
+milestone):
+
+```lisp
+(module loop_sum_to_run
+  (fn main
+    (doc "loop-recur iter 3 — sum 1..10 via loop/recur. Expected stdout: 55.")
+    (type (fn-type (params) (ret (con Unit)) (effects IO)))
+    (params)
+    (body (app print (app sum_to 10))))
+  (fn sum_to
+    (type (fn-type (params (con Int)) (ret (con Int))))
+    (params n)
+    (body
+      (loop (acc (con Int) 0) (i (con Int) 1)
+        (if (app > i n)
+            acc
+            (recur (app + acc i) (app + i 1)))))))
+```
+
+Its prose projection, **before** (current, misleading):
+
+```rust
+// module loop_sum_to_run
+
+/// loop-recur iter 3 — sum 1..10 via loop/recur. Expected stdout: 55.
+fn main() -> Unit with IO {
+  print(sum_to(10))
+}
+
+fn sum_to(n: Int) -> Int {
+  loop {
+    acc = 0;
+    i = 1;
+    if i > n {
+      acc
+    } else {
+      recur(acc + i, i + 1)
+    }
+  }
+}
+```
+
+**After** (this milestone):
+
+```rust
+// module loop_sum_to_run
+
+/// loop-recur iter 3 — sum 1..10 via loop/recur. Expected stdout: 55.
+fn main() -> Unit with IO {
+  print(sum_to(10))
+}
+
+fn sum_to(n: Int) -> Int {
+  loop(acc = 0, i = 1) {
+    if i > n {
+      acc
+    } else {
+      recur(acc + i, i + 1)
+    }
+  }
+}
+```
+
+The empty-binder loop (`examples/loop_forever_build.ail`'s
+`(loop (i (con Int) 0) (recur (app + i 1)))` has one binder; a
+genuinely binder-less `(loop <body>)` is also legal) renders
+`loop() { … }` — parentheses are always emitted, for regularity
+and symmetry with `recur()` (which already renders the no-arg form
+with empty parens). Single-binder example
+(`examples/loop_forever_build.ail`):
+
+```rust
+fn spin(n: Int) -> Int {
+  loop(i = 0) {
+    recur(i + 1)
+  }
+}
+```
+
+### Implementation shape (secondary — supporting, not the point)
+
+One arm in `crates/ailang-prose/src/lib.rs`, the `Term::Loop` case
+of `write_term` (currently lib.rs:938–954).
+
+Before:
+
+```rust
+Term::Loop { binders, body } => {
+    // loop-recur iter 1: minimal-correctness Form-B render.
+    // Prose surface for loop is not yet designed; render the
+    // shape so a reader sees it without overcommitting.
+    out.push_str("loop {\n");
+    for b in binders {
+        indent(out, level + 1);
+        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('}');
+}
+```
+
+After:
+
+```rust
+Term::Loop { binders, body } => {
+    out.push_str("loop(");
+    for (i, b) in binders.iter().enumerate() {
+        if i > 0 {
+            out.push_str(", ");
+        }
+        out.push_str(&b.name);
+        out.push_str(" = ");
+        write_term(out, &b.init, level, 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('}');
+}
+```
+
+The init expressions render at `level` (they are on the keyword
+line, not inside the indented block) — mirrors how `recur`'s args
+already render at the call-site level (lib.rs:956–965). The doc
+comment that says "Prose surface for loop is not yet designed" is
+removed (it is now designed). `Term::Recur` is **unchanged**: it
+already renders `recur(a, b)` correctly and is now visibly
+isomorphic to the loop head.
+
+The two non-render `Term::Loop` sites — `count_free_var`
+(lib.rs:~1167) and `subst_var_with_term` (lib.rs:~1341) — are
+**not touched**; they implement shadowing/substitution semantics,
+not rendering.
+
+## Components
+
+- `crates/ailang-prose/src/lib.rs` — rewrite the `Term::Loop` arm
+  of `write_term`. ~12 LOC in one arm. No signature change, no new
+  function, no new dependency.
+- `examples/loop_sum_to_run.prose.txt` (new) and
+  `examples/loop_forever_build.prose.txt` (new) — committed snapshot
+  expectations carrying the Option-A bytes.
+- `crates/ailang-prose/tests/snapshot.rs` — two `#[test]` functions
+  (`snapshot_loop_sum_to_run`, `snapshot_loop_forever_build`)
+  invoking the existing `check_snapshot` harness. These cover the
+  two structurally distinct cases: multi-binder + non-recur exit,
+  and single-binder + recur-only (no exit).
+
+## Data flow
+
+`examples/<stem>.ail` → `ailang_surface::load_module` →
+`ailang_prose::module_to_prose` → byte-compare against committed
+`examples/<stem>.prose.txt`. Unchanged harness; this milestone only
+adds two stems to the set and changes the bytes the renderer
+produces for `Term::Loop`.
+
+No runtime, codegen, typecheck, or schema data path is touched.
+
+## Error handling
+
+None applicable. Prose rendering is total over a well-formed AST
+(the AST is already validated by `load_module` before reaching the
+renderer). The change introduces no new failure mode and no new
+diagnostic. The empty-binder case is handled by the loop emitting
+`loop() { … }` (the `for` loop body simply does not execute; the
+`(` / `)` are emitted unconditionally).
+
+## Testing strategy
+
+RED-first, via the existing snapshot harness:
+
+1. **RED.** Author `examples/loop_sum_to_run.prose.txt` and
+   `examples/loop_forever_build.prose.txt` with the **desired**
+   Option-A bytes, plus the two `#[test]` functions. Against the
+   current renderer these fail (it emits the old `loop { acc = 0;
+   … }` shape), pinning the symptom.
+2. **GREEN.** Apply the `write_term` `Term::Loop` rewrite. Both
+   snapshots pass.
+3. **No-regression.** The full `crates/ailang-prose` test suite
+   stays green — no other fixture contains `Term::Loop`, so no
+   other snapshot changes (confirmed: no existing
+   `examples/*.prose.txt` contains `loop`).
+4. **Determinism** is covered structurally — the renderer is a pure
+   function of the AST; the snapshot equality check *is* the
+   determinism assertion.
+
+Explicitly **out of scope for test coverage** (because untouched):
+the Form-A ↔ JSON-AST cross-form-identity preflight and the
+`merge-prose` cycle. The spec asserts these are not on the changed
+path; no new test is added there because nothing there changes.
+
+Multi-line wrapping of a long binder list is **out of scope**:
+single-line comma-separated, consistent with how `recur` args and
+fn-call args already render. If a future fixture needs wrapping it
+is a separate, separately-motivated change.
+
+## Acceptance criteria
+
+- `cargo test -p ailang-prose` green, including the two new
+  `snapshot_loop_*` tests.
+- `ail prose examples/loop_sum_to_run.ail` emits the **After**
+  block above byte-for-byte (binders on the `loop(...)` keyword
+  line; the `{ … }` body contains no `name = init;` lines).
+- `ail prose examples/loop_forever_build.ail` emits `loop(i = 0) {`
+  with `recur(i + 1)` as the body.
+- No diff in any other `examples/*.prose.txt`.
+- No change to `examples/*.ail`, `*.ail.json` build artefacts,
+  typecheck, codegen, runtime, or `docs/DESIGN.md` (the loop/recur
+  semantics are unchanged; only their reading projection changes).
+- `docs/PROSE_ROUNDTRIP.md` unchanged (the cycle it documents is
+  untouched; prose remains a lossy one-way projection).
+
+### Feature-acceptance criterion (DESIGN.md gate)
+
+This is a projection change, not an authoring feature, so clause 1
+("an LLM author naturally produces code that uses it") is evaluated
+against the *reading* surface, not a new construct: the program is
+unchanged; the deliverable is its honest projection. The three
+clauses:
+
+1. **Naturally used:** the prose surface is the LLM/human reading
+   and diffing surface for every module containing a loop — it is
+   used by construction, not opt-in.
+2. **Measurably improves correctness / removes redundancy:** yes —
+   it removes a projection that actively implies wrong (re-init-
+   every-iteration) loop semantics. A reading surface that lies
+   about the body it projects is a correctness defect in that
+   surface; the fix is the removal of that defect.
+3. **Reintroduces no eliminated bug class:** none. Prose has no
+   parser and relaxes no semantic constraint; the Form-A surface,
+   typechecker, codegen, and round-trip invariant are untouched.
+
+Passes on all three.