diff --git a/formal-consensus/RULEAZA-TOT.md b/formal-consensus/RULEAZA-TOT.md
index b823aa5..cf851ea 100644
--- a/formal-consensus/RULEAZA-TOT.md
+++ b/formal-consensus/RULEAZA-TOT.md
@@ -29,13 +29,15 @@ python run_consensus_verification.py
 It runs ALL the `*_smt.py` models in this directory (the completeness guard refuses a green result if a model that is
 present is not wired). It prints PASS / FAIL per model, the time of each, and the tally of verdict lines.
 
-**Measured 2026-10-07** (Windows, Python 3.14.4 / z3 4.16.0; the times vary with the machine):
+*The previous measurement, 2026-10-07, gave the same counts below in ~37 s.*
+
+**Measured 2026-11-04** (Windows, Python 3.14.4 / z3 4.16.0, on a loaded machine; the times vary with the machine):
 
 ```
 models run: 37   passed: 37   (16 consensus + 11 contract + 10 application)
 verdict lines: 301 PROVED   159 CEX-FOUND   0 FAILED
-wall time:  ~37s total   (slowest: qbft_safety_smt.py ~20s)
-coverage: 37 of 37 *_smt.py files wired
+wall time: 123.06s total   (slowest: qbft_safety_smt.py at 62.39s)
+coverage: 37 of 37 *_smt.py files in this directory are wired into this run
 RESULT: ALL MODELS PASS (proofs PROVED, negative controls fired)
 ```