diff --git a/docs/manual/cli.md b/docs/manual/cli.md
index c5b5bf2..c7980b1 100644
--- a/docs/manual/cli.md
+++ b/docs/manual/cli.md
@@ -16,7 +16,8 @@ Run a spec against an app for a fixed duration.
 |---|---|---|
 | `--spec` | required | Path to the TypeScript spec. |
 | `--bundle-id` | required | Target app bundle ID (Android: applicationId). |
-| `--launcher-activity` | resolved | Optional `<pkg>/<activity>` to launch. Overrides default resolution. |
+| `--device` | optional (android) | Android device serial, as `adb devices` reports it. Required when more than one device is attached. |
+| `--android-app-path` | optional (android) | Path to the APK. Clear-state reinstalls from it instead of running `pm clear`. |
 | `--platform` | `android` | Target platform: `android`, `ios`, or `web`. |
 | `--avd` | optional (android) | Android AVD name to boot if no device is connected. Required only when no device is connected and multiple AVDs exist. |
 | `--ios-device` | optional (ios) | iOS target: a simulator name/UDID to boot, or a connected device's name, UDID, or CoreDevice id. |
@@ -24,6 +25,7 @@ Run a spec against an app for a fixed duration.
 | `--duration` | `5m` | Total test duration (`30s`, `5m`, `2h`, `1d`). |
 | `--max-steps` | `0` | Stop after this many steps (`0` = no cap, the duration governs). A step budget is what makes two generators comparable. |
 | `--exit-on-violation` | `false` | Stop the run at the first property violation and exit `2`. |
+| `--arm` | optional | Experiment label recorded in the run's metadata. Used by the campaign tool to tell one sweep cell from another. |
 | `--seed` | `0` | PRNG seed. `0` uses a random seed and records it in `meta.json`. |
 | `--generator` | `seeded` | Who picks each action: `seeded` (the run's PRNG) or `llm` (a vision model). See [the LLM generator](../spec-language/#llm-generator). |
 | `--output` | `./runs` | Output directory for traces. |
diff --git a/docs/manual/runs.md b/docs/manual/runs.md
index cec7b05..847c0d1 100644
--- a/docs/manual/runs.md
+++ b/docs/manual/runs.md
@@ -13,7 +13,7 @@ A run is not a unit test. The closer picture is: boot a fuzzer for an hour and s
 ```
 sanderling test --spec spec.ts --bundle-id com.example.app --duration 30m
   │
-  ├── launch the app under test (pass --clear-data to wipe app data first)
+  ├── launch the app under test (wipes app data first unless --clear-data=false)
   ├── boot the sidecar (or connect to Chrome on web)
   ├── bundle the spec, load it into the JS runtime
   │
@@ -63,4 +63,6 @@ A run ends when:
 - `--duration` elapses, or
 - the process is interrupted (Ctrl+C).
 
-Additional conditions (`--max-steps`, `--exit-on-violation`, hard crash handling) land in the [v0.1.0 milestone](https://github.com/priyanshujain/sanderling/milestone/1).
+- `--max-steps` is reached, or `--exit-on-violation` was passed and a property was violated.
+
+Hard crash handling lands in the [v0.1.0 milestone](https://github.com/priyanshujain/sanderling/milestone/1).
diff --git a/skills/README.md b/skills/README.md
new file mode 100644
index 0000000..50c7887
--- /dev/null
+++ b/skills/README.md
@@ -0,0 +1,15 @@
+# Skills for writing sanderling specs
+
+Agent skills for adopting sanderling: getting it running against your app, writing
+property specifications, reviewing them for the failure modes that make a spec
+look like it works when it does not, and reading a run honestly.
+
+Copy the ones you want into your agent's skills directory (`.claude/skills/` for
+Claude Code) or point your agent at this directory directly.
+
+Start with `sanderling-setup`, then `sanderling-spec-authoring`. Run
+`sanderling-spec-review` over anything before you trust it.
+
+The reasoning behind the rules these encode is in
+[docs/development/design-principles.md](../docs/development/design-principles.md),
+section 8 in particular.
diff --git a/skills/sanderling-property-patterns/SKILL.md b/skills/sanderling-property-patterns/SKILL.md
new file mode 100644
index 0000000..183170c
--- /dev/null
+++ b/skills/sanderling-property-patterns/SKILL.md
@@ -0,0 +1,420 @@
+---
+name: sanderling-property-patterns
+description: Decide what a sanderling spec should assert. A catalogue of property shapes that are sound (cross-panel agreement, bounds on an effect, counting actions against effects, input and navigation invariants), each with the tempting unsound version beside it. Use when starting a spec, when adding a property to one, or when a property keeps convicting an app that behaved.
+---
+
+# Choosing what to assert
+
+You have sanderling driving your app and now you have to say what must be true.
+This is the hard part, and it fails in two directions: you freeze, or you write
+six properties none of which can ever be false.
+
+One rule orders everything below. **Soundness outranks detection.** A property
+that convicts more often and is sometimes wrong is strictly worse than one that
+convicts less and is never wrong, because a false conviction costs someone a day
+and then costs the whole suite its credibility. When a property cannot establish
+what it needs, it declines.
+
+Each shape below gives the sound form and the tempting form next to it, because
+the tempting one is usually what gets written first. The examples are from the
+two specs in this repo: `replay-ui/sanderling/spec.ts` (sanderling fuzzing its
+own trace browser) and `examples/folio/sanderling/spec.ts` with
+`examples/folio/sanderling/predicates.ts` (a KMP finance app).
+
+Once you have written properties, run `sanderling-spec-review` over them. It
+audits what this file helps you build.
+
+## 1. Two parts of the UI derive the same fact and must agree
+
+Reach for this first, always. If your app shows the same number in two places,
+or shows a thing and a count of that thing, or renders a list and a selection
+into that list, you have a property and you do not have to think about windows,
+calibration, or attribution to write it.
+
+It is the strongest shape available. It holds on any run against any data, so
+nothing needs recalibrating when a fixture changes; it needs no reasoning about
+which action caused what; and an app that drifted on one of the two paths cannot
+satisfy it. It is the backbone of `replay-ui/sanderling/spec.ts`, which states it
+three times over: the toolbar's step count against the number of rows the list
+renders, the toolbar's step against the step the screenshot panel built its URL
+from, and the tab badge's violation count against the number of rows the
+violations panel shows.
+
+```ts
+const stepCountMatchesTheList = always(() => {
+  const current = toolbar.current;
+  const rows = stepRows.current;
+  if (!current || current.stepCount === null || rows.length === 0) return true;
+  return current.stepCount === rows.length;
+});
+```
+
+**What goes wrong: reading the second value off the wrong element.** Scope each
+reading to the panel you mean, by name, not by position in the tree.
+
+```ts
+// tempting: the first screenshot on the page
+s.ax.find({ "data-testid": "screenshot" })
+// sound: the before panel's screenshot
+s.ax.find([{ "data-testid": "state-before" }, { "data-testid": "screenshot" }])
+```
+
+Both versions pass most of the time. The fuzzer put the before panel on another
+tab, which left the after panel's image first on the page, and the first version
+fired against a UI that was behaving correctly.
+
+**What else goes wrong: never getting both readings onto one step.** This
+shape's failure mode is vacuity, not false conviction, which makes it quiet. An
+undirected run over replay-ui went 40 steps without switching a single tab out
+of roughly 15 clickable elements, leaving both tab-facing properties vacuously
+true. The fix is in the action tree, not the property: give the action that
+brings the second reading into view its own weight.
+
+```ts
+const switchATab = actions(() => {
+  const tabs = tabElements.current;
+  return tabs.length === 0 ? [] : [Tap({ on: from(tabs).generate() })];
+});
+
+export const actionsRoot = weighted(
+  [25, switchATab],
+  [20, showAViolatingStepWithItsPanel],
+  [25, defaultActions],
+);
+```
+
+Weighting one half is usually not enough, and this is the part that surprises
+people. `badgeCountMatchesThePanel` needs a badge, which a tab strip renders
+only for a step that has a violation, and a panel to compare it against, which
+exists only while a particular tab is selected. Undirected actions put both on
+the same step 0 times in the 80 steps of replay-ui's first dogfood run. Aiming
+at the violating step alone just moved the misses to the other side: still 0
+judged. `showAViolatingStepWithItsPanel` in that spec aims at both halves in
+sequence, selecting a violating row and then opening a panel if none is up.
+
+It also opens the *after* panel deliberately, because the before panel's
+screenshot is what `screenshotShowsTheSelectedStep` reads, and covering it up
+would buy one property's evidence with another's. When two properties read the
+same screen, an action tree can starve one to feed the other, and nothing in the
+run output will say so.
+
+## 2. An effect must not exceed what the actions could have caused
+
+When the app has an effect you can measure (money moved, rows added, a counter
+climbed), state a bound on it rather than a prediction of it.
+
+**Prefer an upper bound to an equality.** This is the single most valuable
+sentence in this file.
+
+`examples/folio/sanderling/predicates.ts` states one rule about one app both
+ways, so the two are worth reading side by side. Each line is the last line of
+its predicate, after the guards, at a step where exactly one submit sits in the
+window:
+
+```ts
+// sound, committedAmountExceedsOneSubmit: the violation is moving by MORE
+// than the one submit in this window could account for
+Math.abs(currAccountBalance - prevAccountBalance) > typedAmount
+// tempting, submitChangesBalanceByTypedAmount: it moved by exactly what I typed
+Math.abs(currTotalBalance - prevTotalBalance) === typedAmount
+```
+
+Both catch the bug, because a double submit moves the balance by twice the typed
+amount. Only the second also convicts an app that behaved. A balance that has
+not moved is a commit still in flight (folio's `createTransaction` runs in a
+coroutine), a submit the app rejected, or a tap that never landed, and none of
+those is evidence of anything.
+
+The asymmetry is the point. Moving by more than one submit's worth is not
+something a correct app can do, so the bound needs no case for any of the three.
+The equality needs a case for each, and every one you forget is a false
+conviction. Compare the two guard stacks and the price is exactly legible: the
+equality declines on `confirmedApplied` and on `acrossRelaunch`, and the bound
+carries neither, because a submit that may not have landed and a restart that
+may have eaten the commit both leave the balance under the bound anyway. Those
+are the two facts the runner cannot promise (see below), and needing to guard
+against both is a cost of the equality, not of the app.
+
+You do give something up, so make the trade deliberately. A bound cannot see a
+balance that moved by *less* than the typed amount, and for a ledger that is a
+real bug. The question to settle before giving it up is whether your readings are
+tight enough to tell "moved by less" from "has not finished moving yet". If they
+are not, the equality was never detecting that bug either; it was reporting it at
+random.
+
+The bound has one precondition, and it is the same one as shape 3: it bounds the
+effect by what the actions in the window could have caused, so the window has to
+count every action that could cause the effect. Miss one and the bound is not a
+bound.
+
+## 3. Count the actions, not the amounts
+
+The same bound, stated in counts. One action must not produce two effects.
+
+```ts
+!committedTransactionsExceedSubmits({
+  countsBefore: homeTxnCounts.previous ?? null,
+  countsAfter: homeTxnCounts.current,
+  submitsInWindow: submitsSinceCounts.current,
+})
+```
+
+Reach for this whenever the effect is countable. No arithmetic on values the UI
+formatted and you parsed back, no float precision to reason about, and it stays
+sound however wide the window between two readings gets, since both sides
+accumulate over the same window.
+
+It has exactly two failure modes and both are about the window. Neither makes it
+unsound. Both make it useless, quietly.
+
+**The window has to close often enough to attribute anything.** The window opens
+when you last read the fact and closes when you read it again, so a run that
+wanders away from that screen accumulates budget on one side of the bound
+without accumulating evidence on the other. Measured on a real iOS run: it went
+from step 19 to step 136 without returning to the screen the property reads,
+giving a transaction rise of 15 against a window of 37 submits. 15 is not more
+than 37, so nothing was reported. The same run also gave 4 against 7, 6 against
+13, and 1 against 1. Sound throughout, detected nothing.
+
+The obvious fix is to read the fact somewhere the run visits often. The better
+one, when the wide window is the app's own shape rather than an accident, is to
+**state the same rule a second time over a narrower window**, which is what
+folio's spec now does:
+
+```ts
+const submitCommitsOneTransactionPerAction = always(
+  next(
+    () =>
+      !committedTransactionsExceedSubmits({ /* Home's counts, wide window */ }) &&
+      !committedAmountExceedsOneSubmit({ /* this account's balance, narrow window */ }),
+  ),
+);
+```
+
+The counting form can only close its window on a Home reading, and a walk that
+stays inside the transaction flow leaves it hundreds of steps and dozens of
+submits wide. The second conjunct says the same thing in money about the one
+account whose screen the walk is already on, and the transaction flow redraws
+that balance on nearly every frame, so its window is usually a single action
+wide, narrow enough to tell one commit from two. One rule, two windows, and the
+narrow one is where the detection actually comes from.
+
+That only works because the two readings are kept from spanning two accounts:
+`readAccountBalance` drops its carrier on every route that is not the ledger or
+the transaction screen, transition frames included. A narrow window buys nothing
+if the pair it compares straddles two different subjects.
+
+**The window must not be spent on actions that provably could not cause the
+effect.** A bound inflated by taps that commit nothing is a bound the app can
+never exceed, which is slack a real double submit hides behind. Folio's
+transaction submit is `clickable(enabled = amount.isNotBlank())`, so a tap with
+an empty field never fires at all, and the app's own `parseCents` refuses
+anything outside `^\d+(\.\d{1,2})?$` or parsing to zero. Measured over four
+recorded Android runs, 19, 11, 25 and 25 of 35, 26, 42 and 42 submit taps landed
+with the amount field empty, which is roughly half the budget in every one.
+
+`submitCouldCommit` in `predicates.ts` is that rule, and note how narrowly it is
+drawn. It returns false only where folio's own code **must** have refused, and
+returns true for anything it cannot rule out, including an undefined reading and
+an amount too large for the app to hold. Over-counting costs a detection;
+under-counting convicts a healthy app.
+
+Establishing that an action could not have had an effect is app knowledge, not
+something the runner can tell you, and it has to come from the frame the tap
+read. Folio reads the amount field on the landing frame, which is sound because
+the tap changes nothing about it and one action runs per step.
+`element.enabled` is on every `AccessibilityElement` for the general case,
+though whether your platform populates it honestly is worth checking on a real
+tree rather than assuming.
+
+The mirror of this rule matters just as much: an action whose effect you cannot
+rule out **must** be counted. Leaving out submits whose dispatch the runner
+could not confirm is what once convicted a healthy app here, when the property
+saw a transaction rise of one against a window of zero.
+
+## 4. A value the user can reach must stay inside its legal range
+
+Anything the user can type, or a URL can carry, or a deep link can set, is
+attacker-controlled input to your app even when the attacker is a fuzzer. The
+property is that it stays legal, and it is cheap: one reading, no window, no
+attribution.
+
+```ts
+const selectedStepIsInRange = always(() => {
+  const current = toolbar.current;
+  if (!current || current.step === null || current.stepCount === null) return true;
+  return current.step >= 1 && current.step <= current.stepCount;
+});
+```
+
+Two things make that sound. The bound comes from the app's own reading of how
+many steps the run has, not from a number you typed after looking at a fixture.
+And it asserts legality rather than a prediction:
+
+```ts
+// tempting: I tapped next, so it must now be on step n + 1
+toolbar.current.step === (toolbar.previous?.step ?? 0) + 1
+```
+
+which is false at the end of the run, false when the tap did not land, and false
+whenever the app is within its rights to clamp. Assert what must not happen.
+
+## 5. State machine and navigation invariants
+
+Every screen with a selection, a mode, or a route has invariants that are true
+by construction and therefore worth stating, because "by construction" is
+exactly what breaks.
+
+**Exactly one, not at least one.** The looser version is the tempting one and it
+gives up the interesting half of the bug.
+
+```ts
+const exactlyOneStepIsSelected = always(() => {
+  const rows = stepRows.current;
+  if (rows.length === 0) return true;
+  return rows.filter((row) => row.active).length === 1;
+});
+```
+
+Two selected rows is a stuck selection. Zero is the toolbar showing a step the
+list has no row for, which is what an off-by-one or a failed clamp looks like
+from the list's side, and `>= 1` would never see it.
+
+**A view change must not be a navigation.** Switching a tab, opening a menu or
+toggling a theme must leave the app where it was.
+
+```ts
+const switchingTabsKeepsTheStep = always(
+  next(() => {
+    const previousTabs = activeTabs.previous;
+    const previousToolbar = toolbar.previous;
+    const currentToolbar = toolbar.current;
+    if (previousTabs === undefined || previousTabs === activeTabs.current) return true;
+    if (!previousToolbar || !currentToolbar) return true;
+    return previousToolbar.step === currentToolbar.step;
+  }),
+);
+```
+
+Note the guard: it declines unless the tab strip actually changed. A property
+about an event must first establish that the event happened.
+
+The tempting unsound version of a navigation property is asserting the route you
+were hoping for, `route.current === "home"` after tapping submit. The app is
+within its rights to show a validation error and stay, and folio does exactly
+that for an amount of zero. State what must not happen, not what you wanted to.
+
+Deriving the route at all deserves care, and folio's `routeOfFrame` is the
+pattern: it returns the screen only when exactly one screen marker is in the
+tree, and null otherwise. Android's hierarchy dump carries the outgoing and the
+incoming screen together on 425 of 1879 steps measured across 17 runs, better
+than one frame in five. Such a frame is evidence about neither screen, and
+ranking the markers to pick one is how a spec convicts itself on an animation.
+
+## 6. The ones you get for free
+
+```ts
+import { noUncaughtExceptions, noLogcatErrors } from "@sanderling/spec/defaults";
+
+export const properties = { noUncaughtExceptions, /* yours */ };
+```
+
+Export `noUncaughtExceptions` before you write anything of your own. It costs a
+line, it needs no app knowledge, and a fuzzer typing `'; DROP TABLE--` and a
+4096-character string into every field it finds will surface real breakage
+through it. `noLogcatErrors` is stricter and Android-only; it holds trivially
+elsewhere, so it is worth turning on once you know your app's log hygiene can
+support it.
+
+They do not substitute for the shapes above. An app can be thoroughly wrong
+about money without throwing once.
+
+## The rules that cut across all of them
+
+**Absence is unknown, never a default.** Extractors return null when the element
+is not there, and a property handed null declines. `0`, `""` and `[]` are the
+values that turn a property into one that fires on healthy runs: folio's
+balances once parsed as `0` on web, so the check became `|0 - 0| === typed` and
+was false at every healthy submit. An empty list has the same problem in the
+other direction, and it is worse because it looks reasonable. Android renders
+Home's own node a frame or two before its list, so `findAll` over the cards
+comes back empty while the screen already claims to be Home. That is unknown,
+not "no accounts", and reading it as zero accounts killed folio's counting
+invariant outright: `countsBefore` was `{}` at every evaluation point of all 17
+runs measured.
+
+**Attribution needs injective keys.** If two distinct objects can produce the
+same identity key, a value silently jumps between unrelated series. Merged UI
+text is the usual culprit: web collapses an account card into a single node
+whose text runs the name into the count, so an account named `Travel1` with 25
+transactions and one named `Travel12` with 5 both render `TRTravel125
+transactions`. No function of that string can separate them. Where a key can
+collide, drop the reading rather than guess: `homeTxnCountsOf` leaves out any
+name carried by more than one card, because subtracting two different accounts'
+counts convicts a healthy app of double-submitting.
+
+**Match whole keys, not endings.** `endsWith` attribution judges an older
+account named `Emergency Fund` when the user typed `Fund`: have the new card
+clipped out of the reading, the way a list clips any card, and the old account
+is convicted for money it has held all along. Substring matching is looser
+still. Build every form of the key the platforms can produce and compare each
+one whole, which is what `createdAccountHasNonZeroBalance` does with
+`account.name === typed || account.name === initialsOf(typed) + typed`. Note
+that this bought detections as well as soundness: under the suffix test, a name
+that two cards ended with was thrown away as unattributable rather than matched
+to the one card that actually carried it.
+
+**What the runner could not promise.** `state.lastAction` is
+`Action & { applied: true | null; relaunched: true | null }`, and collapsing any
+of its states is unsound:
+
+- `null`, the whole field, means no action ran
+- `applied: true` means the runner saw the dispatch succeed
+- `applied: null` means it was dispatched and nobody can find out whether it
+  landed, because an RPC deadline can fire after the tap arrived
+- `relaunched: true` means the runner had to bring the app back to the
+  foreground after this action, so the two readings straddle a restart
+
+One rule covers the last two, and it is the rule that decides shape 2 for you.
+An action the runner cannot fully vouch for **still counts toward a bound on
+what the app could have done**, and it **never licenses attributing an effect to
+it**. So a bound counts it and an equality has to decline on it. That is why
+`committedAmountExceedsOneSubmit` needs no `confirmedApplied` guard and no
+`acrossRelaunch` guard while `submitChangesBalanceByTypedAmount` needs both: a
+property demanding the effect of an action that may never have run, or that a
+restart may have swallowed, convicts the app of the runner's own uncertainty.
+
+`relaunched` is the same shape of fact as `applied`, applied to app state rather
+than to dispatch. The action itself did happen. What nobody can promise across
+it is that the process ran continuously, that the commit survived, or that the
+screen is showing the same slice of the same list it was. So a property assuming
+continuous state declines, via `acrossRelaunch(lastAction)`, and folio uses it
+in three places: `createdAccountHasNonZeroBalance` declines because Home redraws
+from the top and the card carrying the typed name may be an older account laid
+out where the new one used to be, the equality property declines because it
+demands an effect, and `countSubmitsInWindow` uses it to **stop trusting its own
+refusal evidence**, since a relaunch is the one thing that can put a form state
+on screen other than the one the tap read.
+
+Both fields are `true | null` rather than booleans, and that is deliberate: only
+the positive report is a fact the runner can vouch for, so `null` is "not
+reported" rather than "did not happen". `relaunched` shows why it has to be that
+way. Web and iOS cannot read the foreground at all, so they never relaunch the
+app and equally cannot promise it never restarted, and a `false` there would be
+a claim nobody is in a position to make. Read the absence as a guarantee and you
+have made the same mistake as reading a missing value as zero, one level up.
+
+**Testing a property means both directions, every time.**
+
+- it fires on the bug it exists to catch
+- it stays silent on a run where the app behaved
+
+The second is the one people skip and the one that catches unsoundness. Build
+the fixture where the effect happens legitimately, at the boundary the property
+draws, and assert silence: the commit that is still settling, the submit the app
+refused, the card that scrolled into view rather than being created, the pair of
+readings taken either side of a relaunch. A property you have only ever seen go
+red is a property you have half tested.
+
+Then hand it to `sanderling-spec-review`, which will ask how many steps it
+actually judged on a real run.
diff --git a/skills/sanderling-run-triage/SKILL.md b/skills/sanderling-run-triage/SKILL.md
new file mode 100644
index 0000000..98240b7
--- /dev/null
+++ b/skills/sanderling-run-triage/SKILL.md
@@ -0,0 +1,210 @@
+---
+name: sanderling-run-triage
+description: Work out what a finished sanderling run actually proves. Use before trusting a green run, before filing the bug a red run seems to show, and any time the exit code is the only thing anyone has looked at.
+---
+
+# Reading a run honestly
+
+A run produces one number that is easy to read and several that are worth
+reading. The easy one says whether a process finished. It does not say whether
+anything was checked, whether what was checked was your app, or whether the
+violation it reports is about the app at all.
+
+Work through the sections in order and report what you established and what you
+could not. "This run is not evidence, and here is the signal that says so" is a
+complete and useful answer.
+
+## 1. The exit codes
+
+- **0** means the run completed. It does **not** mean no violations. Without
+  `--exit-on-violation` a run that recorded violations still exits 0: measured
+  on a ten step web run that recorded two, `run complete: 10 steps` and
+  `2 violation record(s)`, exit code 0.
+- **2** means the run recorded a violation under `--exit-on-violation` and
+  stopped there. The same ten step run with the flag exits 2 after four steps.
+- **1** means the harness broke. A bad target gives
+  `error: launch app: page load error net::ERR_UNSAFE_PORT` and exit 1, and
+  writes no run directory at all, because the trace is created after the launch
+  succeeds.
+
+Anything other than 0 and 2 means the run did not complete, and a missing
+`trace.jsonl` under a 0 or a 2 means there is nothing to judge rather than
+nothing to report.
+
+Exit 2 is not a conviction. `.github/scripts/folio-run.sh` is the worked example
+worth reading in full: it exists because a thrown predicate reaches exit 2 by the
+identical path a real conviction does, and so does a violation of a real but
+unrelated property in the same spec. It sorts a trace's violations three ways,
+by name and by `is_error`: convictions of the properties the leg gates on,
+predicates that threw, and other real violations the leg has nothing to say
+about. Do the same sort by hand before you call a 2 a finding.
+
+## 2. Reading a witness
+
+Witnesses live in `trace.jsonl`, one object per step under `witnesses`, keyed by
+property name. A real conviction and a real throw from the same run:
+
+```json
+{"step": 4, "violations": ["countStaysUnderThree"],
+ "witnesses": {"countStaysUnderThree": {
+   "reason": "predicate false", "step": 4, "detected_step": 4,
+   "extractors": {"count": 3}}}}
+
+{"step": 5, "violations": ["throwsOnceCountIsFour"],
+ "witnesses": {"throwsOnceCountIsFour": {
+   "reason": "Error: boom: no reading for this screen at <eval>:501:37(14)",
+   "is_error": true, "step": 5, "detected_step": 5,
+   "extractors": {"count": 4}}}}
+```
+
+`step` is where the failed obligation was armed and `detected_step` is where the
+evaluation produced the violation; for a deferred obligation (a `next`, an
+`eventually`) they differ, and `extractors` is `detected_step`'s state, not
+`step`'s.
+
+The discipline is one sentence: open the witness and confirm those values could
+actually produce that verdict. An iOS witness read `typedAmount = 0`, and
+`submitChangesBalanceByTypedAmount` in `examples/folio/sanderling/predicates.ts`
+returns true at `typedAmount === 0` before it compares anything. So the trace
+appeared to show a conviction that could not have happened. The verdict was real
+and the artifact was lying, and until that was resolved neither the bug report
+nor the fix could be trusted.
+
+When a witness value looks impossible, suspect the reading before you suspect
+the property. Values reach a witness through the driver, and the driver can be
+wrong in ways the spec cannot see: erasing a text field used to leave characters
+behind, because a backspace only deletes to the left of the cursor and the
+runner taps the field's centre, and 7 of 19 measured `InputText` observations
+left residue that the spec then reasoned about as if it were the typed value.
+
+Two more things the witness tells you, if the spec extracts them. folio declares
+`extract("lastAction", s => s.lastAction)` precisely so they land in the trace:
+`applied: true` means the runner saw the dispatch succeed, `applied: null` means
+it was dispatched and nobody knows whether it landed, and `relaunched: true`
+means the app restarted between the two readings. A property attributing an
+effect to an action of unknown fate is unsound; see `sanderling-spec-review`.
+
+Finally, a property violates once. After it fires, its residual stays `false`
+(or `{"op": "error", ...}`) for every remaining step and it is never evaluated
+again. Measured across steps 4 to 10 of that run, `countStaysUnderThree` reads
+`{"op": "false"}` at every step after the first. So the violation count is a
+count of distinct properties, not of occurrences, and everything after a
+property's first violation is unchecked by that property.
+
+## 3. A green run fails in two ways
+
+Either it checked nothing, or it checked and the fuzzer never reached the bug.
+These need opposite responses (fix the spec or the hooks; spend more budget or
+better actions) and the exit code distinguishes neither.
+
+The first is not a hypothetical. Against an empty page, six steps, exit 0, `no
+violations`, and `countNeverNegative` judged **0 of 6**: its extractor returned
+null every step, its guard short-circuited, and its residual read `{"op":
+"true"}` at every step, exactly as it reads when it compares real values.
+
+So count, per property, the steps where its guard passed and it compared
+something (**judged**) against the steps where it returned true without
+comparing anything (**declined**). `.github/scripts/replay-ui-summary.sh` does
+this for the replay-ui spec and prints a judged/declined table for exactly this
+reason. To do it by hand from a trace:
+
+- fold `extractor_changes` forward per step. Only extractors whose value changed
+  are recorded, so a step with no entry for an extractor means unchanged, not
+  absent. Measured: `{"count": {"prev": 0, "curr": 2}}` at one step and no
+  `count` entry at the next.
+- skip steps carrying `skipped_verification` or `transitional`. They advance
+  nothing.
+- apply each property's own guard to the folded values and count.
+
+That script also carries the honest warning about this technique: restating a
+property's guard outside the property is a second copy that can drift, so it
+checks that the trace's property names still match the ones it counts and that
+the spec still declares the extractors it reads, and it fails loudly when either
+moves.
+
+Do not try to read judged-versus-declined off `residuals`. `always(p)` residuals
+to `{"op": "true"}` whether `p` compared real values or short-circuited, so the
+two are indistinguishable there.
+
+## 4. A red run fails in two ways
+
+Either a property was proved false about the app, or a predicate threw.
+`is_error` in the witness separates them and they mean opposite things.
+
+A conviction is a claim about the app. A throw is a claim about the spec, and it
+is worse than an unhelpful result: the property is violated from that step on
+whatever the app does, so it checks nothing for the rest of the run, and under
+`--exit-on-violation` the run ended there so nothing past it was checked by
+anything. The `reason` carries the JavaScript error and its location, which is
+usually enough to find it: `Error: boom: no reading for this screen at
+<eval>:501:37(14)`.
+
+The third case is a real violation of a property that is not the one you are
+asking about. It is a finding, and it is somebody's bug, but the run has nothing
+to say about the question you asked it. Name the property before you claim the
+result.
+
+## 5. When a run is not evidence at all
+
+Some runs never got far enough for any of the above to matter, and every one of
+them exits 0 and reports no violations.
+
+**It never reached the app.** A launch flake left a fuzzer on the device
+launcher for 200 steps in 65 seconds, two nodes per snapshot, exit 0, no
+violations (issue #81). The check is that the app's own marker appears in the
+trace at all: the folio CI leg greps for `"AddTransactionScreen"` and fails the
+run when it is absent, which is more honest than any exit code it could read.
+The run's stdout also carries `app left foreground; relaunching` with the
+package it found instead.
+
+**The hierarchy is a handful of nodes.** `nodes=` in each step line is the
+cheapest signal there is. Measured: 6 on a four-element page, 2 on an empty one.
+A run whose `nodes` never leaves single digits is looking at a launcher, a
+crash screen, or a page that failed to boot.
+
+**It never left one screen.** `screen=` constant for the whole trace, or a
+`route` extractor that never changes value.
+
+**Steps far faster than the run's own median.** Take the per-step deltas from
+each step's `timestamp` and compare them against the run's median. A stretch of
+steps at a fraction of it is a driver that is not waiting for an app, because
+there is no app to wait for: 200 steps in 65 seconds is 325 ms a step, against
+seconds a step for a run that is driving something real.
+
+**It spent its budget on one action.** Count `next_action` by kind and selector.
+A run whose actions are one selector explored nothing, whatever its step count.
+
+None of these change the exit code. All of them change what the run proves,
+which is nothing.
+
+## 6. `skipped_verification`, `transitional`, and the judged count
+
+The runner skips the verifier for a step whose hierarchy was still moving: an
+Android NavHost mid cross-fade after the retry budget, or a hierarchy fetch that
+failed or came back empty. Pushing such a tree would poison the previous/current
+extractor advance and make the next clean step convict a healthy app, so the
+step is recorded for replay and judged by nothing. `transitional` marks the
+tree; `skipped_verification` is set exactly when the verifier was skipped.
+
+The run says so itself:
+
+```
+7 step(s) judged by nothing: the screen was still moving when it was read
+```
+
+Subtract it. `run complete: 240 steps` with that line is a 233 step run for
+every purpose that matters, and `replay-ui-summary.sh` reports the pair as
+"N steps recorded, M verified" for the same reason. A run with many of these is
+telling you the driver could not get a clean read of your app, which is a
+finding about the setup and worth chasing rather than quietly accepting the
+smaller number.
+
+## Reporting
+
+For any run, report: the exit code and whether `--exit-on-violation` was set;
+steps recorded against steps verified; per property, judged against declined;
+for every violation, its `is_error` and the witness values you actually opened;
+and which of the section 5 signals you checked. Name the step behind any claim.
+
+A run is evidence only for the properties that judged, and only for the app it
+was actually looking at. Everything else it produced is a log.
diff --git a/skills/sanderling-setup/SKILL.md b/skills/sanderling-setup/SKILL.md
new file mode 100644
index 0000000..f6f45f8
--- /dev/null
+++ b/skills/sanderling-setup/SKILL.md
@@ -0,0 +1,260 @@
+---
+name: sanderling-setup
+description: Get sanderling running against an app that is not folio. Use before writing a spec for a new app, when deciding what test hooks the app needs, and when a run will not start or starts and sees nothing.
+---
+
+# Getting sanderling onto your app
+
+The goal of setup is not a run that finishes. It is a run whose output you can
+believe. Two things decide that, and both are usually treated as chores: the
+handles the app exposes, and the state the app starts in. Everything else here
+is plumbing.
+
+Every flag below is one the binary accepts. `sanderling test -h` is the
+authority, not this file and not the manual: the manual currently documents
+`--launcher-activity`, which the binary answers with `flag provided but not
+defined`. Check before you use a flag you have not seen work.
+
+## 1. Install, then check the host
+
+The CLI installs from the release script, and the spec package from npm:
+
+```sh
+curl -fsSL https://raw.githubusercontent.com/priyanshujain/sanderling/master/install.sh | bash
+npm install --save-dev @sanderling/spec
+```
+
+Both come from the same release tag and the CLI bundles the package's TypeScript
+when it evaluates your spec, so they move together.
+
+`sanderling doctor` reports the host's readiness per platform and exits non-zero
+if anything is missing. On a Mac with no Android SDK it says:
+
+```
+OK    adb on PATH
+FAIL  emulator on PATH or under ANDROID_HOME: not on PATH and ANDROID_HOME is unset
+OK    java 17+ on PATH
+FAIL  sidecar JAR is real (not placeholder): placeholder JAR embedded; run `make sidecar && make sanderling` to embed the real fat JAR
+error: 2 check(s) failed
+```
+
+Scope it with `--platform web|android|ios|ios-device|all` (default `all`). Web
+needs a Chromium that launches headless. Android needs `adb`, an emulator on
+PATH or under `ANDROID_HOME`, Java 17 or newer, and the embedded sidecar JAR.
+iOS needs `xcrun` and `simctl`; `ios-device` adds `devicectl`, the macOS usbmuxd
+socket, a connected paired device, and App Store Connect signing credentials.
+
+Read the doctor's Android result as advisory rather than final: its emulator
+check today looks only at PATH, `ANDROID_HOME` and `ANDROID_SDK_ROOT`, while a
+run also searches `~/Library/Android/sdk`, `~/Android/Sdk` and the Homebrew
+command-line-tools paths. The run's own error names every location it tried, so
+that is the one to trust. In the other direction, a missing SDK can surface
+during a run as `sidecar health check: context deadline exceeded` about thirty
+seconds in, which names the symptom and not the cause (issue #69). If you see
+it, go back to `sanderling doctor --platform android` before believing anything
+about the sidecar.
+
+Two traps if you build from source rather than installing a release. A plain
+`go build ./cmd/sanderling` embeds a placeholder sidecar JAR, so every Android
+run stops at `sidecar: binary built without -tags withsidecar`; `make sanderling`
+(or `make sanderling-android`) embeds the real one. And `go run ./cmd/sanderling
+test` collapses the process exit code: a run that exits 2 comes back from
+`go run` as 1 with `exit status 2` printed. Use the built binary whenever the
+exit code matters, which is always in CI.
+
+## 2. Point it at the app
+
+Android takes the applicationId, boots an AVD with `--avd`, and picks between
+attached devices with `--device <serial>` as `adb devices` prints it:
+
+```sh
+sanderling test --spec spec.ts --bundle-id com.example.app --avd Pixel_7_API_34
+```
+
+iOS takes `--platform ios` and `--ios-device`, which accepts a simulator name or
+UDID, or a connected device's name, UDID, or CoreDevice id. `--ios-app-path`
+points at the `.app` bundle and is what makes clear-state real; see section 4.
+
+Web takes a URL as the bundle id:
+
+```sh
+sanderling test --spec spec.ts --platform web --bundle-id http://127.0.0.1:8799/index.html
+```
+
+The web target has to genuinely load. A page that boots to a blank canvas still
+produces steps, still exits 0, and proves nothing: folio's own web leg needs
+COOP/COEP headers or its sqlite worker never starts, which is why
+`.github/scripts/folio-run.sh` serves the build itself instead of using a stock
+static server. Confirm the app rendered before you read anything else.
+
+## 3. Test hooks are a prerequisite, not a polish step
+
+This is the part that decides whether a spec is possible at all. The header of
+`replay-ui/sanderling/spec.ts` states it as the lesson it is:
+
+> The hooks it drives (data-testid, data-step, ...) were added to the UI for
+> this spec. Needing them is the lesson: a UI with no stable handles is a UI
+> nothing can assert on, and that is as true for a person writing a test as it
+> is for a fuzzer.
+
+A fuzzer is not asking for anything a human test author does not need. It is
+only less able to squint at a screenshot and guess. Budget the hooks as part of
+adopting sanderling, before the spec, not after the first vacuous run.
+
+`testTag` is the portable name. `internal/hierarchy/hierarchy.go` aliases it to
+`resource-id`, `identifier` and `accessibilityIdentifier`, so one selector
+matches on every platform. What you have to add differs:
+
+**Compose on Android.** `Modifier.testTag("AddAccountSubmit")` alone does not
+reach the accessibility tree. The tree only carries it when a root composable
+sets `semantics { testTagsAsResourceId = true }`. folio does this once, at the
+app root, through an expect/actual bridge:
+`examples/folio/app/shared/src/androidMain/kotlin/app/folio/ui/TestTagBridge.android.kt`.
+Without it every `testTag` selector matches nothing, every property over it
+declines, and the run goes green having checked nothing.
+
+**Web.** `data-testid` is the hook. Every `data-*` attribute on the element
+reaches the spec under `attrs`, camel-cased the way `dataset` does it, so
+`data-step-count` reads as `attrs.stepCount`. That is how the replay-ui spec
+reads a panel's own claim about which step it is showing rather than re-deriving
+it. Hooks that carry a value, not just an identity, are what make cross-panel
+agreement properties possible.
+
+**iOS.** `accessibilityIdentifier`, set via `.accessibilityIdentifier` in
+SwiftUI or UIKit. Compose Multiplatform maps `testTag` to it for you.
+
+Two rules about the names themselves. A `testTag` selector falls through to a
+substring compare, so `{testTag: "Sub"}` matches `AddAccountSubmit`: make each
+hook a whole distinct name rather than a fragment of another. And give every
+screen a marker of its own, because a route extractor is what lets a property
+decline on the screens it has nothing to say about.
+
+The check that a hook exists is not that you added it. It is that you can point
+at a step in a real trace where a selector over it resolved to a value.
+`sanderling-spec-authoring` covers which hooks a spec needs and in what order to
+add them; this section is about what each platform requires before any of that
+reaches the tree.
+
+## 4. A run must start from a known state
+
+`--clear-data` defaults to true and is the difference between a repeatable run
+and a measurement of your own leftovers. A second run that inherits the first
+one's accounts, cache and completed onboarding diverges at step 1: the seed
+reproduces nothing, the two runs' step counts are not comparable, and any number
+you quote from the pair is noise.
+
+What "clear" reaches depends on the platform, and in two cases it silently
+reaches less than you expect:
+
+- Android wipes app data through the sidecar. On OEM builds that deny
+  `pm clear`, pass `--android-app-path <apk>` and it uninstalls and reinstalls
+  instead.
+- iOS simulator without `--ios-app-path` resets the data container only and
+  prints `clear-state requested without an app path: resetting the data
+  container only`. With the path it does a full `simctl` uninstall and install.
+  The container wipe is a real reset and folio's own iOS leg relies on it; the
+  reinstall path is the one that races FrontBoard.
+- iOS on a physical device without `--ios-app-path` does not clear at all. It
+  prints `clear-state on a physical device requires --ios-app-path for a
+  reinstall; skipping (state not cleared)` and carries on. A device run left on
+  the default flag inherits every previous run's data.
+- Web clears cookies and the target origin's storage. It cannot touch your
+  backend. If your app's state lives on a server, reset it yourself between
+  runs.
+
+`--clear-data=false` is a legitimate choice in one situation: you have just
+installed a fresh build, so the app is already in clear state and an in-run
+reinstall would only add a failure mode. Outside that, a run that resumes is a
+run you cannot repeat.
+
+## 5. The device does not have to be local
+
+Android talks to whatever adb server the environment names.
+`ADB_SERVER_SOCKET=tcp:host:port` (or `tcp:port` for a server on this machine)
+is read first, then the older `ANDROID_ADB_SERVER_ADDRESS` and
+`ANDROID_ADB_SERVER_PORT` pair, then the loopback default. The CLI shells out to
+`adb` and inherits it; the JVM sidecar resolves the same variables when it
+attaches to a serial.
+
+Two things to get right. Pass `--device <serial>` exactly as the remote server
+reports it: with no serial the sidecar's target is a local `localhost:5555`, not
+your remote device. And a serial that already looks like `host:port` is dialled
+straight at adbd, bypassing any server, which is a different path with different
+failure modes. A value the sidecar cannot parse fails the run rather than
+falling back to loopback, and that is deliberate: emulator serials are numbered
+per server, so a quiet fallback would drive whatever this machine calls
+`emulator-5554` and report the results as the remote device's.
+
+## 6. What a first run prints
+
+A ten step web run, in full:
+
+```
+bundled spec: 16532 bytes (sha256=71375ed5bfc7)
+bundled web spec: 33131 bytes (sha256=779bae3c8fee)
+spec loaded into verifier
+trace dir: runs/20260815-172356
+running for 1m30s or 10 steps, whichever comes first (seed=7)
+step index=1 screen="/index.html" nodes=6
+...
+step index=10 screen="/index.html" nodes=6
+
+elapsed: 1.715s
+
+run complete: 10 steps
+no violations.
+```
+
+`nodes=` is the first number to read and the cheapest lie detector you have. On
+that page, four elements plus html and body gave `nodes=6`. The same command
+against an empty page gives `nodes=2` for every step, and still exits 0 with no
+violations. If `nodes` is a handful and never grows, the run is looking at
+something that is not your app.
+
+`screen=` is the route marker your spec's screen hooks produce. A run where it
+never changes never left one screen.
+
+The summary can carry a third line you should never skim past:
+
+```
+7 step(s) judged by nothing: the screen was still moving when it was read
+```
+
+Those steps were recorded but no property judged them, so the run's step count
+and its checked count are different numbers. `sanderling-run-triage` is about
+what to do with that.
+
+Set `--max-steps` whenever you intend to compare two runs: a step budget is what
+makes them comparable, since duration alone does not. `--seed` fixes the PRNG,
+and seed 0 draws a random one and records it in `meta.json`.
+
+## 7. The run directory
+
+Each run writes `<output>/<UTC timestamp>/`, containing `meta.json`,
+`trace.jsonl`, and one PNG per step under `screenshots/`. `--output` defaults to
+`./runs`.
+
+`meta.json` is the run's identity: seed, spec path, bundled spec sha256,
+platform, bundle id, start and end times, generator, `max_steps`,
+`duration_millis`, host, and the `--arm` label if you set one. Two runs that
+differ in any of those are different runs and cannot be pooled.
+
+If the app never launched, there is no run directory at all: the launch error
+comes before the trace is created. `error: launch app: ...` with nothing under
+`./runs` means the run never began, which is a different thing from a run that
+began and found nothing.
+
+Open a run with `sanderling replay <dir>`, which accepts either the parent runs
+directory or a single run directory.
+
+## Reporting
+
+Say what you actually ran and what came back: the `doctor` output you got rather
+than the one you expected, the exact `sanderling test` command, the step count
+and the `nodes=` figure from the first run, and for each hook you added, the step
+in a real trace where a selector over it resolved. Name what you could not
+establish, particularly any platform you did not run on.
+
+Setup is finished when a property can be written that could fail. Write it with
+`sanderling-spec-authoring`, review it with `sanderling-spec-review`, and read
+the run it produces with `sanderling-run-triage`.
diff --git a/skills/sanderling-spec-authoring/SKILL.md b/skills/sanderling-spec-authoring/SKILL.md
new file mode 100644
index 0000000..a8c34b8
--- /dev/null
+++ b/skills/sanderling-spec-authoring/SKILL.md
@@ -0,0 +1,353 @@
+---
+name: sanderling-spec-authoring
+description: Write a sanderling spec for an app: test hooks, extractors, selectors, properties, and an action tree that reaches the states the properties read. Use when adopting sanderling for a new app, when adding a property to an existing spec, and when a run is green because it never reached the state the property was written for.
+---
+
+# Writing a sanderling spec
+
+A spec is a TypeScript module the runner evaluates once per step. It exports
+`properties` and `actionsRoot`, plus an optional `setup` and `generator`.
+Writing one is easy. Writing one that would catch a real bug is not, because a
+spec that checks nothing looks exactly like a spec that checks everything: both
+are a green run.
+
+So the order below is arranged around getting evidence early that each piece
+reads what you think it reads. When the spec is written, audit it with
+`sanderling-spec-review` before trusting a green run from it.
+
+## Write it in this order
+
+Hooks, then extractors, then **one** property, then run it and read the witness,
+then everything else. Writing six properties before the first run is how people
+end up with six that cannot fire, and nothing in the output tells you which.
+
+## Hooks first
+
+Your app needs stable handles or nothing can name what it is asserting on. The
+hooks the replay UI's spec drives (`data-testid`, `data-step`) were added to the
+UI for that spec, and its header says why: a UI with no stable handles is a UI
+nothing can assert on, and that is as true for a person writing a test as it is
+for a fuzzer.
+
+Put a hook on the screen or route markers, on every container you will scope a
+lookup to, and on every fact you will read. `testTag` is the portable one: it
+surfaces as resource-id on Android and accessibilityIdentifier on iOS, and on
+web it resolves to `data-testid` or `id`.
+
+## Extractors
+
+`extract(name, fn)` reads one fact off `state.ax` per step. `.current` is this
+step's value, `.previous` the last step's, `undefined` on the first step.
+
+Name every one. The name is what you get back later: `extractor_changes` in
+`trace.jsonl` carries the prev/curr pair for each extractor whose value moved,
+and the witness recorded at a violation carries the extractor values behind it,
+by name. An unnamed extractor shows up as `extractor_3`, which tells you nothing
+at the point you most need to know what the property was looking at.
+
+The rule that decides whether the spec is worth anything:
+
+> **Return `null` when the element is absent. Never `0`, `""`, or `[]`.**
+
+An unreadable fact is unknown, and a default turns unknown into a claim. Both
+directions bite. Folio parsed a missing balance as `0` and its property became
+`Math.abs(0 - 0) === typedAmount`, false at every healthy submit. Read a missing
+panel's row count as `0` and the property says the cart is empty when the truth
+is that the cart is not on screen. Where the ambiguity is real, call it unknown:
+an empty `findAll` is both "no rows" and "not drawn yet", and folio treats it as
+unknown, which costs the very first account of a run and buys back every card
+that arrived late.
+
+Extractors run before properties and action generators, and they may not read
+each other. If two readings must come off one parse, put the parse in a helper
+both call: `examples/folio/sanderling/predicates.ts` does this with
+`oncePerFrame`, keyed on the state object, since both hosts build a new state
+object per step.
+
+## Selectors
+
+`ax.find` and `ax.findAll` take a string (`"id:CartBadge"`), an object
+(`{id: "CartBadge"}`), or an array of objects for a path. Element handles carry
+their own `.find` / `.findAll` scoped to their subtree.
+
+The two forms resolve identically: an object key is matched by the same rule its
+string form uses, so `{id: "X"}` and `"id:X"` can never pick different elements.
+What differs is the rule per key. Measured against an Android dump holding
+`com.app:id/CartBadge`, whose content-desc is `Cart, 3 items`, alongside
+`AddAccountSubmit`:
+
+| Selector | Resolves to |
+|---|---|
+| `{id: "CartBadge"}` | the badge: `id` matches the whole resource-id, or the part after `:id/` |
+| `{id: "Sub"}` | nothing: `id` wants a whole name, not a fragment |
+| `{testTag: "CartBadge"}` | the badge: `testTag` reaches resource-id on Android and accessibilityIdentifier on iOS |
+| `{testTag: "Sub"}` | `AddAccountSubmit`, because every key outside the `id` / `desc` / `descPrefix` special cases is a **substring** match |
+| `{desc: "Cart"}` | the badge: `desc` takes the whole description, or an iOS merged label starting `Cart, ` |
+
+`testTag` is the portable key and the one to reach for, but name the element in
+full. A substring match on `Sub` is not a match, it is a coincidence, and it
+will one day pick a different control.
+
+A selector that matches nothing makes every property over it vacuous, and
+nothing anywhere reports that. This is why the selector you verify is the one
+you found a real value for in a witness, not the one that looked right when you
+wrote it.
+
+**Scope the lookup to a container instead of taking the first match on the
+page.** From `replay-ui/sanderling/spec.ts`: an earlier draft of
+`screenshotShowsTheSelectedStep` took the first screenshot on the page, the
+fuzzer put the "before" panel on another tab, which left the "after" panel's
+image first, and the property fired against a UI that was behaving correctly. It
+now reads `s.ax.find([{ "data-testid": "state-before" }, { "data-testid": "screenshot" }])`
+and is scoped to the panel it means.
+
+A screen marker is not enough scope on its own during a navigation. Android's
+hierarchy dump carries the outgoing and the incoming screen together on 425 of
+1879 steps measured across 17 runs, better than one frame in five, so a find
+scoped to a screen the app has already left still resolves. Decide the route once
+per frame, return `null` when more than one screen marker is present, and have
+every reading take its answer from there. `routeOfFrame` in folio's
+`predicates.ts` is that rule and carries the measurements.
+
+## Properties
+
+`always(f)` requires `f` at every step. `next(f)` inside it compares this step
+to the next, which is how you state "this action had that effect". `now(f)`
+evaluates at the current step inside a formula body.
+`eventually(f).within(n, "steps" | "seconds" | "milliseconds")` requires `f`
+before the window closes; unbounded, it never fails a finite run. At the top
+level an `eventually` is one goal for the whole run, armed once and discharged
+for good the first time it holds; written inside `always` it re-arms at every
+step, which asks for the window to be met from everywhere. Every formula has
+`.implies`, `.and`, `.or`, `.not`.
+
+The stock properties are in `@sanderling/spec/defaults`. Put
+`noUncaughtExceptions` in every spec: it fails when the run captures an uncaught
+throwable or a `Sanderling.reportError` call, it needs no hooks and no
+calibration, and it is free. `noLogcatErrors` (also exported from
+`@sanderling/spec/defaults/properties`) fails on any error-level logcat line and
+is Android-only, holding vacuously elsewhere.
+
+## What makes a good first property
+
+Prefer a **cross-panel agreement**: two parts of the UI that derive the same fact
+by different paths must say the same thing. The toolbar prints a step count and
+the list renders rows; a badge counts violation records and the panel counts the
+rows it can show for them. Those hold on any run, so they never need
+recalibrating against a fixture, and an app that gets the fact wrong in one of
+the two places cannot satisfy them however it was driven there.
+`replay-ui/sanderling/spec.ts` is six of these plus `noUncaughtExceptions`, and
+its header explains the choice.
+
+Contrast a property that needs the fuzzer to reach a specific state, like
+folio's "a submit moves the balance by exactly the amount typed". That is where
+the real bugs are, and it is the harder thing to keep honest: it needs an action
+tree that reaches the state, a window that closes often enough to bound what
+happened inside it, and attribution that cannot blame the wrong action. Folio's
+counting form went 117 steps between two readings on one iOS run and gathered 37
+submits against a rise of 15 transactions, which is perfectly sound and says
+nothing at all; the fix was to state the same rule over a number the app redraws
+on nearly every frame, so the window is usually one action wide. Write these
+second, and read `sanderling-spec-review` before you believe one.
+
+Whichever you write, name the input that makes it return false before you move
+on. If you cannot, it is decoration.
+
+## Actions
+
+`actions(() => Action[])` returns the candidate actions for this step and the
+picker chooses one. The verbs are `Tap`, `DoubleTap`, `LongPress`, `InputText`,
+`Scroll`, `Swipe`, `PressKey`, and `Wait`. The built-in generators are `taps`,
+`doubleTaps`, `longPresses`, `typing`, `scrolls`, `swipes`, `pressKeys`, and
+`waitOnce`; `defaultActions` bundles them at taps and typing 100, scrolls 50,
+swipes 25, double taps 10.
+
+`weighted([n, generator], ...)` composes them with relative weights.
+`whenRoute(routeExtractor, routes, body)` runs `body` only on the named screens.
+The optional `setup` export runs before `actionsRoot` for as long as it returns
+actions, which is where login and onboarding belong; it re-engages on its own if
+the app logs itself out mid-run. Values come from `from(items)`,
+`integers().between(min, max)`, `strings().length(min, max).alpha()`,
+`emails().domain(host)`, and `edgeCaseText()`, all drawn from the run's seeded
+PRNG so a seed replays exactly.
+
+**The default enumeration explores, but reaching a specific interesting state
+usually needs a weighted action of your own.** With about 15 clickable elements
+on the replay UI's page, an undirected run went 40 steps without switching a
+single tab, which left both tab-facing properties vacuously true. Its badge
+agreement is worse: it needs two readings on one step, a badge, which only a
+step that has a violation renders, and a violations panel to compare it against.
+Undirected actions put both on the same step **0 times in the 80 steps of the
+first dogfood run**. The property was reachable in principle and judged nothing
+in practice, and aiming at the step alone just moved the misses to the other
+side, 0 judged either way. It took an action that selects a violating step and
+then opens a panel if none is up. Folio weights its transaction chain at 45 for
+the same reason: both balance properties observe that flow and nothing else
+reaches it.
+
+So for every property, name the action in the tree that puts everything it reads
+on screen at the same step. If there is none, add one, and give it enough weight
+that a short run gets there.
+
+## Soundness outranks everything else here
+
+A property must never convict an app that behaved correctly. A property that
+convicts more often and is sometimes wrong is strictly worse than one that
+convicts less and is never wrong, because a false conviction costs someone a day
+and then costs the whole suite its credibility. **When in doubt, a property
+should decline to judge.**
+
+Declining costs at most a detection. Convicting a healthy app costs the spec.
+Concretely that means unknown stays `null`, a bound is preferred to an equality
+where the window can hold more than one cause, and a value carried across a
+screen change is dropped rather than compared.
+
+It also means reading `state.lastAction` for what it actually promises, which is
+three different things and not one:
+
+- `state.lastAction === null`: no action ran.
+- `applied: true`: the runner saw the dispatch succeed.
+- `applied: null`: it was dispatched and nobody knows whether it landed.
+
+The rule is short. **An action of unknown fate still counts toward bounds on
+what the app could have done, but it never licenses attributing an effect to
+it.** Leave it out of the bound and you convict a healthy app: folio saw a
+transaction rise of one against a window of zero submits and called it a double
+submit. Demand its effect and you convict the app of the runner's own
+uncertainty.
+
+`relaunched: true` says the runner had to bring the app back to the foreground
+after the action, so the two readings straddle a restart. The action still
+happened and still counts toward the bound, but nothing about state running
+continuously between the two readings survives it, and a property demanding that
+action's effect has to decline. Like `applied`, its null is "not reported", not
+"the app never restarted": web and iOS cannot read the foreground at all, so only
+an explicit `true` licenses declining.
+
+## Run it, then read the witness
+
+**Write one property, run it, and read the witness before you write the second.**
+This is the step that gets skipped and it is the one that pays. A spec that has
+never had its readings confirmed against a real run looks exactly like a spec
+that has, right up until you find out that an extractor reads `null` on the
+platform you care about, or that a selector matches nothing, or that the value
+being compared is not the value you thought.
+
+```sh
+sanderling test --spec spec.ts --bundle-id com.example.app --platform android --duration 2m
+sanderling replay
+```
+
+Confirm two things before adding anything. First, that each extractor holds a
+real value at some step, by finding it in `extractor_changes` in `trace.jsonl`;
+the replay UI's hierarchy panel separately tells you whether the element your
+selector names is in the tree at all. Second, that the property actually
+compared values on some step rather than short-circuiting on its own guard. A
+green run is evidence only if you can point at a step where a property fired.
+
+Only then write the next property.
+
+Once a property is worth keeping, its logic is worth testing away from the
+device. Folio keeps its predicates in a plain module and unit-tests them in
+`pkg/spec/test/folio-*.test.ts`, run by `make test-spec-api`; the app's own
+Kotlin tests are `make test-folio`. Those files are the model for testing a
+property in isolation, including the direction people skip: a fixture where the
+effect happens legitimately, asserting that the predicate stays silent.
+
+## A spec to adapt
+
+Complete and self-contained: a storefront whose header badge and cart panel both
+know how many things are in the cart.
+
+```ts
+import { InputText, Tap, actions, always, extract, from, integers, weighted } from "@sanderling/spec";
+import { defaultActions, noUncaughtExceptions } from "@sanderling/spec/defaults";
+
+function wholeNumber(text: string | undefined): number | null {
+  if (!text) return null;
+  const parsed = Number(text.trim());
+  return Number.isInteger(parsed) ? parsed : null;
+}
+
+// The header badge: the app's own count of what is in the cart.
+const badgeCount = extract("badgeCount", s =>
+  wholeNumber(s.ax.find({ testTag: "CartBadge" })?.text));
+
+// The same fact by another path: the rows the cart panel renders. No panel is
+// null rather than 0, because nothing on screen is a fact we do not have, and
+// 0 would claim the cart is empty.
+const cartRowCount = extract("cartRowCount", s => {
+  const panel = s.ax.find({ testTag: "CartPanel" });
+  return panel ? panel.findAll({ testTag: "CartRow" }).length : null;
+});
+
+const checkoutEnabled = extract("checkoutEnabled", s => {
+  const button = s.ax.find({ testTag: "CheckoutButton" });
+  return button ? button.enabled === true : null;
+});
+
+// Two parts of the UI count the cart by different routes through the app's own
+// state, so they cannot disagree about how many things are in it.
+const badgeMatchesTheCart = always(() => {
+  const badge = badgeCount.current;
+  const rows = cartRowCount.current;
+  if (badge === null || rows === null) return true;
+  return badge === rows;
+});
+
+// Checkout is offered exactly when there is something to check out.
+const emptyCartCannotCheckOut = always(() => {
+  const rows = cartRowCount.current;
+  const enabled = checkoutEnabled.current;
+  if (rows === null || enabled === null) return true;
+  return rows > 0 || !enabled;
+});
+
+export const properties = {
+  noUncaughtExceptions,
+  badgeMatchesTheCart,
+  emptyCartCannotCheckOut,
+};
+
+const productCards = extract("productCards", s => s.ax.findAll({ testTag: "ProductCard" }));
+const cartButton = extract("cartButton", s => s.ax.find({ testTag: "CartButton" }));
+const quantityField = extract("quantityField", s =>
+  s.ax.find([{ testTag: "CartPanel" }, { testTag: "QuantityField" }]));
+
+const addAProduct = actions(() => {
+  const cards = productCards.current;
+  return cards.length === 0 ? [] : [Tap({ on: from(cards).generate() })];
+});
+
+const openTheCart = actions(() => {
+  const button = cartButton.current;
+  return button ? [Tap({ on: button })] : [];
+});
+
+const quantities = integers().between(1, 5);
+
+const changeAQuantity = actions(() => {
+  const field = quantityField.current;
+  return field ? [InputText({ into: field, text: String(quantities.generate()) })] : [];
+});
+
+// Both properties read the cart panel, so a run that never opens it judges
+// nothing. defaultActions carries the rest of the app.
+export const actionsRoot = weighted(
+  [35, addAProduct],
+  [25, openTheCart],
+  [15, changeAQuantity],
+  [25, defaultActions],
+);
+```
+
+Both properties here decline whenever the panel is off screen, which is honest
+and also the thing to measure first: if `openTheCart` never wins the draw, they
+judge nothing, exactly like the replay UI's badge property did for 80 steps.
+
+The two real specs in the repo are the fuller references.
+`replay-ui/sanderling/spec.ts` is the cross-panel spec written the way this page
+recommends. `examples/folio/sanderling/spec.ts` with its `predicates.ts` is the
+harder kind, a spec that attributes effects to actions across screens, and every
+comment in it records a way it was once wrong. `docs/manual/spec-language.md` is
+the lookup reference for anything not covered here.
diff --git a/skills/sanderling-spec-review/SKILL.md b/skills/sanderling-spec-review/SKILL.md
new file mode 100644
index 0000000..4bef943
--- /dev/null
+++ b/skills/sanderling-spec-review/SKILL.md
@@ -0,0 +1,149 @@
+---
+name: sanderling-spec-review
+description: Review a sanderling spec for properties that cannot fail, cannot pass, or convict a healthy app. Use before trusting any spec, after any spec change, and whenever a run is green but you are not sure it checked anything.
+---
+
+# Reviewing a sanderling spec
+
+A spec that is wrong does not look wrong. It looks like a passing run. Every
+failure below was found in a real spec that had been green for weeks, and each
+was caught by reading a witness rather than an exit code.
+
+Work through the checks in order. Report what you actually verified and what you
+could not; a review that says "I could not establish this" is worth more than one
+that implies coverage it did not check.
+
+## 1. Can each property ever fail?
+
+For every property, find the input that makes it return false, and say what it is.
+If you cannot name one, the property is decoration.
+
+The common shape is a guard that short-circuits on absent elements:
+
+```ts
+const badgeMatchesPanel = always(() => {
+  const badges = violationBadges.current;
+  const panels = panelCounts.current;
+  if (badges.length === 0 || panels.length === 0) return true;  // declines
+  return panels.every((c) => c === badges[0]);
+});
+```
+
+That guard is correct in isolation: with nothing on screen there is nothing to
+disagree about. It is also how a property judges zero steps in an eighty step run
+and reports success. Measured on a real run, that exact property judged **0 of 80
+steps** while the job went green.
+
+So counting matters. For each property, count the steps where its guard passed
+and it actually compared values (**judged**) against the steps where it returned
+true without comparing anything (**declined**). A property that judged nothing
+proved nothing, whatever the exit code said.
+
+You can reconstruct this from a trace: fold `extractor_changes` forward per step
+to recover each extractor's value, then apply the property's own guard. Do not
+try to read it from `residuals`: `always(p)` residuals back to `{"op":"true"}`
+whether `p` compared real values or short-circuited, so the two are
+indistinguishable there.
+
+## 2. Can each property ever pass?
+
+The mirror failure. A missing fact read as a value instead of as unknown turns a
+property into one that fires on every healthy run.
+
+```ts
+// balances parse to 0 when the element is missing
+Math.abs(currBalance - prevBalance) === typedAmount   // 0 - 0 === typed, always
+```
+
+Check every extractor: does it return `null` when the element is absent, or does
+it return `0`, `""`, or `[]`? An unreadable fact is unknown, never a default.
+
+## 3. Would it convict an app that behaved correctly?
+
+This is the only unforgivable failure. A property that convicts more often and is
+sometimes wrong is strictly worse than one that convicts less and is never wrong,
+because a false conviction costs someone a day and then costs the whole suite its
+credibility.
+
+Test both directions for every property, always:
+
+- it fires on the bug it exists to catch
+- it stays silent on a run where the app behaved
+
+The second test is the one that matters and the one people skip. Build a fixture
+where the effect happens legitimately and assert silence.
+
+## 4. Is the attribution sound?
+
+When a property blames an effect on an action, check it cannot blame the wrong one.
+
+**Identity keys must be injective.** If two distinct objects can produce the same
+key, a value can jump between unrelated series without anything noticing. Merged
+UI text is the usual culprit: an account named `Travel1` with 25 transactions and
+one named `Travel12` with 5 can both render `TRTravel125 transactions`. No
+function of that string can separate them.
+
+**Match whole keys, not endings or substrings.** `endsWith` attribution judges an
+older account named `Emergency Fund` when the user typed `Fund`.
+
+Selector matching has the same trap and it is easy to miss which keys carry it.
+`id`, `text`, `desc` and `descPrefix` resolve by their own rules, so `{id: "Sub"}`
+correctly matches nothing. Every other key, `testTag` included, falls through to a
+substring compare, so `{testTag: "Sub"}` matches `AddAccountSubmit`. That is not a
+match, it is a coincidence, and a property built on it judges whichever element
+happens to contain the fragment.
+
+**Drop the carrier when the screen changes.** A value carried across a route
+change is a value read from a screen that is no longer there.
+
+## 5. Are the windows bounded?
+
+A property that compares two readings and counts actions between them is only as
+good as how often it closes the window.
+
+Real numbers from a real leg: a run went from step 19 to step 136 without
+returning to the screen the property read, so it saw a rise of 15 against a window
+of 37 actions. 15 is not more than 37, so nothing was reported, and the same run
+also gave 4 against 7, 6 against 13, and 1 against 1. The property was sound the
+whole time and detected nothing.
+
+Two fixes, and prefer the first:
+
+- **Close the window more often.** Read the fact somewhere the run visits often,
+  not somewhere it visits rarely.
+- **Do not spend budget on actions that cannot have caused anything.** If the
+  submit button is disabled when the field is empty, a tap on it committed
+  nothing and must not count. That one change halved the window on a real spec.
+
+Prefer an **upper bound** to an equality. `|delta| > typedAmount` is sound where
+`|delta| === typedAmount` convicts a commit still in flight, a refused submit, and
+a tap that never landed.
+
+## 6. Does every selector actually resolve?
+
+A selector that matches nothing makes every property over it vacuous, and nothing
+reports it. Verify by finding a step whose witness holds a real value for it, not
+by reading the selector and believing it.
+
+## 7. Does the property know what the runner could not promise?
+
+`state.lastAction` distinguishes three things, and a property that collapses them
+is unsound:
+
+- `null` means no action ran
+- `applied: true` means the runner saw the dispatch succeed
+- `applied: null` means it was dispatched and nobody knows whether it landed
+
+An action of unknown fate still counts toward **bounds on what the app could have
+done**, and never licenses attributing an effect **to** it. `relaunched: true`
+says the app restarted between two readings, so a property assuming continuous
+state must decline.
+
+## Reporting
+
+For each property give: can it fail, can it pass, does it convict a healthy app,
+how many steps it judged on a real run, and what you could not check. Name the
+step and the witness values behind any claim that a property works.
+
+A green run is evidence only if you can point at a step where a property actually
+fired. Read the witness, not the exit code.