# Evolution 16 — formal assurance: what was checked, by what, and what that is not

**No theorem was proved and no model checker (TLA+, Alloy, Z3) was used.** Three lighter methods were applied to the
implementation itself. Each is bounded, and each result holds only inside its bound.

## Properties

| # | Property | Kind | Checked by |
|---|---|---|---|
| P1 | No consequential action is dispatched without a live admission | state invariant | exploration I2, I3; verifier `dispatch.admitted_first`; M16-03..05 |
| P2 | A dispatch is bound to the exact action, agent, authorization and mission version of its admission | state invariant | verifier `dispatch.bound_to_admitting_contract_version`; M16-23 |
| P3 | Revoked, expired or cancelled authority dispatches nothing new | temporal (after X, never Y) | exploration I2; thread test on cancellation |
| P4 | Delegated authority at dispatch is within every hop of a live chain to the principal | state invariant | verifier `dispatch.authority_live_at_dispatch` (independent recomputation) |
| P5 | An unresolved transaction is never reported as confirmed or rolled back, and the mission never completes over one | state invariant | exploration I4, I5; M16-14, M16-16 |
| P6 | A non-repeatable action is not dispatched twice for one outcome | state invariant | exploration I1; crash sweep; M16-01, M16-02 |
| P7 | A required verifier check that was not performed cannot yield VERIFIED | verdict rule | `evidence_no_witnessed_head`, CLI exit-code test |
| P8 | A failed check cannot yield VERIFIED | verdict rule | by construction of the verdict expression; 9 FAILED evidence families |
| P9 | A widening is never classified as anything but EXPANDING | function property | 200 single widenings + 400 random change sequences; two implementations agree |
| P10 | A contract version is installed at most once and only over the current head | state invariant | scenarios; 6-thread test; verifier `contract.*` |
| P11 | Recovery reproduces every recorded decision or refuses to start | determinism | replay equality test; divergence test; crash sweep |
| P12 | An unapproved skill candidate cannot enter the trusted path | — | **not checked by Evolution 16**; existing governed_evolution tests only |

## Method 1 — bounded exhaustive exploration (`recovery_explore.py`)

State space: one compensatable write action after a completed read; alphabet of 11 events (admit, three kinds of
dispatch outcome, crash, restart, honest observation, compensation, revoke, cancel, finalize); **all** sequences of
length 1 to 4: 11 + 121 + 1,331 + 14,641 = 16,104. Each is executed on a fresh real runtime with a simulated target;
invariants I1-I6 are checked after every event and I7 (verifier never FAILED on an honest journal, never VERIFIED over
an unresolved transaction) at the end. Result: `bounded_exploration.json`.

Assumptions: the observer is honest; one caller at a time; the target behaves like the simulator.
Excluded: sequences longer than 4; concurrency; dishonest observers; contract succession during a dispatch; actions of
other classes; more than one action in flight.

## Method 2 — mutation adequacy (`recovery_lab_mutations.py`)

25 single-site removals of runtime checks. A killed mutant shows a scenario depends on that check; it says nothing
about checks not in the list. Two checks are declared untestable in isolation because another layer enforces the same
thing (the mission-expiry test, and one of the two layers of M16-23).

## Method 3 — differential and property tests

Two independent implementations of the widening classifier (runtime and verifier) are compared on random inputs. The
verifier's transaction state machine and delegation check are independent re-implementations and are compared with the
runtime across all exploration sequences through I7. "Independent" here means separate code; **both were written by
the same author in the same session**, so a shared misunderstanding would not be caught.

## What this does not establish

Not a proof of all executions. Not a proof about the Evolution 15 decision logic, which is taken as given. Not a
statement about production. Not about cryptographic strength beyond using Ed25519 and SHA-256 as provided by the
`cryptography` library. The interleavings of threads were tested with a handful of thread tests, not explored.