# Evolution 7 — Formal verification

Run `e7-20261012T134603Z-5cbb38e7` · source revision `a97b94ddb6876c2266400e6303f3e578cb853833` (branch `ironclad-prompt8-qualification`, working tree not clean) · generated by `scripts/sovereign/evidence_pipeline_e7.py`

Solver: z3 5.1.0 · Python 3.14.4 · model file SHA-256 `3ea2fb7ffc415720629dfe811bcbceec5861b4a278d5106f7934d22211c275e4` ·
run time 0.208 s · command `python3 verification/sovereign/e7_cain_talos_z3.py`

**22 of 22 properties hold.** UNSAT / no_violation means no counterexample exists within the encoded model and its stated assumptions. It is a local model result, not a proof of the implementation and not evidence of production enforcement.

For each property the script runs three queries: the counterexample query (must be UNSAT, or "no violation" for
the exhaustive state exploration), a control (must be SAT: the guarded behaviour is reachable, so the property
is not vacuous), and a mutant with the control removed (must produce a counterexample).

| Id | Property | Kind | Result | Control | Mutant | Holds |
|---|---|---|---|---|---|---|
| F7-01 | No ALLOW without a valid signature by a configured trust root, bound issuer and key window | z3 | unsat | sat | sat | yes |
| F7-02 | No ALLOW on malformed, legacy or unknown-protocol envelopes | z3 | unsat | sat | sat | yes |
| F7-03 | No ALLOW without a usable clock, outside the validity window, or beyond the lifetime bound | z3 | unsat | sat | sat | yes |
| F7-04 | No ALLOW for a revoked key, revoked decision, or an envelope under the invalidation floor | z3 | unsat | sat | sat | yes |
| F7-05 | No ALLOW on any identity mismatch (audience, principal, tenant, agent, session) | z3 | unsat | sat | sat | yes |
| F7-06 | No ALLOW on action or target mismatch | z3 | unsat | sat | sat | yes |
| F7-07 | Exact authorization-to-execution binding: no ALLOW unless the request to be run is valid, hashes to the signed parameters_digest, and lies inside the signed scope | z3 | unsat | sat | sat | yes |
| F7-08 | No ALLOW on policy version or digest mismatch | z3 | unsat | sat | sat | yes |
| F7-09 | CAIN DENY is terminal; REQUIRE_APPROVAL needs a verified approval | z3 | unsat | sat | sat | yes |
| F7-10 | Replay resistance: no ALLOW for a consumed nonce | z3 | unsat | sat | sat | yes |
| F7-11 | Fail closed on ledger failure, non-durable ledger, or clock rollback | z3 | unsat | sat | sat | yes |
| F7-12 | No ALLOW for an unsupported enforcement profile | z3 | unsat | sat | sat | yes |
| F7-13 | Every one of the 34 checks is individually necessary and every verdict value is reachable | z3 | unsat | sat | sat | yes |
| F7-14 | The request is delivered to the worker only after ALLOW, a recorded execution intent and every required sandbox control being measured (fail closed on verifier, ledger, worker and sandbox failure) | z3 | unsat | sat | sat | yes |
| F7-15 | Scope monotonicity / privilege attenuation: the effective scope never exceeds the rule ceiling in read paths, write paths, network, ports, memory or time | z3 | unsat | sat | sat | yes |
| F7-16 | A replaced or newly created ledger cannot be used to replay: any envelope the old ledger could have consumed is refused by the new one (also covers the emergency floor) | z3 | unsat | sat | sat | yes |
| F7-17 | Bounded validity: an accepted envelope has at most max_ttl + tolerance seconds left, and none after exp | z3 | unsat | sat | sat | yes |
| F7-18 | No oracle before authentication: for an envelope that fails a pre-authentication check, the verdict is the same whatever the ledger, identity, policy or scope state is | z3 | unsat | sat | sat | yes |
| F7-19 | Concurrent consumption: with 2, 3 or 4 verifiers holding one envelope, at most one execution in every interleaving | explicit-state | no_violation | sat | violation_found | yes |
| F7-20 | Crash, restart and retry at any point never yield a second execution (durable ledger; and a ledger that lost its history refuses the envelope under the floor rule) | explicit-state | no_violation | sat | violation_found | yes |
| F7-21 | Revocation ordering: a revocation committed before the consumption transaction began always prevents execution | explicit-state | no_violation | sat | violation_found | yes |
| F7-22 | Ambiguous outcomes: an execution intent is started at most once; terminal states (including UNCERTAIN after a crash) never change, so nothing is retried automatically | explicit-state | no_violation | sat | violation_found | yes |

## What each property represents and assumes

**F7-01** — represents: TalosVerifyKernel._verify, steps for: algorithm, trust_root, signature, issuer, key_window. Assumptions and abstraction: Each check is abstracted to one Boolean that is true iff the real check passes. The model says nothing about whether the real check computes that Boolean correctly (e.g. that Ed25519 verification is sound); that link is the differential test E7-F-LINK-*.

**F7-02** — represents: TalosVerifyKernel._verify, steps for: structure, protocol. Assumptions and abstraction: Each check is abstracted to one Boolean that is true iff the real check passes. The model says nothing about whether the real check computes that Boolean correctly (e.g. that Ed25519 verification is sound); that link is the differential test E7-F-LINK-*.

**F7-03** — represents: TalosVerifyKernel._verify, steps for: clock, ttl, not_expired, not_future. Assumptions and abstraction: Each check is abstracted to one Boolean that is true iff the real check passes. The model says nothing about whether the real check computes that Boolean correctly (e.g. that Ed25519 verification is sound); that link is the differential test E7-F-LINK-*.

**F7-04** — represents: TalosVerifyKernel._verify, steps for: key_not_revoked, decision_not_revoked, floor. Assumptions and abstraction: Each check is abstracted to one Boolean that is true iff the real check passes. The model says nothing about whether the real check computes that Boolean correctly (e.g. that Ed25519 verification is sound); that link is the differential test E7-F-LINK-*.

**F7-05** — represents: TalosVerifyKernel._verify, steps for: audience, principal, tenant, agent, session. Assumptions and abstraction: Each check is abstracted to one Boolean that is true iff the real check passes. The model says nothing about whether the real check computes that Boolean correctly (e.g. that Ed25519 verification is sound); that link is the differential test E7-F-LINK-*.

**F7-06** — represents: TalosVerifyKernel._verify, steps for: action, target. Assumptions and abstraction: Each check is abstracted to one Boolean that is true iff the real check passes. The model says nothing about whether the real check computes that Boolean correctly (e.g. that Ed25519 verification is sound); that link is the differential test E7-F-LINK-*.

**F7-07** — represents: TalosVerifyKernel._verify, steps for: request_valid, binding, scope. Assumptions and abstraction: Each check is abstracted to one Boolean that is true iff the real check passes. The model says nothing about whether the real check computes that Boolean correctly (e.g. that Ed25519 verification is sound); that link is the differential test E7-F-LINK-*.

**F7-08** — represents: TalosVerifyKernel._verify, steps for: policy_version, policy_digest. Assumptions and abstraction: Each check is abstracted to one Boolean that is true iff the real check passes. The model says nothing about whether the real check computes that Boolean correctly (e.g. that Ed25519 verification is sound); that link is the differential test E7-F-LINK-*.

**F7-09** — represents: TalosVerifyKernel._verify, steps for: not_deny, approval. Assumptions and abstraction: Each check is abstracted to one Boolean that is true iff the real check passes. The model says nothing about whether the real check computes that Boolean correctly (e.g. that Ed25519 verification is sound); that link is the differential test E7-F-LINK-*.

**F7-10** — represents: TalosVerifyKernel._verify, steps for: nonce_fresh. Assumptions and abstraction: Each check is abstracted to one Boolean that is true iff the real check passes. The model says nothing about whether the real check computes that Boolean correctly (e.g. that Ed25519 verification is sound); that link is the differential test E7-F-LINK-*.

**F7-11** — represents: TalosVerifyKernel._verify, steps for: ledger_lookup, durable_ledger, consume_available, no_clock_rollback. Assumptions and abstraction: Each check is abstracted to one Boolean that is true iff the real check passes. The model says nothing about whether the real check computes that Boolean correctly (e.g. that Ed25519 verification is sound); that link is the differential test E7-F-LINK-*.

**F7-12** — represents: TalosVerifyKernel._verify, steps for: profile. Assumptions and abstraction: Each check is abstracted to one Boolean that is true iff the real check passes. The model says nothing about whether the real check computes that Boolean correctly (e.g. that Ed25519 verification is sound); that link is the differential test E7-F-LINK-*.

**F7-13** — represents: the whole decision procedure. Assumptions and abstraction: Same abstraction as F7-01..12.

**F7-14** — represents: TalosVerifyKernel.execute + talos_worker.run_confined/required_controls_missing. Assumptions and abstraction: Controls are Booleans meaning 'the launcher reported it measured this control' (and, for the PID namespace, 'the parent verified it in /proc'). The model does not establish that a measured control is effective against a given attack; the isolation tests E7-W-* observe that.

**F7-15** — represents: CainJitDecisionEngine._attenuate_scope and ResourceScope.is_within. Assumptions and abstraction: Path sets and port sets are modelled as 16-bit sets (membership of a path under a ceiling root is one bit); the component-wise path comparison itself is tested, not modelled (E7-A-090).

**F7-16** — represents: TalosDurableLedger._create_schema / consume_authorization_atomic floor rule. Assumptions and abstraction: Integer seconds. Assumes the verifier that accepted the envelope enforced iat <= now + allowance and that the old consumption happened no later than the new ledger's creation second. Does NOT cover restoring an older copy of the same ledger without raising the floor (documented limit).

**F7-17** — represents: TalosVerifyKernel._verify step 7 and validate_envelope (exp > iat). Assumptions and abstraction: Integer seconds on the kernel's own clock. A clock moved backwards is outside this model; the ledger high-water mark (X-series, E7-A-044) covers rollback.

**F7-18** — represents: ordering of TalosVerifyKernel._verify (signature before any ledger read). Assumptions and abstraction: Covers the verdict value only, not timing.

**F7-19** — represents: TalosDurableLedger.consume_authorization_atomic (BEGIN IMMEDIATE). Assumptions and abstraction: Check-and-insert is one atomic step, as SQLite provides for one database file on one host. Not a model of two ledger files or two hosts.

**F7-20** — represents: ledger durability + new-ledger invalidation floor + kernel.execute ordering. Assumptions and abstraction: Up to two crashes. 'Durable' assumes a committed SQLite transaction survives the crash. The volatile variant models ledger loss/replacement, not restore of an older copy.

**F7-21** — represents: revocation re-checked inside consume_authorization_atomic. Assumptions and abstraction: A revocation that commits after consumption does not stop an execution already authorised (bounded by the scope's wall-clock limit; cancellation of a running worker is not implemented).

**F7-22** — represents: talos_ledger._TRANSITIONS, transition_execution, reconcile_incomplete. Assumptions and abstraction: State machine only; that the kernel calls it in this order is tested (E7-L-010..012, E7-E-038).


## How the model is tied to the code

`CHAIN` in the model file lists the kernel's 34 checks in order with the verdict each returns.
`tests/sovereign/evolution_07/test_e7_formal_link.py` drives the real kernel into each single-failure state and
into seeded random multi-failure states and requires the kernel's verdict to equal the model's prediction; it
also requires every reason code in the kernel source to map to a modelled check and the reverse. Reordering,
removing or adding a check on either side fails the suite.

## Audit of the Evolution 6 model (18 invariants)

`verification/sovereign/e6_cain_talos_z3.py` still reports 18/18 UNSAT, and that result was never evidence about
the code: its verdict term includes `parameters_digest_match` and `worker_isolated`, and at the Evolution 6
baseline the kernel had no parameters-digest check at all (any command ran under any envelope for the same
action and target) and fell back to an unconfined child when Landlock setup raised. Nothing connected the
model to the implementation, so the drift was invisible. Each of its invariants has the form
"verdict == ALLOW and not guard" over a verdict defined as the conjunction of the guards, which is UNSAT by
construction. The Evolution 6 "8/8 mutations killed" were eight tests that fed invalid inputs to unmodified
code; no code was mutated.

## Excluded from every model

Soundness of Ed25519 and SHA-256; correctness of CPython, SQLite, the Linux kernel, Landlock and seccomp;
timing and other side channels; behaviour on any host other than the build host; anything about production.