diff --git a/docs/_template/page.html b/docs/_template/page.html
index f8c29b1..37fcc02 100644
--- a/docs/_template/page.html
+++ b/docs/_template/page.html
@@ -34,6 +34,7 @@
       <ul>
         <li><a href="__ROOT__manual/getting-started/">Getting started</a></li>
         <li><a href="__ROOT__manual/writing-specs/">Writing specs</a></li>
+        <li><a href="__ROOT__manual/spec-language/">Spec language reference</a></li>
         <li><a href="__ROOT__manual/runs/">Runs</a></li>
         <li><a href="__ROOT__manual/inspect/">Inspect</a></li>
         <li><a href="__ROOT__manual/cli/">CLI reference</a></li>
diff --git a/docs/development/architecture.md b/docs/development/architecture.md
index f0eb863..ad335a8 100644
--- a/docs/development/architecture.md
+++ b/docs/development/architecture.md
@@ -15,12 +15,14 @@ flowchart TB
     end
 
     SC["Maestro sidecar (JVM)"]
+    DC["Device / Emulator"]
     CH["Chrome (CDP)"]
     RD[("runs/")]
     IN["sanderling inspect\nHTTP + SSE"]
     UI["Web UI (React)"]
 
     D -->|gRPC| SC
+    SC -->|UIAutomator / XCTest| DC
     D -->|CDP| CH
 
     T --> RD --> IN --> UI
diff --git a/docs/manual/index.md b/docs/manual/index.md
index 0f9c1da..6cb8cd7 100644
--- a/docs/manual/index.md
+++ b/docs/manual/index.md
@@ -6,5 +6,6 @@ title: Manual
 
 - [Getting started](./getting-started/)
 - [Writing specs](./writing-specs/)
+- [Spec language reference](./spec-language/)
 - [Runs](./runs/)
 - [CLI reference](./cli/)
diff --git a/docs/manual/spec-language.md b/docs/manual/spec-language.md
new file mode 100644
index 0000000..e394fef
--- /dev/null
+++ b/docs/manual/spec-language.md
@@ -0,0 +1,237 @@
+---
+title: Spec language reference
+---
+
+# Spec language reference
+
+## Module structure
+
+A spec is a TypeScript module evaluated by the Go runner each step. It must export `properties` and `actionsRoot` on `globalThis` (the bundler entry point does this automatically via the final two lines):
+
+```ts
+import { ... } from "@sanderling/spec";
+
+export const properties = { ... };
+export const actionsRoot = weighted(...);
+
+(globalThis as { actions?: unknown }).actions = actionsRoot;
+(globalThis as { properties?: unknown }).properties = properties;
+```
+
+## State
+
+Every extractor callback receives a `State`:
+
+```ts
+interface State {
+  ax: AccessibilityTree;
+  snapshots: Record<string, unknown>;
+  lastAction: Action | null;
+  logs: readonly LogEntry[];
+  exceptions: readonly ExceptionRecord[];
+  time: number;   // ms since run start
+}
+```
+
+| Field | Description |
+|---|---|
+| `ax` | Live UI hierarchy for this step |
+| `snapshots` | Key-value data pushed by the app SDK (empty if SDK not integrated) |
+| `lastAction` | The action dispatched in the previous step, or `null` on the first step |
+| `logs` | Log entries collected since the previous step |
+| `exceptions` | Uncaught exceptions or `Sanderling.reportError()` calls since the previous step |
+| `time` | Milliseconds elapsed since the run started |
+
+## Selectors
+
+Selectors are passed to `ax.find()`, `ax.findAll()`, and element-scoped `.find()` / `.findAll()`.
+
+### String selectors
+
+| Form | Matches |
+|---|---|
+| `id:<value>` | Exact match on resource-id, or element whose resource-id ends with `:id/<value>` (Android) |
+| `text:<value>` | Substring match on text content |
+| `desc:<value>` | Exact match on accessibility description; also matches when description starts with `<value>, ` (iOS merged labels) |
+| `descPrefix:<prefix>` | Starts-with match on accessibility description |
+| `<attr>:<value>` | Substring match on any raw attribute by name |
+
+Boolean attributes (`"true"` / `"false"`) use exact match rather than substring.
+
+### Object selectors
+
+Pass an object to apply multiple attribute filters with AND semantics:
+
+```ts
+s.ax.find({ accessibilityText: "LoginScreen" })
+s.ax.find({ accessibilityText: "account_card", clickable: "true" })
+```
+
+Every key-value pair must match. Substring and boolean rules apply per attribute.
+
+### Path queries
+
+Chains of string selectors separated by ` > ` scope each segment to the subtree of the previous match. Path queries are only supported on the tree root (`ax.find`, `ax.findAll`), not on element-scoped `.find`/`.findAll`.
+
+```ts
+s.ax.find("id:HomeScreen > descPrefix:account_card:")
+s.ax.find("id:LedgerScreen > desc:ledger_balance_display")
+```
+
+### Cross-platform aliases
+
+These key aliases are resolved automatically so selectors work across platforms without changes:
+
+| Write this | Also checks |
+|---|---|
+| `content-desc` | `accessibilityText` |
+| `accessibilityText` | `content-desc` |
+| `label` | `accessibilityText` |
+| `accessibilityLabel` | `accessibilityText` |
+| `identifier` | `resource-id` |
+| `accessibilityIdentifier` | `resource-id` |
+
+## AccessibilityElement fields
+
+Fields available on every element returned by `find` / `findAll`:
+
+| Field | Type | Description |
+|---|---|---|
+| `id` | `string` | resource-id (Android) or accessibility identifier (iOS) |
+| `text` | `string` | Visible text content |
+| `desc` | `string` | Accessibility description (`content-desc` / `accessibilityText`) |
+| `class` | `string` | View class (Android), element type (iOS), or HTML tag (web) |
+| `clickable` | `boolean` | Element is interactive |
+| `enabled` | `boolean` | Element is enabled |
+| `checked` | `boolean` | Checkbox or toggle state |
+| `focused` | `boolean` | Element has input focus |
+| `selected` | `boolean` | Selection state |
+| `bounds` | `{ left, top, right, bottom }` | Bounding box in device pixels |
+| `x` | `number` | Center X (derived from bounds) |
+| `y` | `number` | Center Y (derived from bounds) |
+| `attrs` | `Record<string, string>` | All raw attributes from the driver |
+
+## Platform notes
+
+### Android
+
+- `id` maps to the Android resource-id (e.g., `com.example:id/button`). The `id:<value>` selector matches by suffix after `:id/`, so `id:button` matches `com.example:id/button`.
+- `desc` maps to `content-desc`.
+- `class` is the Java view class name (e.g., `android.widget.TextView`).
+- `attrs` contains raw UIAutomator attributes: `package`, `scrollable`, `checkable`, etc.
+
+### iOS
+
+- `id` maps to the `accessibilityIdentifier` set via `.accessibilityIdentifier` in SwiftUI/UIKit.
+- `desc` maps to `accessibilityText`, which Maestro builds by merging `accessibilityLabel` and the element's value (e.g., `"Close, icon description"`). The `desc:<value>` selector handles this by also matching when the description starts with `<value>, `.
+- `class` is the XCUITest element type (e.g., `XCUIElementTypeButton`).
+- `attrs` contains raw XCUITest attributes: `title`, `placeholderValue`, `hasFocus`, etc.
+
+### Web (Chrome)
+
+- `id` maps to the HTML `id` attribute.
+- `desc` is derived from `aria-label`, `alt`, or `title`.
+- `class` is the lowercase HTML tag name (e.g., `button`, `input`).
+- `attrs` contains all HTML attributes available to CDP.
+
+### KMP (Kotlin Multiplatform)
+
+KMP apps are tested identically to native apps. An Android KMP build uses the Android driver; an iOS KMP build uses the iOS driver. There is no separate KMP driver. The accessibility tree structure reflects the target platform, so the same selector portability rules apply.
+
+## Extractors
+
+```ts
+const loggedIn = extract((s) => !!s.ax.find("id:home-tab-bar"));
+loggedIn.current    // T - value from the current step
+loggedIn.previous   // T | undefined - value from the previous step, undefined on first step
+```
+
+Extractors are evaluated before properties and action generators. Use `.previous` to detect transitions between steps.
+
+## LTL operators
+
+| Function | Meaning |
+|---|---|
+| `always(f)` | `f` must hold at every step |
+| `eventually(f).within(n, unit)` | `f` must hold at some step within `n` `"milliseconds"`, `"seconds"`, or `"steps"` |
+| `now(f)` | `f` evaluated at the current step (for use inside `always`/`next` bodies) |
+| `next(f)` | `f` evaluated at the step immediately after the current one |
+
+**Formula combinators** - available on every `Formula`:
+
+| Method | Meaning |
+|---|---|
+| `.implies(other)` | If `this` holds, `other` must also hold |
+| `.and(other)` | Both must hold |
+| `.or(other)` | At least one must hold |
+| `.not()` | Negation |
+
+## Actions
+
+### Constructors
+
+```ts
+Tap({ on: element | string })
+InputText({ into: element | string, text: string })
+Swipe({ from: element | Point, to: element | Point, durationMillis?: number })
+PressKey({ key: Key })
+Wait({ durationMillis: number })
+```
+
+`Key` values: `"back"`, `"home"`, `"enter"`, `"tab"`, `"up"`, `"down"`, `"left"`, `"right"`.
+
+On web, `"back"` maps to Backspace and `"home"` is not supported. All other keys work on all platforms.
+
+### Built-in generators
+
+| Generator | Behaviour |
+|---|---|
+| `taps` | Random tap on a clickable element |
+| `swipes` | Random swipe gesture |
+| `waitOnce` | Idles one step |
+| `pressKey` | Presses a random supported key |
+
+### `actions(generator)`
+
+Wraps a callback that returns `Action[]`. The callback runs each step the generator is eligible.
+
+```ts
+const doLogin = actions(() => {
+  if (loggedIn.current) return [];
+  const submit = loginSubmit.current;
+  return submit ? [Tap({ on: submit })] : [];
+});
+```
+
+### `weighted(...entries)`
+
+Assembles a weighted tree. Each entry is `[weight, generator]`. Weights are relative within the tree.
+
+```ts
+export const actionsRoot = weighted(
+  [50, doLogin],
+  [10, taps],
+  [2,  swipes],
+);
+```
+
+### `from(items)`
+
+Returns a `Sampler<T>` that cycles through a fixed list. Use `.generate()` to pick an item.
+
+```ts
+const names = from(["Checking", "Savings", "Travel"]);
+// inside an actions() callback:
+InputText({ into: nameField, text: names.generate() })
+```
+
+## Default properties
+
+```ts
+import { noUncaughtExceptions, noLogcatErrors } from "@sanderling/spec/defaults/properties";
+```
+
+| Property | Fails when |
+|---|---|
+| `noUncaughtExceptions` | An uncaught exception or `Sanderling.reportError()` call is captured |
+| `noLogcatErrors` | Logcat emits any error-level (`E`) lines since the previous step |
diff --git a/docs/manual/writing-specs.md b/docs/manual/writing-specs.md
index b32d517..4b46753 100644
--- a/docs/manual/writing-specs.md
+++ b/docs/manual/writing-specs.md
@@ -9,16 +9,13 @@ A spec has three parts: extractors, properties, and actions.
 ```ts
 import { extract, always, now, actions, weighted, Tap, taps, swipes } from "@sanderling/spec";
 
-// 1. Extractors pull values from each observed state.
 const loggedIn = extract((s) => !!s.ax.find("id:home-tab-bar"));
 
-// 2. Properties are LTL formulas evaluated every step.
 export const properties = {
   cartNeverNegative: always(() => cartCount.current >= 0),
 };
 
-// 3. Actions are a weighted tree of what sanderling is allowed to do.
-export const actions = weighted(
+export const actionsRoot = weighted(
   [10, taps],
   [2, swipes],
 );
@@ -28,84 +25,207 @@ The Go runner calls into the JS runtime each step. Extractors re-read the curren
 
 ## The `State` object
 
-What extractors see:
+What extractors receive:
 
 ```ts
 interface State {
-  ax: AccessibilityTree;               // view hierarchy
-  screen: { id: string; hash: string };
+  ax: AccessibilityTree;
+  snapshots: Record<string, unknown>;
   lastAction: Action | null;
-  logs: LogEntry[];                    // since previous state
-  exceptions: Exception[];
-  time: number;                        // ms since run start
+  logs: readonly LogEntry[];
+  exceptions: readonly ExceptionRecord[];
+  time: number;   // ms since run start
 }
 ```
 
-`ax.find("text:Click me")`, `ax.find("id:login-form")`, `ax.findAll("role:todo-row")` are the common accessors. Prefer stable testID-style identifiers over positional selectors, for the same reason you would in Espresso or XCUITest.
+`ax` is the live UI hierarchy. `snapshots` carries any key-value data pushed by the app SDK. `logs` and `exceptions` contain entries collected since the previous step.
 
-## Pattern: preconditions (login, onboarding)
+## Extractors
 
-sanderling has no setup phase and no fixtures. Preconditions are action generators with two properties:
+`extract()` wraps a getter that runs against every new state. The returned object exposes `.current` (this step's value) and `.previous` (last step's, or `undefined` on the first step).
 
-1. High weight, so they fire whenever applicable.
-2. Gated on a state extractor, so they return an empty tree when not applicable and self-disable once the precondition is met.
+```ts
+const loggedIn = extract((s) => !!s.ax.find("id:home-tab-bar"));
+const balance = extract<number>((s) => s.snapshots["account.balance"] as number ?? 0);
+
+// Inside a property or action:
+loggedIn.current     // boolean
+loggedIn.previous    // boolean | undefined
+```
+
+Extractors are cheap. Prefer one extractor per concept and reuse it across properties and action generators.
+
+## Finding elements
+
+`ax.find(selector)` returns the first matching `AccessibilityElement`, or `undefined`. `ax.findAll(selector)` returns all matches. Both are available on the tree root and on any element (scoped to its subtree).
+
+**String selectors:**
+
+| Form | Match rule |
+|---|---|
+| `id:<value>` | Exact match on resource-id, or suffix after `:id/` (Android) |
+| `text:<value>` | Substring match on text content |
+| `desc:<value>` | Exact match on accessibility description, or starts-with for iOS merged labels |
+| `descPrefix:<prefix>` | Starts-with on accessibility description |
+| `<attr>:<value>` | Substring match on any raw attribute by name |
+
+**Object selectors** (AND of all given attributes):
+
+```ts
+s.ax.find({ accessibilityText: "LoginScreen" })
+s.ax.find({ accessibilityText: "login_email" })
+```
+
+**Path queries** (global only):
+
+```ts
+s.ax.find("id:HomeScreen > descPrefix:account_card:")
+```
+
+Each segment is matched within the subtree of the previous match.
+
+**Cross-platform aliases** are resolved automatically. `label` and `accessibilityLabel` both resolve to `accessibilityText`; `content-desc` and `accessibilityText` are interchangeable; `identifier` and `accessibilityIdentifier` resolve to `resource-id`.
+
+See the [Spec language reference](./spec-language/) for the complete selector grammar and per-platform field availability.
+
+## Properties
+
+Properties are named LTL formulas exported from the spec. The verifier evaluates each one every step and fails the run when a formula is violated.
+
+```ts
+export const properties = {
+  balanceNeverNegative: always(() => balance.current >= 0),
+  loginReachable: eventually(() => loggedIn.current).within(30, "seconds"),
+};
+```
+
+**Operators:**
+
+- `always(f)` - `f` must hold at every step.
+- `eventually(f).within(n, unit)` - `f` must hold at some step within `n` milliseconds, seconds, or steps.
+- `now(f)` - evaluates `f` at the current step (used for implication antecedents).
+- `next(f)` - evaluates `f` at the next step.
+
+**Combinators** - available on any formula:
+
+```ts
+now(() => loggedIn.current).implies(now(() => cartCount.current !== undefined))
+formulaA.and(formulaB)
+formulaA.or(formulaB)
+formulaA.not()
+```
+
+`implies`, `and`, `or`, and `not` compose freely.
+
+## Actions
+
+Action generators return a list of actions to perform. The runner samples one from the weighted tree and dispatches it through the driver.
+
+**Built-in generators** (pass directly to `weighted`):
+
+- `taps` - autonomous random taps on clickable elements.
+- `swipes` - autonomous random swipe gestures.
+- `waitOnce` - idles one step.
+- `pressKey` - presses a random supported key.
+
+**Action constructors:**
+
+```ts
+Tap({ on: element })                         // tap an element or selector string
+InputText({ into: element, text: "hello" })  // clear and type into a field
+Swipe({ from: elementOrPoint, to: elementOrPoint, durationMillis?: number })
+PressKey({ key: "back" | "home" | "enter" | "tab" | "up" | "down" | "left" | "right" })
+Wait({ durationMillis: number })
+```
+
+**Samplers** - cycle over a fixed list:
+
+```ts
+const names = from(["Checking", "Savings", "Travel"]);
+names.generate()  // picks from the list
+```
+
+**Custom generators:**
+
+```ts
+const doLogin = actions(() => {
+  if (loggedIn.current) return [];
+  const emailField = loginEmail.current;
+  const submit = loginSubmit.current;
+  if (!emailField || !submit) return [];
+  return [InputText({ into: emailField, text: "test@example.com" }), Tap({ on: submit })];
+});
+```
+
+**Weighted trees:**
+
+```ts
+export const actionsRoot = weighted(
+  [100, dismissOnboarding],
+  [50,  doLogin],
+  [10,  taps],
+  [2,   swipes],
+  [1, weighted(
+    [3, openDeepLink("app://home")],
+    [1, openDeepLink("app://settings")],
+  )],
+);
+```
+
+Weights are relative within each tree. Nested trees get their own local budget.
+
+## Default properties
+
+`@sanderling/spec/defaults/properties` exports ready-made properties:
+
+```ts
+import { noUncaughtExceptions, noLogcatErrors } from "@sanderling/spec/defaults/properties";
+
+export const properties = {
+  noUncaughtExceptions,  // fails if the app throws an uncaught exception
+  noLogcatErrors,        // fails if logcat emits any error-level lines
+};
+```
+
+## Pattern: preconditions
+
+sanderling has no setup phase. Preconditions are action generators with high weight that self-disable once the condition is satisfied.
 
 ```ts
 const onLoginScreen = extract((s) => !!s.ax.find("id:login-form"));
+const loginEmailField = extract((s) => s.ax.find("id:email-field"));
+const loginSubmit = extract((s) => s.ax.find("id:sign-in-button"));
 
 const doLogin = actions(() => {
   if (!onLoginScreen.current) return [];
-  const emailField = state.ax.find("id:email-field");
-  const signInButton = state.ax.find("id:sign-in-button");
-  if (!emailField || !signInButton) return [];
+  const email = loginEmailField.current;
+  const submit = loginSubmit.current;
+  if (!email || !submit) return [];
   return [
-    InputText({ into: emailField, text: "test@example.com" }),
-    Tap({ on: signInButton }),
+    InputText({ into: email, text: "test@example.com" }),
+    Tap({ on: submit }),
   ];
 });
 ```
 
-Stack these for onboarding, consent dialogs, cold-start flows:
+Stack these for onboarding, consent dialogs, and cold-start flows:
 
 ```ts
-const dismissOnboarding = actions(() => {
-  const skip = state.ax.find("text:Skip");
-  return skip ? [Tap({ on: skip })] : [];
-});
-
-export const actions = weighted(
-  [100, dismissOnboarding],  // clear the path first
-  [50,  doLogin],            // log in when the login screen appears
-  [10,  taps],               // exploration
+export const actionsRoot = weighted(
+  [100, dismissOnboarding],
+  [50,  doLogin],
+  [10,  taps],
   [2,   swipes],
 );
 ```
 
-Lifecycle of a run:
-
-```
-Step 1:   fresh install, onboarding visible
-          eligible: dismissOnboarding (weight 100)
-          picks: Tap "Skip"
-
-Step 2-3: login screen visible
-          eligible: doLogin (weight 50)
-          picks: InputText / Tap to sign in
-
-Step 4+:  home screen, onboarding and login generators return []
-          eligible: taps, swipes
-          picks: autonomous exploration
-```
-
-Session state (tokens, keychain, prefs) persists through the rest of the run. If the app logs the user out mid-run, `doLogin` re-fires automatically. No retry logic, no special-casing.
+Once `onLoginScreen.current` is false, `doLogin` returns `[]` and drops out of the eligible set automatically.
 
 ## Pattern: conditional properties
 
-Use gating extractors the same way inside properties. Express "only check X when Y holds" with `now(...).implies(...)`:
+Gate a property so it only applies when a precondition holds:
 
 ```ts
-const loggedIn = extract((s) => !!s.ax.find("id:home-tab-bar"));
-
 export const properties = {
   cartPersistsWhenLoggedIn: always(
     now(() => loggedIn.current).implies(now(() => cartCount.current !== undefined)),
@@ -113,44 +233,30 @@ export const properties = {
 };
 ```
 
-`implies`, `and`, `or`, and `not` are methods on any formula. Combine them freely.
+## Pattern: step-to-step invariants
 
-## Pattern: eventually
-
-`always` asserts something holds at every step. `eventually` asserts it holds at some step, usually with a time bound:
+Use `next()` to express invariants that span two consecutive steps:
 
 ```ts
-loginSucceedsWithin30s: eventually(() => loggedIn.current).within(30, "seconds"),
-```
-
-`within` takes `"milliseconds"`, `"seconds"`, or `"steps"`. Useful for liveness checks: the loading spinner eventually goes away, the deep link eventually lands on `/home`.
-
-## Pattern: weighted exploration sub-trees
-
-Nest `weighted` to group related actions and tune their collective rate:
-
-```ts
-export const actions = weighted(
-  [100, dismissOnboarding],
-  [50,  doLogin],
-  [10,  taps],
-  [2,   swipes],
-  [1, weighted(
-    [3, openLink("todos://home")],
-    [1, openLink("todos://settings")],
-    [1, openLink("todos://item/42/edit")],
-  )],
+const newAccountBalanceIsZero = always(
+  next(() => {
+    const prev = accounts.previous ?? [];
+    const curr = accounts.current;
+    if (prev.length === 0 || curr.length === 0) return true;
+    const prevIds = new Set(prev.map((a) => a.id));
+    return curr.filter((a) => !prevIds.has(a.id)).every((a) => a.balance === 0);
+  }),
 );
 ```
 
-Weights are relative within a tree, so nested trees get their own local budget. This is how you keep low-frequency but high-value actions (deep links, background/foreground, rotate) from drowning out normal tapping.
-
 ## Anti-patterns
 
-**Positional taps.** `Tap({ on: { x: 100, y: 200 } })` works for a demo but breaks on any layout change. Always prefer an `ax.find("id:...")` reference.
+**Accessing `state` outside of `extract`.** The `state` argument exists only inside the `extract()` callback. Use extractors and `.current` everywhere else.
 
-**Sleep or wait-for-time.** `Wait(3000)` inside an action generator is a smell. If you need to wait for a condition, use an extractor and gate the next action on it.
+**Positional taps.** `Tap({ on: { x: 100, y: 200 } })` breaks on any layout change. Always prefer an `ax.find("id:...")` reference.
 
-**Retry logic inside generators.** Generators should be pure: given the same state they produce the same actions. Retry is the runner's responsibility.
+**Unbounded `eventually`.** Without `.within(...)`, `eventually` never fails within a finite run. Almost always you want a bound.
 
-**Unbounded `eventually`.** Without a `.within(...)`, `eventually` never fails within a finite run. It just stays residual. Almost always you want a bound.
+**`Wait()` inside generators.** Waiting for a condition belongs in an extractor guard, not inside a generator.
+
+**Retry logic inside generators.** Generators must be pure. Given the same state they produce the same actions. Retry is the runner's responsibility.