# Expected results

| Check | Expected | Exit code |
|---|---|---|
| `verify_ihvrk_evidence.py` | 9 checks: E1 manifest hashes, E2 tests, E3 Z3, E4 TLC, E5 mutation, E6 sample ledger, E7 ×3 tampered copies rejected; all PASS | 0 |
| any evidence file altered | E1 FAIL (`hash mismatch`) | 1 |
| `pytest ihvrk/tests` as root on cgroup v2 | 0 failed, 0 error (count in test_results.json) | 0 |
| `pytest ihvrk/tests` without root | runtime tests reported **skipped**, not passed | 0 |
| `python3 -m ihvrk.solver.ihvrk_solver` | `"all_as_expected": true` | 0 |
| TLC design | `No error has been found`, ~8.66M distinct states | – |
| TLC `no_auth_check`, `no_digest_check` | `Invariant NoUnauthorizedExecution is violated` | 12 |
| TLC `permit_reuse` | `Invariant NoDoubleExecution is violated` | 12 |
| TLC `no_nonce_consume` | no error (expected; see SECURITY_INVARIANTS.md) | 0 |
| mutation | `30/30` | 0 |

How the verifier labels results: PASS = checked and holds; FAIL = checked and does not hold; SKIP = not checked
(reason shown). In `test_results.json`: `passed`, `failed`, `error` and `skipped` are counted separately. A test that
never ran does not appear as passed. Simulations are labelled in the documents (e.g. SOFTWARE_TEST keys,
synthetic identities). Properties without evidence are listed in LIMITATIONS.md, not here.