class-a-downgrade-refusedformal: partial
A receipt cannot turn a relying-party-pinned Class-A approver key into a bare Class-B signature path by self-declaring a weaker key class.
quorum-separation-of-dutiesformal: verified
A quorum cannot count the initiator as an approver or let one device key fill two approval seats.
scoped-authority-is-pinnedformal: partial
An authority proof is accepted only under a relying-party-pinned registry issuer and only within its action, role, policy, time, currency, amount, organization, and delegation scope.
reliance-requires-pinned-profileformal: partial
A cryptographically valid packet still refuses reliance unless signed action material satisfies the relying party's pinned assurance, organization-bound authority, exact registry head and epoch floor, policy, revocation, issuer, and consumption profile.
revocation-is-pinned-and-freshformal: not modeled
Revocation state is accepted only under a pinned revoker key, for the exact target, and within the relying party's freshness window.
timestamp-proof-requires-pinned-tsaformal: not modeled
A timestamp token carries weight only when its imprint binds the expected receipt digest and its signer matches a relying-party-pinned TSA key.
evidence-challenge-is-durably-registered-and-consumedformal: partial
An AE-CHALLENGE binds the canonical action and governing policy, is exposed only after atomic durable registration of its exact body, and is consumed on the first valid evaluation attempt across workers and restarts.
durable-consumption-is-owner-fencedformal: verified
Across concurrent workers and process restarts, one receipt has at most one active reservation, and only its opaque owner token can commit or release it.
ambiguous-effect-is-never-auto-retriedformal: partial
After an external executor is invoked, an exception is treated as an indeterminate effect and the approval is consumed or frozen rather than made reusable.
aec-execution-is-action-keyed-and-fleet-fail-closedformal: partial
The stateful AEC execution gate pins custom component verifiers, verifier keys, human profiles, and the requirement at construction, captures the validated store and logger methods, and refuses transaction-scoped trust configuration. It reserves one non-expiring key derived only from the executor-bound canonical action digest before effect, so presenter-controlled decoy components, alternate proof forms, or post-construction method replacement cannot mint a fresh replay key for the same action. Production construction also requires an ownership-fenced durable consumption backend and a strict atomic shared-head evidence log that continues across replicas and restarts; the gate independently rehashes and exactly matches each acknowledgment, and successful atomic append readback must equal the submitted sequence, predecessor, identifier, and content.
rx-sidecar-minimizes-patient-dataformal: not modeled
Rx evidence artifacts reject unknown or direct patient and clinical fields, use pairwise patient references and keyed source-record commitments, export a projection rather than recursively copying the transaction, and disclose it only under a pinned audience, purpose, policy, retention, artifact, and key-scope profile.
verify-package-is-byte-reproducibleformal: not modeled
The verify SDK canonicalizes package file modes, packs twice to byte-identical tarballs, and the publish workflow attests and publishes that exact tarball before comparing the registry copy byte-for-byte.
python-release-artifacts-are-byte-reproducibleformal: not modeled
The Python verifier builds its wheel and source distribution twice under a pinned source epoch, attests and publishes those exact bytes, and refuses a downloaded PyPI wheel or source distribution whose bytes differ.
all-package-releases-use-verifiable-bytesformal: not modeled
Every declared npm and PyPI package release requires a version-bound owner dispatch and protected-environment approval or explicit recorded administrator bypass, tests source from an immutable tag on main, constructs reproducible package bytes, attests the exact artifact plus security and conformance manifests, publishes through OIDC, and compares every registry artifact byte-for-byte after publication.
model-to-matter-clearance-is-exact-and-single-useformal: not modeled
A Model-to-Matter presentation clears at most once only when all six evidence types verify under the executor's constructor-pinned profile, bind the same exact digest-only action, satisfy freshness and the pinned revocation provider, and survive durable challenge and action consumption. The production executor refuses transaction-scoped profile, store, revocation, time, and retry configuration and captures validated state methods against post-construction replacement.
aec-role-substitution-refusedformal: not modeled
EP-AEC returns allow only when the relying party independently pins both its requirement and the exact executor action. Presenter labels are non-authoritative. The ep-receipt human leg requires a fresh Section 6.2 Trust Receipt with Class-A WebAuthn, a pinned approver directory, RP audience, signed WebAuthn origin allowlist, policy hash, and log key; a bare operator-signed envelope is refused. The ep-quorum leg requires a fresh exact pinned policy plus RP audience, signed WebAuthn origin allowlist, context policy, and key-to-identity-to-role directory. These predicates execute identically in JavaScript, Python, and Go.