# Evolution 18 — formal assurance

What was done: properties stated precisely, checked by property-based tests (hypothesis, 300 random cases each for
the grading rules), by the executed corpus, and by mutation (26 weakened checks, each must make at least one corpus
scenario fail). No model checker and no proof assistant was used. **The platform is not formally verified**; the
properties below are tested over finite generated inputs and 82 concrete scenarios.

| # | Property (specification wording) | Precise statement in the code | Checked by | Mutants that must break it |
|---|---|---|---|---|
| P1 | An action cannot execute without authorization bound to its canonical effect | `execute` reaches the executor only if the authorization verifies under a pinned approver key, `decision == ALLOW`, and the re-derived effect digest, tool, passport digest, runtime and policy version equal the signed ones | AB-01..10, AD-02..04 | M01, M02, M06, M07, M10 — all killed |
| P2 | A changed effect invalidates the prior authorization | same, plus the signed object identity equals the identity re-pinned at admission, and the executor acts through those pins | AB-01/02, TT-01..08 | M04, M16, M17, M18 — killed |
| P3 | A required observation cannot be replaced by a missing event | a declared effect with no counting sensor that saw it is graded `UNAVAILABLE`/`SELF_REPORTED`/`INSTRUMENTED`, never an external level; a covering sensor that did not see it makes the verdict `FAILED` | `test_property_grade_never_overstates`, EO-04, EO-06, OC-04/05 | M11, M12, M13 — killed |
| P4 | Contradictory evidence cannot produce an unqualified VERIFIED | `contradictions` non-empty ⇒ verdict `FAILED` (enforcer and verifier) | property test, CX-01..03 | M14 — killed |
| P5 | Revoked or expired authority cannot authorize a new action | checked at admission and immediately before each mutating call; recorded at completion | CR-01..06, AB-09 | M05 — killed |
| P6 | An incomplete transaction cannot be reported as fully rolled back | `FULLY_COMPENSATED` ⇔ every changed object is restored to the signed prior state by a VERIFIED run; the verifier recomputes this | RC-01..04 | M25 — killed |
| P7 | A receipt binds to the correct mission, action and policy version | these are inside the enforcer-signed receipt and the approver-signed authorization and are compared by the verifier | RR-02, AB-07 | (covered by signature checks; no separate mutant) |
| P8 | An observation method cannot claim more than it provides | sensors declare `observable`; a level is granted only for effect types the sensor declares; same key/process/method never corroborates; every grade carries the independence ceiling; the verifier rejects a stated level above the derived one | property tests, OC-03, OC-07, IE-05 | M11, M12, M20 — killed |
| P9 | Temporal proximity is not causation | `causal_path` follows only causal relations | CO-02, CO-04, graph unit test | M22 — killed |
| P10 | One authorization, one execution | once-ledger (threads, restart); verifier memory across receipts | AB-08, PV-03, PE-03, RR-03, ledger test | M03, M19, M23 — killed |
| P11 | Two independent implementations of the grading rules agree | `grade` (bridge) vs `derive_grade` (clean-room verifier) on 300 random cases | `test_property_two_implementations_agree` | — |

Mutation result: 26 of 26 killed (`mutation_results.json`). One mutant (M18, "follow the link at the target")
survived the first run: the corpus checked that the victim file was unchanged, and following the link still ended in
the inode comparison. The scenario now also requires that the link is never opened (opening a FIFO or device is itself
an effect); M18 is killed by TT-05. No mutant is classified as equivalent.

Assumptions: Ed25519 and SHA-256 are secure; the kernel implements `O_NOFOLLOW`, `O_EXCL`, descriptor-relative calls
and inotify as documented; the sensors' processes are not tampered with by the same user; the reader's sensor anchors
were obtained independently. State space: the generated cases use ≤4 declared effects over 4 resources and ≤3
sensors; races are injected at three fixed points, not explored exhaustively. Not modelled: multiple enforcers,
network effects, kernel or root compromise, timing side channels.