diff --git a/examples/folio/sanderling/predicates.ts b/examples/folio/sanderling/predicates.ts
index 4edd358..52cf62c 100644
--- a/examples/folio/sanderling/predicates.ts
+++ b/examples/folio/sanderling/predicates.ts
@@ -1,24 +1,75 @@
-// Computes the Home-screen total balance from the visible AccountCard balances.
-// When no Home cards are visible (Ledger, AddTransaction, etc.) the carrier
-// value is returned so the property compares apples to apples across screen
-// transitions. The Ledger LedgerBalance is intentionally ignored because it is
-// a single-account number on a different scale than the Home multi-account sum.
-// A single unreadable card makes the whole total null: a partial sum looks
-// exactly like money moving, and the balance property would fire on a healthy
-// step.
-export function computeHomeTotalBalance(args: {
-  cardBalanceTexts: (string | undefined)[];
+// Reads the Home screen's own TOTAL BALANCE node and advances the carrier the
+// spec holds between Home visits.
+//
+// The app computes that number over ALL accounts, so it does not care which
+// account cards happen to be laid out inside the viewport. Summing the visible
+// AccountCard balances did: a card clipped at the bottom edge exposes no
+// AccountBalance child, and a partial sum looks exactly like money moving.
+//
+// Three cases, and the difference between the reported value and the carrier is
+// the whole point:
+//   - off Home there is nothing to read, so the last total we actually read is
+//     reported and carried on unchanged;
+//   - on Home with an unreadable total the reading is UNKNOWN, so null is
+//     reported (the property treats null as vacuous) while the carrier keeps
+//     the last value we did read. Writing null into the carrier is what used to
+//     poison every later step: off-Home steps hand the carrier back, so one
+//     unreadable Home turned the property vacuous for the rest of the run;
+//   - on Home with a readable total, that total is both the reading and the new
+//     carrier, and `fresh` says the comparison window closes here.
+export interface HomeTotalReading {
+  value: number | null;
+  carrier: number | null;
+  fresh: boolean;
+}
+
+export function readHomeTotalBalance(args: {
+  onHome: boolean;
+  totalText: string | undefined;
   previousCarrier: number | null;
-}): number | null {
-  const { cardBalanceTexts, previousCarrier } = args;
-  if (cardBalanceTexts.length === 0) return previousCarrier;
-  let sum = 0;
-  for (const text of cardBalanceTexts) {
-    const cents = parseDollarCents(text);
-    if (cents === null) return null;
-    sum += cents;
-  }
-  return sum;
+}): HomeTotalReading {
+  const { onHome, totalText, previousCarrier } = args;
+  if (!onHome) return { value: previousCarrier, carrier: previousCarrier, fresh: false };
+  const total = parseDollarCents(totalText);
+  if (total === null) return { value: null, carrier: previousCarrier, fresh: false };
+  return { value: total, carrier: total, fresh: true };
+}
+
+// Is this the action that commits a transaction? Nothing else in Folio reaches
+// Repository.createTransaction: AddTransactionViewModel.submit() is the only
+// caller, AddTransactionEvent.Submit is the only thing that runs it, and the
+// TxnSubmit button's onClick is the only thing that sends that event.
+export function isTxnSubmitTap(
+  lastAction: { kind?: string; on?: string | object } | null,
+): boolean {
+  if (lastAction == null) return false;
+  if (lastAction.kind !== "Tap" && lastAction.kind !== "DoubleTap") return false;
+  const on = lastAction.on;
+  const onString = typeof on === "string" ? on : on != null ? JSON.stringify(on) : "";
+  return onString.includes("TxnSubmit");
+}
+
+// Counts the submit actions inside the window the balance property compares
+// over: from the last Home total we read to this step, inclusive of this step's
+// action.
+//
+// Counting ACTIONS rather than transactions is deliberate. A double-tap is one
+// action that commits two transactions, which is precisely the bug, so a rule
+// phrased in transactions could not tell the bug apart from two healthy
+// submits. A rule phrased in actions can: one action in the window means the
+// whole balance delta belongs to that action, and comparing it against the
+// amount typed for it is fair.
+//
+// The reset lands on `fresh`, the same event that advances the carrier, so the
+// count always describes exactly the interval the two compared totals span.
+export function countSubmitsInWindow(args: {
+  previousCount: number;
+  lastAction: { kind?: string; on?: string | object } | null;
+  fresh: boolean;
+}): { reported: number; next: number } {
+  const { previousCount, lastAction, fresh } = args;
+  const reported = previousCount + (isTxnSubmitTap(lastAction) ? 1 : 0);
+  return { reported, next: fresh ? 0 : reported };
 }
 
 // Parses formatCents output like "$5.00", "-$1,234.56", "+$0.50" back to
@@ -47,8 +98,9 @@ export function parseDollarCents(text: string | undefined): number | null {
 // of "12 transactions" into the amount.
 const TRAILING_BALANCE = /[-+]?\$[\d,]+\.\d{2}\s*$/;
 
-// The transaction-count label sits between the name and the balance.
-const TRAILING_TXN_COUNT = /\d+\s*transactions?\s*$/;
+// The transaction-count label sits between the name and the balance. The group
+// captures the digit run so the count can be read from the same match.
+const TRAILING_TXN_COUNT = /(\d+)\s*transactions?\s*$/;
 
 export function cardBalanceText(args: {
   childText: string | undefined;
@@ -79,6 +131,68 @@ export function cardAccountName(args: {
   return head.slice(0, label.index).trim();
 }
 
+// The digit run in front of a card's "transaction(s)" label, kept as TEXT.
+//
+// A string rather than a number because web merges the card into one node and
+// an account whose name ends in digits runs them into the count: the account
+// named "-1" holding 2 transactions merges to "-1-12 transactions", whose
+// maximal digit run reads 12. That prefix is fixed for a given account, so two
+// readings whose runs are the SAME LENGTH still differ by exactly the true
+// difference (19 to 120 is impossible; 19 to 110 is a length change). Two runs
+// of different lengths do not, and 9 to 10 would read as 19 to 110, a delta of
+// 91 out of a delta of 1. Keeping the run as text is what lets the predicate
+// see the length change and drop the pair instead of convicting on it.
+//
+// Android and iOS expose AccountTxnCount as its own node, where the run is just
+// the count and the length rule costs nothing but a window per decade.
+export function cardTxnCountDigits(args: {
+  childText: string | undefined;
+  cardText: string | undefined;
+}): string | undefined {
+  const { childText, cardText } = args;
+  const source = childText ?? cardText?.replace(TRAILING_BALANCE, "");
+  return source?.match(TRAILING_TXN_COUNT)?.[1];
+}
+
+// Every accepted submit commits exactly one transaction, so over any window the
+// number of transactions committed cannot exceed the number of submit actions
+// taken. A double-submit is one action committing two, which is the only way to
+// break it. Rejected submits (parseCents refuses the amount) commit nothing, so
+// the normal case sits comfortably under the bound.
+//
+// Only accounts present in BOTH readings are counted, and only upward movement.
+// A card that scrolled out of the viewport, or one whose count could not be
+// read, simply drops out of the sum. That makes the result a LOWER BOUND on the
+// transactions committed, and a lower bound that already exceeds the submit
+// count is still a real violation. Missing cards can cost a detection; they
+// cannot manufacture one.
+//
+// Transactions are never deleted (Ledger.sq has no DELETE for them), so a
+// per-account count only ever rises; the max(0, ...) is defensive, not load
+// bearing.
+export function committedTransactionsExceedSubmits(args: {
+  countsBefore: Record<string, string> | null;
+  countsAfter: Record<string, string> | null;
+  submitsInWindow: number;
+}): boolean {
+  const { countsBefore, countsAfter, submitsInWindow } = args;
+  if (countsBefore === null || countsAfter === null) return false;
+  if (!Number.isSafeInteger(submitsInWindow)) return false;
+  let committed = 0;
+  for (const name of Object.keys(countsAfter)) {
+    const before = countsBefore[name];
+    const after = countsAfter[name];
+    if (before === undefined || after === undefined) continue;
+    // Different run lengths are not comparable: see cardTxnCountDigits.
+    if (before.length !== after.length) continue;
+    const from = parseInt(before, 10);
+    const to = parseInt(after, 10);
+    if (!Number.isSafeInteger(from) || !Number.isSafeInteger(to)) continue;
+    if (to > from) committed += to - from;
+  }
+  return committed > submitsInWindow;
+}
+
 // Parses raw user input in the transaction amount field into integer cents.
 // Mirrors the Folio app's parseCents (app/shared/.../util/Format.kt): whole
 // numbers like "50" become 5000 cents, decimals like "5.50" become 550, more
@@ -109,23 +223,32 @@ export function parseTypedAmount(text: string | undefined | null): number {
 // button, the absolute change in total balance must equal the amount the
 // user typed. A double-submit lands two transactions and shifts the balance
 // by 2x the typed amount, tripping this check. The route gate skips steps
-// whose landing screen is not Home: totalBalance is only freshly computed
-// from visible AccountCards on Home, so off-Home comparisons would read a
-// stale carrier value and false-fire.
+// whose landing screen is not Home: totalBalance is only freshly read from
+// Home's own TOTAL BALANCE node, so off-Home comparisons would read a stale
+// carrier value and false-fire.
+//
+// submitsInWindow is what keeps the comparison honest. prevTotalBalance is the
+// last total we READ, not the total as of the previous transaction, so the two
+// compared numbers can straddle any number of commits: a real run produced a
+// 13000 delta against a typed 19600 because the window held a double-submit's
+// two 19600 debits AND an unrelated 26200 credit. A delta like that is not
+// evidence about the amount typed into any one submit, so anything other than
+// exactly one submit action in the window is vacuous. Exactly one still catches
+// the bug: the double-tap is a single action.
 export function submitChangesBalanceByTypedAmount(args: {
   route: string | null;
   lastAction: { kind?: string; on?: string | object } | null;
+  submitsInWindow: number;
   typedAmount: number;
   prevTotalBalance: number | null;
   currTotalBalance: number | null;
 }): boolean {
-  const { route, lastAction, typedAmount, prevTotalBalance, currTotalBalance } = args;
+  const { route, lastAction, submitsInWindow, typedAmount } = args;
+  const { prevTotalBalance, currTotalBalance } = args;
+
   if (route !== "home") return true;
-  if (lastAction == null) return true;
-  if (lastAction.kind !== "Tap" && lastAction.kind !== "DoubleTap") return true;
-  const on = lastAction.on;
-  const onString = typeof on === "string" ? on : on != null ? JSON.stringify(on) : "";
-  if (!onString.includes("TxnSubmit")) return true;
+  if (!isTxnSubmitTap(lastAction)) return true;
+  if (submitsInWindow !== 1) return true;
   if (typedAmount === 0) return true;
   // An unknown total on either side is not evidence of anything. Comparing one
   // would turn every unreadable Home into a violation.
diff --git a/examples/folio/sanderling/spec.ts b/examples/folio/sanderling/spec.ts
index 7daab1a..a60dd6f 100644
--- a/examples/folio/sanderling/spec.ts
+++ b/examples/folio/sanderling/spec.ts
@@ -11,13 +11,17 @@ import {
   weighted,
   whenRoute,
 } from "@sanderling/spec";
+import type { State } from "@sanderling/spec";
 import { defaultActions, doubleTaps } from "@sanderling/spec/defaults";
 import {
   cardAccountName,
   cardBalanceText,
-  computeHomeTotalBalance,
+  cardTxnCountDigits,
+  committedTransactionsExceedSubmits,
+  countSubmitsInWindow,
   parseDollarCents,
   parseTypedAmount,
+  readHomeTotalBalance,
   submitChangesBalanceByTypedAmount,
 } from "./predicates";
 
@@ -50,18 +54,70 @@ const accounts = extract<Account[]>("accounts", s =>
       cardBalanceText({ childText: card.find({ testTag: "AccountBalance" })?.text, cardText: card.text })),
   })));
 
-// Total balance: sum of AccountCard balances visible on Home. The carrier
-// deliberately tracks only the Home multi-account total. Ledger's
+// Total balance: Home's own TOTAL BALANCE node, which the app computes over
+// every account rather than over the cards that happen to be laid out inside
+// the viewport. The carrier deliberately tracks only that Home total. Ledger's
 // LedgerBalance is a single-account number on a different scale and would
 // corrupt cross-screen comparisons if mixed in. Off-Home steps carry forward
-// the last-seen Home sum so `previous` and `current` stay on the same scale.
-let lastHomeTotal: number | null = 0;
+// the last-read Home total so `previous` and `current` stay on the same scale.
+const homeTotalText = (s: State) =>
+  s.ax.find([{ testTag: "HomeScreen" }, { testTag: "TotalBalance" }])?.text;
+const onHome = (s: State) => s.ax.find({ testTag: "HomeScreen" }) != null;
+
+let lastHomeTotal: number | null = null;
 const totalBalance = extract<number | null>("totalBalance", s => {
-  const cards = s.ax.findAll([{ testTag: "HomeScreen" }, { testTag: "AccountCard" }]);
-  const cardBalanceTexts = cards.map(c =>
-    cardBalanceText({ childText: c.find({ testTag: "AccountBalance" })?.text, cardText: c.text }));
-  lastHomeTotal = computeHomeTotalBalance({ cardBalanceTexts, previousCarrier: lastHomeTotal });
-  return lastHomeTotal;
+  const reading = readHomeTotalBalance({
+    onHome: onHome(s),
+    totalText: homeTotalText(s),
+    previousCarrier: lastHomeTotal,
+  });
+  lastHomeTotal = reading.carrier;
+  return reading.value;
+});
+
+// Submit actions inside the window `totalBalance.previous` and
+// `totalBalance.current` span. Recomputed rather than shared with the extractor
+// above because extractor getters may not read one another; both derive
+// freshness from the same reading, so they reset on the same step.
+let submitsSinceHomeTotal = 0;
+const submitsInWindow = extract("submitsInWindow", s => {
+  const fresh = readHomeTotalBalance({
+    onHome: onHome(s),
+    totalText: homeTotalText(s),
+    previousCarrier: null,
+  }).fresh;
+  const window = countSubmitsInWindow({
+    previousCount: submitsSinceHomeTotal,
+    lastAction: s.lastAction,
+    fresh,
+  });
+  submitsSinceHomeTotal = window.next;
+  return window.reported;
+});
+
+// Transactions committed per account, read off the Home cards. Carried across
+// off-Home steps exactly like totalBalance, and for the same reason: the pair
+// the property compares has to be two Home readings, not a Home reading and
+// whatever happened to be on screen. A card whose count is unreadable is left
+// out of the map rather than guessed at; the predicate treats a missing account
+// as no evidence.
+let lastHomeTxnCounts: Record<string, string> | null = null;
+const homeTxnCounts = extract<Record<string, string> | null>("homeTxnCounts", s => {
+  if (!onHome(s)) return lastHomeTxnCounts;
+  const counts: Record<string, string> = {};
+  for (const card of s.ax.findAll([{ testTag: "HomeScreen" }, { testTag: "AccountCard" }])) {
+    const name = cardAccountName({
+      childText: card.find({ testTag: "AccountName" })?.text,
+      cardText: card.text,
+    });
+    const digits = cardTxnCountDigits({
+      childText: card.find({ testTag: "AccountTxnCount" })?.text,
+      cardText: card.text,
+    });
+    if (name !== "" && digits !== undefined) counts[name] = digits;
+  }
+  lastHomeTxnCounts = counts;
+  return counts;
 });
 
 const lastAction = extract("lastAction", s => s.lastAction);
@@ -111,6 +167,7 @@ const submitMovesBalanceByTypedAmount = always(
     submitChangesBalanceByTypedAmount({
       route: route.current,
       lastAction: lastAction.current,
+      submitsInWindow: submitsInWindow.current,
       typedAmount: parseTypedAmount(txnAmountField.previous?.text),
       prevTotalBalance: totalBalance.previous ?? null,
       currTotalBalance: totalBalance.current,
@@ -118,6 +175,21 @@ const submitMovesBalanceByTypedAmount = always(
   ),
 );
 
+// Property 3: one submit action commits at most one transaction. Counting
+// actions against transactions needs no amounts and no float arithmetic, and it
+// stays sound however wide the window between two Home readings gets, because
+// both sides of the comparison accumulate over the same window. It is the
+// double-submit stated directly: one tap, two rows.
+const submitCommitsOneTransactionPerAction = always(
+  next(() =>
+    !committedTransactionsExceedSubmits({
+      countsBefore: homeTxnCounts.previous ?? null,
+      countsAfter: homeTxnCounts.current,
+      submitsInWindow: submitsInWindow.current,
+    }),
+  ),
+);
+
 const DEMO_EMAIL = "demo@folio.app";
 const DEMO_PASSWORD = "ledger123";
 
@@ -175,6 +247,7 @@ const addTxn = whenRoute(route, ["home", "ledger", "add-transaction"], () => {
 export const properties = {
   newAccountBalanceIsZero,
   submitMovesBalanceByTypedAmount,
+  submitCommitsOneTransactionPerAction,
 };
 
 export const setup = login;