diff --git a/packages/kaisel/doc/migration/from-auto-route.md b/packages/kaisel/doc/migration/from-auto-route.md
index 4ff8af0..8651719 100644
--- a/packages/kaisel/doc/migration/from-auto-route.md
+++ b/packages/kaisel/doc/migration/from-auto-route.md
@@ -439,6 +439,48 @@ class AppCodec extends KaiselConfigCodec<AppRoute> {
 The codec is the only place strings live. Every other layer reasons
 about typed routes.
 
+## Verb translation
+
+The full navigation surface, since a real migration touches far more than the
+concept mapping above. (One port measured 787 router calls across 41 files.)
+
+| auto_route | kaisel |
+| --- | --- |
+| `push(X)` | `push(X)` |
+| `push<T>(X)` (awaited) | `pushForResult<T>(X)` |
+| `navigate(X)` | `push(X)` |
+| `replace(X)` | `replaceTop(X)` |
+| `replaceAll([...])` | `set([...])` |
+| `popAndPush(X)` | `replaceTop(X)` |
+| `pop()` | `pop()` |
+| `pop<T>(result)` | `pop(result)` — the result is `Object?`, so the type is not checked against the awaiting `pushForResult<T>` |
+| `maybePop()` | `context.maybePop()` — **not** `pop()`; see below |
+| `pushAndPopUntil(X, predicate:)` | `pushAndPopUntil(X, predicate:)` |
+| `popUntilRouteWithName(n)` | `popUntil((route) => route is N)` |
+| `popUntilRoot()` | `popUntilRoot()` |
+| `router.root` / `router.parent` | n/a — the stack is flat |
+| `router.stackData` | `router.stack` |
+| `entry.routeData` | the entry **is** the route |
+| `entry.routeData.args` | destructure the route: `Product(:final id)` |
+| `route.settings.name == X.name` | `route is X` — see below |
+| `isRouteActive(X.name)` | `stack.any((route) => route is X)` |
+
+### Two rows that bite
+
+**`maybePop()` → `pop()` is wrong.** It is the most natural-looking
+translation and it silently changes behaviour: `pop()` mutates the kaisel
+stack directly, so an open `Drawer`'s local history entry is never consumed
+and a `PopScope(canPop: false)` veto is never consulted. Use
+`context.maybePop()`, which asks the `Navigator` first. In one migration
+`maybePop` was 155 of 170 pop-family calls — this is the common case, not an
+edge one.
+
+**`route.settings.name == X.name` → `route is X`.** Rewriting `.name`
+mechanically produces `route == BuyRoute` — comparing a `String` to a
+`Type`. That **compiles**; only `unrelated_type_equality_checks`, an
+*info*-level lint, catches it. Left alone it ships as a permanently-false
+condition. Pattern-match on the type instead.
+
 ## Already at parity — or better
 
 **DevTools.** kaisel ships its own zero-integration DevTools extension — a live
diff --git a/skills/kaisel/NAVIGATION.md b/skills/kaisel/NAVIGATION.md
index 3d1155d..cc7e43f 100644
--- a/skills/kaisel/NAVIGATION.md
+++ b/skills/kaisel/NAVIGATION.md
@@ -42,6 +42,9 @@ below show the typed form first.
 | `replaceTop(route)` | Removes top, pushes new | `Future<void>` | Swap current screen in place (no back history) |
 | `pushOrReplaceTop(route)` | Push if top differs in runtime type; replace if same | `Future<void>` | Adaptive master-detail; tab-style in-place updates |
 | `set(routes)` | Replaces entire stack | `Future<void>` | Auth state transitions, deep-link landing |
+| `popUntil(predicate)` | Pops down to an anchor | `Future<void>` | "Back to the cart", unwinding several screens at once |
+| `pushAndPopUntil(route, predicate:)` | Pops to an anchor, then pushes | `Future<void>` | Finish a flow and land on a result screen |
+| `popUntilRoot()` | Pops everything above the root | `Future<void>` | "Home" from anywhere |
 | `run<T>(flow)` | Opens a typed modal flow | `Future<T?>` (flow result) | Modal sub-flows (payment, wizard, picker) |
 
 `pushForResult<T>` and `run<T>` both return `Future<T?>`. The difference is
@@ -284,6 +287,38 @@ page state — but derivation happens on state *events*, not widget
 builds, and every derived stack still flows through the guard pipeline.
 `stackFor` is a pure function you can unit test without a widget tree.
 
+## popUntil / pushAndPopUntil / popUntilRoot
+
+```dart
+final router = context.router<AppRoute>();
+
+router.popUntil((route) => route is Cart);
+router.pushAndPopUntil(const Receipt(), predicate: (route) => route is Home);
+router.popUntilRoot();
+```
+
+Anchor-relative unwinding, for when "go back" means several screens at once.
+Each is one mutation through the guard pipeline, not a loop of pops.
+
+**Use for:** finishing a checkout onto a receipt without leaving the payment
+screens behind it; a "back to cart" affordance; a Home button that clears
+everything above the root.
+
+**Notes:**
+
+- The anchor is the **topmost** entry matching the predicate; anything below
+  it stays.
+- **When nothing matches, the two differ deliberately.** `popUntil` keeps the
+  root — the stack can never be emptied — while `pushAndPopUntil` replaces
+  the whole stack with the pushed route, since there was no anchor to stop
+  at.
+- Browser history follows the verb each one resembles: `pushAndPopUntil` adds
+  an entry like `push`, the pop verbs move back like `pop`. (`set` replaces
+  the current entry — that's the difference from rolling these yourself on
+  top of it.)
+- `set` is still the primitive; these are the common shapes named, with the
+  off-by-one at the anchor handled for you.
+
 ## run
 
 ```dart