SPECIFICATION Spec
\* Quiescent states are legal: an account sitting idle with credentials and no
\* live sessions (or the pristine pre-signup state) is a valid resting point;
\* a stuttering-only run is fine.
CHECK_DEADLOCK FALSE
CONSTANTS
    MaxCreds = 3
INVARIANTS
    TypeOK
    NeverOrphaned
    NoPrivilegeEscalationDelete
    PasskeySurvivesPhishedKey