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.