aere-network/aere-research
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

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

Browse Source
This commit is contained in:
Aere Network 2026-11-04 06:19:21 +02:00
parent 89ed8ca22d
commit 9b5476a3e4
1 changed files with 5 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
formal-consensus/RULEAZA-TOT.md
View File

@ -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)
```