diff --git a/.github/scripts/folio-run.sh b/.github/scripts/folio-run.sh
index ffd0b37..360a714 100755
--- a/.github/scripts/folio-run.sh
+++ b/.github/scripts/folio-run.sh
@@ -3,12 +3,13 @@
 # exit code the job expects. Kept out of the workflow YAML so it can be run by
 # hand, which is how it was calibrated:
 #
-#   SEED=3 MAX_STEPS=240 .github/scripts/folio-run.sh android
+#   SEED=9 MAX_STEPS=200 .github/scripts/folio-run.sh android
 #
-# web and ios expect exit 2: folio's double-submit bug is still there, and a run
-# that no longer finds it is a regression in the fuzzer, not a pass. android is a
-# health gate instead, because a run there is not a function of its seed; see
-# docs/development/ci.md.
+# web and ios expect a conviction: folio's double-submit bug is still there, and
+# a run that no longer finds it is a regression in the fuzzer, not a pass. The
+# exit code alone does not say that much, so this script reads the trace: see
+# GATED_PROPERTIES below. android is a health gate instead, because it convicts
+# in four runs out of five rather than five; see docs/development/ci.md.
 set -uo pipefail
 
 platform="${1:?usage: folio-run.sh android|ios|web}"
@@ -86,31 +87,95 @@ esac
 code=$?
 
 run_dir="$(ls -d "$output"/*/ 2>/dev/null | tail -1)"
+trace="${run_dir:-.}/trace.jsonl"
 steps=0
-[ -n "$run_dir" ] && steps=$(wc -l < "$run_dir/trace.jsonl" | tr -d ' ')
-violated=$(grep -ho '"violations":\[[^]]*\]' "$run_dir/trace.jsonl" 2>/dev/null | head -1)
+[ -f "$trace" ] && steps=$(wc -l < "$trace" | tr -d ' ')
+
+# The two properties that state folio's double-submit. Anything else the spec
+# proves false is a different finding, and this leg has nothing to say about it.
+GATED_PROPERTIES="submitMovesBalanceByTypedAmount,submitCommitsOneTransactionPerAction"
+
+# Exit 2 means "the run recorded a violation", and that is NOT the same as "the
+# run convicted folio". A predicate that THROWS is recorded as a violation too,
+# with is_error set and the thrown text as its reason, and it reaches exit 2 by
+# the identical path. So does a violation of newAccountBalanceIsZero, a real but
+# unrelated property in the same spec, which one android seed produces. Reading
+# the exit code alone leaves the gate green with detection dead.
+#
+# So sort the trace's violations three ways, by name and by is_error:
+#   line 1  convictions: a gated property that was proved false
+#   line 2  thrown: a predicate that blew up, with the reason it gave
+#   line 3  other: a real violation of some property this leg does not gate on
+classified=$(TRACE="$trace" GATED="$GATED_PROPERTIES" python3 - <<'PY'
+import json, os
+
+gated = set(os.environ["GATED"].split(","))
+convictions, thrown, other = [], [], []
+try:
+    lines = open(os.environ["TRACE"], encoding="utf-8", errors="replace")
+except OSError:
+    lines = []
+for line in lines:
+    try:
+        step = json.loads(line)
+    except ValueError:
+        continue
+    witnesses = step.get("witnesses") or {}
+    for name in step.get("violations") or []:
+        witness = witnesses.get(name) or {}
+        if witness.get("is_error"):
+            reason = " ".join(str(witness.get("reason") or "").split())
+            thrown.append("%s: %s" % (name, reason) if reason else name)
+        elif name in gated:
+            convictions.append(name)
+        else:
+            other.append(name)
+for names in (convictions, thrown, other):
+    print(", ".join(names))
+PY
+)
+convicted=$(printf '%s\n' "$classified" | sed -n '1p')
+thrown=$(printf '%s\n' "$classified" | sed -n '2p')
+other=$(printf '%s\n' "$classified" | sed -n '3p')
 
 {
   echo "### folio on $platform"
   echo
   echo "- seed \`$seed\`, budget $max_steps steps / $duration"
   echo "- $steps steps recorded, exit $code"
-  [ -n "$violated" ] && echo "- $violated"
+  [ -n "$convicted" ] && echo "- convicted on: $convicted"
+  [ -n "$other" ] && echo "- also violated: $other"
+  [ -n "$thrown" ] && echo "- **a predicate threw**: $thrown"
 } >> "$summary"
 
+# A thrown predicate fails every leg, android included. It is not evidence about
+# folio: the property that threw is violated from that step on whatever the app
+# does, and --exit-on-violation ends the run there, so nothing past it was
+# checked. Reporting that as a conviction, or as android's bonus, is the hole
+# this check exists to close.
+if [ -n "$thrown" ]; then
+  echo "folio/$platform: a predicate threw, so exit $code is not a verdict about folio: $thrown" >&2
+  echo "folio/$platform: fix the spec (examples/folio/sanderling/) and run again" >&2
+  exit 1
+fi
+
 if [ "$platform" = "android" ]; then
-  # A health gate, not a conviction gate. The android hierarchy dump can show
-  # two screens mid-transition, and such a step applies no action, so the same
-  # seed walks a different trajectory each run and the bug turns up in about two
-  # runs in five. Demanding a conviction would cry wolf more often than it would
-  # catch the regression it exists to catch. Reaching the transaction screen is
-  # what this leg proves: the app built, installed, launched and drove.
+  # A health gate, not a conviction gate: android convicts in four runs out of
+  # five, and a gate that fails the fifth would report a regression it had not
+  # found. Reaching the transaction screen is what this leg proves: the app
+  # built, installed, launched and drove.
   case "$code" in
     0) ;;
-    2) echo "folio/android: found the submit bug in $steps steps (a bonus, not required)" ;;
+    2)
+      if [ -n "$convicted" ]; then
+        echo "folio/android: found the submit bug in $steps steps (a bonus, not required)"
+      else
+        echo "folio/android: violated $other, which is not the double-submit; judging health only"
+      fi
+      ;;
     *) echo "folio/android: the harness failed with exit $code" >&2; exit "$code" ;;
   esac
-  if ! grep -q '"AddTransactionScreen"' "$run_dir/trace.jsonl"; then
+  if ! grep -q '"AddTransactionScreen"' "$trace" 2>/dev/null; then
     echo "folio/android: the run never reached AddTransactionScreen, so it never got past login" >&2
     exit 1
   fi
@@ -119,7 +184,18 @@ if [ "$platform" = "android" ]; then
 fi
 
 case "$code" in
-  2) echo "folio/$platform: found the submit bug in $steps steps"; exit 0 ;;
-  0) echo "folio/$platform: the run finished clean; the double-submit bug was NOT found in $steps steps (seed $seed)" >&2; exit 1 ;;
+  2)
+    if [ -z "$convicted" ]; then
+      echo "folio/$platform: exit 2, but the violation was ${other:-nothing this trace records}, not the double-submit this leg gates on" >&2
+      exit 1
+    fi
+    echo "folio/$platform: found the submit bug in $steps steps ($convicted)"
+    exit 0
+    ;;
+  0)
+    echo "folio/$platform: the run finished clean; the double-submit bug was NOT found in $steps steps (seed $seed)" >&2
+    echo "folio/$platform: the spec ran without throwing, so this is the fuzzer no longer reaching the bug, not a broken spec" >&2
+    exit 1
+    ;;
   *) echo "folio/$platform: the harness failed with exit $code" >&2; exit "$code" ;;
 esac