SPECIFICATION Spec
\* Quiescent states are legal: e.g. all tenants cleaned up with no pending
\* onboarding is a valid idle state (Claim/Mutate can always re-fire, but a
\* stuttering-only run is fine).
CHECK_DEADLOCK FALSE
CONSTANTS
    Users = {u1, u2}
    Tenants = {t1, t2}
    AnonSandbox = {t2}
    TokenIds = {k1, k2}
    svc = svc
INVARIANTS
    TypeOK
    OwnersWereClaimed
    NoAnonOwners
    MutatorsWereAuthorized
    TokensImplyOwnerMinted
    NoAnonTokens
    TokenMutatorsHadMintedTokens