Invitation

Atom grounded on Final Critique 5 — 2026-06-23 12 invariants TLA+ model buggy twin ×2 regulated · via 1 composer security overlay composed by 1

Derived card — generated from the corpus (status line, invariant headers, sibling formal-model files, Composes edges). The specification below is canonical. composition graph →

Table of contents

Invitation

Summary

Invitation tracks the life of an invitation issued to an outside party to join something — a new employee, a customer, a collaborator, a patient. It answers “what is the state of this invitation, and who accepted it?” An invitation is issued before the invitee even has an identity in the system, which is exactly what makes it useful: it is the bridge from outsider to registered participant. Each invitation is identified by a random token that the invitee presents to act on it, and it starts Pending. It is resolved by a write to one of three recorded end states — Accepted (recording, permanently, the identity that joined), Declined (a deliberate refusal, recorded as its own outcome), or Revoked (the inviter withdrew it). If instead its time window simply passes, the invitation is shown as Expired — a status worked out on the fly by comparing the clock to the deadline, not written into the record. Resolving exactly once is the core guarantee: after it is resolved by a write, any further attempt is told it is already resolved. This also cleanly handles two people trying to accept at the same time — one wins, the other is told; and an attempt on a lapsed (Expired) invitation is told it has expired. The key moment is acceptance, where a concrete identity is bound to what may have started as an invitation to an unknown party. Declined is what sets this apart from a plain bearer token: a refusal is a recorded human decision, distinct from simply never using the invitation. It deliberately does not handle the credential setup, identity record, or login that usually follow acceptance — those are separate patterns.

Intent

Systems that admit external entities — new employees joining an organization, customers enrolling in a service, collaborators gaining access to a shared workspace, patients registering with a provider — face a structural challenge: the invitation must be issued before the invitee’s system identity exists, yet the moment of acceptance is when the system identity must be established. The invitation is the bridge between “external stranger” and “registered participant,” and it must carry a record of the entire arc: who invited whom, when, whether the invitee responded, and — at the critical moment of acceptance — which identity was bound.

The pattern isolates that lifecycle record from the surrounding machinery. Invitation does not implement the credential registration that follows acceptance — that is Credential’s surface (atom #11). It does not implement the identity record that the accepted invitee becomes — that is Party Identity’s surface. It does not implement the session issued to the newly accepted participant — that is Session’s surface. It does not implement the onboarding workflow that sequences all of these steps — that is External Onboarding’s surface. Invitation answers one structural question: what is the current state of this invitation, and if it was accepted, who accepted it? The answer is derivable from the invitation record alone.

The Declined terminal state is what distinguishes Invitation from Capability (atom #13) at the EOS Pass 2 boundary. Both atoms use bearer-token transport: the holder of a token presents it to resolve the invitation or redeem the capability. Both are time-bounded; both can be revoked. The structural difference is that Declined represents a deliberate human decision — a named participant chose to refuse — which is semantically distinct from the invitation simply not being used (which is shown as the derived Expired status — a read-time projection, not a stored outcome). Capability has no declined state because a bearer either redeems a capability or they do not; the non-use is not a decision that the system records as a first-class outcome. Invitation has Declined because a potential participant’s refusal matters to the system’s audit record independently of whether the invitation token was simply never presented.

This is a freestanding atom in the EOS (Essence of Software — Daniel Jackson’s framework for specifying software concepts as freestanding, composable units) sense. It has its own state (the invitation record and its resolution), its own actions (initiate, accept, decline, revoke), and its own operational principles (single-resolution, expiry-is-derived, opaque invitee at initiation, identity binding at acceptance). It does not implement the downstream provisioning that follows acceptance, the notification that delivers the invitation token, or the policy governing who may invite whom. Each is a composing-pattern concept; see Composition notes.

Structure

Identity model

Every invitation known to the system has an Invitation Token — an opaque, cryptographically random, immutable, system-generated value produced by Initiate. The token is both the record’s identity and the bearer credential the invitee presents to Accept or Decline. The token’s security properties follow the same reasoning as Capability: it must be unguessable and unpredictable.

The fields set on Initiate — Inviter Ref, Invitee Ref, Context, Initiated At, Expires At — are immutable properties of the record. Expires At is computed once at Initiate from the injected clock (Expires At = Now + TTL) and stored; it is the sole input the expiry derivation needs thereafter. The resolution fields (Accepting Identity Ref, Accepted At, Declined At, Revoked At, Revoked By Ref, Revocation Reason) are null until the relevant terminal write fires and immutable once set. There is no expired_at field: expiry is derived at read time from Expires At and the clock, never written, so there is no stored expiry timestamp to keep consistent.

Invitee Ref is optional at Initiate time: the inviting actor may not know the invitee’s system identity when the invitation is created (the invitee may not yet be registered in any system). Whether the Invitee Ref resolves to a known identity, matches the Accepting Identity Ref, or is null at all are matters the atom treats as valid operating states. The composing pattern decides what to do with any mismatch.

Tokens are not reused after an invitation reaches a terminal state.

Inputs and Outputs

Actions: The current clock reading and the token are pipeline-injected at the I/O seam (the execution contract’s clock_t and id_t, supplied at Step 3 — not read inside the transition, not trusted from the caller, and not action parameters). The injected clock is consumed for two clearly separated purposes: stamping immutable timestamps on a write (execution time), and evaluating the pure expiry derivation in a guard (no write). It therefore appears in no signature below. See the Logic-confinement note in Decision points.

Initiate — (Projected contract: initiate(inviter_ref, invitee_ref, context, ttl) → invitation_token | rejected(invalid-request | storage-failure))
Accept — (Projected contract: accept(invitation_token, accepting_identity_ref) → accepted | rejected(invalid-request | expired | already-resolved(state) | not-known | storage-failure))
Decline — (Projected contract: decline(invitation_token) → declined | rejected(expired | already-resolved(state) | not-known | storage-failure))
Revoke — (Projected contract: revoke(invitation_token, revoked_by_ref, reason) → revoked | rejected(invalid-request | expired | already-resolved(state) | not-known | storage-failure))

There is no expire action. A lapsed invitation needs no write to become Expired; expiry is surfaced by the read projection below. already-resolved(state) names a stored terminal only — Accepted, Declined, or Revoked; the lapsed-window case is the distinct expired rejection.

Read surface (render time):

Read — (Projected contract: read(filter) → records) — each returned record carries its stored fields plus a derived Effective Status: Expired when Status = Pending ∧ Now ≥ Expires At, otherwise the stored Status. Effective Status is a pure projection over the record and the pipeline-injected clock Now (supplied at the I/O seam, not a parameter); it is never stored.

Inputs:

Inviter Ref — an opaque reference to the actor issuing the invitation. Recorded as an immutable property. Non-null and non-empty required.
Invitee Ref — an opaque reference to the intended invitee. Optional — may be null if the inviting actor does not know the invitee’s system identity at initiation time. When supplied, stored as an immutable property and never validated by the atom.
Context — an opaque descriptor of what the invitee is being invited to join (e.g., an organization identifier, a workspace reference, a role). Opaque to the atom; interpreted by the composing pattern. Non-null and non-empty required.
TTL — a duration value specifying how long the invitation is valid. Null uses the deployment’s default invitation TTL. Expires At = Initiated At + TTL. Must be positive if supplied.
Invitation Token — the bearer token the invitee presents to Accept, Decline; the inviting party or administrator presents to Revoke.
Accepting Identity Ref — an opaque reference to the identity that is accepting the invitation. Supplied to Accept. This is the binding: whoever calls Accept provides the identity that will be permanently recorded as having accepted. Non-null and non-empty required.
Revoked By Ref — opaque reference to the actor withdrawing the invitation. Non-null and non-empty required.
Reason — caller-supplied reason for revocation. Non-null and non-empty required.
Now (not a parameter — pipeline-injected) — the clock reading (clock_t), supplied by the pipeline at the I/O seam, not passed by the caller and not present in any action signature. It is not caller-trusted and is not read inside any transition. It is used only to stamp immutable write timestamps (execution time) and to evaluate the pure expiry derivation in a guard and in Read’s Effective Status projection (no write).

Outputs:

The current set of invitation records. For each: Invitation Token, Inviter Ref, Invitee Ref (nullable), Context, Initiated At, Expires At, Status (the stored status: Pending, Accepted, Declined, or Revoked), Accepting Identity Ref (nullable), Accepted At (nullable), Declined At (nullable), Revoked At (nullable), Revoked By Ref (nullable), Revocation Reason (nullable), and the derived Effective Status (the stored Status, except Expired when Status = Pending ∧ Now ≥ Expires At).
Initiate returns a new Invitation Token on success, or a rejection.
Accept returns accepted on success, or a rejection — expired if the window has lapsed (Now ≥ Expires At), or already-resolved(state) if the invitation was already written to a stored terminal.
Decline returns declined on success, or a rejection (expired or already-resolved(state)).
Revoke returns revoked on success, or a rejection (expired or already-resolved(state)).

State

Each invitation record carries a stored Status field. The state machine has one non-terminal state and three stored terminal states; Expired is a fourth status that is derived, never stored:

Pending — the invitation has been issued and awaits resolution. The only non-terminal stored state.
Accepted — the invitation was accepted and an identity was bound. Stored terminal.
Declined — the invitation was deliberately declined. Stored terminal.
Revoked — the invitation was withdrawn before resolution. Stored terminal.
Expired (derived — never stored) — a still-Pending record whose window has lapsed (Now ≥ Expires At). Computed at read time by the Effective Status projection from the immutable Expires At and the injected clock; no transition fires and no field is written when an invitation lapses.

Transitions (every write below stamps its timestamp from the injected Now; no transition reads the clock internally). Expiry is listed for contrast: it is not a transition and writes nothing.

action	from	to	guard (against injected Now)	stamps (writes)	result
Initiate	(no record)	Pending	valid request (TTL positive or default)	fresh Invitation Token; Inviter Ref; Invitee Ref; Context; Initiated At = Now; Expires At = Now + TTL	the new Invitation Token
Accept	Pending	Accepted	Now < Expires At	Accepting Identity Ref; Accepted At = Now	`accepted`
Decline	Pending	Declined	Now < Expires At	Declined At = Now	`declined`
Revoke	Pending	Revoked	Now < Expires At	Revoked At = Now; Revoked By Ref; Revocation Reason	`revoked`
expiry (derived — not a transition)	Pending	Pending (unchanged)	Now ≥ Expires At	nothing written	shown Expired

The transitions in detail, with the single-resolution precedence, atomicity, and writes-nothing semantics that the table abbreviates:

initiate(inviter_ref, invitee_ref, context, ttl) → a new invitation record is created in Pending status with a fresh injected Invitation Token, the supplied Inviter Ref, Invitee Ref (nullable), Context, Initiated At = Now, and Expires At = Now + TTL (or default) — where Now is the pipeline-injected clock at the seam. Returns Invitation Token.
accept(invitation_token, accepting_identity_ref) → permitted only when stored Status = Pending and Now < Expires At; status transitions from Pending to Accepted; Accepting Identity Ref and Accepted At = Now are recorded. Returns accepted. (When Now ≥ Expires At the guard returns expired and writes nothing.)
decline(invitation_token) → permitted only when stored Status = Pending and Now < Expires At; status transitions from Pending to Declined; Declined At = Now is recorded. Returns declined.
revoke(invitation_token, revoked_by_ref, reason) → permitted only when stored Status = Pending and Now < Expires At; status transitions from Pending to Revoked; Revoked At = Now, Revoked By Ref, and Revocation Reason are recorded. Returns revoked.
Expiry is not a transition. When Now ≥ Expires At, a Pending record is shown as Expired by Read’s Effective Status projection; nothing is written, no scheduler is required, and there is no expire action. This is the “derive the idealization, do not lag it with a stored flag” discipline — the lapsed state is computed from Expires At and the clock, not remembered.
(no transitions out of Accepted, Declined, or Revoked; Expired is derived, so nothing transitions into or out of it.)

The non-mutating render-time surface of this state machine is Read (read(filter), defined in Inputs and Outputs): it reads stored state and computes each record’s derived Effective Status against the pipeline-injected clock. Read fires no transition and writes nothing; it is the only surface that surfaces the derived Expired status.

Each invitation record carries:

Invitation Token — opaque, cryptographically random, immutable, system-generated. Set on Initiate. Never changes. The bearer credential.
Inviter Ref — opaque reference to the inviting actor. Set on Initiate. Never changes.
Invitee Ref — opaque reference to the intended invitee. Nullable. Set on Initiate. Never changes.
Context — opaque descriptor of what the invitee is being invited to join. Set on Initiate. Never changes.
Initiated At — wall-time when Initiate was called. Immutable.
Expires At — absolute expiry time. Set on Initiate. Immutable. Never null.

Status — the stored status: Pending

Accepted

Declined

Revoked. Set to Pending on Initiate; immutable once written to a terminal. The derived Expired is not a value of this field — it appears only in the Effective Status read projection.

Accepting Identity Ref — the identity that accepted the invitation. Null until Accept fires. Immutable once set.
Accepted At — set when status transitions to Accepted. Null otherwise. Immutable once set.
Declined At — set when status transitions to Declined. Null otherwise. Immutable once set.
Revoked At — set when status transitions to Revoked. Null otherwise. Immutable once set.
Revoked By Ref — opaque reference to the revoking actor. Null until revocation. Immutable once set.
Revocation Reason — caller-supplied reason string. Null until revocation. Immutable once set.

Flow

Inviting actor creates an invitation. Calls initiate(inviter_ref, invitee_ref, context, ttl) → invitation_token. The atom creates the record and returns the token. The inviting actor delivers the token to the invitee through an appropriate out-of-band channel (email link, direct message, printed QR code).
Invitee accepts. Calls (or the system calls on their behalf after presenting the token) accept(invitation_token, accepting_identity_ref) → accepted. The atom records the accepting identity and transitions the invitation to Accepted. The composing pattern (e.g., External Onboarding) proceeds to create a Party Identity record, register a Credential, and issue a Session.
Invitee declines. Calls decline(invitation_token) → declined. The atom records the refusal and transitions the invitation to Declined. The composing pattern notifies the inviting actor and closes the onboarding arc.
Invitation lapses (expiry, derived). The deadline passes without resolution. No action and no write are required: a still-Pending record now reads as Expired via Read’s Effective Status projection (Now ≥ Expires At). A subsequent Accept/Decline/Revoke on it is rejected expired (its guard compares the injected Now to Expires At, writing nothing). A composing pattern that wants to notify the inviting actor reads the effective status; the record itself is untouched.
Inviting actor revokes. Calls revoke(invitation_token, revoked_by_ref, reason). The atom transitions to Revoked and records the attribution. Future action attempts return already-resolved(Revoked).

Decision points

Logic confinement (clock and id). The clock and the token are pipeline-injected at the I/O seam, never produced inside a transition and never action parameters. The execution contract reads the clock once and supplies Now (clock_t) at the seam (Step 3); it likewise supplies the fresh Invitation Token (the injected id_t) to Initiate. Neither appears in any signature above — they are consumed inside the atom by exactly two confined uses. First, the pure expiry guard: a guard’s expiry test is a pure function of the stored record and the injected Now — is_expired(record, now) ≜ record.status = Pending ∧ now ≥ record.expires_at — and it writes nothing. Second, the timestamp stamps: the only clock writes are the immutable timestamps inside a committed transition (Initiated At, Accepted At, Declined At, Revoked At), each stamped from the same injected Now. Expiry itself never writes; it is surfaced only by Read’s Effective Status projection (which consumes the same injected clock). Rejection priority for the resolving writes: Not Known → already-resolved(state) → expired → Invalid Request → Storage Failure.

At initiate(inviter_ref, invitee_ref, context, ttl):

Inviter Ref and Context must be non-null and non-empty; otherwise Invalid Request.
Invitee Ref may be null — the atom permits invitations whose intended recipient is not yet a known system entity. Whether the deployment permits null Invitee Ref is a deployment-configuration decision.
TTL must be positive if supplied; null uses the deployment default. Zero or negative is Invalid Request. The deployment default must be configured; absent, Invalid Request.
Initiated At = Now and Expires At = Now + TTL are computed once from the injected Now and stored immutably.
If the store write fails, Storage Failure is returned with no partial record.

At accept(invitation_token, accepting_identity_ref):

The atom looks up the invitation by Invitation Token. If no record is found, Not Known.
If the stored Status is a terminal (Accepted, Declined, or Revoked), already-resolved(state) naming that stored terminal. This is the single-resolution invariant in action.
Expiry guard (derived, no write): if is_expired(record, now) — stored Status = Pending ∧ Now ≥ Expires At — return expired. The record is left Pending; nothing is written. (A reader sees Effective Status = Expired.)
Accepting Identity Ref must be non-null and non-empty; otherwise Invalid Request.
The transition to Accepted and the writes of Accepting Identity Ref and Accepted At = Now are atomic. Under concurrent Accept calls, exactly one commits the transition; all others receive already-resolved(Accepted).
If the store write fails, Storage Failure is returned; the record remains Pending.
The atom does not validate that Accepting Identity Ref matches Invitee Ref. Whether the accepting identity was the intended invitee belongs to the composing pattern.

At decline(invitation_token):

The atom looks up the invitation by Invitation Token. If no record, Not Known.
If the stored Status is a terminal, already-resolved(state).
Expiry guard (derived, no write): if is_expired(record, now), return expired; the record is left Pending and nothing is written.
The transition to Declined and the write of Declined At = Now are atomic. If the store write fails, Storage Failure; the record remains Pending.
Decline takes no identity argument: the declining actor’s identity is not recorded. The deliberate refusal is recorded as the stored terminal Declined, not as an attribution record. Whether the declining actor is the intended invitee is not validated. Composing patterns that need to record who declined may do so in their own records.

At revoke(invitation_token, revoked_by_ref, reason):

The atom looks up the invitation by Invitation Token. If no record, Not Known.
If the stored Status is a terminal, already-resolved(state).
Expiry guard (derived, no write): if is_expired(record, now), return expired; nothing is written. (A caller wishing to end a Pending invitation before its window lapses calls Revoke while Now < Expires At; once lapsed, the invitation already reads Expired and needs no withdrawal.)
Revoked By Ref and Reason must be non-null and non-empty; otherwise Invalid Request.
The transition to Revoked and the writes of Revoked At = Now, Revoked By Ref, and Revocation Reason are atomic. If the store write fails, Storage Failure.

(There is no expire action: a lapsed invitation requires no write to be Expired — see the expiry guard above and Read’s Effective Status projection.)

Behavior

Single-resolution is the atom’s central invariant. Every write that resolves an invitation — Accept, Decline, Revoke — checks the stored status as its first operation. If the stored status is already a terminal (Accepted, Declined, Revoked), the action returns already-resolved(state) without modifying any record. The check-and-commit from Pending to a stored terminal must be atomic (see Invariant 2): under concurrent resolving writes, exactly one commits and the rest see already-resolved. An implementation that writes two terminal states for one invitation has violated the atom’s core contract.
Expiry is derived, not written. When Now ≥ Expires At, a still-Pending invitation is shown Expired by Read’s Effective Status projection, and a resolving write attempted on it is rejected expired — but no record is written, there is no expired_at field, and there is no expire action. The clock that decides expiry is the injected Now, consumed by a pure derivation; it is never read inside a transition and never lags behind a stored flag. This is the “derive the idealization, do not lag it with a flag” discipline (see pressure-testing.md §Formal-model authoring pitfalls).
Accept binds an identity; Decline does not. Accept requires Accepting Identity Ref and records it permanently. Decline records only Declined At. This asymmetry is intentional: acceptance creates a system relationship (a new participant joined); declination closes the open invitation without creating a relationship. Whether to record who declined is a composing-pattern decision.
Opaque invitee at initiation is a feature, not a gap. The Invitee Ref field is optional and the atom never validates it against the Accepting Identity Ref at accept time. This accommodates the common real-world scenario where an invitation is sent to an email address that does not yet correspond to any system identity, and the identity is only created at acceptance time. The composing External Onboarding pattern decides what relationship between Invitee Ref and Accepting Identity Ref is required by the deployment.
Declined is a named stored terminal, not a fallback. A declined invitation is not a lapsed (derived Expired) invitation and is not a revoked one. It represents a deliberate act by a party who held the invitation token and chose to refuse. An implementation that collapses Declined into the derived Expired (treating a refusal as mere non-use) loses the structural distinction. The audit record should distinguish “was never opened / the window lapsed” (the derived Expired), “was seen and refused” (stored Declined), and “was withdrawn by the inviter” (stored Revoked).
already-resolved(state) carries the stored terminal; expired is distinct. When a write is called on a stored-resolved invitation, the rejection includes the stored terminal so the caller knows what resolution occurred: already-resolved(Accepted) signals something different than already-resolved(Declined) or already-resolved(Revoked). A write on a lapsed invitation (still-Pending, Now ≥ Expires At) instead yields the distinct expired rejection — the invitation was never written to a terminal; its window simply closed.

Feedback

Each successful action produces an observable, measurable change:

After Initiate — a new invitation record appears in Pending status with a fresh Invitation Token, Inviter Ref, Invitee Ref (nullable), Context, Initiated At, and Expires At. Total record count increases by one. The token is returned to the caller.
After Accept — Status transitions to Accepted; Accepting Identity Ref and Accepted At are set.
After Decline — Status transitions to Declined; Declined At is set.
After Revoke — Status transitions to Revoked; Revoked At, Revoked By Ref, and Revocation Reason are set.
On expiry — no change: when Now ≥ Expires At, a still-Pending record’s Effective Status reads Expired, but no field is written, the record count does not change, and no transition fires. Expiry is observable only through Read (the derived Effective Status), never through a write.

Rejected actions produce named rejection codes observable to the caller. already-resolved(state) carries the stored terminal that blocked the action; expired signals a lapsed (still-Pending, past-window) invitation. Together they give the caller a complete picture of why the invitation cannot be acted upon.

The invitation store is queryable. Per-record fields, and each record’s derived Effective Status, are observable to authorized administrative surfaces. Composing patterns may query by Inviter Ref to list pending invitations for an actor, by Context to audit onboarding activity for a specific workspace, or by Effective Status to generate acceptance-rate or lapse-rate metrics.

Invariants

Invariant 1 — Initiation immutability. Once an invitation record is created, Invitation Token, Inviter Ref, Invitee Ref, Context, Initiated At, and Expires At never change. The resolution fields are null until the terminal write fires and immutable once set. (There is no expired_at resolution field — expiry is derived, Invariant 12.)

Invariant 2 — Single-resolution (by write). An invitation is resolved by at most one write to a stored terminal state — Accepted, Declined, or Revoked — and no further write is permitted after that. Any write called on a stored-resolved invitation returns already-resolved(state). The check-and-commit from Pending to a stored terminal must be atomic, so that under concurrent resolution attempts exactly one commits. Expiry is not a resolution: a Pending invitation whose window lapses is never written; it is shown Expired by derivation (Invariant 12), and any write on it is rejected expired.

Invariant 3 — Acceptance binds identity. When an invitation transitions to Accepted, Accepting Identity Ref and Accepted At are recorded atomically with the status transition. A record with Status = Accepted and a null Accepting Identity Ref is evidence of an implementation defect. The Accepting Identity Ref is immutable once set.

Invariant 4 — Opaque invitee at initiation. Invitee Ref may be null at Initiate time. The atom never validates Invitee Ref against Accepting Identity Ref at Accept time. These are two independent, opaque references; whether they represent the same real-world entity belongs to the composing pattern.

Invariant 5 — Three structurally distinct stored terminals; Expired is derived. The stored terminals are distinguishable in the record store. A record with Status = Accepted has non-null Accepting Identity Ref and Accepted At. A record with Status = Declined has non-null Declined At. A record with Status = Revoked has non-null Revoked At, Revoked By Ref, and Revocation Reason. No two stored terminals share an identical field pattern. Expired is not a stored terminal and carries no fields of its own — it is the derived Effective Status of a Pending record with Now ≥ Expires At (Invariant 12). An implementation that stores Expired, adds an expired_at field, or collapses two stored terminals into one representation violates this invariant.

Invariant 6 — already-resolved carries the stored terminal; lapse is expired. Every rejection of a write on a stored-resolved invitation includes the stored terminal name in the payload: already-resolved(Accepted), already-resolved(Declined), or already-resolved(Revoked). A bare already-resolved without the state name is not conformant. A write on a lapsed invitation (still-Pending, Now ≥ Expires At) is rejected with the distinct reason expired, never already-resolved(Expired) — there is no stored Expired to name.

Invariant 7 — Expiry deadline immutability. Expires At is computed once at Initiate from the injected Now and never mutated; it is the sole stored input to the expiry derivation (Invariant 12). Extending validity requires initiating a new invitation (a still-Pending original may be Revoked first); the deadline of an existing invitation is never moved.

Invariant 8 — Revocation attribution completeness. Every invitation record with Status = Revoked has non-null Revoked At, Revoked By Ref, and Revocation Reason. A Revoked record missing any of these is evidence of a process violation.

Invariant 9 — Every invitation has a finite lifetime. Expires At is never null. Invitations that do not expire are not expressible; an implementation that initiates invitations without an Expires At violates this invariant. The derived Expired status (Invariant 12) depends on this field always being present.

Invariant 10 — Invitation durability. Once Initiate returns an Invitation Token, the invitation record is durably persisted. A Storage Failure rejection guarantees no partial record was written. The atom provides no deletion surface.

Invariant 11 — Token uniqueness. No two invitation records share an Invitation Token across the lifetime of the system. The token is the injected id_t; a write that would reuse an existing Invitation Token is rejected as Storage Failure, so uniqueness is store-enforced, not merely probabilistic. Tokens are not reused after an invitation reaches a terminal state. This guarantees lookup determinism: a token resolves to exactly one invitation record, and actions on that token are unambiguous.

Invariant 12 — Expiry is derived, never written. No invitation record carries a stored Expired status or an expired_at field. An invitation’s Expired condition is the value of the pure projection effective_status(record, now) = Expired ⟺ (status = Pending ∧ now ≥ expires_at), computed at read time from the immutable Expires At and the injected clock Now. The clock is never read inside a transition, and no write fires when an invitation lapses. This is what lets single-resolution (Invariant 2) range over writes alone, and it removes the stored-flag-that-lags-the-clock failure mode (see pressure-testing.md §Formal-model authoring pitfalls).

Invariants 2 and 3 together give the onboarding integrity property — the identity binding at acceptance is trustworthy because it is produced by exactly one atomic write, never overwritten, and requires a non-null identity at call time. Invariant 4 (opaque invitee at initiation) is what makes Invitation usable before the invitee has a system identity. Invariants 5 and 12 together are what make the audit record informative: an external evaluator reading the invitation store can distinguish every stored resolution path and can compute the derived Expired status from Expires At and the read-time clock.

Examples

New employee onboarding — accept

An HR system initiates an invitation for a new hire:

initiate(inviter_ref: hr_admin_h01, invitee_ref: null, context: "org::acme::dept::engineering", ttl: 604800) → invitation_token: tok_inv_g7h2k1

Invitee Ref is null because the new hire does not yet have a system identity. The pipeline injects the seam clock — here 2026-09-01T09:14:00Z — so Initiated At = Now and Expires At = Initiated At + 7 days.

The HR system emails the new hire a link embedding the token. On their first day, the new hire clicks the link and creates their account. The onboarding handler calls:

accept(invitation_token: tok_inv_g7h2k1, accepting_identity_ref: user_u114) → accepted

The pipeline injects the seam clock 2026-09-08T09:14:00Z. The atom checks the stored Status = Pending and Now < Expires At (the 7-day window is still open), then transitions the invitation to Accepted, recording accepting_identity_ref: user_u114 and accepted_at: 2026-09-08T09:14:00Z (stamped from the injected Now). These fields are now immutable. The composing External Onboarding pattern proceeds: it creates a Party Identity record for user_u114, registers their credential, and issues their first session.

Workspace collaboration — decline

A user receives an invitation to join a shared project workspace:

initiate(inviter_ref: user_u91, invitee_ref: user_u55, context: "workspace::project-alpha", ttl: 172800) → invitation_token: tok_inv_p4q9r2

The invitee sees the invitation in their notification panel and clicks “Decline”:

decline(invitation_token: tok_inv_p4q9r2) → declined

The pipeline injects the seam clock 2026-10-15T11:22:00Z. The atom transitions to Declined, recording declined_at: 2026-10-15T11:22:00Z. The inviting user_u91 is notified that the invitation was declined. The invitation record is permanently Declined — it cannot be accepted, re-declined, revoked, or expired. Any subsequent action returns already-resolved(Declined).

Invitation revoked before use

An administrator initiates an invitation but then discovers the intended recipient should not be admitted:

initiate(inviter_ref: admin_a01, invitee_ref: user_u77, context: "org::acme::role::contractor", ttl: 86400) → invitation_token: tok_inv_c2d8e3 (seam clock 2026-06-30T07:00:00Z)

revoke(invitation_token: tok_inv_c2d8e3, revoked_by_ref: admin_a01, reason: "contractor-engagement-cancelled") → revoked (seam clock 2026-06-30T08:00:00Z)

The atom transitions to Revoked, recording Revoked At, revoked_by_ref: admin_a01, and revocation_reason: "contractor-engagement-cancelled". If the intended recipient had received the link and attempts to use it:

accept(tok_inv_c2d8e3, accepting_identity_ref: user_u77) → rejected(already-resolved(Revoked)) (seam clock 2026-06-30T09:00:00Z)

The window is still open (Now < Expires At), so this is not an expired rejection: the caller learns the invitation was Revoked — not merely lapsed or already accepted.

Rejection paths

Accept — already-resolved(Accepted) (concurrent attempt): Two requests to accept the same invitation arrive simultaneously (both at seam clock 2026-09-08T09:14:00Z). The first commits atomically: accept(tok_inv_g7h2k1, user_u114) → accepted. The second arrives microseconds later and finds stored Status = Accepted: accept(tok_inv_g7h2k1, user_u115) → rejected(already-resolved(Accepted)). User u115’s attempt is rejected. The invitation is resolved to exactly one identity — user_u114. This is Invariant 2 in action.

Decline — expired (derived): An invitee receives an invitation but takes two weeks to decide, by which time the 7-day window has passed. They click “Decline”:

decline(invitation_token: tok_inv_p4q9r2b) → rejected(expired) (seam clock 2026-10-29T09:00:00Z)

The guard evaluates is_expired(record, now) — the stored Status is still Pending but Now ≥ Expires At — and returns expired. Nothing is written: the record stays stored-Pending, Declined At stays null, and there is no expired_at field. A Read of the record now reports Effective Status = Expired, derived from the immutable Expires At and the read-time clock. The invitation was not declined; its window simply closed.

Regulated adversarial scenarios

Three scenarios the atom must survive in regulated contexts:

Regulator audit. A HIPAA (Health Insurance Portability and Accountability Act) compliance officer asks “can you prove that every user who accessed patient records joined via a documented, auditable invitation from an authorized administrator?” The auditor queries the invitation store for all Accepted invitations with Context referencing the patient records system. Each accepted invitation record shows: Inviter Ref (the administrator who invited them), Accepted At (when they joined), and Accepting Identity Ref (the identity that was bound). Invariant 3 (acceptance binds identity) is the structural guarantee: every Accepted record has an immutable Accepting Identity Ref and an immutable Inviter Ref. The auditor can trace every current system user back to the specific invitation — and the specific administrator — that admitted them. No participant entered the system without a documented invitation.

Disputed onboarding. A former employee claims “I never accepted an invitation to this system — my account was created without my knowledge.” The investigator queries the invitation store for invitations with Accepting Identity Ref matching the employee’s identity. The query finds one: status: Accepted, accepted_at: 2026-03-15T10:42:00Z, invitation_token: tok_inv_e5f6g7. Invariant 2 (single-resolution) means there is exactly one resolved invitation for this identity. The record shows when the token was presented and the acceptance was committed. Whether the former employee personally clicked the link or whether someone else acted with their token is outside the atom’s scope — the atom records that a bearer of tok_inv_e5f6g7 presented the invitation at 10:42Z on that date and supplied accepting_identity_ref: user_u114. The composing External Onboarding pattern’s Audit Trail records the surrounding context (what device, what IP, what credential was registered) which the investigator pursues separately.

Breach investigation. A security team discovers that invitation tokens for a high-security system were exposed in a system log between 2026-11-01 and 2026-11-07. They query the invitation store for all invitations with Initiated At in that window and Context referencing the high-security system, reading each record’s Effective Status against the investigation-time clock. The query returns 12 invitations. Five are Accepted (the team verifies these acceptances were legitimate by cross-referencing the Accepting Identity Ref values against known employees). Four read Pending and are still within their window — the team Revokes these immediately. Two read Expired — still stored-Pending but past their window, so no write ever occurred and none is needed (any Accept on them is rejected expired). One is Declined. Invariants 5 and 12 (three distinct stored terminals plus the derived Expired) make this triage possible from the store alone: each record’s stored status and fields, plus the read-time Effective Status, tell the team exactly what happened to it.

Edge cases and explicit non-goals

What this atom does not cover:

Downstream provisioning. The atom records that an invitation was accepted and by whom. It does not create a Party Identity record, register a Credential, issue a Session, grant Permissions, or take any other action in response to acceptance. All of that is the composing External Onboarding pattern’s responsibility. The invitation record is the trigger and the audit anchor; the provisioning steps are the composing pattern’s wiring.
Invitee notification. The atom does not send emails, push notifications, or any other communications to the invitee. Delivering the Invitation Token to the invitee is the caller’s responsibility. The atom produces the token; the delivery channel is outside its scope.
Who-may-invite-whom policy. Whether a given Inviter Ref is authorized to invite participants to the given Context is governed by the composing pattern’s policy layer. The atom records whatever Inviter Ref is supplied; it does not validate the inviter’s authority.
Invitee-vs-accepting-identity matching. The atom does not validate that Accepting Identity Ref matches Invitee Ref. A composing pattern that requires matching (e.g., the invitation was addressed to a specific external email, and the accepting party must prove control of that email) enforces this constraint above the atom layer.
Re-invitation after declination or lapse. If an invitee declines (or lets the window lapse) and the inviting actor wants to try again, the actor calls Initiate again to create a new invitation. The original record remains in the store as immutable history — a Declined stored terminal, or a still-Pending record that simply reads Expired. The atom provides no “re-open” action.
Invitation transfer. The atom does not model passing an invitation from one potential invitee to another. The Invitation Token is a bearer credential; whoever presents it to Accept becomes the Accepting Identity Ref. Whether this is acceptable in a given deployment is a policy decision for the deployment layer. Composing patterns that prohibit transfer may validate Invitee Ref against Accepting Identity Ref before calling Accept.
Multi-use invitations. Each invitation is single-use: Accept resolves it permanently. A “team invitation link” that many people can follow is not an Invitation in this atom’s sense — it is a Capability (atom #13) with max_redemptions = N and a scope that encodes the team onboarding action. Each redemption of the Capability triggers a separate Invitation Initiate + Accept sequence for that specific invitee.
Identity proofing. The atom records who accepted the invitation but does not verify the accepting identity’s real-world credentials (government ID, professional license, liveness check). Identity proofing belongs to Party Identity and the Customer Onboarding composition. The invitation establishes that someone joined via a documented channel; it does not establish who they really are.
Clock accuracy and the injected clock. The write timestamps Initiated At, Accepted At, Declined At, and Revoked At are stamped from the injected clock Now (the pipeline’s clock_t), never read inside a transition; the same injected Now drives the pure expiry derivation and Read’s Effective Status. The atom assumes a single deployment clock; clock skew, monotonicity, and timezone normalization are deployment concerns. Trusted timestamping (RFC 3161 — the Internet standard “Request for Comments” document 3161 defining a trusted time-stamping protocol) is a composing pattern for deployments requiring externally verifiable timestamps. Because expiry is derived rather than stamped, two readers evaluating Effective Status with slightly skewed clocks near Expires At may briefly disagree on whether a record is Expired — the standard read-time-derivation consequence, bounded by the deployment’s clock-skew envelope and harmless because no write is at stake.
Invitation store tamper-evidence. Composing with Tamper Evidence provides cryptographic proof that no invitation record was retroactively altered — useful in regulated deployments where the Inviter Ref and Accepting Identity Ref fields are used as legal evidence.

Terms

The canonical concepts this spec refers to. Each [Term] marker in the prose above links to its card here. A card states what the concept is, in plain English, plus its Kind — one of four: Type (a thing or category), Operation (a behavior), Member (a value of an enumerated Type), or, for a named datum, Field (a datum a Type carries — what does it carry?) or Parameter (a value an Operation needs — what does it need?). A card also names the Type it is a Member of / Field of, the Operation it is a Parameter of, and its Role where the domain assigns one. A card carries one Projects line — the concept’s single canonical lowering token, the one place the concrete name stays visible on the page — for every Field, Parameter, and pinned/wire Member. Everything else about casing (each target’s snake / camel / pascal / const / wire form) is derived from that one token by tools/harness/term-adapter.mjs, never hand-written. (annotation.md Terms registry; representational only — it changes no guarantee, invariant, or behavior of the atom above.)

Initiate

The behavior that issues a new invitation. It assigns a fresh Invitation Token, records Inviter Ref, Invitee Ref (optional), Context, Initiated At = Now, and Expires At = Now + TTL, and returns the Invitation Token (or a rejection). The record enters Pending.

Kind: Operation

Accept

The write that resolves a Pending invitation to Accepted, binding Accepting Identity Ref and stamping Accepted At. Permitted only when stored Status = Pending and Now < Expires At (else expired); a stored-resolved invitation returns already-resolved(state). Returns accepted.

Kind: Operation

Decline

The write that resolves a Pending invitation to Declined, stamping Declined At. Records no identity — a deliberate refusal, distinct from non-use. Same Pending-and-unexpired guard as Accept. Returns declined.

Kind: Operation

Revoke

The write that withdraws a Pending invitation, resolving it to Revoked and recording Revoked By Ref, Revocation Reason, and Revoked At. Same Pending-and-unexpired guard. Returns revoked.

Kind: Operation

Read

The read-only behavior that returns invitation records matching a filter. Each record carries its stored fields plus the derived Effective Status; it fires no transition and writes nothing. The only surface that surfaces the derived Expired.

Kind: Operation

Invitation Token

The opaque, cryptographically random, immutable, system-generated identity of an invitation record — the injected id_t, produced by Initiate. It is both the record’s identity and the bearer credential the invitee presents to Accept or Decline. Store-unique, never reused (Invariant 11).

Kind: Field Field of: Invitation Projects: invitation_token

Inviter Ref

The opaque reference to the actor issuing the invitation. Set on Initiate, immutable; non-null required. The atom does not validate the inviter’s authority.

Kind: Field Field of: Invitation Projects: inviter_ref

Invitee Ref

The optional opaque reference to the intended invitee. May be null at Initiate — the invitee may have no system identity yet. Set immutably when supplied; never validated against Accepting Identity Ref (Invariant 4).

Kind: Field Field of: Invitation Projects: invitee_ref

Context

The opaque descriptor of what the invitee is being invited to join (organization, workspace, role). Set on Initiate, immutable, interpreted by the composing pattern; non-null required.

Kind: Field Field of: Invitation Projects: context

Initiated At

The wall-time Initiate was called, stamped from the injected Now. Immutable.

Kind: Field Field of: Invitation Projects: initiated_at

Expires At

The absolute deadline, computed once at Initiate as Now + TTL and stored. Immutable, never null (Invariant 9). The sole stored input to the expiry derivation; there is no stored Expired flag or expired_at field.

Kind: Field Field of: Invitation Projects: expires_at

Status

The stored status — Pending, Accepted, Declined, or Revoked. Set to Pending on Initiate; immutable once written to a terminal. Expired is not a value of this field — it is the derived Effective Status, never stored.

Kind: Field Field of: Invitation Projects: status

Accepting Identity Ref

The identity bound at acceptance — supplied to Accept and recorded permanently. Null until Accept fires; immutable once set (Invariant 3). Non-null required at Accept.

Kind: Field Field of: Invitation Projects: accepting_identity_ref

Accepted At

The timestamp the invitation transitioned to Accepted, stamped from the injected Now. Null otherwise; immutable once set.

Kind: Field Field of: Invitation Projects: accepted_at

Declined At

The timestamp the invitation transitioned to Declined, stamped from the injected Now. Null otherwise; immutable once set.

Kind: Field Field of: Invitation Projects: declined_at

Revoked At

The timestamp the invitation transitioned to Revoked, stamped from the injected Now. Null otherwise; immutable once set.

Kind: Field Field of: Invitation Projects: revoked_at

Revoked By Ref

The opaque reference to the actor withdrawing the invitation. Set at Revoke; non-null required (Invariant 8); immutable once set.

Kind: Field Field of: Invitation Projects: revoked_by_ref

Revocation Reason

The caller-supplied reason for revocation — written from the Reason parameter. Set at Revoke; non-null required (Invariant 8); immutable once set.

Kind: Field Field of: Invitation Projects: revocation_reason

Effective Status

The derived status Read surfaces: Expired when Status = Pending ∧ Now ≥ Expires At, otherwise the stored Status. A pure projection over the record and the injected Now; never stored (Invariant 12).

Kind: Field Field of: Invitation Projects: effective_status

TTL

The duration Initiate consumes to compute Expires At = Initiated At + TTL. Must be positive if supplied; null uses the deployment default. Not stored under this name — only the resulting Expires At persists.

Kind: Parameter Parameter of: Initiate Projects: ttl

Reason

The required, non-empty reason string Revoke consumes — written into Revocation Reason. Not stored under this name; an empty or whitespace-only value is rejected Invalid Request.

Kind: Parameter Parameter of: Revoke Projects: reason

Now

The current clock reading the pipeline consumes — the injected clock_t, supplied at the I/O seam, never read inside a transition and never a signature parameter. It stamps the immutable write timestamps (Initiated At, Accepted At, Declined At, Revoked At) and drives the pure expiry derivation in guards and Read (no write).

Kind: Parameter Parameter of: Initiate Projects: now

Pending

The only non-terminal stored Status: the invitation has been issued and awaits resolution. A Pending record past Expires At reads Expired by derivation but stays stored-Pending (no write).