diff --git a/verify/budget.sh b/verify/budget.sh
index 549bc70..4a47c7f 100755
--- a/verify/budget.sh
+++ b/verify/budget.sh
@@ -50,10 +50,28 @@ guard_load() {
 }
 
 # Run a command inside the budget: capped memory, capped time, low priority.
+#
+# The virtual-memory ceiling turns a runaway into a clean allocation failure
+# rather than an OOM kill that takes something else with it. It suits native
+# processes; see `budgeted_jvm` for why it does not suit a JVM.
 budgeted() {
   guard_load
-  # A virtual-memory ceiling turns a runaway into a clean allocation failure
-  # rather than an OOM kill that takes something else with it.
   ( ulimit -v $(( VERIFY_MEM_MB * 1024 )) 2>/dev/null || true
     exec nice -n "$VERIFY_NICE" ionice -c3 timeout --signal=INT "$VERIFY_TIMEOUT" "$@" )
 }
+
+# As above, without the virtual-memory ceiling.
+#
+# A JVM reserves far more address space than it will ever commit -- compressed
+# class space alone asks for a gigabyte before any heap -- so `ulimit -v` sized
+# to the intended heap stops it starting at all. It fails as
+# "Could not allocate compressed class space", which reads like a memory
+# shortage and is really the guardrail. Found when this ran on a CI box with a
+# smaller budget than the machine it was written on.
+#
+# The heap is capped by -Xmx instead, which is the JVM's own instrument for the
+# job and is precise about what it limits.
+budgeted_jvm() {
+  guard_load
+  nice -n "$VERIFY_NICE" ionice -c3 timeout --signal=INT "$VERIFY_TIMEOUT" "$@"
+}
diff --git a/verify/tla.sh b/verify/tla.sh
index 6d15073..c84028f 100755
--- a/verify/tla.sh
+++ b/verify/tla.sh
@@ -33,7 +33,7 @@ echo "TLC: ${VERIFY_JOBS} workers, ${TLC_HEAP} heap"
 echo
 
 run_tlc() {
-  budgeted java -XX:+UseParallelGC -Xmx"$TLC_HEAP" -cp "$JAR" tlc2.TLC \
+  budgeted_jvm java -XX:+UseParallelGC -Xmx"$TLC_HEAP" -cp "$JAR" tlc2.TLC \
     -workers "$VERIFY_JOBS" -nowarning -config "$1" Gossip.tla 2>&1
 }
 
@@ -42,8 +42,12 @@ if out=$(run_tlc Gossip.cfg) && grep -q "Model checking completed. No error has
   grep -E "^[0-9]+ states|^The depth" <<<"$out" | sed 's/^/  /'
   echo "  PASS: converges on every schedule"
 else
-  grep -E "^Error|^State [0-9]+|/\\\\ known" <<<"$out" | head -20 | sed 's/^/  /'
   echo "  FAIL: the fix does not hold" >&2
+  # Print everything rather than a filtered view. A grep that matches nothing
+  # returns non-zero, and under `set -o pipefail` that used to abort the script
+  # before it said anything at all -- so the one run that failed was the one
+  # run with no explanation.
+  sed 's/^/  | /' <<<"$out" | tail -30 >&2
   exit 1
 fi