diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json
index e89f55bd..481ab131 100644
--- a/.agents/skills/verify-session-lifecycle/coverage.json
+++ b/.agents/skills/verify-session-lifecycle/coverage.json
@@ -149,7 +149,7 @@
     "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac",
     "skill:model/SessionLifecycle.tla": "cd8639012467f13e",
     "skill:scripts/facts.mjs": "3ef7fa152ec0af36",
-    "skill:scripts/check.sh": "cad764a01b6eee50"
+    "skill:scripts/check.sh": "17f2ce5bd1b1b090"
   },
   "callSites": {
     "writeManifest": [
diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh
index 07ae56de..c09d2607 100755
--- a/.agents/skills/verify-session-lifecycle/scripts/check.sh
+++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh
@@ -365,6 +365,16 @@ fi
 # with at least 1 TLC worker. A run that expects a violation keeps 1 worker,
 # which finds the shortest trace.
 CPUS=$(getconf _NPROCESSORS_ONLN 2>/dev/null || echo 1)
+# getconf counts every online CPU, also in a container whose cgroup v2 quota
+# allows fewer. cpu.max reads "max <period>" without a quota, else
+# "<quota> <period>" in microseconds.
+if read -r quota period 2>/dev/null </sys/fs/cgroup/cpu.max &&
+  [[ $quota =~ ^[1-9][0-9]*$ && $period =~ ^[1-9][0-9]*$ ]]; then
+  quota_cpus=$(((quota + period - 1) / period))
+  if [ "$quota_cpus" -lt "$CPUS" ]; then
+    CPUS=$quota_cpus
+  fi
+fi
 passes=0
 for name in $RUNS; do
   if [ "$(cut -f1 "$OUT/$name/expect.txt")" = pass ]; then
@@ -376,6 +386,7 @@ PASS_WORKERS=1
 if [ "$concurrent" -gt 0 ] && [ "$CPUS" -gt "$concurrent" ]; then
   PASS_WORKERS=$((CPUS / concurrent))
 fi
+echo "CPUs: $CPUS. TLC workers of a run that expects pass: $PASS_WORKERS."
 
 run_tlc() {
   local dir rc=0 workers=1