Notification

Atom grounded on Final Critique 4 — 2026-06-18 9 invariants Alloy model buggy twin ×1 regulated · via 2 composers composed by 2

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

Notification

Summary

Notification records whether a single piece of information actually reached a single recipient. Where Subscription records who wants to know about a class of events, Notification records the outcome of one delivery. It creates a permanent, unchangeable record of a delivery attempt and tracks it to one of three end states: Delivered (the transport layer confirmed receipt), Failed (the transport returned a definite error), or Expired (the delivery window ran out with no recorded outcome). These are kept as three distinct states because each answers a different question and is handled by a different part of the system — the delivery layer, the failure handler, the expiry scheduler. The pattern does not decide who should be notified or how to reach them; by the time it is asked to create a record, the recipient and the content are already settled. Nothing is ever deleted, so the full delivery history of any notification is always recoverable. This is what underlies delivery audit trails in regulated settings, and it is the substrate for retry logic, which records each retry as a new notification rather than altering the failed one.

Intent

When an event fires against a subscription, something must carry the resulting information to the recipient and record whether it arrived. That record is the notification: a durable account of the delivery attempt with enough state to answer the operational questions — did the recipient get this? was delivery attempted and failed? did this expire before it could be delivered?

Notification records delivery. It does not know about subscriptions, events, or routing; those belong to the composing Notification Fanout pattern. What the atom owns is the delivery record for a single recipient from the moment of creation through its terminal outcome: Delivered, Failed, or Expired.

The three terminal states are distinct because they answer different questions. Delivered: did the recipient receive it? Failed: was delivery attempted and did the attempt not succeed? Expired: did this sit undelivered beyond the allowed window without a recorded failure? Collapsing them into a single terminal state would hide information that operators, auditors, and retry logic each need separately.

This is a freestanding (can be specified without naming any other pattern) 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 notification set), its own actions (create, deliver, fail, expire, status_of, pending_for), and its own operational principles (notifications are immutable once recorded; terminal states are irreversible; status_of and pending_for are read-only queries). It does not implement routing, subscription evaluation, retry scheduling, or delivery transport. Each is a separate composable pattern; see Composition notes.

Structure

Identity model

Every notification known to the system has a Notification Id — an opaque, immutable, host-allocated at the I/O seam (injected into the transition, not generated inside it) identifier produced by Create. The id is the notification’s identity; the recipient reference and payload are immutable properties of the notification, not its identity.

The opaque-id model follows the same discipline used across the library. Identifying a notification by (Recipient Ref, Payload) would collapse independently-created notifications into a single record — a recipient may be notified of the same event scope multiple times (e.g., after re-subscribing), and each delivery attempt is a distinct record with its own outcome. Opaque ids preserve one-notification-one-id discipline.

Ids are not reused after a notification reaches a terminal state.

Inputs

A recipient reference identifying who the notification is addressed to. Opaque — the actor registry is a separate concept. The atom requires only that recipient references support equality testing (so Pending For and Status Of queries can filter and look up by recipient); it does not parse, normalize, or otherwise interpret their contents.
A payload carrying what is being communicated. Opaque — the composing system defines payload structure and content. This atom stores and returns the payload unchanged; it does not inspect, parse, or validate its contents.
Actions:
- Create — (Projected contract: create(recipient_ref, payload) → notification_id | rejected(reason))
- Deliver — (Projected contract: deliver(notification_id) → ok | rejected(reason))
- Fail — (Projected contract: fail(notification_id) → ok | rejected(reason))
- Expire — (Projected contract: expire(notification_id) → ok | rejected(reason))
- Status Of — (Projected contract: status_of(notification_id) → {notification_id, recipient_ref, payload, created_at, status, delivered_at?, failed_at?, expired_at?} | not-known)
- Pending For — (Projected contract: pending_for(recipient_ref) → [notification_id, ...])
A clock providing wall-time timestamps, and an id source for Notification Id allocation — both injected at the atom’s single I/O seam. Per the Logic Confinement Principle (see execution-contract.md), the host reads the clock and allocates the Notification Id at the seam, before the transition runs; the pure transition receives the timestamps and Notification Id as injected inputs. Neither is read or generated inside the core transition, and neither is supplied by the business caller — which keeps the transition deterministic and forecloses caller-supplied timestamp or id lying.

String input policy (applies to Recipient Ref and Payload). Values are treated byte-exact: no trimming, no Unicode normalization, no case folding is applied before storage or comparison. A whitespace-only string counts as empty for the presence check and is rejected wherever non-empty is required (i.e., Recipient Ref). The deployment sets a maximum length per string input; a value exceeding it is rejected as Invalid Request. Callers own canonicalization — two Recipient Ref values differing only in case or normalization form are two distinct recipients to this atom.

Outputs

The current set of notifications (Pending, Delivered, Failed, and Expired).
For each notification: Notification Id, Recipient Ref, Payload, Created At, Status, and the applicable terminal timestamp (Delivered At, Failed At, or Expired At).
Create returns the new Notification Id on success, or a rejection naming the failed precondition.
Deliver, Fail, and Expire return ok on success, or a rejection naming the failed precondition.
Status Of returns one of two first-class outcomes: the full notification record (all stored fields for that id), or Not Known if no notification exists for the given id. Both are answers to the query, not success-failure pairs.
Pending For returns the list of Notification Id values for all Pending notifications addressed to the queried recipient. The list is unordered. Composing systems that require delivery in creation order must sort by Created At on the returned ids.

State

A notification occupies one of four named states:

Pending — the notification has been created and delivery has not yet been confirmed, failed, or expired.
Delivered — the notification reached the recipient. Terminal.
Failed — delivery was attempted and did not succeed. Terminal.
Expired — the notification was not delivered and no failure was recorded within the allowed window. Terminal.

Each notification carries:

Notification Id — opaque, immutable, host-allocated at the I/O seam (injected into the transition, not generated inside it). Set on Create. Never changes.
Recipient Ref — opaque reference to the intended recipient. Set on Create. Never changes.
Payload — opaque content of the notification. Set on Create. Never changes.
Created At — wall-time when the notification was created. Set on Create. Never changes.
Status — pending, delivered, failed, or expired. Set to pending on Create; transitions to a terminal state on the corresponding action.
Delivered At — wall-time when delivery was confirmed. Absent unless status is delivered; set on Deliver. Never changes after set.
Failed At — wall-time when the failure was recorded. Absent unless status is failed; set on Fail. Never changes after set.
Expired At — wall-time when the expiry was recorded. Absent unless status is expired; set on Expire. Never changes after set.

Transitions — writes stamp their timestamp from the injected clock; the two queries below the rule cause no transition. State is unchanged on any rejection, and each terminal transition is serialized per Notification Id (Decision points):

action	from	to	stamps	result	rejections
Create	(none)	Pending	fresh Notification Id; Recipient Ref; Payload; Created At	the new Notification Id	Invalid Request
Deliver	Pending	Delivered	Delivered At	`ok`	Not Known; Not Pending
Fail	Pending	Failed	Failed At	`ok`	Not Known; Not Pending
Expire	Pending	Expired	Expired At	`ok`	Not Known; Not Pending
Status Of	read-only	—	—	the full record, or Not Known	—
Pending For	read-only	—	—	the Pending ids for the recipient	—

The three terminal transitions (Deliver, Fail, Expire) share identical preconditions: the Notification Id must be known (else Not Known) and the notification must be in Pending (else Not Pending). Status Of returns the full notification record for the given id, or Not Known; Pending For returns the Notification Id values for all Pending notifications where notification.recipient_ref = recipient_ref.

Flow

An event fires; the composing pattern creates a notification. The Notification Fanout pattern (or equivalent) calls create(recipient_ref, payload) — the atom records the notification in Pending and returns the id.
The delivery layer attempts to deliver (optional). The transport mechanism (webhook call, WebSocket push, email send) attempts to reach the recipient. This step may be skipped entirely — a notification may be expired before any delivery attempt begins if the deadline passes first.
Delivery outcome is recorded. Exactly one of three transitions applies:
- 3a. Transport succeeds: deliver(notification_id) → Delivered, Delivered At set.
- 3b. Transport fails: fail(notification_id) → Failed, Failed At set.
- 3c. Deadline passes without a delivery attempt, or without a recorded outcome: expire(notification_id) → Expired, Expired At set. Step 2 need not have occurred.
Operators or retry logic consult notification state. pending_for(recipient_ref) returns unresolved notifications; status_of(notification_id) returns the full record for any notification by id, including terminal ones.

Decision points

At create(recipient_ref, payload) — Recipient Ref must be non-empty — specifically, not null, undefined, the empty string, or whitespace-only (per the String input policy); otherwise Invalid Request. The atom does not parse or interpret the opaque value beyond this presence check. Payload must be present — null or absent is rejected as Invalid Request; any non-null payload, including an empty string or empty object, is accepted. The atom does not inspect, validate, or parse payload content. There is no uniqueness constraint: multiple notifications may be created for the same recipient with the same payload — each is a distinct delivery attempt with its own id and outcome.
At deliver(notification_id) — Notification Id must reference a known notification; otherwise Not Known. The notification must be in Pending; transitioning a non-Pending notification is rejected as Not Pending.
At fail(notification_id) — same preconditions as Deliver: Not Known or Not Pending.
At expire(notification_id) — same preconditions: Not Known or Not Pending.
At status_of(notification_id) — no precondition. Empty or malformed Notification Id returns Not Known — no notification has an empty id, so the result is structurally Not Known. Both Not Known and the full record are first-class outcomes; neither is a rejection.
At pending_for(recipient_ref) — no precondition. Empty or malformed Recipient Ref returns an empty list — no notification has an empty recipient, so the result is structurally empty. Returns an empty list if no Pending notifications exist for the recipient. The query is read-only.

Single-record transition serialization is the load-bearing precondition for status monotonicity (Invariant 2) and terminal exclusivity (Invariant 3). Each terminal transition (Deliver, Fail, Expire) must execute as an atomic, serialized unit per Notification Id; without this guarantee, two concurrent transitions could both observe Pending and both proceed, producing two terminal timestamps and violating both invariants. The host environment supplies this serialization; the atom specifies the requirement.

Behavior

Observed behavior, derived from how notification delivery systems are actually deployed:

The three terminal transitions (Deliver, Fail, Expire) are separate actions rather than a single resolve(notification_id, outcome) action. The likely objection: “they share identical preconditions and return shapes; a parameterized action would reduce duplication.” The mechanism: keeping them separate preserves distinct action semantics — the delivery layer, failure handler, and expiry scheduler are independent actors with independent authorization surfaces; a parameterized outcome enum would introduce a new precondition (is the enum value valid?) that currently does not exist. The result: each terminal transition is an unambiguously-named operation with no shared enum validation burden.
The three terminal states are mutually exclusive. A notification transitions from Pending to exactly one terminal state. Once terminal, no further transition is possible; Deliver, Fail, or Expire called on a non-Pending notification returns Not Pending.
Fail vs. Expire — a deployment policy. Failed indicates an explicit delivery attempt that produced a definitive negative outcome (HTTP 5xx response, bounced email, invalid token, connection refused). Expired indicates that the allowed window elapsed without either a successful delivery or a recorded failure. Whether a connection timeout is Fail or Expire is the composing system’s call; the atom only records the outcome, not how it was determined.
Concurrent Deliver, Fail, or Expire calls for the same Notification Id resolve serially under the host environment’s serialization guarantees. The first transition wins; subsequent calls receive Not Pending.
Who calls Deliver, Fail, or Expire is handled at the deployment layer. In a push model, the delivery layer calls these after attempting to push. In a pull model, the host system calls Deliver when the recipient reads the notification. In a scheduled-expiry model, a background process calls Expire for notifications past their deadline. The atom records the transition; the caller is the composing system’s responsibility.
The atom does not enforce who may call Create — any caller may create a notification for any recipient. Authorization to create belongs to the composing system.
Multiple Pending notifications for the same recipient are allowed and independent. Each has its own id, payload, and delivery lifecycle. Pending For returns all of them; the composing system decides the delivery order.
No notification is deleted. All terminal records — Delivered, Failed, Expired — remain in the store for audit and operational purposes. Pending For excludes them; status_of(notification_id) returns them.
A Failed notification does not automatically trigger a retry. If retry is desired, the composing system creates a new notification record for the retry attempt — a distinct record with a distinct id and its own outcome (see Edge cases).
Payload is stored and returned opaque. The atom does not parse, validate, or act on payload content. Whether the payload is a JSON object, a plain string, or a reference to another record is defined entirely by the composing system.
Status Of is a read-only query with no side effects. It returns all stored fields — including the opaque payload — for any notification in any state: Pending, Delivered, Failed, or Expired. No notification becomes inaccessible via Status Of after reaching a terminal state; the record is durable for the lifetime of the system.
Time and Notification Id are injected at the I/O seam: the host reads the clock and allocates Notification Id before the transition runs; the core transition receives both as inputs and neither reads a clock nor mints an id. Caller signatures (create(recipient_ref, payload) and all other actions) are unchanged — timestamps and ids are never caller-supplied.
A notification may remain in Pending indefinitely. The atom does not impose a maximum lifetime; whether and when a Pending notification reaches a terminal state depends on the composing system’s delivery layer and any scheduled-expiry process. A store with long-lived Pending records is not a spec violation — composing systems that need bounded Pending lifetimes wire a scheduled-expiry process that calls Expire at deadline.

Feedback

Each successful action produces an observable, measurable change:

After Create — a new notification appears in Pending with a fresh Notification Id, the supplied Recipient Ref and Payload, and Created At. Total notification count increases by one. Pending count increases by one. The id is returned. Falsifiable: after create(r, p) → n, status_of(n) must return a record with status = pending and recipient_ref = r.
After Deliver — the notification moves to Delivered with Delivered At. Pending count decreases by one; delivered count increases by one; total count unchanged. Falsifiable: status_of(n) must return status = delivered and delivered_at must be set; pending_for(recipient_ref) must not include n.
After Fail — the notification moves to Failed with Failed At. Pending count decreases; failed count increases. Falsifiable: status_of(n) must return status = failed and failed_at set.
After Expire — the notification moves to Expired with Expired At. Pending count decreases; expired count increases. Falsifiable: status_of(n) must return status = expired and expired_at set.
After Status Of — no state change. Returns the full notification record or Not Known.
After Pending For — no state change. Returns the list of Notification Ids in Pending state for the queried recipient.

Create rejections: Invalid Request. Deliver, Fail, Expire rejections: Not Known, Not Pending.

The full notification set — Pending, Delivered, Failed, Expired — is queryable via Status Of and Pending For.

Invariants

The following hold across all valid sequences of actions and constitute the verification surface of the pattern:

Invariant 1 — Notification immutability. Once recorded, a notification’s Notification Id, Recipient Ref, Payload, and Created At never change. Once set, Delivered At, Failed At, and Expired At never change. No field in the notification record is ever overwritten.
Invariant 2 — Status monotonicity. A notification’s status transitions only from Pending to one terminal state: Delivered, Failed, or Expired. No notification returns from a terminal state to Pending or transitions between terminal states.
Invariant 3 — Terminal states are exclusive. At most one of Delivered At, Failed At, Expired At is present for any notification. A notification in Delivered has Delivered At and no other terminal timestamp; likewise for Failed and Expired. A Pending notification has none.
Invariant 4 — Terminal timestamps match status. Delivered At is present if and only if status is delivered. Failed At is present if and only if status is failed. Expired At is present if and only if status is expired.
Invariant 5 — Id stability. A notification’s Notification Id is set on Create and never changes.
Invariant 6 — No id reuse. No two notifications share a Notification Id across the lifetime of the system.
Invariant 7 — Pending query excludes terminals. pending_for(recipient_ref) returns only notifications in Pending state for the queried recipient. Delivered, Failed, and Expired notifications are not included regardless of their Recipient Ref.
Invariant 8 — Timestamp ordering. For any notification in Delivered state, Created At ≤ Delivered At. For any notification in Failed state, Created At ≤ Failed At. For any notification in Expired state, Created At ≤ Expired At. This invariant is best-effort under non-monotonic clocks; if the underlying clock moves backward between Create and the terminal action, the inequality may be violated. The implementor is responsible for the clock discipline that makes each inequality hold; see Edge cases.
Invariant 9 — Notification durability. Notifications are never deleted from the store. Once created, a notification record persists through all state transitions and remains queryable via Status Of for the lifetime of the system. The total notification count is monotonically non-decreasing.

Notification immutability and durability together give the auditability property — the full delivery history of every notification is recoverable from the notification store alone, with no gaps. Terminal-state exclusivity and timestamp matching (Invariants 3 and 4) give the unambiguous record property — for any notification, exactly one delivery outcome is recorded and its timestamp is stable. Status monotonicity and timestamp ordering together give the operational readability property — Pending For is a deterministic snapshot of unresolved deliveries at query time.

Examples

The same atom, three domains, identical mechanic.

Shared Todo — assignment notification delivery

A Notification Fanout pattern creates a notification when a task is assigned: create(dev_d, {type: "task:assigned", task_id: t1, assigned_by: manager_m}) → notif_77. The WebSocket layer pushes the payload to dev_d’s active session and calls deliver(notif_77) → Delivered. status_of(notif_77) returns status = delivered, Delivered At set. pending_for(dev_d) returns [].

If dev_d is offline, the push attempt produces a connection error: fail(notif_77) → Failed. The composing system may create a retry notification: create(dev_d, {same payload}) → notif_78 — a new Pending record, distinct id, independent outcome.

If neither delivery nor failure is recorded within the expiry window: expire(notif_77) → Expired. status_of(notif_77) returns Expired At.

Support queue — escalation alert

When queue 9 escalates, the fanout pattern creates one notification per subscribed supervisor: create(supervisor_s, {type: "escalation", queue: 9, ticket: t22}) → notif_33. Email delivery succeeds: deliver(notif_33) → Delivered. status_of(notif_33) returns status = delivered, Delivered At. Elapsed delivery time is delivered_at − created_at.

Supervisor_s later asks “was I notified about the queue-9 escalation?” — pending_for(supervisor_s) returns an empty list (nothing pending), and status_of(notif_33) returns status = delivered with Delivered At. The delivery record answers the question from stored fields alone.

Compliance system — policy change

An administrator broadcasts a policy update. Three compliance officers each receive a notification: create(officer_a, {type: "policy:updated", policy_id: p7}) → notif_101, similarly for officers b and c. Officer_a’s email bounces: fail(notif_101). Officers b and c are delivered successfully. status_of(notif_101) shows Failed At; status_of(notif_102) and status_of(notif_103) show Delivered At. An operator queries pending_for for each officer — empty for all three. The notification store shows: two Delivered, one Failed; the composing system creates a retry for officer_a or escalates to a secondary channel.

Rejection path — invalid create

A composing system attempts to create a notification with an empty recipient reference: create(recipient_ref: "", payload: {type: "task:assigned", task_id: "t1"}) → rejected(invalid-request). No Notification Id is issued; no record enters the store. The composing system must supply a non-empty recipient reference before the notification can be created.

Regulated adversarial scenarios

Three scenarios the notification store must survive in regulated contexts:

Regulator audit — demonstrate all notifications for a compliance event. A compliance auditor asks “show all notifications created for the policy:updated event on 2025-03-14, and whether each was delivered.” The auditor queries the notification store for notifications where created_at falls on 2025-03-14 and the payload references the relevant policy. Status Of for each returned id shows the delivery outcome — Delivered At, Failed At, or Expired At. The notification store answers from stored fields alone; Invariants 1 and 3-4 guarantee the delivery record is complete and unambiguous.
Disputed delivery — actor claims they were not notified. Officer_a claims they received no notification of policy update p7. The investigator queries the notification store for notifications where recipient_ref = officer_a and the payload references policy_id: p7. If a record exists with Delivered At set, Invariant 1 (notification immutability) is the structural answer: the notification was created with that recipient and delivery was confirmed at that time. If the record shows Failed At or Expired At, the store confirms delivery was not completed and documents why. The notification store is the single source of truth; no external corroboration is required.
Breach investigation — identify Pending notifications that may have exposed payload data. A security incident requires identifying all notifications that were Pending at the time of breach (2025-06-01T03:00Z) and may have carried sensitive payload data. The investigator queries for notifications where created_at ≤ 2025-06-01T03:00Z and either status = pending (still unresolved now) or the applicable terminal timestamp falls after 2025-06-01T03:00Z (meaning the notification was Pending during the breach window but has since resolved). The reconstruction logic mirrors the Subscription pattern: created_at ≤ T and (status = pending or delivered_at > T or failed_at > T or expired_at > T). Status Of for each candidate returns the current record; created_at confirms the exposure window. The notification store answers the exposure scope question from stored fields alone without recourse to logs or developer narration.

Edge cases and explicit non-goals

What this atom does not cover:

Routing and subscription evaluation. This atom creates and tracks delivery records; it does not evaluate subscriptions or determine who should be notified. That belongs to a Notification Fanout composing pattern that wires Subscription + Notification + an event source.
Retry scheduling. A Failed notification does not trigger a retry. The composing system creates a new notification record for the retry attempt: create(recipient_ref, payload) → new_notification_id. The retry is a distinct record with a distinct id and its own outcome. Both the original Failed record and the retry record are preserved in the store.
Transport mechanism. Whether delivery is via WebSocket, webhook, email, push notification, in-app message, or SMS is handled at the deployment layer. The atom records the outcome (Deliver, Fail, Expire); the mechanism that produces that outcome is out of scope.
fail vs. expire boundary. Whether a connection timeout, an invalid token, or a rate-limit response is Fail or Expire is a deployment policy the composing system defines. The atom only records which terminal transition was called; it does not inspect or validate the reason.
Delivery ordering guarantees. Multiple Pending notifications for the same recipient may be delivered in any order. If delivery ordering matters, the composing system is responsible for imposing it. Pending For returns an unordered list; the composing system sorts by Created At if ordered delivery is required.
Recipient read confirmation vs. system delivery confirmation. Deliver covers system-level confirmation that the transport layer accepted the notification. Deployments that additionally require read confirmation (the recipient explicitly acknowledged the notification) should create two separate notification records: one for the push attempt (resolved with Deliver or Fail at push time) and one for the read-acknowledgement (resolved with Deliver when the recipient acknowledges). The bare atom does not distinguish delivery from reading; the distinction requires two records.
Payload validation and schema. Payload is opaque. Whether a payload is well-formed, type-safe, or complete is the composing system’s responsibility before calling Create.
Notification deduplication. Multiple Create calls for the same (Recipient Ref, Payload) pair produce multiple distinct Pending notifications. Composing systems that require at-most-once delivery for a given event should use Duplicate Prevention to guard the Create call.
Recipient registration and lifecycle. Recipient Ref is opaque. Whether a recipient exists or has been deprovisioned belongs to Actor Registry.
Authorization to create. The atom does not enforce who may call Create. Any caller may create a notification for any recipient. Authorization to create belongs to the composing system.
Bulk expiry. There is no bulk-expire surface. Expiring all Pending notifications past a deadline requires querying Pending For for each recipient and calling expire(notification_id) for each eligible id.
Atomicity and crash semantics. Each terminal transition changes two fields simultaneously: Status and one terminal timestamp. A crash mid-Deliver that sets Delivered At without updating Status, or vice versa, violates Invariant 4 (terminal timestamps match status). The implementor is responsible for the transactional boundary that makes both fields change together. The spec does not define recovery semantics for partial writes.
Payload data retention. The notification store retains payload data for every notification for the lifetime of the system (Invariant 9). If payloads contain sensitive data — PII, financial records, medical information — the composing system is responsible for the retention policy. Retention Window is the composing pattern that bounds how long records must be kept and when they may be purged. The bare atom does not implement payload expiry or redaction.
Clock semantics. Created At, Delivered At, Failed At, and Expired At are wall-time from the injected clock. Clock skew, NTP (Network Time Protocol) adjustments, and timezone handling are handled at the deployment layer. Invariant 8 is best-effort under non-monotonic clocks.

Generation acceptance

The audit surface is the notification store inspected on its stored fields — distinct from and complementary to the action surface (Create, Deliver, Fail, Expire, Status Of, Pending For). The action surface answers what does the atom do at runtime?; the audit surface answers what does the atom commit to recording, queryable on stored fields?. A derived implementation must produce a store that supports the audit-surface queries below, independent of whether the runtime action surface exposes them.

A derived implementation of Notification is acceptable — in the regulator-acceptance sense — when an external auditor, given the notification store, can do all of the following without recourse to source code, runbooks, or developer narration:

Enumerate every notification with its full delivery history. Notification Id, Recipient Ref, Payload, Created At, Status, and the applicable terminal timestamp are present and queryable for every notification ever created. No notification is missing from the store.
Reconstruct the delivery status of any notification at any past point in time. Given a Notification Id and a timestamp, the auditor can determine what state the notification was in: if created_at ≤ t and no terminal timestamp is before t, the notification was Pending at t; if delivered_at ≤ t, it was Delivered; and so on. The reconstruction is exact with respect to stored timestamps (Invariants 1 and 4); the wall-clock truth of those timestamps is subject to Invariant 8’s best-effort clock caveat. Under a clock that has moved backward, two stored timestamps may be misordered; the auditor’s answer is still deterministic on stored fields, but may not reflect wall-clock truth.
Confirm terminal state exclusivity. For every notification, at most one of Delivered At, Failed At, Expired At is present. The auditor can verify this directly from the notification store (Invariant 3).
Confirm terminal timestamps match status. For every notification, the presence of a terminal timestamp matches the Status field exactly — no notification has status = delivered with failed_at set, or any other mismatch (Invariant 4).
Identify composing patterns active in this deployment. Whether notification attribution (Actor Identity), event firing history (Event Log), deduplication (Duplicate Prevention), retention (Retention Window), and tamper-evidence on the notification store (Tamper Evidence) are wired in, and with what configuration. The deployment’s fail-vs-expire policy must also be disclosed — which operational events the deployment maps to Fail (e.g., HTTP 5xx, bounced email, invalid token) versus Expire (e.g., elapsed delivery window without a recorded outcome). Without this disclosure, the same operational event may produce failed_at in one deployment and expired_at in another, and cross-deployment audit cannot interpret records uniformly.

This is the generator’s contract: any code generated from this atom must produce a notification store and a query surface that pass the five checks above.

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.)

Create

The behavior that records a new delivery record. It assigns a fresh Notification Id (host-allocated at the seam), records Recipient Ref, Payload, and Created At, and returns the Notification Id (or Invalid Request). The record enters Pending.

Kind: Operation

Deliver

The behavior that records successful delivery, transitioning a Pending notification to terminal Delivered and stamping Delivered At. Rejected for an unknown id (Not Known) or a non-Pending notification (Not Pending).

Kind: Operation

Fail

The behavior that records a definitive delivery failure, transitioning a Pending notification to terminal Failed and stamping Failed At. Same preconditions as Deliver.

Kind: Operation

Expire

The behavior that records lapse of the delivery window without an outcome, transitioning a Pending notification to terminal Expired and stamping Expired At. Same preconditions as Deliver.

Kind: Operation

Status Of

The read-only query returning the full record for a Notification Id in any state, or Not Known if no notification has that id. Never transitions.

Kind: Operation

Pending For

The read-only query returning the Notification Id values of all Pending notifications addressed to a Recipient Ref (unordered; excludes terminals, Invariant 7). Never transitions.

Kind: Operation

Notification Id

The opaque, immutable identity of a notification — host-allocated at the I/O seam (the injected id), produced by Create, never reused (Invariant 6). The recipient and payload are properties of the notification, not its identity.

Kind: Field Field of: the notification record Projects: notification_id

Recipient Ref

The opaque reference to the intended recipient. Set on Create, immutable. Equality is byte-exact (no normalization); Pending For filters on it.

Kind: Field Field of: the notification record Projects: recipient_ref

Payload

The opaque content of the notification. Set on Create, immutable, stored and returned unchanged — never parsed, validated, or interpreted by the atom.

Kind: Field Field of: the notification record Projects: payload

Created At

The wall-time the notification was created, stamped from the injected clock at Create. Immutable (Invariant 1). The lower bound for any terminal timestamp (Invariant 8).

Kind: Field Field of: the notification record Projects: created_at

Status

The notification’s lifecycle state — Pending, Delivered, Failed, or Expired. Set to Pending on Create; transitions once to a terminal (Invariant 2).

Kind: Field Field of: the notification record Projects: status

Delivered At

The wall-time delivery was confirmed, stamped at Deliver. Present iff status is Delivered (Invariants 3 and 4); immutable once set.

Kind: Field Field of: the notification record Projects: delivered_at

Failed At

The wall-time the failure was recorded, stamped at Fail. Present iff status is Failed (Invariants 3 and 4); immutable once set.

Kind: Field Field of: the notification record Projects: failed_at

Expired At

The wall-time the expiry was recorded, stamped at Expire. Present iff status is Expired (Invariants 3 and 4); immutable once set.

Kind: Field Field of: the notification record Projects: expired_at

Pending

The non-terminal state of a created notification whose delivery has not been confirmed, failed, or expired. May transition to exactly one terminal; Pending For returns only records in this state.

Kind: Member Member of: the notification status Role: Outcome

Delivered

The terminal state of a notification that reached the recipient (transport confirmed). Carries Delivered At; absorbing (Invariant 2).

Kind: Member Member of: the notification status Role: Outcome

Failed

The terminal state of a notification whose delivery was attempted and produced a definitive negative outcome. Carries Failed At; absorbing.

Kind: Member Member of: the notification status Role: Outcome

Expired

The terminal state of a notification whose delivery window lapsed without a recorded outcome. Carries Expired At; absorbing.

Kind: Member Member of: the notification status Role: Outcome

Invalid Request

The refusal Create returns when request fields fail — an empty/whitespace Recipient Ref, or a null/absent Payload.

Kind: Member Member of: the Create rejection Role: Outcome Projects: invalid-request

Not Known

The refusal Deliver, Fail, or Expire returns when the Notification Id references no notification in the store. Also the Status Of outcome for an unknown id.

Kind: Member Member of: the action rejection Role: Outcome Projects: not-known

Not Pending

The refusal Deliver, Fail, or Expire returns when the target is not in Pending — i.e., already in a terminal state.

Kind: Member Member of: the action rejection Role: Outcome Projects: not-pending

Composition notes

Notification is freestanding and is designed to compose with:

Subscription — the interest record that determines who should receive a notification. The composing Notification Fanout pattern calls Subscription.subscribers_for(event_scope) and then Notification.create(subscriber_ref, payload) for each result.
Notification Fanout — the composition that wires Subscription + Notification + an event source into an end-to-end delivery pipeline. Notification Fanout is the composition that gives both atoms their operational meaning.
Event Log — records delivery attempts and outcomes as auditable events. Each Deliver, Fail, or Expire call can be appended to an Event Log for replay and investigation.
Actor Identity — records who triggered the creation of a notification when attribution of notification source is required.
Retention Window — the notification store must be retained for the regulatory or operational lifetime the deployment requires.
Tamper Evidence — in regulated contexts, the notification store is a target for after-the-fact manipulation. Cryptographic commitment makes any rewrite detectable.
Duplicate Prevention — composing systems that require at-most-once notification creation for a given event can use Duplicate Prevention to guard the Create call.

Standards references

Observer pattern (GoF) — Notification is the structured-natural-language realization of the notification object: the message delivered from subject to observer.
SMTP / RFC 5321 — SMTP (Simple Mail Transfer Protocol, defined in the Internet standard RFC 5321) email delivery as the canonical push transport. The three terminal states map directly to SMTP disposition: 2xx success (Delivered), 5xx permanent failure (Failed), and timeout without delivery (Expired).
HTTP webhooks — POST-to-URL delivery model standard in web systems. Deliver records a 2xx response; Fail records a 4xx/5xx or connection failure.
W3C Activity Streams 2.0 — semantic vocabulary for describing social and messaging events. Notification payloads in web deployments often conform to Activity Streams objects.
Apple Push Notification Service / Firebase Cloud Messaging — platform push notification services where Deliver corresponds to accepted delivery and Fail corresponds to a rejected or unregistered token.
Daniel Jackson, The Essence of Software — freestanding-atom posture; Payload as an opaque reference whose semantics are defined by the composing system.
Eiffel’s design-by-contract — preconditions on Deliver, Fail, and Expire; named rejection reasons.

Status

grounded on Final Critique 4 — 2026-06-18 (Final Critique 4 — the first AI-conducted adversarial round, fresh-reader Opus, 2026-06-18 — closed one foundational logic-confinement finding: the clock and notification_id are now host-injected at the I/O seam rather than generated inside the transitions; caller signatures unchanged and the invariant set held at 9; see Lineage. Formal layer landed 2026-06-03 — Alloy structural model notification.als + buggy twin verified, see Lineage §Formal model. The pattern was grandfathered at the legacy grounded — 2026-05-20 token until this round.) — structure and invariants specified; status_of query added after Pass 2 identified the missing read surface; Invariant 8 corrected to conditional-per-state form after Pass 1 identified the set-notation error; regulated adversarial scenarios and generation acceptance added after Pass 3 surfaced the compliance example obligation; three-pass lineage records all findings and resolutions. Second entry in messaging.

Lineage notes

This atom is the second entry in the messaging/ category, drafted alongside Subscription as the two-atom foundation for the forthcoming Notification Fanout composition.

Pass 1 — Structural completeness (GRID — the nine-node completeness framework: Intent, System, Friction, Flow, Decision, Feedback, State, Behavior, Proof). Three findings.

Invariant 8 used non-standard set-notation. The original form created_at ≤ {delivered_at | failed_at | expired_at} is ambiguous — the brace-pipe construct does not appear in any prior atom and is not defined. Personal Todo’s Lineage notes canonicalized the “chain inequality with optional terms” error as a known Pass 3 class; Notification repeated it. Fixed: Invariant 8 now states three separate conditional inequalities — one per terminal state.
Flow node collapsed three terminal branches into one step. The deliver, fail, and expire transitions were combined into a single parenthetical in Flow step 3, understating the branching structure. Fixed: Flow step 3 now names three explicit sub-branches (3a Delivered, 3b Failed, 3c Expired) with each terminal action and its timestamp consequence.
State Transitions did not cross-reference Decision points on rejection. The Transitions list described successful state changes without noting that precondition failures leave state unchanged and refer to Decision points for rejection reasons. Fixed: each of the three terminal transitions now notes rejection behavior inline.

Pass 2 — Conceptual independence (EOS). Three findings.

status_of query missing. The Examples section said “querying notif_33 directly shows status delivered” and Edge cases said “direct query by notification_id returns terminal records” — but no status_of action was specified. The atom assumed a read capability it did not define. Fixed: status_of(notification_id) → record | not-known added to Inputs, Outputs, Transitions, Decision points, Behavior, and Feedback.
Payload precondition contradicted opaque posture. Decision points said create rejects invalid-request for non-“well-formed” payload, but the atom also says it does not inspect payload content. An opaque atom cannot evaluate well-formedness. Fixed: the payload precondition now states only that a null or absent payload is rejected; any non-null payload is accepted. “Well-formed” removed.
Retry description in Behavior described composing-system behavior. One sentence explained what the composing system should do for retry. Behavior should describe what the atom does, not what composing systems do; composing-system obligations belong in Edge cases. Fixed: sentence removed from Behavior; Edge cases retry entry now carries the full description.

Pass 3 — Adversarial scrutiny (Linus mode). Five findings.

Three-action vs. parameterized-action choice undefended. deliver, fail, and expire have identical preconditions and return shapes; collapsing them into resolve(id, outcome) is a real alternative. The design choice was not defended in-line. Fixed: Behavior now carries the four-step rubric defense (separate authorization surfaces, no enum validation burden).
fail vs. expire boundary unnamed as deployment policy. The spec described the two terminal failure states without naming who decides the boundary between them. A connection timeout could be either. Fixed: Behavior explicitly names this as a deployment policy and gives examples of each (HTTP 5xx = fail; elapsed window without record = expire).
Concurrent terminal call race condition unnamed. Two concurrent deliver and expire calls for the same notification_id are a real operational scenario; the first wins and the second gets not-pending. Not named. Fixed: Behavior now states serial resolution under host serialization guarantees.
Atomicity and crash semantics absent. Each terminal transition changes two fields (status and one terminal timestamp) that must change together. A partial write violates Invariant 4. Personal Todo names this explicitly. Fixed: Edge cases now carries the atomicity note.
Regulated adversarial scenarios and generation acceptance missing. The compliance system example (policy change broadcast, officer notification audit) invokes a regulated domain; library rules require both sections. Fixed: both sections added, with three adversarial scenarios covering regulator audit, disputed delivery, and breach investigation.

Second-pass review — seven additional findings, all closed.

status_of return signature used [terminal_timestamp] notation. The bracket implied a single optional field called terminal_timestamp; the actual record has three distinct named optional fields (delivered_at?, failed_at?, expired_at?). An implementor reading only the Inputs section could produce one field instead of three, breaking the audit surface. Fixed: signature updated to delivered_at?, failed_at?, expired_at?.
Flow step 2 assumed delivery is always attempted. “The delivery layer attempts to deliver” was presented as a required step before the outcome branches, but a notification may be expired before any delivery attempt begins. Fixed: step 2 now marked optional; branch 3c explicitly notes that step 2 need not have occurred.
status_of and pending_for with empty/malformed inputs unspecified. Decision points said “no precondition beyond id presence” without defining the empty-input outcome. Fixed: both now explicitly state that empty inputs return not-known and [] respectively, by the same rationale as subscribed/subscribers_for in Subscription.
status_of missing from Behavior section. Every other action had behavioral observations; status_of was covered in Outputs and Decision points but not Behavior. Fixed: note added stating status_of is read-only, returns payload through all states including terminal, and no notification becomes inaccessible after resolution.
Terminal timestamp immutability not an invariant. Invariant 1 covered the four creation-time fields; the State section stated delivered_at, failed_at, expired_at “never change after set” informally but this was not elevated to an invariant. The Generation acceptance argument depends on it. Fixed: Invariant 1 extended to cover terminal timestamps explicitly.
No notification durability invariant. “No notification is deleted” appeared in Behavior and Generation acceptance but not as a formal invariant. Fixed: Invariant 9 added — notification records are durable; total count is monotonically non-decreasing.
Breach adversarial scenario used incorrect historical-status language. “Status = pending at that time” conflates current status with historical status. A notification Pending at breach time but since delivered shows status = delivered now; the reconstruction requires timestamp logic, not current-status filtering. Fixed: breach scenario now uses the correct reconstruction: created_at ≤ T and (status = pending or applicable terminal timestamp > T), mirroring the Subscription regulated scenarios.

Refinement round — adversarial rerun. Eight findings, all closed in-pattern.

Generation acceptance overclaimed timeline exactness (Pass 1). Check 2 stated “the timeline is exact (Invariants 1 and 8)” — but Invariant 8 is best-effort under non-monotonic clocks. Sleight-of-hand. Resolved: check 2 now qualifies “exact with respect to stored timestamps (Invariants 1 and 4); wall-clock truth is subject to Invariant 8’s best-effort caveat,” and explicitly names the clock-skew anomaly case.
Generation acceptance assumed an enumeration capability the action surface doesn’t provide (Pass 1). Check 1 (“enumerate every notification”) is not satisfiable from the four action queries — pending_for filters Pending only; status_of requires knowing the id. Resolved: Generation acceptance now opens with an explicit audit-surface / action-surface distinction — the store inspected on stored fields is the audit surface, complementary to and distinct from the action surface.
Recipient_ref equality not stated (Pass 2). The atom treats recipient_ref as opaque but implicitly requires equality for pending_for filtering and status_of lookup. Resolved: Inputs section now states equality-testing is the one operation an opaque reference must support; no parsing or normalization.
Expiry-as-separate-concept considered for extraction (Pass 2). Expiry-as-time-bounded-resolution recurs across atoms (Subscription’s time-bounded subscription, Provisional Commitment’s confirmation window). Kept in-pattern because the three terminal states answer three distinct operational questions (Delivered: did it arrive?; Failed: did the attempt produce a recorded negative outcome?; Expired: did the window pass with no outcome at all?), each called by a different actor (delivery layer, failure handler, expiry scheduler). Recorded here as Pass 2 considered-and-kept.
Empty-check semantics on opaque recipient_ref (Pass 3). “Non-empty” was undefined for an opaque value. Resolved: Decision points now state “non-empty — specifically, not null, undefined, or the empty string” with explicit note that the atom does not parse the opaque value beyond presence.
Fail-vs-expire policy is part of the audit surface but Generation acceptance didn’t require its disclosure (Pass 3). The same operational event maps to different terminal states across deployments, depending on local policy. Cross-deployment audit cannot interpret records uniformly without knowing each deployment’s policy. Resolved: Generation acceptance check 5 now names the fail-vs-expire policy as a required disclosure alongside the composing-pattern configuration.
Pending may persist indefinitely; not stated explicitly (Pass 3). A deployment that never calls expire produces an unbounded Pending set; the atom permits this but didn’t say so. Resolved: Behavior bullet added stating that Pending is allowed to persist indefinitely and that bounded lifetimes are the composing system’s responsibility.
Forthcoming-link cleanup. Composition notes still marked Notification Fanout as *(forthcoming)* after the composition had landed. Per workflow step 5 in CLAUDE.md, the marker is removed and the reference linked.

Library-wide concerns surfaced but not resolved in this round — same set Subscription’s refinement round surfaced (audit-surface convention, opaque-ref empty-check semantics). Per-pattern fixes landed; canonical statements belong in a shared document.

Scheduled rescan: 2026-05-20. One refining finding; closed in-pattern.

Rejection-path example absent (Pass 3). Subscription’s Examples section includes a dedicated “Rejection path” subsection showing rejected(already-subscribed); Notification’s Examples section had no analogous rejection-path example for create. The create rejection reasons (invalid-request) are clearly stated in Decision points, but peer-pattern parity and fresh-reader completeness favor a worked example. Resolved: rejection-path example added showing create(recipient_ref: "", payload: {...}) → rejected(invalid-request) with the consequence (no notification_id issued, no record created).

Formal-layer vote — 2026-06-03: YES (model pending). Invariant 2 (status monotonicity Pending→exactly one terminal, no return), Invariant 3 (terminal exclusivity), and atomic status+timestamp form a state-machine absorption claim. Load-bearing temporal/ordering/safety claims a derived formal model would verify; none exists yet, so the pattern is downgraded to grounded (English) — formal layer pending until the model is authored and verifies (findings flow back into this English spec per the conflict protocol). Vote per pressure-testing.md §Formal models — The formal-layer vote.

Formal model — 2026-06-03: Alloy structural model authored and verified; pattern promoted to grounded. Derived model notification.als + buggy twin notification-buggy.als, checked headless by the org.alloytools.alloy.dist analyzer via tools/harness/check.mjs (drafted by a Sonnet subagent, gated by Opus review + an independent buggy-twin run). What it checks: a static structural model of notification records over the status lifecycle {Pending, Delivered, Failed, Expired} with transitions as pre/post predicates. Nineteen named check asserts cover Invariant 2 (status monotonicity — every transition requires a Pending source; no two terminal statuses co-occur), Invariant 3 (terminal exclusivity — at most one terminal timestamp; each terminal status carries only its own timestamp), Invariant 4 (timestamp ⇔ status biconditional), Invariant 6 (store-level id uniqueness), and transition correctness — all UNSAT. Nine run predicates are all satisfiable (non-vacuity), including the three transition runs, so the lifecycle checks are not vacuous. Buggy twin weakens the TimestampStatusCoherence delivered_at arm from a biconditional (iff) to a one-way implication, letting a Failed/Expired/Pending record also carry delivered_at; the checker finds counterexamples on five asserts (A_Inv3_AtMostOneTerminalTimestamp, A_Inv3_FailedHasOnlyFailedAt, A_Inv3_ExpiredHasOnlyExpiredAt, A_Inv3_PendingHasNoTimestamps, A_Inv4_DeliveredAtIffDelivered). Out of model scope: wall-clock timestamp ordering (Invariant 8 — best-effort; a deployment-level concern). Conflict-protocol outcome: none — the model corroborates the English; canonical English unchanged.

AI adversarial round — Final Critique 4 (first real AI round) — 2026-06-18. This atom grounded 2026-05-20 under the early process — its only prior “adversarial rerun” was author-conducted (no AI model credited; the sole AI involvement was the Alloy formal model) — and carried the legacy grandfathered token. This round is its first AI-conducted adversarial round (fresh-reader Opus, Happy-Torvalds-X2); it is the atom’s Final Critique 4. One foundational finding closed: F1 — Logic Confinement: the clock and notification_id were read/minted inside the transitions (“implicit clock” / “= now” / “system-generated”); they are now host-injected at the I/O seam, with the caller signature create(recipient_ref, payload) unchanged. Refining: a byte-exact string-input policy for recipient_ref/payload; single-record transition serialization named as the load-bearing precondition for Invariants 2 and 3; an acronym gloss. The invariant set held at 9, so the fix is additive with no constituent-change cascade. Formal-layer vote stands YES (Alloy model present); the time/id seam is out of model scope, so F1 does not reopen it. Confirming fresh-reader Opus clearance gate (2026-06-18): CLEAR, 0 foundational. Compositions affected — confirming check only, NOT a re-pass (the create signature and the nine-invariant count are unchanged): Notification Fanout, Preference-Aware Notification Fanout. Grounds at Final Critique 4.

Showcase pass — 2026-06-29. Representational-only annotation/legibility pass; no guarantee, invariant, number, formula, signature, or rejection taxonomy changed. (a) Four-kind [Term] annotation applied across the body and a ## Terms registry added before Composition notes (21 terms): 6 Operations (Create, Deliver, Fail, Expire, Status Of, Pending For); 8 Fields (Notification Id, Recipient Ref, Payload, Created At, Status, Delivered At, Failed At, Expired At — all “Field of: the notification record”, no separate Type card, plain-noun referent); 0 Parameters (every input is stored as-itself); 7 Members (Pending state + Delivered/Failed/Expired terminals + Invalid Request/Not Known/Not Pending rejections). Survivors left backticked: the one labeled projected-contract signature per Operation; the ok success token; the lowercase stored status values (pending/delivered/failed/expired); the status_of return-shape literal; qualified cross-atom calls (Subscription.subscribers_for, Notification.create); the non-existent resolve; concrete example calls, ids, payloads, and timestamp formulas; and external standard tokens. The clock and id are host-injected at the I/O seam and consumed only for timestamp stamping — there is no derived status, so no [Now] term (mirrors legal-hold). (b) Summary/blockquote merge — ## Summary moved to the top (after TOC, before Intent), the descriptive top blockquote folded out after confirming each claim is carried by Summary/Intent/Identity model/Invariant 1/Behavior; no also-known-as line existed, so none was invented. (c) Lineage collapsed into a <details markdown="block"> block. (d) prose cut #1 — Summary state names marked, already one-idea-per-sentence. (e) prose cut #5 — the State “Transitions” list rendered as a transition table (action / from / to / stamps / result / rejections), with the shared terminal preconditions and serialization-per-id semantics kept in the prose beside it. Re-verified, not re-grounded: Status stays at grounded on Final Critique 4 — 2026-06-18. Gates: lint clean (O-term resolver — every marker resolves and every card is used); term-adapter derives cleanly (21 terms); 9 invariants preserved; .als untouched — harness re-run green: notification.als PASS + notification-buggy.als --buggy rejected.