$ /usr/bin/python3 verification/sovereign/e7_cain_talos_z3.py --json /root/cain-studio-platform/reports/sovereign/evolution-07/formal_results.json
# exit_code=0 seconds=0.35

F7-01  HOLDS  result=unsat control=sat mutant=sat  No ALLOW without a valid signature by a configured trust root, bound issuer and key wind
F7-02  HOLDS  result=unsat control=sat mutant=sat  No ALLOW on malformed, legacy or unknown-protocol envelopes
F7-03  HOLDS  result=unsat control=sat mutant=sat  No ALLOW without a usable clock, outside the validity window, or beyond the lifetime bou
F7-04  HOLDS  result=unsat control=sat mutant=sat  No ALLOW for a revoked key, revoked decision, or an envelope under the invalidation floo
F7-05  HOLDS  result=unsat control=sat mutant=sat  No ALLOW on any identity mismatch (audience, principal, tenant, agent, session)
F7-06  HOLDS  result=unsat control=sat mutant=sat  No ALLOW on action or target mismatch
F7-07  HOLDS  result=unsat control=sat mutant=sat  Exact authorization-to-execution binding: no ALLOW unless the request to be run is valid
F7-08  HOLDS  result=unsat control=sat mutant=sat  No ALLOW on policy version or digest mismatch
F7-09  HOLDS  result=unsat control=sat mutant=sat  CAIN DENY is terminal; REQUIRE_APPROVAL needs a verified approval
F7-10  HOLDS  result=unsat control=sat mutant=sat  Replay resistance: no ALLOW for a consumed nonce
F7-11  HOLDS  result=unsat control=sat mutant=sat  Fail closed on ledger failure, non-durable ledger, or clock rollback
F7-12  HOLDS  result=unsat control=sat mutant=sat  No ALLOW for an unsupported enforcement profile
F7-13  HOLDS  result=unsat control=sat mutant=sat  Every one of the 34 checks is individually necessary and every verdict value is reachabl
F7-14  HOLDS  result=unsat control=sat mutant=sat  The request is delivered to the worker only after ALLOW, a recorded execution intent and
F7-15  HOLDS  result=unsat control=sat mutant=sat  Scope monotonicity / privilege attenuation: the effective scope never exceeds the rule c
F7-16  HOLDS  result=unsat control=sat mutant=sat  A replaced or newly created ledger cannot be used to replay: any envelope the old ledger
F7-17  HOLDS  result=unsat control=sat mutant=sat  Bounded validity: an accepted envelope has at most max_ttl + tolerance seconds left, and
F7-18  HOLDS  result=unsat control=sat mutant=sat  No oracle before authentication: for an envelope that fails a pre-authentication check, 
F7-19  HOLDS  result=no_violation control=sat mutant=violation_found  Concurrent consumption: with 2, 3 or 4 verifiers holding one envelope, at most one execu
F7-20  HOLDS  result=no_violation control=sat mutant=violation_found  Crash, restart and retry at any point never yield a second execution (durable ledger; an
F7-21  HOLDS  result=no_violation control=sat mutant=violation_found  Revocation ordering: a revocation committed before the consumption transaction began alw
F7-22  HOLDS  result=no_violation control=sat mutant=violation_found  Ambiguous outcomes: an execution intent is started at most once; terminal states (includ
22/22 properties hold (z3 5.1.0, 0.208s)