From 9b5476a3e42f03a56bb41d18e0c4b6da2179b0c3 Mon Sep 17 00:00:00 2001 From: Aere Network Date: Wed, 4 Nov 2026 06:19:21 +0200 Subject: [PATCH] formal-consensus/RULEAZA-TOT.md: SMT suite re-measured 2026-11-04 (37/37 models, 301 PROVED, 159 CEX-FOUND, 0 FAILED); the 2026-10-07 counts kept as history --- formal-consensus/RULEAZA-TOT.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) 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) ```