Roadmap

Table of contents

Roadmap

What the library is building toward, in dependency order. Atoms before the compositions that name them. Each entry names what it unlocks.

The library’s current state is documented in readme.md. This file records what comes next and why, at the granularity of individual patterns. Priority reflects dependency readiness first, regulatory coverage second — a composition that needs three new atoms is lower priority than one that needs one, regardless of business value, because the blocking atoms must land first.

The topological ordering principle is codified in pressure-testing.md: atoms before compositions, constituents before the applications that name them. This roadmap is organized accordingly.

Current state

Taxonomy flattened; status reconciled — 2026-06-08. The atoms/<category>/ subfolders were dissolved; atoms are stored flat (atoms/<name>.md) with classification derived (overlays from the composition graph; domain the one intrinsic, EOS-gated axis), and the per-category READMEs replaced by a generated browse-by-overlay catalog (atoms/index.md, via tools/taxonomy/generate_views.py). Corpus unchanged at 45 grounded patterns (27 atoms, 18 compositions); the move was path-safe — all 74 formal models still found and green. This ROADMAP’s atom/composition status was then reconciled to reality: the planned-sequence atoms (#7–#14) are all grounded, and the genuine remaining composition backlog is C6, C7, C11, C15, C17, C18 (all unblocked, none blocked on a missing atom). See atoms/TAXONOMY.md.

Coverage GAPs closed — 2026-06-04. The 6 genuine coverage GAPs the inaugural cross-check surfaced (Medication Order Inv 3/4, Credential Inv 7, Legal Hold Inv 6, Provisional Commitment Inv 8, Capacity Constraint Inv 5; plus the Inv 14 reconsideration) are all closed — produced by parallel Sonnet subagents, Opus-gated (diff review + independent harness re-run). Medication Order gained an Alloy structural model (medication-order.als, mirroring clinical-observation.als) covering the pre-dispensing-only + linear-amendment invariants; Credential, Legal Hold, Provisional Commitment, and Capacity Constraint gained TLA+ model extensions (rotation-chain link; two-clock temporal ordering; release/expire transition timestamps; a release action making non-negativity non-vacuous). Capacity Constraint Inv 14 (within-action atomicity) was reconsidered to out-of-scope (a host obligation, not an action-vs-action interleaving — parallels Party Identity Inv 11). Every vote-named load-bearing invariant across the five patterns now carries a named check and its own dedicated, checker-rejected buggy twin — Legal Hold, Provisional Commitment, Capacity Constraint, and (on a 2026-06-04 follow-up audit) Credential each carry a second isolated twin so no previously-covered invariant lost its counterexample when the new check landed. (Credential initially shipped a single combined twin in which the shorter Inv 7 counterexample masked the Inv 2 counterexample; the follow-up split it into credential-buggy.tla (Inv 7) and credential-buggy-toctou.tla (Inv 2).) The five patterns drop their formal coverage: Inv N pending caveat and return to unqualified grounded. See tools/harness/coverage/README.md §Resolution. Harness re-run green: 5 correct models hold, 9 twins rejected.

Provenance (atom #7) grounded — 2026-06-04. The first net-new pattern of the sprint: a regulated compliance atom — an append-only single-artifact custody chain whose load-bearing guarantee is custody continuity (transfers are hand-to-hand, exactly one current custodian at all times, no gap; the outgoing custodian is read from chain state so a false predecessor cannot be forged). The EOS Pass-2 boundary against Event Log holds (custody continuity is not expressible on a content-agnostic event stream), and the disclose overlap with the existing Selective Disclosure atom was extracted as a composing boundary. Sonnet-drafted against an Opus plan, Opus-gated (Pass 1 / 2 / 3 + Final Critique; two foundational + four refining findings closed in-pattern), formal-layer vote YES with an Alloy model (provenance.als) + buggy twin verified in tools/harness/. This brings the library to 39 grounded patterns and unblocks Chain of Custody (C12) — the cross-domain pharma↔legal-evidence reference composition — whose remaining constituents (Actor Identity, Tamper Evidence, Retention Window, Audit Trail) are all already grounded.

Chain of Custody (C12) grounded — 2026-06-04. Immediately after Provenance, C12 was authored end-to-end (Opus plan → Sonnet draft → Opus gate: Pass 1 / 2 / 3 + Final Critique, two foundational + three refining findings closed → TLA+ binding-bijection model + buggy twin verified in tools/harness/). C12 composes Provenance + Audit Trail (substrate) — the substrate supplies Actor Identity attribution, Tamper Evidence sealing, and Retention Window governance transitively, so naming Audit Trail satisfies the “+ Actor Identity + Tamper Evidence + Retention Window” requirement per the compositions-of-compositions convention. Its emergent guarantee is records-alone custody proof (verify_custody): unbroken + attributed + tamper-evident + retention-governed custody from origin to disposition, which neither constituent provides alone. C12 is the library’s cross-domain flagship — pharmaceutical (FDA 21 CFR Part 211 / DEA 1304) and legal-evidence (FRE 901(b)(9)) chain of custody are the same structure, one composition serving both — and the first composition to compose the Provenance atom. This brings the library to 40 grounded patterns (14 grounded compositions) and retires the Chain-of-Custody forthcoming-link in Provenance.

Workflow / State Machine (atom #9) grounded — 2026-06-04. The general-purpose state-machine primitive: a named instance moving through a deployment-declared finite set of states via declared transitions, enforcing only-declared-transitions, exactly-one-current-state, terminal absorption, and a replay-deterministic append-only transition history; it gates (but deliberately does not evaluate) caller-asserted transition guards. EOS boundaries held against Approval Step (the fixed-state sibling — states fixed by the atom vs. declared by the deployment) and Event Log (declared-transition enforcement is not expressible on a content-agnostic stream); guard evaluation and a shared-declaration Definition Registry were extracted as composing concepts. Sonnet-drafted against an Opus plan, Opus-gated (one foundational finding — a fired_at cross-entry monotonicity rule that contradicted the best-effort-clock claim, relaxed to match Event Log — plus one refining, both closed), formal-layer vote YES with an Alloy model (workflow-state-machine.als) + buggy twin verified in tools/harness/. This resolves the workflow one-atom open question (the category now stands on two atoms), unblocks Stateful Workflow Execution (C10) — the last composition that was blocked on a remaining atom, so every C-numbered composition is now grounded or unblocked — and brings the library to 41 grounded patterns.

Stateful Workflow Execution (C10) grounded — 2026-06-04. Immediately after Workflow / State Machine, C10 was authored end-to-end (Opus plan → Sonnet draft → Opus gate: Pass 1 / 2 / 3 + Final Critique, one foundational + one refining finding closed → TLA+ approval-gated-transition model + buggy twin verified in tools/harness/). C10 composes Workflow / State Machine + Approval Step + Permissions + Assignment + Audit Trail (substrate) and is the first composition to compose the Workflow / State Machine atom. Its load-bearing emergent property is the precise closure of an atom-level extraction: Workflow / State Machine deliberately gates on a caller-asserted guard_satisfied without evaluating; C10 evaluates approval-type guards by binding each guarded transition to an Approval Step and asserting guard_satisfied = true only when that step is genuinely Approved — guard evaluation re-converges here. The foundational gate finding (the gate’s Approval Step submitter must be the workflow initiator, else the moot-gate cascade is unauthorized under Approval Step Invariant 5) was closed. This brings the library to 42 grounded patterns (15 grounded compositions) and retires the C10 forthcoming-links in Workflow / State Machine and Approval Step. With it, every one of the seventeen C-numbered compositions is now grounded or unblocked, and no composition is blocked on a remaining atom.

Forensic Recovery (C3) grounded — 2026-06-04. The deliberately-easy follow-on: Soft Delete + Audit Trail (substrate) — the same atom-plus-substrate template as C12, gated quickly. Every delete/restore/purge is attributed, tamper-evidently sealed, and recover_history reconstructs the full ordered lifecycle that Soft Delete’s current-state-only summary discards; the headline invariant is no record is purged without an auditable, sealed record of who/when/why. EOS boundary held: the purge-eligibility gate (Legal Hold / Retention Window) stays with Defensible Retention (C1); C3 records faithfully. The one gate finding — the binding bijection needed its sole-write-path precondition and a verifiability correction (Soft Delete keeps no transition history, so record_to_events + the Audit Trail Event Log is authoritative) — was closed. TLA+ binding-bijection model + buggy twin verified. This brings the library to 43 grounded patterns (16 grounded compositions) and retires the Forensic Recovery forthcoming-links in Soft Delete.

Consent & Preference Management with Revocation Propagation (C2) grounded — 2026-06-04. The GDPR consent-lifecycle composition: Consent + Permissions + Audit Trail (substrate) + a distinct consent-record Retention Window placement. Authored end-to-end (Opus-gated: Pass 1 / 2 / 3 + Final Critique, foundational + refining findings closed → TLA+ binding-bijection model + buggy twin verified in tools/harness/). Two halves to its emergent guarantee: consent-gates-processing (processing_permitted is the single gate every processing system consumes, permitted iff Consent.check → granted) and revocation propagation (the load-bearing one) — withdraw_consent commits the Consent revoke and a consent.revoked event enumerating the complete downstream processing-scope set the consent governed, together or not at all (the revoke ⇔ complete-propagation-record binding bijection, modeled on audit-trail.tla / forensic-recovery.tla). EOS Pass 2: Permissions confirmed a constituent (the inward-authorization surface gating administration) rather than a peer, with the inward/outward separation locked as Invariant 7; downstream cessation and delivery-shaping preference management (C11) extracted as composing concepts. This brings the library to 44 grounded patterns (17 grounded compositions) and retires the C2 forthcoming-links in Consent and KYC (C8).

Reservation Lifecycle (C9) grounded — 2026-06-04. The pool-aware reservation composition: Capacity Constraint Enforcement + Provisional Commitment + Duplicate Prevention + Event Log + Actor Identity — the pool-arithmetic superset of Idempotent Reservation (which wires Provisional Commitment + Duplicate Prevention but not pool arithmetic). Authored against Idempotent Reservation as the structural template (Opus gate: Pass 1 / 2 / 3 + Final Critique → TLA+ allocation-coherence model + buggy twin verified in tools/harness/). The load-bearing emergent guarantee is allocation coherence — the pool’s allocated total stays in exact lockstep with the live-reservation set (Held or Confirmed), within [0, capacity] — which the composition owns via the reservation_to_pool binding (with a slot_released flag): reserve allocates-and-holds atomically (compensating release if the hold fails), confirm_reservation keeps the slot, cancel_reservation/expire_reservation return it exactly once. The three reservation-bug failure modes — oversell, slot-leak, double-release — are each foreclosed by a named mechanism. EOS Pass 2: the binding is the emergent responsibility neither Capacity Constraint (fungible arithmetic, no per-allocation identity) nor Provisional Commitment (per-reservation identity, no pool) owns; Event Log + Actor Identity composed directly (the lighter pairing, Audit Trail named as a peer for litigation-exposed deployments); overbooking (a capacity choice) and un-booking (Reversal) extracted. This brings the library to 45 grounded patterns (18 grounded compositions) and retires the C9 forthcoming-links in Capacity Constraint Enforcement and Provisional Commitment.

Immutable Transaction Ledger with Selective Disclosure (C6) grounded — 2026-06-08. The disclosable-ledger composition: Audit Trail (substrate, → Event Log + Actor Identity + Tamper Evidence + Retention Window) + Selective Disclosure, with Idempotent Reservation / Duplicate Prevention as optional at-most-once-append enrichment (named, not core) — the same atom-plus-substrate template as C12 (Chain of Custody) and C3 (Forensic Recovery). Authored end-to-end (Opus gate: Pass 1 / 2 / 3 + Final Critique; one foundational finding — the disclosed-subset membership predicate, pinned to ledger.entry transaction events validated against the substrate Event Log — and two refining findings closed → TLA+ binding-bijection model + buggy twin verified in tools/harness/). Two load-bearing emergent guarantees: disclosure-accountability binding bijection — every disclose_subset writes, atomically, one Selective Disclosure record and one ledger.disclosed Audit Trail event, so the act of disclosing is itself an immutable, attributed ledger entry (the TLA+ model subject, mirroring chain-of-custody.tla / forensic-recovery.tla); and verifiable partial disclosure — any disclosed subset is independently provable authentic against the ledger seal while the undisclosed remainder stays undisclosed and uncompromised, stated as a behavioral capability obligation on the substrate’s tamper-evidence (Merkle proofs / accumulators / signed packages are typical realizations in rationale only, not a mechanism mandate — pinning one would contradict Tamper Evidence’s own mechanism-neutrality). EOS Pass 2: the authorization gate (Consent / Permissions), at-most-once append (Idempotent Reservation), hold-blocks-purge (Legal Hold / Defensible Retention), and artifact custody (Provenance) are all externalized as peers or optional enrichments, not absorbed. C6 is the first composition to compose the Selective Disclosure atom and the cross-domain reference case for the disclosable immutable ledger — broker-dealer trade confirmations (SEC Rule 17a-4), healthcare accounting-of-disclosures (HIPAA §164.528), and clinical-trial submissions (21 CFR Part 11) are the same structure. This brings the library to 46 grounded patterns (19 grounded compositions) and retires the C6 forthcoming-links in Selective Disclosure and Provenance. C6’s fresh-reader Opus council (Final Critique 5) surfaced a new roadmap item: a forthcoming Subset Proof (selective tamper-evidence) atom — the verification dual of Tamper Evidence’s whole-set seal, “prove a named subset of a sealed set is included without revealing the complement” — which would let C6 delegate its verification_bundle to a named constituent surface rather than construct it at the composition layer. Named here as a backlog atom, not yet authored; until it lands, C6’s subset-proof surface is composition-introduced and rests on the configured Tamper Evidence mechanism’s inclusion-proof capability.

Data Subject Rights Fulfillment (C7) grounded — 2026-06-09 (Final Critique 5). The data-subject-rights composition: Selective Disclosure + Defensible Retention (C1, substrate → Legal Hold + Retention Window + Audit Trail) + Consent (read-only authority oracle). The load-bearing reframe: C7 is not a “rights system” but a conflict-resolution system over a record universe — when a subject exercises access (GDPR Article 15) or erasure (Article 17), four claims collide per record (access, erasure, legal hold/retention, consent), and C7 resolves each into exactly one recorded, attributed disposition (access: included / withheld(...); erasure: erased / retained(legal-hold | retention-obligation | other-lawful-basis)). Two load-bearing emergent guarantees: no-silent-omission (every in-scope record carries exactly one disposition; none silently dropped) and the request ⇔ accountable-complete-fulfillment binding bijection (the complete disposition set, the response-disclosure, and the sealed dsar.*_fulfilled event commit together or not at all). The erasure path wraps C1’s purge_record gate — ok→erased, under-legal-hold→retained(legal-hold) (Art 17(3)(e)), not-eligible→retained(retention-obligation) (Art 17(3)(b)) — adding only the Art 17(1)(b) Consent-oracle branch; Consent is consulted read-only, never mutated. Authored end-to-end: author gating review (two foundational + five refining closed), formal-layer vote YES with a TLA+ model checking the binding bijection and a no-silent-omission coverage totality (the property C6’s binding-only model did not need) + two buggy twins (one per load-bearing invariant) verified in tools/harness/, and a fresh-reader Opus council (Pass 1 GRID / Pass 2 EOS / Pass 3 Linus-X2) that surfaced three foundational findings — the Consent oracle’s expired/not-known outcomes undefined in the erasure branch, the C1-internal-vs-C7 orphan conflation, and an Invariant 1 atomicity overclaim — all folded, foundational now at zero. C7 is the first composition authored under the capability-provenance rule, the first to compose Consent as a read-only oracle and Defensible Retention (C1) as a substrate. It seeds a forthcoming Completeness Model atom (accountable enumeration of a record universe with per-record disposition — a shared C7/C8 primitive C7 exposes, not a C7-owned abstraction) and retires the C7 forthcoming-links in Consent, Legal Hold, Selective Disclosure, and Provenance. The Phase 4 Opus Happy-Torvalds-X2 clearance gate cleared in a fresh session on 2026-06-09 (claude-opus-4-8): foundational findings at zero, six refining/rhetorical findings folded, and the correct TLA+ model + both buggy twins re-verified (CORRECT holds at 2 states; -buggy rejected on Inv1_BindingBijection; -buggy-coverage rejected on Inv2_NoSilentOmission). C7 grounds on Final Critique 5, bringing the library to 47 grounded patterns (20 grounded compositions).

Authenticated Actor (C17) grounded — 2026-06-10 (Final Critique 4). The authenticated-principal composition: Credential (the authentication / gating surface) + Actor Identity (the attestation surface) — answering the three demos/attributed-permissions-admin/CORNERS.md §Cross-atom identity surface aliasing questions as three emergent invariants. The load-bearing emergent guarantee is the revocation cascade as forward closure: attest_as_actor is gated on the bound credential’s live Active status, read atomically with the attestation write (serialized on the gating (principal_ref, credential_type) credential record — the row Credential.revoke also locks), so a revoked login produces no new attestations — while attestations made before revocation stay valid, because the cascade is forward-closure only, never a set-revocation (attestations are immutable point-in-time records, so there is no active-attestation set to walk). The other two emergent invariants — secret-surface separation (cross-routing foreclosed structurally; distinct-provisioning an externally-clearable deployment obligation) and the principal_ref ⇔ actor_ref namespace bijection (register-time conflict guard + atomic strict-inverse maps + immutability) — are the structural conditions that make the cascade and its audit trail meaningful. Authored end-to-end: three-round baseline + author Final Critique (three foundational + four refining closed), formal-layer vote YES with a TLA+ revocation-cascade model + TOCTOU buggy twin verified in tools/harness/ (CORRECT holds at 16 states; -buggy rejected on Inv1_NoSignAfterRevoke), and the Phase 4 Opus Happy-Torvalds-X2 fresh-reader clearance gate cleared 2026-06-10 (claude-opus-4-8): foundational findings at zero, five refining folded, model + twin re-verified, and capability provenance re-derived head-on against the constituent specs (the cascade gate confirmed housed at the composition layer, not mis-attributed to Actor Identity, which cannot see a credential revocation). C17 is Login’s outbound-attestation counterpart (Login forward-closes the session set; C17 forward-closes the attest surface), the first composition to pair Credential with Actor Identity, and retires the two Authenticated Actor pending markers in Credential and Actor Identity. This brings the library to 48 grounded patterns (21 grounded compositions).

Actor Suspension (C18) grounded — 2026-06-10 (Final Critique 4). The outbound multi-surface de-authorization composition: Actor Identity (the suspended actor’s composition-introduced Active/Suspended lifecycle) + Permissions (grant-revocation target) + Session (session-revocation target) + Audit Trail (substrate → Event Log + Actor Identity + Tamper Evidence + Retention Window) + optional Credential. Login’s outbound-side counterpart — where Login (C13) wires Credential.verify → Session.issue on the way in, C18 wires suspend → revoke every grant + every session (and optionally the credential) on the way out. Three emergent invariants: atomicity of multi-surface revocation (after suspend_actor succeeds, zero active grants and zero active sessions committed as one transaction, no partial state — the load-bearing claim, with all-or-nothing the default precisely because a half-suspended actor is a worse security state than a clean failure, a deliberate inversion of Login’s best-effort cascade), audit completeness (the sealed actor.suspended event enumerates every revoked grant_id and session_token), and suspension cascade ordering (the Active→Suspended gate fires the cascade exactly once; a second suspend_actor is a no-op; a benign already-terminal target is counted, not aborted — mirroring Login’s Final Critique 4 finding FC1). Authored end-to-end: three-round baseline + author Final Critique, formal-layer vote YES with a TLA+ atomic-cascade model + non-atomic buggy twin verified in tools/harness/ (CORRECT holds at 2 states, saturated; the twin rejected on Invariant 1), and the Phase 4 Opus Happy-Torvalds-X2 fresh-reader clearance gate cleared 2026-06-10 (claude-opus-4-8): foundational findings at zero, five refining folded, model + twin re-verified, and capability provenance re-derived head-on against the constituent specs (the Active/Suspended lifecycle confirmed composition-introduced — Actor Identity carries no lifecycle state — and unified_actor_namespace an honest deployment-config capability with its coincidence routed to an externally-clearable check). C18 realizes the deprovisioning-cascade obligation Permissions’ Mass revocation edge case and Actor Identity’s actor-lifecycle deferral both anticipate, and composes with C17 (closing the attest surface) plus Credential revocation to close the full outbound surface. This brings the library to 49 grounded patterns (22 grounded compositions).

Capability-Backed Sharing (C15) grounded — 2026-06-10 (Final Critique 4). The accountable-bearer-sharing composition: Capability (the bearer token whose scope is an authorized disclosure) + Selective Disclosure (the disclosure-accounting record) + Audit Trail (substrate → Event Log + Actor Identity + Tamper Evidence + Retention Window) — mirroring C6’s substrate-plus-Selective-Disclosure shape. It reconciles two designs that look incompatible: bearer-token sharing (possession authorizes; the redeemer is never identified) and regulated disclosure audit (every disclosure accountable to a named, non-repudiable authorizing party). The load-bearing emergent property is the audit-subject asymmetry — every capability-backed disclosure names the allocator (attested under their own credential at allocation, carried immutably in the capability) and, by construction, no redeemer, resting on Capability’s declared Invariants 3 (bearer redemption) and 5 (audit asymmetry) surfaced through redeem’s allocator_ref return, never an ambient “the system records no redeemer.” Its second load-bearing claim is the disclosure-accountability binding bijection (mirroring C6): each redemption-that-discloses commits the Selective Disclosure record, the sealed sharing.disclosed event, and the redemption-decrement together or not at all — a recoverable store write under the host transaction, so closer to C6 than to C7’s irreversible purge. Formal-layer vote YES with a TLA+ binding-bijection model + non-atomic buggy twin verified in tools/harness/ (CORRECT holds at 4 states, saturated; -buggy rejected on Inv2_BindingBijection), and the Phase 4 Opus Happy-Torvalds-X2 fresh-reader clearance gate cleared 2026-06-10 (claude-opus-4-8): foundational findings at zero, four refining/rhetorical folded, model + twin re-verified mechanically, and capability provenance plus every constituent invariant count (Capability 1–12, Selective Disclosure 1–6, Audit Trail 1–8) re-derived head-on against the constituent specs. C15 is the library’s worked example of the object-capability (OCAP) model composed with regulated audit, the first composition to compose Capability with Selective Disclosure, and retires the C15 forthcoming-reference in Capability. This brings the library to 50 grounded patterns (23 grounded compositions).

Composition-state adjudication (Refactor 1) and the Idempotency Result Memo proposal — 2026-06-10. The Execution Contract now owns composition-state semantics with a two-arm rule (execution-contract.md §Composition state): every Application-state element is either a derived index — fully rebuildable from constituent stores, with a named rebuild procedure, excluded from the atomicity surface, claiming no cross-constituent consistency — or evidence of a not-yet-extracted atom, declared extraction-pending with the proposed atom named. This closes the spec-format/Contract composition-state divergence inside the newly assigned ownership seam (spec-format owns containers; the Contract owns section-content semantics; the Contract’s mapping tables plus section-name classification are the SSOT bridge, with the section-name lint check specified — see spec-format.md §Ownership seam). The non-derivable pole forces a new backlog atom proposal: Idempotency Result Memo — token → result, single write, window-governed eviction; the result-replay half of idempotent-replay semantics that Duplicate Prevention’s own spec explicitly disclaims (DP answers have I seen this identity? — membership, no payload; the Memo answers what did I return for it?). Named here as a backlog atom, not yet authored; its formal obligations lift substantially from the existing idempotent-reservation.tla (exactly-once-in-window, unsafe-eviction-ordering). Until it lands, Idempotent Reservation’s token_results (and Reservation Lifecycle’s inherited copy) is the worked extraction-pending case, and C6’s disclosure_to_event is the worked derived-index pole. The corpus-wide Application-state classification audit is recorded as methodology debt #9 below.

As of the 2026-06-03 formal-layer vote sweep (aggressive bar), all 38 then-grounded patterns were fully grounded — the backlog models having landed and the bar reconsidered. (This is the 2026-06-03 cohort, not the current total; the running per-grounding bullets above carry the library to 47 grounded patterns.) Coverage cross-check — inaugural sweep (2026-06-04): all 22 vote-yes models were run through the formal-layer coverage cross-check (tools/harness/coverage/, see its README). 14 fully clean; 4 by-construction flags resolved (2 promoted to explicit checks — Event Log Inv 1, Provisional Commitment Inv 3; 2 recorded as deliberate frame properties — Approval Step Inv 9, Medication Order Inv 9); and 6 genuine coverage GAPs across 5 patterns (Medication Order Inv 3/4, Credential Inv 7, Legal Hold Inv 6, Provisional Commitment Inv 8, Capacity Constraint Inv 5/14) — each a second vote-named invariant with partial/no formal coverage, now honestly labeled formal coverage: Inv N pending on those patterns’ Status lines and queued early-sprint. Not English regressions; the primary load-bearing invariant of each is verified with a rejected twin. The entire formal-model backlog is complete: 18 TLA+ models (Opus-authored) and 4 Alloy structural models (Sonnet-drafted, Opus-gated) landed; 3 clock/precedence patterns were reconsidered to English-only (formal-not-warranted). Zero pending. Every model ships a buggy twin the checker rejects as the vacuity guard. Eight backlog models landed (the four high-stakes TLA+ models plus the Med–High tier: Assignment, Medication Order, Preference / Personalization, Approval Step). Bar reconsideration (2026-06-03): the aggressive-bar YES on three of the five flagged clock/precedence patterns was downgraded to NO (formal-not-warranted) on a second pass — Retention Window, Session, Consent are records-alone/precondition claims a model would only re-confirm, so they return to fully grounded English-only; Provisional Commitment and Duplicate Prevention keep their YES (genuine action-vs-action races — confirm-vs-auto-expiry, concurrent first-record) and remain in the TLA+ queue. See each pattern’s Lineage §Formal-layer vote for the per-pattern rationale. KYC / Customer Onboarding (C8) grounded on Final Critique 4 (2026-06-03). Formal-model backlog progress (2026-06-03): the four high-stakes TLA+ models are landed — Party Identity (party-identity.tla, 532 states clean), Event Log (event-log.tla, 119 states), Audit Trail (audit-trail.tla, buggy twin shows the non-atomic cascade is unsafe, 9 states), and Capacity Constraint Enforcement (capacity-constraint-enforcement.tla, buggy twin shows the TOCTOU race overshoots capacity, 7 states) — each with a buggy twin the checker rejects, all verified via tools/harness/; see each pattern’s Lineage §Formal model. Remaining lane: the 4 Alloy/structural drafts (Sonnet) and the ~17 lower-stakes TLA+ models (minus any removed by the bar reconsideration). The reproducible dual harness (tools/harness/: TLA+ via tla-checker WASM, Alloy via the alloy.dist jar under an npm-provisioned JRE 17) was stood up and all pre-existing models audited through it — surfacing a never-typechecked assertion in capability.als (fixed) and two further findings (see §”Harness audit findings” below). The next move on the atom side is one of the two remaining unstarted planned atoms (#7 Provenance, #9 Workflow / State Machine); on the composition side, one of the nine unblocked-and-unstarted compositions (C2, C3, C6, C7, C9, C11, C15, C17, C18 — see compositions section).

Formal-layer vote sweep — 2026-06-03. A formal-layer vote was cast for all 38 then-grounded patterns per pressure-testing.md §Formal models. The 13 that remain fully grounded: model present (7) — Capability, Attributed Permissions Admin, External Onboarding, Login, Privileged Access Provisioning, Session-Gated Authorization, Multi-Party Approval; voted formal-not-warranted (6) — Actor Identity, Selective Disclosure, Tamper Evidence, Personal Todo, Soft Delete, Notification Fanout. The other 25 voted YES but have no formal model authored yet; they are downgraded to grounded (English) — formal layer pending and constitute the model backlog. Update 2026-06-03: The entire formal-model backlog has landed — all 38 patterns are fully grounded. The 18 TLA+ models (the four high-stakes; the Med–High tier Assignment, Medication Order, Preference, Approval Step; the two kept clock candidates Provisional Commitment, Duplicate Prevention; the five remaining High-stakes Credential, Invitation, Idempotent Reservation, Defensible Retention, KYC; and the three Med Legal Hold, Shared Todo, Undo History) plus the 4 Alloy structural models (Permissions, Notification, Subscription, Clinical Observation — Sonnet-drafted, Opus-gated via review + independent buggy-twin run). A bar reconsideration restored three (Retention Window, Session, Consent) to fully grounded as English-only. Zero pending.

Formal-model backlog (triage — 2026-06-03). The 25 pending patterns, classified by property class → tool, with a suggested author by subtlety/stakes. Each model also ships a buggy twin (a deliberately-wrong variant the checker must reject) as the vacuity guard, and findings fold back into the canonical English per the conflict protocol. This table is the single home for the tool/author assignment (per DRY, it is deliberately not duplicated into each spec’s vote entry — the vote entries carry the why, the load-bearing invariants).

Alloy / structural — Sonnet may draft, Opus reviews:

Pattern	Tool	Author	Load-bearing property
Permissions ✅ landed 2026-06-03	Alloy	Sonnet draft → Opus gate	Active→Revoked monotonicity; terminal absorption — `permissions.als` + buggy twin (revoke drops Active precondition; 2 checks find counterexamples)
Notification ✅ landed 2026-06-03	Alloy	Sonnet draft → Opus gate	status monotonicity; terminal exclusivity — `notification.als` + buggy twin (timestamp `iff`→`implies`; 5 checks find counterexamples)
Subscription ✅ landed 2026-06-03	Alloy	Sonnet draft → Opus gate	at-most-one-active per key; no-id-reuse — `subscription.als` + buggy twin (drops at-most-one-active fact; check finds counterexample)
Clinical Observation ✅ landed 2026-06-03	Alloy	Sonnet draft → Opus gate	linear amendment chains (no branching) — `clinical-observation.als` + buggy twin (`lone`→`set` successor; 2 checks find counterexamples)

TLA+ / behavioral — Opus authors (interleaving, ordering, time, cascade):

Pattern	Tool	Stakes	Load-bearing property
Party Identity ✅ landed 2026-06-03	TLA+	High	Verified requires passed-after-most-recent-suspend (insertion order) — `party-identity.tla` + buggy twin (re-introduces the F3 defect; rejected at 22 states); 532 states clean
Event Log ✅ landed 2026-06-03	TLA+	High (foundational)	append-only + sequence monotonicity — `event-log.tla` + buggy twin (volatile-restart resets seq to 1; rejected at 14 states); 119 states clean
Audit Trail ✅ landed 2026-06-03	TLA+	High (substrate)	cascade-on-purge atomicity across 4 stores; honest-destruction — `audit-trail.tla` + buggy twin (non-atomic cascade → dangling partial; rejected at 4 states); 9 states clean
Capacity Constraint Enforcement ✅ landed 2026-06-03	TLA+	High	allocated ≤ capacity under serializable concurrency — `capacity-constraint-enforcement.tla` + buggy twin (TOCTOU check-then-commit overshoots to 3>2; rejected at 27 states); 7 states clean
Credential ✅ landed 2026-06-03	TLA+	High	active uniqueness under concurrent register — `credential.tla` + buggy twin (TOCTOU register → two Active; rejected at 33 states); 105 states clean
Invitation ✅ landed 2026-06-03	TLA+	High	single-resolution atomicity under concurrent accept/decline/revoke — `invitation.tla` + buggy twin (re-resolution override; rejected at 6 states); 5 states clean
Idempotent Reservation ✅ landed 2026-06-03	TLA+	High	exactly-once-in-window; unsafe eviction ordering — `idempotent-reservation.tla` + buggy twin (early eviction → double-effect; rejected at 14 states); 17 states clean
Defensible Retention ✅ landed 2026-06-03	TLA+	High	hold-blocks-purge (named race); multi-hold independence — `defensible-retention.tla` + buggy twin (purge ignores active hold; rejected at 8 states); 7 states clean
KYC / Customer Onboarding (C8) ✅ landed 2026-06-03	TLA+	High	adverse-trigger-precedes-suspend; open-trigger ⇔ Suspended — `kyc-customer-onboarding.tla` + buggy twin (suspend without trigger; rejected at 3 states); 3 states clean
Assignment ✅ landed 2026-06-03	TLA+	Med–High	reassign atomicity (no observable both/neither Active) — `assignment.tla` + buggy twin (non-atomic reassign → two-Active window; rejected at 6 states); 47 states clean
Medication Order ✅ landed 2026-06-03	TLA+	Med–High	hold carries prior_state; reinstate restores exactly it — `medication-order.tla` + buggy twin (reinstate-to-default; rejected at 11 states); 31 states clean
Preference / Personalization ✅ landed 2026-06-03	TLA+	Med–High	supersession atomicity (no observer sees two in-effect) — `preference.tla` + buggy twin (non-atomic supersession → two-in-effect; rejected at 5 states); 32 states clean
Approval Step ✅ landed 2026-06-03	TLA+	Med–High	approver/submitter exclusivity; concurrent step independence — `approval-step.tla` + buggy twin (unguarded approve; rejected at 4 states); 16 states clean
~~Consent~~ 🟢 reconsidered → NO (English-only), 2026-06-03	—	Med	earlier-terminal-event-wins (revoke vs expiry) — precedence by insertion order; records-alone, no model
Legal Hold ✅ landed 2026-06-03	TLA+	Med	concurrent-hold independence/isolation — `legal-hold.tla` + buggy twin (cascading release; rejected at 12 states); 27 states clean
~~Session~~ 🟢 reconsidered → NO (English-only), 2026-06-03	—	Med	conjunctive validity; revoked-precedes-expired — conjunction of record fields; interleaving lives in Session-Gated Authorization
~~Retention Window~~ 🟢 reconsidered → NO (English-only), 2026-06-03	—	Med (clock)	no-early-purge — single-action time-gated precondition; hold-blocks-purge race lives in Defensible Retention
Provisional Commitment ✅ landed 2026-06-03	TLA+	Med (clock)	confirm-within-window (expiry race) — kept YES, then modeled: `provisional-commitment.tla` + buggy twin (confirm-after-window; rejected at 10 states); 17 states clean
Duplicate Prevention ✅ landed 2026-06-03	TLA+	Med (clock)	single-recording; window monotonicity — kept YES, then modeled: `duplicate-prevention.tla` + buggy twin (re-record extends window; rejected at 11 states); 14 states clean. Surfaced + fixed a conflict-protocol case-2 model mis-encoding (lagging flag → derived membership)
Shared Todo ✅ landed 2026-06-03	TLA+	Med	cascade-on-delete (recall before delete); at-most-one-responsible — `shared-todo.tla` + buggy twin (delete without recall → dangling assignment; rejected at 4 states); 3 states clean
Undo History ✅ landed 2026-06-03; extended Tier A+B 2026-06-14	TLA+	Med	Inv 1/2/3/4 machine-checked over a real event-sourcing replay (`derived` = `StatusOf` replay, not an integer abstraction): log faithfulness, state equivalence, undo targeting, replay validity — `undo-history.tla` + 3 buggy twins (oldest-targeting → Inv 3/4; stale-undo → Inv 2; phantom-append → Inv 1), one vacuity guard per checked invariant; 563 states clean at MaxEvents=4/Ids={1,2}

Tally (original aggressive bar): ~4 Alloy/Sonnet, ~21 TLA+/Opus. Final 2026-06-03 state: all 18 TLA+ models landed (corroborating their English specs; one surfaced a conflict-protocol case-2 model mis-encoding, fixed in the derivation), 3 downgraded to English-only on the bar reconsideration (Retention Window, Session, Consent), leaving only the 4 Alloy/Sonnet structural drafts pending. The bar reconsideration was the right lever, exactly as anticipated here: the clock-based and precedence entries were the defensible “English + records-alone is sufficient” reconsiderations, and three of the five cleared it. Harness is settled (tools/harness/), so each model’s pass/fail is mechanical.

Harness chosen — tools/harness/ (2026-06-03). One reproducible dual harness, provisioned npm-only (no firewalled downloads): TLA+ via the tla-checker WASM checker (extends the original grants/tla-poc/run.mjs approach), Alloy via the org.alloytools.alloy.dist jar running headless under an npm-provisioned JRE 17 (javajre-linux-64; the JRE lives on the native /tmp FS because unpacking it into the mounted repo drops libjli.so). node check.mjs <model> [--buggy] enforces correct-holds / buggy-rejected; node audit.mjs runs every model. Each backlog model ships with a buggy twin as the vacuity guard. See tools/harness/README.md.

Harness audit findings (2026-06-03). All nine pre-existing formal models were run through the new harness. Six were clean (session-gated-authorization.als, attributed-permissions-admin.als, login.tla, attributed-permissions-admin.tla, MultiPartyApproval.tla + buggy twin). Three findings, all in patterns marked grounded, all outside the formal-model backlog — logged here for routing:

capability.als — never-typechecked assertion (fixed). Line 193 read r.status = Revoked implies no (r.status = Expired) — no applied to a boolean. The file never typechecked under the CLI, so assertion A_TerminalModesDistinguishable was never actually checked despite Capability shipping grounded on Final Critique 4. Corrected to r.status != Expired (case-2 model mis-encoding; English untouched). With it fixed, all 22 check assertions now run and hold — but the run surfaced a second finding: 4 vacuous run commands (ShowExhaustionTransition, ShowMultiUsePartialRedeem, ShowRevokeTransition, ShowExpireTransition) — transition examples with no instance in scope. Needs case-1-vs-2 diagnosis; not hand-patched.
privileged-access-provisioning.tla — not verifiable under the chosen checker. Its .cfg uses ACTION_CONSTRAINT, which the WASM checker does not support; the model returns NoInitialStates and is effectively unverified by this harness. Resolution is either the official tla2tools.jar (a firewalled download, unavailable in-sandbox) or a model rewrite expressing the constraint as an invariant.
external-onboarding.tla — low state count. Passes but explores only 44 states; worth confirming the bounds actually exercise the interleavings the English defends.

Atoms grounded (at grounded or grounded (English) — formal layer pending; see sweep note above):

compliance (13): Actor Identity, Capability, Consent, Credential, Invitation, Legal Hold, Party Identity, Permissions, Provenance, Retention Window, Selective Disclosure, Session, Tamper Evidence
healthcare (2): Clinical Observation, Medication Order
messaging (3): Notification, Preference / Personalization, Subscription
productivity (2): Assignment, Personal Todo
resource-lifecycle (3): Capacity Constraint Enforcement, Provisional Commitment, Soft Delete
temporal (2): Duplicate Prevention, Event Log
workflow (2): Approval Step, Workflow / State Machine

Atoms partially resolved: none — Preference / Personalization grounded on Final Critique 5 (2026-05-29); see atom #10 below.

Compositions grounded (at grounded or grounded (English) — formal layer pending; see sweep note above): Actor Suspension, Attributed Permissions Admin, Audit Trail, Authenticated Actor, Capability-Backed Sharing, Chain of Custody, Consent & Preference Management, Data Subject Rights Fulfillment, Defensible Retention, External Onboarding, Forensic Recovery, Idempotent Reservation, Immutable Transaction Ledger, KYC / Customer Onboarding, Login, Multi-Party Approval, Notification Fanout, Preference-Aware Notification Fanout, Privileged Access Provisioning, Reservation Lifecycle, Session-Gated Authorization, Shared Todo, Stateful Workflow Execution, Undo History.

The healthcare atoms (Clinical Observation, Medication Order) are outside the core dependency-ordered sequence — they were authored as worked examples of the methodology applied to a domain where the regulatory surface is HIPAA (Health Insurance Portability and Accountability Act) and 21 CFR Part 11 rather than the BSA (Bank Secrecy Act) / AML (Anti-Money Laundering) / GDPR (General Data Protection Regulation) / SOX (Sarbanes-Oxley Act) cluster the compliance atoms anchor. They are grounded and composable; their downstream compositions (e.g., a Clinical Trial Data Capture composition, a Medication Administration Record composition) are not on this roadmap yet because the worked-example value is in the atoms themselves rather than in any specific composition the library is committed to delivering next.

Planned-sequence atoms — all grounded (roadmap history)

All of atoms #7–#14 are now grounded; none remains on the planned sequence. The detailed entries below are retained as roadmap history (originally sequenced by how many downstream compositions each unblocked).

7. Provenance

Category: compliance — resolved to compliance (compliance-infrastructure primitive, regulated overlay).

Status: grounded 2026-06-04 (Alloy model provenance.als + buggy twin verified in tools/harness/). Sonnet-drafted against an Opus plan; Opus-gated through Pass 1 / 2 / 3 + Final Critique (two foundational + four refining findings closed in-pattern). Unblocks Chain of Custody (C12). The descriptive entry below is retained as roadmap history.

What it is. A compliance and temporal primitive: an append-only chain recording the origin, custody history, and transformation history of a record or artifact. Provenance answers where did this come from, who has handled it, and what has been done to it. It is distinct from Event Log (which records what happened in a system) and from Actor Identity (which verifies who performed an action) — Provenance specifically models the chain of custody of a thing, not a stream of system events. Each custody event is immutable once recorded; the chain is append-only.

Why it’s next. Of the remaining atoms, Provenance is the highest-leverage in terms of composing surface: it strictly blocks Chain of Custody (C12) — the library’s cross-domain reference case spanning pharmaceutical and legal-evidence custody — and additionally enriches Immutable Transaction Ledger (C6), Data Subject Rights Fulfillment (C7), and KYC (Know Your Customer) / Customer Onboarding (C8) as an optional composing atom for chain-of-custody guarantees. The scoping requires careful EOS Pass 2 work to establish what “this thing’s custody history” means without absorbing the event-log or actor-identity responsibilities — the boundary against Event Log is the key conceptual-independence test.

Key invariants (anticipated). Each provenance entry is immutable once recorded. The chain is append-only — no entry is removed or reordered. Every entry names a custodian (an actor reference), a timestamp, and an event type (originated, received, transformed, transferred, disclosed, archived). The chain is complete — no custody gap is permitted between recorded entries; a gap is a finding, not a valid state.

Standards anchored. ISO 23081 (records management metadata — provenance as a required metadata element); W3C PROV (data provenance ontology); FDA 21 CFR Part 211 (pharmaceutical chain of custody); SEC (Securities and Exchange Commission) Rule 17a-4 (records must be maintained as originally created — provenance of the original form).

Unlocks. Strictly blocks Chain of Custody (C12) — Provenance is C12’s core atom, not an enrichment. Additionally enriches Immutable Transaction Ledger (C6), DSAR (C7), and KYC (C8) as an optional composing atom for chain-of-custody guarantees; those three are unblocked without Provenance but gain emergent invariants when composed with it.

9. Workflow / State Machine

Category: workflow

Status: grounded 2026-06-04 (Alloy model workflow-state-machine.als + buggy twin verified in tools/harness/). Sonnet-drafted against an Opus plan; Opus-gated through Pass 1 / 2 / 3 + Final Critique (one foundational + one refining finding closed). Unblocks Stateful Workflow Execution (C10) and resolves the workflow-category one-atom open question (it is the second workflow atom). The descriptive entry below is retained as roadmap history.

What it is. A workflow primitive: a named entity moving through a defined, finite set of states via explicitly declared transitions. The atom does not know what the entity is — it knows the entity’s current state, the transitions that are valid from that state, and the history of how it got there. States and transitions are declared at instantiation; the atom enforces that only declared transitions are applied and that the full transition history is auditable. A Workflow instance has exactly one current state at all times; concurrent active states and fork-join constructs are composing concepts, not part of the atom.

Why it’s after Capacity Constraint. Approval Step (atom #4, grounded) opened the workflow/ category but left it a single-entry category. Workflow / State Machine is the general primitive that justifies the category: Approval Step is a specific kind of state machine (one designed for human approval decisions); Workflow / State Machine is the general case. The two atoms compose into Stateful Workflow Execution (C10), which produces multi-actor gated workflows with tamper-evident transition histories — a pattern that recurs in regulated manufacturing, financial operations, and HR processes. Once this atom lands, the workflow category stands on its own and the broader axial-split taxonomy question can be revisited with two workflow atoms as evidence.

Key invariants (anticipated). Only declared transitions are valid — an undeclared transition is rejected with invalid-transition. The current state is always exactly one of the declared states. The full transition history — prior state, target state, triggering action, timestamp, actor — is auditable and append-only. A state declared as terminal at instantiation is absorbing — no further transitions are accepted. Transition guards are declared at instantiation; the atom enforces that a guard must be satisfied before a transition fires, but does not evaluate the guard — that is the caller’s obligation.

Standards anchored. FDA 21 CFR Part 11 (electronic records in regulated workflows — each state transition is a regulated event); ISO 9001 §8.5.1 (production workflow controls); BPMN 2.0 (the canonical notation for stateful workflow — this atom is the primitive behind a BPMN state diagram); HL7 (Health Level Seven) FHIR (Fast Healthcare Interoperability Resources) Task resource (clinical workflow state machine — Task states map directly to this atom’s state machine).

Unlocks. Stateful Workflow Execution (C10). Resolves the workflow-category one-atom question (resolved 2026-06-04 — the category now stands on two grounded atoms).

10. Preference / Personalization

Category: messaging

Status: grounded on Final Critique 5 — 2026-05-29. Author-conducted foundation passes (Pass 1 GRID, Pass 2 EOS, Pass 3 Linus) and one refinement round; fresh-reader AI Phase 3 round (2026-05-25); first Opus Phase 4 gate (2026-05-25 — Final Critique 4) surfaced 3 foundational findings, all closed; the 2026-05-29 fresh-reader Phase 3 + Opus Happy Torvalds X2 rerun (Final Critique 5) returned zero foundational findings (17 refining, 1 rhetorical, all closed in-pattern) and grounds the atom. It lives at atoms/preference.md. The five anticipated invariants below are realized as ten hard invariants (record immutability, status monotonicity, at-most-one-currently-in-effect, supersession atomicity, channel-set membership at creation, value-preserving suspension, query determinism, no id reuse, store durability, configuration-record integrity) plus Temporal property 11 (timestamp ordering, best-effort under non-monotonic clocks).

What it is. A messaging primitive: a durable binding of a principal’s delivery preferences — channel priority, frequency limits, quiet hours, format preferences, per-topic opt-downs — that governs how a notification reaches a recipient, independently of whether they are subscribed (Subscription) or whether processing is legally permitted (Consent). The three atoms are distinct: Subscription governs which topics a principal follows; Consent governs whether the system may process or communicate with the principal at all; Preference governs the delivery envelope when Subscription and Consent have both permitted the notification. States: Active, Suspended (preferences retained but delivery suppressed for the principal), Deleted.

Why it’s last. Subscription, Notification, and Notification Fanout are all grounded; Consent is grounded. The next natural question in the messaging surface is: how does a subscriber control the shape of delivery? Preference / Personalization is the atom that answers it. It sits last in the planned sequence because the composing surface (Preference-Aware Notification Fanout, C11) is narrower than the other remaining atoms’, not because the atom is less important — it just unblocks one composition rather than several.

Key invariants (anticipated). A principal has at most one active Preference record — preferences are not additive; a new preference set replaces the prior one (with the prior set retained in history). Preference updates are not retroactive — a notification already queued before an update is delivered under the prior preferences; the update governs future deliveries only. A Suspended Preference record suppresses delivery without removing subscriptions — the subscriber retains their topic bindings while suppressing notifications. Preference / Personalization does not define what channels exist or what format options are valid — those are deployment-specific enumerations declared at instantiation.

Standards anchored. CAN-SPAM Act (opt-out and frequency controls for commercial email); TCPA (frequency and consent controls for SMS and phone marketing); GDPR Article 7(3) (preference changes must be as easy as the original grant — the Preference atom’s update action is the mechanism).

Unlocks. Preference-Aware Notification Fanout (C11).

11. Credential

Classification: stored flat as atoms/credential.md — no category folder. Its regulated and security classifications are overlays derived from its composers, not a folder it is filed under; this resolves the former provisional compliance/ placement and the question of a dedicated security/identity folder. See the usage-derived taxonomy.

Status: grounded 2026-05-19 (Final Critique 4); formal layer landed 2026-06-03 (credential.tla + buggy twins). Retained below as roadmap history.

What it is. An authentication primitive: a durable binding between a principal and a secret or token that the principal presents to prove they are who they claim to be. Credential models the registration of that binding, the verification of presented material against it, the rotation of the binding to a new secret while retiring the prior one, and the revocation of the binding entirely. Each credential record is tied to exactly one principal at registration and that binding is immutable; rotation produces a new credential record bound to the same principal, never a mutation of the prior one. The prior record transitions to the terminal state Rotated, preserving the full rotation history in the record store. Actions: register, verify, rotate, revoke.

Why it’s next. Credential retires the Authentication *(forthcoming)* debt in atoms/actor-identity.md — Actor Identity verifies who an actor is; Credential is the mechanism by which that verification is operationalized as a bound secret the actor can present. The two atoms are distinct: Actor Identity is a persistent identity record; Credential is the authentication surface the identity record can bind. Of the four new atoms, Credential and Session are the highest-leverage pair: Credential strictly blocks C13 (Login), which wires Credential verification to Session issuance. It additionally enriches C16 (External Onboarding), where a credential is registered at the moment an invited party’s identity is accepted.

Key invariants (anticipated). verify returns verified only for the principal bound at registration — sole-holder verification is absolute. Once a credential transitions to Revoked, no future verify call returns verified — revocation is absorbing. Rotation never mutates the prior credential record; it produces a new record and transitions the prior record to Rotated. State machine: Active → Rotated Revoked Expired (three terminal states). The full rotation and revocation history is auditable from the record store alone.

Standards anchored. NIST SP 800-63B (authenticator assurance levels — IAL/AAL tiers); OpenID Connect Core 1.0 (credential material exchange); RFC 7519 (JWT — credential token encoding); FIDO2/WebAuthn (phishing-resistant authenticator binding); PCI DSS (Payment Card Industry Data Security Standard) Requirement 8 (credential management controls); ISO/IEC 27001 §A.9.4 (system and application access controls). Explicitly not citing NIST 800-63A — identity proofing belongs upstream to Party Identity.

Unlocks. Strictly blocks C13 (Login — Credential + Session + Actor Identity). Additionally enriches C16 (External Onboarding — the credential registration step in the onboarding arc).

12. Session

Classification: stored flat as atoms/session.md — no category folder. Its regulated and security classifications are overlays derived from its composers, not a folder it is filed under; this resolves the former provisional compliance/ placement and the question of a dedicated security/identity folder. See the usage-derived taxonomy.

Status: grounded 2026-05-19 (Final Critique 4); formal-layer vote reconsidered to NO (formal-not-warranted; records-alone, interleaving lives in Session-Gated Authorization). Retained below as roadmap history.

What it is. A time-limited authenticated channel primitive: a record attesting that a given principal was authenticated at a specific moment and that the authentication remains valid until the session expires or is explicitly revoked. Session does not perform authentication — that is Credential’s surface. Session records the result of a successful authentication and makes it queryable by composing systems for the duration of its validity. Each session carries an expires_at timestamp set at issuance and never mutated; extension of a session produces a new session record, not a modification of the prior one. Actions: issue, validate, expire, revoke. State machine: Active → Expired Revoked (two terminal states).

Why it’s next. Session is the time-bounding surface that Credential verification produces: a successful verify produces a short-lived authenticated channel; that channel is a Session. Without Session, Credential verification has no durable expression that composing systems can query — Login (C13) needs both. Session additionally unblocks Session-Gated Authorization (C14), which gates every permission check on session validity before the permission check runs.

Key invariants (anticipated). A session is valid if and only if it has been issued, now < expires_at, and it has not been revoked — the validity bound is conjunctive. validate(token) returns valid | invalid(expired | revoked | not-known) — three first-class invalid outcomes, mirroring Actor Identity’s verify discipline, never collapsed to a single invalid. Revocation is absorbing: a revoked session cannot be re-validated. expires_at is set at issue time and never mutated; a session that needs a longer lifetime is re-issued, not extended in place.

Standards anchored. NIST SP 800-63B §7 (session management and reauthentication requirements); OWASP ASVS V3 (session management verification standard); RFC 6265 (HTTP state management — cookie-based session binding); SAML 2.0 §4.1.4 (session establishment and termination); RFC 6819 (OAuth 2.0 threat model, session-related threat mitigations); OIDC Session Management 1.0 (session lifecycle and logout across identity providers).

Unlocks. Strictly blocks C13 (Login — Credential + Session + Actor Identity) and C14 (Session-Gated Authorization — Session + Permissions).

13. Capability

Classification: stored flat as atoms/capability.md — no category folder. The object-capability literature anchors it as a security primitive; under the usage-derived taxonomy that shows up as a derived security overlay (alongside regulated), not a folder placement. This resolves the former provisional compliance/ placement. See the usage-derived taxonomy.

Status: grounded 2026-05-19 (Final Critique 4; Alloy model capability.als + buggy twin). Retained below as roadmap history.

What it is. A bearer-token authorization primitive: an unforgeable token that carries its own authorization to access a specific resource or perform a specific action. The defining property of a Capability is that possession of the token is sufficient authorization — the redeemer’s identity is intentionally irrelevant at redemption time. Capability generalizes single-use links (a password-reset link), multi-use API tokens (a service credential scoped to a single resource), and pre-authorized action tokens under one structural pattern. Each capability carries a remaining_redemptions counter set at allocation (default 1) and decremented monotonically on each redemption; a capability with remaining_redemptions = 0 is exhausted and terminal. Actions: allocate, redeem. State machine: Allocated → Redeemed Expired Revoked (three terminal states, with exhaustion via counter being the structural route to Redeemed).

Why it’s next. Capability is the library’s forcing function for making the OCAP-vs-Permissions distinction explicit. Permissions is identity-keyed: a permission check gates on who is asking. Capability is bearer-keyed: the token gates on what is being presented, with no identity check at redemption time. The two atoms compose into structurally distinct patterns with different audit signatures. Without a Capability atom, a composing system is forced to model bearer-token semantics inside Permissions or an ad-hoc construct, hiding the architectural distinction the library exists to make visible. Capability strictly blocks C15 (Capability-Backed Sharing), the library’s worked example of bearer-token semantics composing with regulated audit.

Key invariants (anticipated). Redemption requires only possession of the token — no identity check at redemption time; the redeemer’s identity is structurally irrelevant and intentionally so. The allocator’s identity is recorded at allocation time and attestable via Actor Identity, producing an asymmetric audit record: allocator is known, redeemer is not. remaining_redemptions is set at allocation and decremented monotonically; it never increases. Exhaustion (counter at 0), expiry, and revocation are three structurally distinct terminal modes and are never conflated in the record or in validation logic.

Standards anchored. Daniel Jackson, Software Abstractions — Capability [Resource] concept (the atom’s structural core); Mark Miller and the object-capability (OCAP) literature (bearer-key authorization semantics); Levy (1984), Capability-Based Computer Systems (canonical reference for bearer-token capability semantics); Birgisson et al. (2014), Macaroons (context-limited bearer credentials — a constrained Capability variant); RFC 6749 §1.4 (OAuth 2.0 access tokens — cited with explicit caveats about OAuth’s identity-bound conflations diverging from pure OCAP; this atom defines the pure OCAP surface, not the OAuth surface).

Unlocks. Strictly blocks C15 (Capability-Backed Sharing — Capability + Selective Disclosure + Audit Trail substrate). The atom’s primary value on EOS Pass 2 is forcing the OCAP-vs-Permissions distinction to be made explicit in the library.

14. Invitation

Classification: stored flat as atoms/invitation.md — no category folder. Its core responsibility is onboarding an external entity into a system identity context; under the usage-derived taxonomy that is captured by its derived security and regulated overlays rather than a dedicated identity folder. This resolves the former provisional compliance/ placement. See the usage-derived taxonomy.

Status: grounded 2026-05-19 (Final Critique 4); formal layer landed 2026-06-03 (invitation.tla + buggy twin). Retained below as roadmap history.

What it is. A lifecycle primitive for inviting an external entity to join a context: a durable record of the invitation event itself, from the moment the invitation is issued through its resolution — accepted, declined, expired, or revoked before resolution. The defining property of Invitation is that the invitee’s identity may not be known or validatable at initiation time; the moment of acceptance is when an identity is bound. Actions: initiate, accept, decline, revoke, expire. State machine: Pending → Accepted Declined Expired Revoked (four terminal states). accept carries an accepting_identity_ref argument — the identity is bound at the moment of acceptance and is immutable thereafter.

Why it’s next. Invitation is the library’s mechanism for onboarding an unknown external entity into a system identity context. Party Identity (atom #6, grounded) models a persistent verifiable identity; Invitation is the gate through which an external party first enters the identity surface. Without Invitation, the library has no structured account of how an external party comes to exist in the system at all — C16 (External Onboarding) cannot be specified without it. Invitation also completes the Capability-vs-Invitation design question (see Open taxonomy question): both atoms use bearer-token transport; the distinction is that Invitation carries Declined as a first-class semantic outcome (a human decision, not a system event) and binds an identity at resolution — two properties Capability does not have.

Key invariants (anticipated). Exactly one transition out of Pending — once an invitation has been accepted, declined, expired, or revoked, any subsequent action attempt returns already-resolved(state). The invitee_ref at initiation may not resolve to a known system identity; it is not validated at initiate time and is not required to match the accepting_identity_ref at accept time — opaque invitee at initiation is structurally intentional. The identity bound at acceptance (accepting_identity_ref) is immutable once set; it cannot be rebound or updated after the accept transition.

Standards anchored. GDPR Article 32 (security of processing — invitation tokens are credentials in transit and must be treated accordingly); HIPAA §164.312 (access control requirements — invitation-based provisioning is a covered access-granting mechanism); SCIM 2.0 (System for Cross-domain Identity Management — invitation-style user provisioning is adjacent to SCIM’s POST /Users with an invite flow). Standards anchoring is lighter for Invitation than for Credential, Session, or Capability; the atom earns its keep on EOS Pass 2 conceptual independence rather than regulatory depth.

Unlocks. Strictly blocks C16 (External Onboarding — Invitation + Party Identity + Credential + Audit Trail substrate).

Grounded atoms — short status (formerly atoms #1–#6, #8)

The seven atoms below were on the planned sequence and have shipped. Detailed authoring notes are in the atom files themselves; the entries below are retained as roadmap-history.

Legal Hold — grounded on Final Critique 4 — 2026-05-20. Compliance primitive; actor-issued hold preventing record purge regardless of retention eligibility. Unblocked C1 (Defensible Retention, now grounded) and C7 (DSAR).
Consent — grounded on Final Critique 4 — 2026-05-20. Compliance primitive; data subject’s agreement to a specified processing purpose with grant/revoke/expire lifecycle. Unblocked C2 (Consent & Preference Management), C7 (DSAR), C8 (KYC).
Soft Delete — grounded on Final Critique 4 — 2026-05-20. Resource-lifecycle primitive; recoverable deletion with explicit purge. Unblocked C3 (Forensic Recovery).
Approval Step — grounded on Final Critique 4 — 2026-05-20. Workflow primitive; single approval gate with Pending/Approved/Rejected/Withdrawn lifecycle. Unblocked C4 (Multi-Party Approval, now grounded). First entry in workflow.
Selective Disclosure — grounded on Final Critique 4 — 2026-05-20. Compliance primitive; durable record of what subset of a record was disclosed, to whom, when, and under what authority. Unblocked C6 (Immutable Transaction Ledger) and C7 (DSAR).
Party Identity — grounded on Final Critique 4 — 2026-05-20. Compliance primitive; persistent verifiable identity record for an external party with Unverified/Verified/Suspended/Closed lifecycle. Unblocked C8 (KYC / Customer Onboarding). Survived foundation round plus Opus Phase 4 clearance gate; six clearance-gate findings closed in-pattern.
Capacity Constraint Enforcement — grounded on Final Critique 5 — 2026-05-20. Resource-lifecycle primitive; named, bounded pool of a finite resource with arithmetic enforcing total allocated never exceeds declared capacity under four named host obligations. Unblocked C9 (Reservation Lifecycle). Foundation round plus two Phase 4 Opus clearance-gate rounds (round 1: 11 foundational findings closed; round 2: 3 foundational + 5 refining + 1 rhetorical closed). First atom grounded under the 92%-good threshold codified in this revision of pressure-testing.md.

Compositions — current state

Compositions are sequenced by readiness. All eighteen original C-numbered compositions are grounded (C1–C18), joined by Saga (C19) — the first grounded composition from the dream-compositions pipeline beyond that backlog — for nineteen C-numbered grounded compositions (and twenty-five grounded compositions in all, counting the six that predate C-numbering); C15 (Capability-Backed Sharing) grounded 2026-06-10 on Final Critique 4 — the 23rd grounded composition — Capability + Selective Disclosure + Audit Trail (substrate), reconciling bearer-token sharing with regulated disclosure audit through the audit-subject asymmetry (allocator named and attested; redeemer structurally unnamed, by construction on Capability Invariants 3/5) and the disclosure-accountability binding bijection, on clearance of the Phase 4 Opus Happy-Torvalds-X2 fresh-reader gate (foundational findings at zero, four refining/rhetorical folded, TLA+ binding-bijection model + non-atomic buggy twin re-verified, capability provenance and every constituent invariant count re-derived head-on against the constituent specs); C17 (Authenticated Actor) grounded 2026-06-10 on Final Critique 4 — the 21st grounded composition — Credential + Actor Identity, the revocation-cascade-as-forward-closure emergent guarantee, on clearance of the Phase 4 Opus Happy-Torvalds-X2 fresh-reader gate (foundational findings at zero, five refining folded, TLA+ revocation-cascade model + TOCTOU buggy twin re-verified, cascade gate confirmed housed at the composition layer); C18 (Actor Suspension) grounded 2026-06-10 on Final Critique 4 — the 22nd grounded composition — Actor Identity + Permissions + Session + Audit Trail (substrate) + optional Credential, the outbound multi-surface atomic de-authorization counterpart to Login, on clearance of the Phase 4 Opus Happy-Torvalds-X2 fresh-reader gate (foundational findings at zero, five refining folded, TLA+ atomic-cascade model + non-atomic buggy twin re-verified, capability provenance re-derived head-on so the Active/Suspended lifecycle is confirmed composition-introduced rather than mis-attributed to Actor Identity); C7 (Data Subject Rights Fulfillment) grounded 2026-06-09 on Final Critique 5 — the 20th grounded composition — on clearance of the Phase 4 Opus Happy-Torvalds-X2 gate (foundational findings at zero, six refining/rhetorical folded, formal model + twins re-verified); C11 (Preference-Aware Notification Fanout) grounded 2026-06-12 on Final Critique 9 — the 24th grounded composition, closing the C-numbered backlog at eighteen of eighteen (see §C11 grounded below); none is blocked on a remaining atom. C6 (Immutable Transaction Ledger with Selective Disclosure) grounded 2026-06-08 — Audit Trail (substrate) + Selective Disclosure, the first composition to compose the Selective Disclosure atom; ships a TLA+ disclosure-accountability binding-bijection model + buggy twin. C2 (Consent & Preference Management) and C9 (Reservation Lifecycle) grounded 2026-06-04 — C2 wires Consent + Permissions + Audit Trail (substrate) for the consent-gates-processing gate plus the revocation-propagation binding bijection; C9 wires Capacity Constraint + Provisional Commitment + Duplicate Prevention + Event Log + Actor Identity for the allocation-coherence guarantee (the pool-arithmetic superset of Idempotent Reservation). Both ship TLA+ models + buggy twins verified in tools/harness/. C3 (Forensic Recovery), C10 (Stateful Workflow Execution), and C12 (Chain of Custody) all grounded 2026-06-04 — C10 immediately after its spine atom Workflow / State Machine, C12 immediately after its core atom Provenance, C3 as an easy template-driven Soft Delete + Audit Trail substrate composition. C11 became unblocked when Preference / Personalization grounded on 2026-05-29. Provenance also enriches three other compositions (C6, C7, C8) as an optional composing atom for chain-of-custody guarantees — those compositions remain unblocked without it, but gain emergent invariants when composed with it once it lands.

Grounded

The nineteen C-numbered grounded compositions are catalogued below (C1–C18, plus Saga as C19). (Six further grounded compositions predate the C-numbering — Attributed Permissions Admin, Audit Trail, Idempotent Reservation, Privileged Access Provisioning, Shared Todo, Undo History — bringing the grounded total to twenty-five; see the summary list under Current state above.) Each has its full spec, Lineage notes, and — where the formal-layer vote was YES — a verified model + buggy twin in its own file.

C1. Defensible Retention — grounded on Final Critique 4 — 2026-05-20. Legal Hold + Retention Window + Audit Trail (substrate). Hold-blocks-purge gate; lawful destruction provable from records alone. Anchors SOX §802, HIPAA §164.530(j), SEC Rule 17a-4, GDPR Article 17, FRCP Rule 37(e).
C2. Consent & Preference Management — grounded on Final Critique 4 — 2026-06-04. Consent + Permissions + Audit Trail (substrate). processing_permitted gate + revocation-propagation binding bijection. TLA+ model + buggy twin. Anchors GDPR Articles 6–7, 7(3), CCPA/CPRA, HIPAA §164.508.
C3. Forensic Recovery — grounded on Final Critique 4 — 2026-06-11 (English 2026-06-04; coverage GAP MC-C3-1 closed 2026-06-11 — model covers both Invariant 4 arms). Soft Delete + Audit Trail (substrate). Every delete/restore/purge attributed, tamper-evident, recover_history-recoverable; no purge without an audit record. TLA+ binding-bijection model + buggy twin. Anchors GDPR Article 17, HIPAA §164.312(b), FRCP Rule 37(e), SOX §802.
C4. Multi-Party Approval — grounded on Final Critique 4 — 2026-05-20. Approval Step + Permissions + Assignment + Audit Trail (substrate). N approval steps under a quorum rule; first composition to compose another composition. Anchors SOX §404, FDA 21 CFR Part 11, ICH E6 GCP, ISO 9001 §8.5.1.
C5. Notification Fanout — grounded on Final Critique 4 — 2026-05-20. Subscription + Notification. First composition to produce a variable number of effects from a single trigger. Completes the messaging atom pair.
C6. Immutable Transaction Ledger — grounded on Final Critique 6 — 2026-06-10. Audit Trail (substrate) + Selective Disclosure. Disclosure-accountability binding bijection + verifiable partial disclosure; first to compose Selective Disclosure. TLA+ model + buggy twin. Anchors SEC Rule 17a-4, HIPAA §164.528, 21 CFR Part 11, GDPR Article 15.
C7. Data Subject Rights Fulfillment — grounded on Final Critique 5 — 2026-06-09. Selective Disclosure + Defensible Retention (C1, substrate) + Consent (read-only oracle). Per-record disposition with no-silent-omission + request⇔fulfillment binding bijection; erasure wraps C1’s purge gate. First composition authored under the capability-provenance rule. TLA+ binding + coverage model + two buggy twins. Anchors GDPR Articles 15–17, CCPA/CPRA, HIPAA §164.524 / §164.526 / §164.528.
C8. KYC / Customer Onboarding — grounded on Final Critique 4 — 2026-06-03. Party Identity + Retention Window + Audit Trail (substrate). Verification-gates-activity via the composition’s own case index; adverse-trigger monitoring + post-closure retention floor. Anchors FATF Recommendations 10–12, BSA/AML 31 CFR §1020.220, FinCEN 31 CFR §1010.230, EU AMLD5, GDPR Article 6(1)(c).
C9. Reservation Lifecycle — grounded on Final Critique 5 — 2026-06-18. Capacity Constraint + Provisional Commitment + Duplicate Prevention + Event Log + Actor Identity. Allocation coherence (no oversell, leak, or double-release); the pool-arithmetic superset of Idempotent Reservation. TLA+ allocation-coherence model + buggy twin. Anchors ISO 9001 §8.5, PCI DSS Req. 10, IATA Resolution 830a.
C10. Stateful Workflow Execution — grounded on Final Critique 4 — 2026-06-04. Workflow / State Machine + Approval Step + Permissions + Assignment + Audit Trail (substrate). Approval-gated transitions — guard evaluation re-converges; first to compose Workflow / State Machine. TLA+ model + buggy twin. Anchors SOX §404, FDA 21 CFR Part 11, ISO 9001 §8.5.1, BPMN 2.0.
C12. Chain of Custody — grounded on Final Critique 4 — 2026-06-11 (English 2026-06-04; coverage GAP MC-C12-1 closed 2026-06-11 — model covers both Invariant 4 arms). Provenance + Audit Trail (substrate). Records-alone custody proof (verify_custody); pharma ≡ legal-evidence chain of custody in one composition; first to compose Provenance. TLA+ binding-bijection model + buggy twin. Anchors FDA 21 CFR Part 211, DEA 21 CFR Part 1304, FRE 901(b)(9), ISO 17025.
C13. Login — grounded on Final Critique 5 — 2026-05-23. Credential + Session + Audit Trail. Verify→issue wiring; the cascade — revoking a Credential invalidates every Session derived from it. Anchors NIST SP 800-63B, OIDC Core 1.0, SAML 2.0.
C14. Session-Gated Authorization — grounded on Final Critique 6 — 2026-05-23. Session + Permissions. Every permission query gated on session validity; principal binding — the queried principal is always the session-extracted one. Anchors NIST SP 800-53 AC-3 + AC-12, OWASP ASVS V3.3, PCI DSS Req. 7 + 8.
C15. Capability-Backed Sharing — grounded on Final Critique 4 — 2026-06-10. Capability + Selective Disclosure + Audit Trail (substrate). Audit-subject asymmetry (the allocator is named and attested; the redeemer is structurally unnamed, by construction on Capability Invariants 3/5) + disclosure-accountability binding bijection (the Selective Disclosure record, the sealed sharing.disclosed event, and the redemption-decrement commit together or not at all — closer to C6 than C7). The library’s worked example of the object-capability model composed with regulated audit; first to compose Capability with Selective Disclosure. TLA+ binding-bijection model + non-atomic buggy twin. Anchors GDPR Article 32, HIPAA §164.514(d), OCAP.
C16. External Onboarding — grounded on Final Critique 5 — 2026-05-23. Invitation + Credential + Party Identity + Audit Trail. Invitation-gates-enrollment — no Party Identity without a preceding accepted Invitation in the same call. Anchors GDPR Articles 6–7, SOC 2 CC6.2, NIST SP 800-63A, SCIM 2.0.
C17. Authenticated Actor — grounded on Final Critique 4 — 2026-06-10. Credential + Actor Identity. Revocation cascade as forward closure — attest_as_actor gated on the bound credential’s live Active status, read atomically with the attestation write, so a revoked login produces no new attestations while prior ones stay valid; plus secret-surface separation and the principal_ref ⇔ actor_ref namespace bijection. Login’s outbound-attestation counterpart; first to pair Credential with Actor Identity. TLA+ revocation-cascade model + TOCTOU buggy twin. Anchors NIST SP 800-63B §5.2, NIST SP 800-57, PCI DSS Req. 8.6, FIPS 140-3.
C18. Actor Suspension — grounded on Final Critique 4 — 2026-06-10. Actor Identity + Permissions + Session + Audit Trail (substrate) + optional Credential. Atomic multi-surface revocation (after suspend_actor, zero active grants + zero active sessions in one all-or-nothing transaction — a half-suspended actor is worse than a clean failure, inverting Login’s best-effort posture) + audit completeness (the sealed actor.suspended event enumerates every revoked grant_id/session_token) + suspension cascade ordering (Active→Suspended gate fires once; second suspend a no-op; benign already-terminal counted). Login’s outbound-side counterpart. TLA+ atomic-cascade model + non-atomic buggy twin. Anchors NIST SP 800-53 AC-2(3) + AC-6(5), SOX §404, HIPAA §164.308(a)(3)(ii)(C), PCI DSS Req. 8.1.3, ISO/IEC 27001 §A.9.2.6.
C19. Saga / Compensable Workflow — grounded on Final Critique 4 — 2026-06-16. Workflow / State Machine + Event Log (compensating action sub-atomic). The external-side-effect complement of Undo History — completed steps reversed by a recorded compensating action, not replay-skip; durable-execution engine + orchestration-vs-choreography below the contract. TLA+ all-or-compensated + idempotency-under-retry model + two buggy twins (skip-comp → Inv 4, double-apply → Inv 7). First grounded from the dream-compositions pipeline; sibling of C10 over the Workflow / State Machine spine.

Status cells in this document mirror each pattern file’s own Status line — the pattern file is the source of truth and carries the marker of its latest complete round. A mismatch between a row here and the pattern’s Status line is a finding (the status-mirror check; see open-questions.md §Status-line grammar). Rows corrected against the pattern files 2026-06-11; rows not individually verified that day retain their original grounding dates pending the mechanical check.

C11 grounded — the C-numbered backlog closes

C11. Preference-Aware Notification Fanout — `grounded on Final Critique 12 — 2026-06-12`

Constituents (corrected at landing): Subscription + Notification + Preference + Event Log, composed directly — Notification Fanout is the unshaped sibling and structural template, not a constituent (the C9 superset precedent: re-wire the atoms plus more rather than wrap a grounded composition whose action surface exposes no insertion point for the shaping gate). The earlier sketch on this row listed Notification Fanout as a constituent; the spec’s Composes section is the source of truth. Audit Trail and Consent are named peers. Unblocked 2026-05-29 when Preference grounded; the final unstarted C-numbered row, now authored.

What it adds. The fanout loop with a shaping gate between the subscriber query and each create: every queried subscriber receives exactly one journaled disposition — created (shaped to channel and format), failed-with-cause, or suppressed-with-reason (suspended, no-record, quiet-window, frequency-cap, channel-opt-out). The TCPA quiet-window angle is first-class: a stored-preference arm plus a statutory-window arm, both stated as conditional invariants with declared antecedents. Frequency-cap safety is per-commit, conditional on the declared serialization capability, with the cap TOCTOU race as the formal model’s subject — TLA+ model + overshoot buggy twin verified in tools/harness/ 2026-06-12, mirroring capacity-constraint-enforcement’s twin. redispose is the journaled, gate-re-evaluated retry surface that re-verifies the audience and the shape across its unbounded horizon. Authored through Round 1 plus nine fresh-reader Final Critique rounds — FC4–FC8 closed 16 foundational; FC9 returned zero foundational (the first grounding gate, Pass 2 clean from FC8 on). A post-grounding fresh-reader rescan then reopened the gate — FC10 surfaced a gate fail-closed/precedence ordering defect, and FC11 a reconciliation-surface provenance cluster (resolved by adding the composition-introduced reconcile_gaps / reconcile_overshoots surface, taking the action surface to three) — and the pattern re-grounded on Final Critique 12 (zero foundational), all findings closed in-pattern every round. This brings the library to 51 grounded patterns (24 grounded compositions), closes the original C-numbered composition backlog at eighteen of eighteen, and retires the C11 forthcoming-links in Preference and C2.

Standards anchored. TCPA (47 U.S.C. §227; 47 CFR §64.1200(c)(1)), CAN-SPAM §7704, GDPR Articles 7(3) and 21(2), CASL, ePrivacy.

Saga (C19) grounded — first of the dream-compositions pipeline

Saga / Compensable Workflow grounded — 2026-06-16 (Final Critique 1). The external-side-effect complement of Undo History: a forward sequence of local steps each paired with a recorded compensating action, made eventually all-or-nothing across failure without a distributed transaction. Composes Workflow / State Machine + Event Log (the compensating action is a sub-atomic recorded closure, not an atom); the durable-execution engine and orchestration-vs-choreography stay below the contract. Decomposition source-grounded against the Temporal server + Java/TS SDKs (dream-compositions §7). Formal-layer vote YES, discharged: saga.tla machine-checks all-or-compensated (Inv 4) and idempotency-under-retry (Inv 7) on the WASM tla-checker, green at N=2 (22 states), monotone-growth saturation N=2..6; two buggy twins rejected with per-invariant teeth (saga-skip-comp-buggy → Inv 4, saga-double-apply-buggy → Inv 7). Ground by a fresh-reader Opus Happy-Torvalds-X2 clearance gate (Phase 3 + Phase 4 merged) with zero foundational findings (four refining/rhetorical folded in-pattern). The first composition grounded from the dream-compositions pipeline beyond the original C-numbered backlog; sibling of C10 over the Workflow / State Machine spine. This brings the library to 52 grounded patterns (25 grounded compositions).

Summary table

#	Pattern	Type	Status	Unblocks / Notes
—	Personal Todo, Assignment	Atoms	Personal Todo: `grounded` 2026-05-13; Assignment: `grounded` 2026-05-13	`productivity`
—	Duplicate Prevention, Event Log	Atoms	`grounded` 2026-05-13	`temporal`
—	Provisional Commitment	Atom	`grounded` 2026-05-13	`resource-lifecycle`
—	Actor Identity, Retention Window, Tamper Evidence, Permissions	Atoms	Actor Identity, Tamper Evidence: `grounded` 2026-05-13; Retention Window, Permissions: `grounded` 2026-05-13	`compliance`
—	Subscription, Notification	Atoms	`grounded` 2026-05-13	`messaging`
—	Clinical Observation, Medication Order	Atoms	`grounded` 2026-05-13	`healthcare` (outside core sequence)
1	Legal Hold	Atom	`grounded — 2026-05-20`	C1, C7
2	Consent	Atom	`grounded — 2026-05-20`	C2, C7, C8
3	Soft Delete	Atom	`grounded — 2026-05-20`	C3
4	Approval Step	Atom	`grounded — 2026-05-20`	C4
5	Selective Disclosure	Atom	`grounded — 2026-05-20`	C6, C7
6	Party Identity	Atom	`grounded — 2026-05-20`	C8
7	Provenance	Atom	`grounded` 2026-06-04	Unblocks C12 (Chain of Custody); enriches C6, C7, C8; Alloy model + buggy twin
8	Capacity Constraint Enforcement	Atom	`grounded — 2026-05-20`	C9
9	Workflow / State Machine	Atom	`grounded` 2026-06-04	Unblocks C10; resolves workflow-category one-atom question; Alloy model + buggy twin
10	Preference / Personalization	Atom	`grounded` 2026-05-29	C11; grounded on Final Critique 5; ten hard invariants + Temporal property 11
11	Credential	Atom	`grounded` 2026-05-19	C13 (Login); enriches C16; retires Authentication forthcoming-link in actor-identity.md
12	Session	Atom	`grounded` 2026-05-19	C13 (Login), C14 (Session-Gated Authorization)
13	Capability	Atom	`grounded` 2026-05-19	C15 (Capability-Backed Sharing)
14	Invitation	Atom	`grounded` 2026-05-19	C16 (External Onboarding)
—	Undo History	Composition	`grounded` 2026-05-13	Personal Todo + Event Log
—	Idempotent Reservation	Composition	`grounded` 2026-05-13	Provisional Commitment + Duplicate Prevention
—	Audit Trail	Composition	`grounded` 2026-05-13	Event Log + Actor Identity + Retention Window + Tamper Evidence
—	Shared Todo	Composition	`grounded` 2026-05-13	Personal Todo + Permissions + Assignment
C5	Notification Fanout	Composition	`grounded — 2026-05-20`	Subscription + Notification
—	Attributed Permissions Admin	Composition	`grounded on Final Critique 6` — 2026-05-23	Permissions + Actor Identity; first two-compliance-atom composition; ships with dynamic Alloy trace model
—	Privileged Access Provisioning	Composition	`grounded on Final Critique 4`; Round 5 re-pass clean 2026-06-03	Multi-Party Approval + Credential + Session + Capability + Audit Trail; approval-gates-provisioning invariant; session-gated exercise; TLA+ behavioral model ships alongside
C1	Defensible Retention	Composition	`grounded on Final Critique 4 — 2026-05-20`	Legal Hold + Audit Trail + Retention Window
C2	Consent & Preference Management	Composition	`grounded on Final Critique 4 — 2026-06-04`	Consent + Permissions + Audit Trail (substrate); consent-gates-processing + revocation-propagation binding bijection; TLA+ model
C3	Forensic Recovery	Composition	`grounded on Final Critique 4 — 2026-06-11` (English 2026-06-04; GAP MC-C3-1 closed 2026-06-11)	Soft Delete + Audit Trail (substrate); attributed + tamper-evident + full-history-recoverable destruction lifecycle; purge-eligibility gate delegated to C1; TLA+ binding-bijection model
C4	Multi-Party Approval	Composition	`grounded on Final Critique 4 — 2026-05-20`	Approval Step + Permissions + Assignment + Audit Trail
C6	Immutable Transaction Ledger	Composition	`grounded on Final Critique 6 — 2026-06-10`	Selective Disclosure + Audit Trail (substrate, → Event Log + Actor Identity + Tamper Evidence + Retention Window); disclosure-accountability binding bijection + verifiable partial disclosure; TLA+ binding-bijection model; first composition to compose Selective Disclosure
C7	Data Subject Rights Fulfillment	Composition	`grounded on Final Critique 5 — 2026-06-09`	Selective Disclosure + Defensible Retention (C1, substrate) + Consent (read-only oracle); no-silent-omission + binding-bijection; TLA+ binding + coverage model with two buggy twins; first composition authored under the capability-provenance rule
C8	KYC / Customer Onboarding	Composition	`grounded on Final Critique 4 — 2026-06-03`	Party Identity + Retention Window + Audit Trail (substrate); verification-gates-activity via the composition’s own case index
C9	Reservation Lifecycle	Composition	`grounded on Final Critique 4 — 2026-06-04`	Capacity Constraint + Provisional Commitment + Duplicate Prevention + Event Log + Actor Identity; allocation-coherence binding; TLA+ model
C10	Stateful Workflow Execution	Composition	`grounded on Final Critique 4 — 2026-06-04`	Workflow / State Machine + Approval Step + Permissions + Assignment + Audit Trail (substrate); approval-gated transitions (guard evaluation re-converges); TLA+ model; first composition to compose Workflow / State Machine
C12	Chain of Custody	Composition	`grounded on Final Critique 4 — 2026-06-11` (English 2026-06-04; GAP MC-C12-1 closed 2026-06-11)	Provenance + Audit Trail (substrate, → Actor Identity + Tamper Evidence + Retention Window); records-alone custody proof; TLA+ binding-bijection model; cross-domain pharma≡legal-evidence flagship; first composition to compose Provenance
C11	Preference-Aware Notification Fanout	Composition	`grounded on Final Critique 12 — 2026-06-12`	Subscription + Notification + Preference + Event Log, composed directly (Notification Fanout is the unshaped sibling, not a constituent — row corrected at landing); disposition trichotomy + quiet-window (stored + statutory) + per-commit cap safety + composition-introduced reconciliation surface; TLA+ cap-TOCTOU model + buggy twin verified; the 24th grounded composition — C-numbered backlog complete
C13	Login	Composition	`grounded on Final Critique 5 — 2026-05-23`	Credential + Session + Audit Trail; cascade invariant: Credential revocation invalidates all derived Sessions via `credential_to_sessions` map
C14	Session-Gated Authorization	Composition	`grounded on Final Critique 6 — 2026-05-23`	Session + Permissions; principal binding as emergent invariant — session-extracted principal gates every permission query
C15	Capability-Backed Sharing	Composition	`grounded on Final Critique 4` 2026-06-10	Capability + Selective Disclosure + Audit Trail (substrate); audit-subject asymmetry (allocator named and attested, redeemer structurally unnamed by construction on Capability Invariants 3/5) + disclosure-accountability binding bijection; first to compose Capability with Selective Disclosure. TLA+ binding-bijection model + non-atomic buggy twin.
C16	External Onboarding	Composition	`grounded on Final Critique 5 — 2026-05-23`	Invitation + Credential + Party Identity + Audit Trail; invitation-gates-enrollment as load-bearing invariant; actor credential pre-check before Invitation.accept
C17	Authenticated Actor	Composition	`grounded on Final Critique 4` 2026-06-10	Credential + Actor Identity; owns revocation cascade (forward closure), secret surface separation, and principal_ref / actor_ref namespace binding. TLA+ revocation-cascade model + TOCTOU buggy twin. Implementation-discovered gap via APA demo.
C18	Actor Suspension	Composition	`grounded on Final Critique 4` 2026-06-10	Actor Identity + Permissions + Session + Audit Trail (substrate) + optional Credential; emergent invariants: atomicity of multi-surface revocation under one all-or-nothing transaction, audit completeness over revocation scope, and suspension cascade ordering. Outbound-side counterpart to C13 Login’s inbound credential cascade. TLA+ atomic-cascade model + non-atomic buggy twin.
C19	Saga / Compensable Workflow	Composition	`grounded on Final Critique 1 — 2026-06-16`	Workflow / State Machine + Event Log (compensating action sub-atomic); external-side-effect complement of Undo History (reverses by compensating action, not replay-skip); all-or-compensated + idempotency-under-retry; TLA+ model + two buggy twins (skip-comp → Inv 4, double-apply → Inv 7); durable-execution engine below the contract; the 25th grounded composition, first of the dream-compositions pipeline

Formal model coverage

Per pressure-testing.md §Formal models, whether a formal model is a prerequisite for grounded is decided per pattern by the formal-layer vote: a vote-yes pattern (one carrying load-bearing temporal, ordering, concurrency, or safety claims) requires a verifying model before unqualified grounded; a vote-no pattern grounds English-only under the minimum-formalism principle. The inventory below records which grounded patterns currently ship formal-model siblings, and which have explicit deferred-formal-models entries in their Lineage notes.

Shipped

Pattern	Type	Alloy	TLA+	Files
Capability	Atom	✓	—	`atoms/capability.als` + `capability_check.py`
Attributed Permissions Admin	Composition	✓	✓	`compositions/attributed-permissions-admin.als`, `attributed-permissions-admin.tla` + `.cfg`
Privileged Access Provisioning	Composition	—	✓	`compositions/privileged-access-provisioning.tla` + `.cfg` + `privileged_access_provisioning_check.py`
Login	Composition	—	✓	`compositions/login.tla` + `.cfg`
External Onboarding	Composition	—	✓	`compositions/external-onboarding.tla` + `.cfg`
Session-Gated Authorization	Composition	✓	—	`compositions/session-gated-authorization.als`

Deferred — recorded in Lineage notes

Pattern	Type	Candidate artifacts	Recorded
Preference / Personalization	Atom	TLA+ on supersession atomicity (Invariant 4) + linearizable-per-`principal_ref` requirement + check-4 indistinguishability; Alloy on the records relation (preference + configuration records, Invariants 5 and 10, bootstrap-ordering)	`atoms/preference.md` Lineage notes, Phase 4 round, Deferred work — formal models item

All other grounded patterns

No formal-model siblings shipped and no deferred-formal-models Lineage entry. Per the methodology this is a respectable state — grounded is the bar, formal models are the complement. New deferred candidates should land as a Deferred work — formal models item in the relevant pattern’s Lineage notes (mirroring the Preference pattern), and graduate to this table’s Shipped section when the artifact lands.

Convention

A pattern moves from Deferred to Shipped when (a) the artifact exists at the path named here, (b) a Formal model entry is recorded in the pattern’s Lineage notes per pressure-testing.md (what the artifact is, what it checks, bounds/scope, deliberate exclusions, result), and (c) the row in this table is updated. Findings from formal-model runs route through the standard review channel — a contradiction inside the spec becomes a Pass-3-shaped finding in Lineage notes, not an in-flight spec rewrite.

Methodology debts — open

These are methodology-level items the library has accumulated and not yet resolved. They are recorded here so a future session picks them up rather than re-deriving them.

1. Propagation pass for the 92%-good threshold and three-class finding taxonomy. pressure-testing.md §”What grounded means” was extended on 2026-05-15 with the 92%-good grounding threshold (a pattern grounds when the Phase 4 clearance gate’s foundational findings reach zero, even if refining and rhetorical findings remain) and the foundational / refining / rhetorical three-class finding taxonomy. Capacity Constraint Enforcement is the first atom whose Lineage notes were authored under the new taxonomy and the new compact finding-→-fix line format (F-id — short name — class → fix in one or two sentences). All other grounded patterns retain Lineage notes in the prior narrative-paragraph form and Status lines that reference the prior unbounded “gate runs again until clean” rule rather than the threshold. A propagation pass should: (a) update each grounded pattern’s Status line to reference the threshold and the foundational-density-at-grounding count, (b) refactor each pattern’s Lineage notes to the compact format with explicit class labels per finding, (c) process in dependency order (atoms before compositions that name them) so cross-references stay stable. Priority order for the pass: Party Identity (most recent prior gate-clearing atom; the format is most directly comparable), then the canonical regulated-audit stack (Event Log, Actor Identity, Retention Window, Tamper Evidence, Audit Trail), then the remaining atoms and compositions in their grounded-date order.

Progress 2026-06-16: new patterns are now authored directly under the threshold and the compact F-id — short name — class → fix format (Saga is the latest); the corpus-wide retrofit has not run — ~14 of 52 patterns reference the threshold and ~9 carry the compact format — so this stays open as a batched sweep, best ridden on the scheduled-rescan automation (and naturally paired with item 9’s fold). Item 2 rides the same pass.

2. Methodology cross-reference from existing pattern Lineage notes to the threshold. Patterns whose Lineage notes refer to “the gate runs again until clean” or similar pre-threshold phrasing should be updated to point at pressure-testing.md §”The 92%-good grounding threshold” once the propagation pass runs. This is a substring-search-and-replace rather than a content rewrite; the existing findings and fixes stay, only the methodology rationale anchors update.

3. Decide whether the threshold counts toward grandfathering — RESOLVED 2026-06-18. The grandfathered cohort was brought to standard in a dedicated sweep: every pattern that predated the AI adversarial round received its first real fresh-reader Final Critique under the 92%-good threshold and now carries the canonical grounded on Final Critique 4 (capacity-constraint at 5). The pragmatic read held — a threshold-clean Phase 4 is bringing a pattern to standard. Grandfathering and the legacy grounded — date form are retired (pressure-testing.md §Status line format; changelog Removed).

4. Author-fatigue / round-count signal. Capacity Constraint Enforcement required two Phase 4 rounds (11 + 9 findings closed across both) before clearing under the new threshold. The library’s prior gate-clearing pattern (Party Identity) cleared in one round (6 findings). The two-round count for CCE is correlated with the atom’s surface area — 14 invariants, four host obligations, two state machines, regulated overlay, eight composing patterns. The empirical pattern: more surface = more rounds, with diminishing structural-finding density per round. The threshold is what makes the loop terminate cleanly. No action required, but a useful data point for future rich-surface atoms (Workflow / State Machine and Provenance are likely candidates).

6. Formal verification pass — Alloy for snapshots, TLA+ for traces. The library has no codified formal verification step. The three-pass methodology (GRID / EOS / Linus) plus Final Critique does the intellectual work that formal verification depends on — defining system state, naming actions, stating invariants, eliminating ambiguity — but stops short of machine-checked verification. The discovery (captured in discoveries.md, 2026-05-19): once a Grace Commons spec is grounded, generating Alloy or TLA+ models from it is largely mechanical, because the spec already contains the named actions, preconditions, postconditions, and numbered invariants the model requires. The feedback loop is: English specification → formal model → counterexamples → refined specification. The formal pass is not a separate discipline; it is a mechanical extension of the same thinking.

The tool split, by question type rather than by artifact type: Alloy handles snapshot questions — “is there any configuration of state where this invariant is violated?” (structural soundness, impossible constraints, reference validity, audit chain completeness). TLA+ handles trace questions — “is there any sequence of steps where this property breaks?” (concurrent action invariant violations, atomicity of operations, failures leaving state unchanged, temporal always/eventually properties, interleaving possibilities). In practice, atoms tend to generate structural questions (Alloy) and compositions tend to generate temporal and concurrency questions (TLA+), but the mapping is by question type, not artifact type — Invitation’s concurrent-accept is TLA+ territory even though it is an atom; a simple two-atom structural composition may be fully checkable in Alloy.

The ordering is fixed by the discovery: prose first, formal second. The English spec is canonical; the formal model translates from it, not the other way around. A formal model written before the prose spec is grounded is built on shifting ground — the three-pass review will change the spec and break the model.

What needs to land in pressure-testing.md: a named Step 4 — formal verification — with the Alloy/TLA+ question-type split, the prose-first ordering rationale, and guidance on when the step is required (regulated atoms and compositions with concurrency-critical invariants) vs. optional (structural-only compositions with no temporal emergent invariants). The Attributed Permissions Admin composition is the canonical worked example: it shipped with a static Alloy structural model and a dynamic Alloy 6 LTL (Linear Temporal Logic) model verifying its load-bearing temporal claims.

Resolved 2026-06-16. The premise — “the library has no codified formal verification step” — no longer holds. The formal layer is codified in pressure-testing.md: §Formal models carries the Alloy-structural / TLA+-behavioural question-type split, §The English/formal SSOT contract carries the prose-first, English-canonical / model-derived ordering, and §The formal-layer vote carries the per-pattern when-required-vs-optional guidance under the minimum-formalism principle — plus the model-present bar, the coverage cross-check, and the conflict protocol. Every vote-yes pattern now ships a verified model + a rejected buggy twin through tools/harness/ (Saga, grounded 2026-06-16, is the latest worked example). What item 6 asked to land has landed and been exceeded; the lone residual — whether it is labelled a “Step 4” — is cosmetic and deliberately declined (the formal-layer vote, not a fixed pipeline step, is the right shape). Retire from the open list on the next pass.

7. Logic Confinement Principle — full application to projector and verification harness. The Logic Confinement Principle is now a first-class architectural commitment in execution-contract.md. The Beacon reference implementation satisfies rules 1 (core is pure), 2 (single seam), 3 (explicit inputs for clock/id), and 6 (async at the edge) fully. Two rules remain partially satisfied: rule 4 (explicit construction — createEvent before appendEvent — rather than hidden work inside transactional functions) and rule 5 (compiler-emitted local invariant assertions, not distributed runtime assumptions). Closing these requires: (a) separating event construction from event insertion in the composition layer, making the constructed event an explicit value before the transaction boundary; (b) designing the projector to emit local invariant assertions compiled from each atom’s named invariant set. First natural targets: the projector architecture and the verification harness derivation pipeline. Scoped to the NLnet grant period as a named deliverable; surfaced 2026-05-29.

5. Compliance-folder sustainability under the #11–#14 cluster — RESOLVED (2026-06-08). This debt anticipated that Credential, Session, Capability, and Invitation (#11–#14) would overload a compliance/ folder with atoms that carry regulated surfaces (NIST 800-63B, PCI DSS, OWASP ASVS, GDPR) but are not of compliance — they are authentication, session-management, object-capability, and onboarding primitives whose regulated surface exists only because regulation touches authentication and access. The forcing function landed and was resolved structurally rather than by re-foldering: the usage-derived taxonomy dissolved the category folders entirely, atoms are stored flat, and regulated / security are derived overlays read from the composition graph — so an authentication primitive carries the security and regulated overlays without being filed under compliance, and the “which folder” question disappears rather than being re-answered. See atoms/TAXONOMY.md and the 2026-06-08 entry in discoveries.md.

8. Spec-to-implementation lineage manifest (the “recipe”). Each reference implementation (Beacon, the Multi-Party Approval demo, and every future projection) currently records its derivation from the spec corpus only implicitly — recoverable only by reverse-engineering imports and domain-file names, as a 2026-05-29 audit of Beacon’s spec set demonstrated when its composition list had to be inferred rather than read. That implicit lineage is a gap, not a convenience: the grant’s round-trip benchmark (“regenerate the reference implementation from its grounded specifications”) cannot run without an explicit statement of which specifications, and the implementation-discovered-findings loop (contributing.md §”Implementation-discovered findings”) cannot close without it either — a spec that moves on Final Critique N must be able to name the implementations it has just made stale, and a finding surfaced during a build must route to a specific spec passage rather than to a whole file. The deliverable is a machine-readable per-implementation manifest that is (a) bidirectional — implementation → the spec files and grounding versions it derives from, and spec → its dependent implementations; (b) version-pinned — each dependency carries the spec’s grounding marker or commit so drift is detectable; and (c) granular enough to route findings — a code symbol (table, guard, invariant check) traces to a named action or numbered invariant in the spec, not merely to the file. Discipline: the manifest is generated from the implementation’s actual references and CI-checked against the corpus, never hand-authored — a hand-maintained lineage file is itself an unverified artifact, exactly the drift the methodology exists to prevent. The canonical manifest is structured; the human-readable lineage view is a projection of it — Grace Commons applied to itself. Scoped to the NLnet grant period as a named deliverable underpinning both the projector and the round-trip benchmark; surfaced 2026-05-29.

9. Corpus Application-state audit under the composition-state rule. The 2026-06-10 adjudication (execution-contract.md §Composition state) classifies every composition Application-state element as derived index or extraction-pending, but the grounded corpus was authored before the rule existed and none of its specs carries a classification yet. The audit: for each grounded composition, classify every Application-state element against the rule’s one question (fully derivable from constituent stores through declared read surfaces?), record the rebuild procedure for derived indexes, flag non-derivable elements extraction-pending with the proposed atom named, and fold the classification into each spec’s Application state subsection. Every fold is an edit to a grounded pattern, so each rides a touch-triggered re-pass round — batch them with the scheduled-rescan automation wave rather than as manual one-offs. The known poles to run first: C6 disclosure_to_event (derivable), Idempotent Reservation token_results (non-derivable → Idempotency Result Memo), Reservation Lifecycle reservation_to_pool + slot_released (mixed — the flag may carry compensation truth the Event Log entries also record; the audit decides whether the atomic-write coupling makes it derivable or not). A provisional classification matrix is staged at working-ideas/composition-state-audit.md (working staging, not canonical; dies into the patterns’ Application state subsections and Lineage notes as the folds land). Surfaced 2026-06-10, Refactor 1.

Progress 2026-06-16: new compositions now carry the derived-index / extraction-pending classification (5 of 25 to date, Saga included); the corpus retrofit fold across the older compositions remains open — pair it with item 1’s threshold-propagation sweep.

10. Tiny Map / composition-card convention + sweep. A compact “composition at a glance” card — the constituent atoms feeding the composition, the composition’s emergent verb, and a footer naming its complement and sibling with the one-line distinction — proposed (2026-06-16) as a scannable Tier-1 bridge at the head of every composition spec. Worked exemplar (Saga): Workflow / State Machine + Event Log → Saga · advance-or-compensate; footer complement · Undo History (compensating action vs replay-skip) and sibling · Stateful Workflow Execution (failure-compensation vs approval-gating). The load-bearing semantic rule: the card renders composition — both constituents are parts of Saga — not a dataflow pipeline (an early sketch drew WSM → Saga → Event Log, which misreads as Event Log being downstream of Saga). Two coupled pieces, neither yet done: (a) decide the convention — whether to adopt a ## Tiny Map section into spec-format.md’s composition shape, positioned near the head (the sketch put it directly after the title, before Summary), fixing the card’s content (constituents → composition + emergent verb; complement/sibling footer) and rendering (ASCII for portability and/or Mermaid for the site, per working-ideas/architecture-map.mermaid); adding a section to the canonical shape is a methodology change, so it lands via a short spec-format proposal, not ad hoc. (b) sweep — once adopted, add the card to every grounded composition and reconcile the complement/sibling vocabulary against each spec (the methodology distinguishes sibling — shared spine — from complement — opposite mechanism; Saga’s own spec already carries both). Saga is the natural first card. Surfaced 2026-06-16.

Taxonomy question — resolved (2026-06-08)

The workflow category’s one-atom question was resolved 2026-06-04: it stands on two atoms — Approval Step (the fixed-state pole — states fixed by the atom) and Workflow / State Machine (the general-declared pole — states declared by the deployment). The broader axial-split question is now also resolved — see below.

The broader axial split — resolved (2026-06-08). The categories (productivity, temporal, resource-lifecycle, compliance, messaging, workflow, healthcare) did mix conceptual axes — healthcare domain-scoped, the others concept-scoped, compliance conflating pure-infrastructure atoms with atoms-that-happen-to-be-regulated. The usage-derived taxonomy (atoms/TAXONOMY.md) resolved it: atoms are stored flat, cross-cutting classification (regulated, security, standards) is derived from the composition graph as overlays, and domain is the single intrinsic, EOS-gated axis (seeded on Medication Order; held on Clinical Observation as the masquerade case). The resolution came out sharper than the “regulation as a regulated: true flag” framing once guessed here: regulation is not a stored flag but a derived fact. The deferral discipline paid off — waiting until the catalog forced the cut let classification be read off a reviewed substrate (the composition graph) rather than guessed one folder per atom.

Capability-vs-Invitation bearer-token question. Both Capability (atom #13) and Invitation (atom #14) use bearer-token transport: the holder of the token is authorized to take an action, with no identity check at the point of action. Both are time-bounded and both can be revoked. The argued distinction is that Capability is for resource access — the token authorizes access to a specific resource or action, and the redeemer’s identity is permanently and intentionally irrelevant — while Invitation is for identity onboarding — the token authorizes a single entry event, and the resolution of that event binds an identity that is then permanently recorded. The structural difference is Declined as a first-class outcome: a Capability has no declined state because a bearer either redeems it or doesn’t; an Invitation carries Declined as a named terminal state because a human’s deliberate refusal is semantically distinct from non-use. The authoring discipline resolves this: draft Capability first (atom #13) and use it as the Pass 2 mirror when drafting Invitation. If Invitation cannot be specified as freestanding — if its specification must name Capability’s structure to distinguish itself — the two collapse into one atom (bearer-token-with-lifecycle) and the distinction is carried as a mode or subtype rather than a separate atom.

Q3 2026 – Q2 2027: Year 1 Goal — ~100 Near-Perfect Atoms

Target: Reach approximately 100 high-quality, pressure-tested atoms and compositions by the end of the first year, with strong healthcare coverage and initial cross-domain atoms. The first 25 atoms and 13 compositions were produced in roughly three weeks while simultaneously building the methodology, the framework, and the live demo — with a second architect and dedicated tooling, this target is directional but realistic.

Key Initiatives

1. Logic Confinement Principle. Formalize and fully apply the Logic Confinement Principle across the entire library and tooling. Core must remain pure (synchronous, deterministic, no I/O, no implicit time, randomness, or crypto). Single seam discipline, explicit inputs, behavior as data transformation, and async-at-the-edge rules apply to all projections. Update projector and verification harness to enforce these constraints mechanically. Beacon demo refactored to fully conform as the reference implementation.

2. Tag-Based Ontology (not folders). Replace folder hierarchy with a rich, multi-dimensional tagging system driven by data rather than card-sorting. Tags will cover: Domain, Behavioral Property, Lifecycle Stage, Regulatory Anchor, Composition Role, Technical Property, Maturity. Enables dynamic views — “All EHDS-relevant atoms”, “All audit-related patterns”, “Cross-domain universals”. Ontology evolves organically from actual composition usage, regulatory overlap, and implementation data. The usage-derived taxonomy (flat storage + derived overlays, landed 2026-06-08) is the first realization of this tag-based direction — overlays are data-driven tags read off the composition graph; this initiative extends it into a richer multi-dimensional ontology.

3. Healthcare Core Expansion. Ground 55–65 new healthcare-focused atoms, building on the existing Clinical Observation and Medication Order base. Primary downstream target: EHDS implementation patterns. A first triaged candidate backlog — separating genuinely-new atoms from domain specializations of existing concept-scoped atoms — is recorded in §”Healthcare atom backlog” below; the expansion draws from that deduplicated backlog, not a raw wishlist.

4. Cross-Domain Attack. Begin deliberate extraction and generalization of universal atoms — Audit Trail, Multi-Party Approval, Defensible Retention, Consent Propagation variants and related patterns. This phase will intentionally stress and evolve the ontology.

5. Tooling Maturity. Deliver second-author-ready projector and verification harness — the core NLnet grant deliverable. The tooling makes the ~100-atom target achievable by a two-person team within the grant period.

Healthcare atom backlog — triaged candidate list (2026-06-04)

Seeded from an external brainstorm of OpenEMR / Open Hospital atom candidates and triaged against the library’s reuse thesis. The thesis matters here more than anywhere: most healthcare “atoms” people list are domain specializations of existing concept-scoped atoms, not new freestanding concepts. “Audit Logging” is not a new atom — it is Event Log + Audit Trail. “Patient Identity” is Party Identity with a medical-record-number field. Grounding redundant domain-named atoms would defeat the cross-domain reuse the library exists to demonstrate. This section records the triage so the Healthcare Core Expansion initiative draws from a deduplicated backlog.

Triage verdicts: grounded (already in the library); reuse (covered by an existing pattern — no new atom; the candidate is that pattern applied to a healthcare subject); not-an-atom (deployment config, a reference enumeration, a wire format, a foreign-key link, or a projection — not a stateful EOS concept with its own state machine, actions, and invariants); new-atom (a genuinely freestanding concept worth grounding, subject to the EOS Pass-2 test); composition (an application of two or more atoms).

Already grounded, or covered by reuse (no new atom)

Candidate	Verdict	Covered by
Medication Order	grounded	`atoms/medication-order.md`
Vital Signs Observation	reuse	Clinical Observation (vitals are clinical observations)
Patient Identity	reuse	Party Identity (a patient is a party; MRN is a deployment field)
Patient Consent	reuse	Consent (purpose-scoped agreement; treatment-consent and HIPAA authorization are scopes)
Patient Record Access / PHI Access Event	reuse	Permissions + Session-Gated Authorization (C14) + Selective Disclosure + Audit Trail
Encounter Status / Order Status	reuse	Workflow / State Machine (a declared status lifecycle)
Appointment Slot / Booking / Cancellation / Provider Schedule	reuse	Capacity Constraint Enforcement + Provisional Commitment + Reservation Lifecycle (C9); provider availability is a time-indexed capacity pool
User Authentication	reuse	Credential + Session + Login (C13)
Role-Based Access	reuse	Permissions (a role is a named reusable grant set — see the Role new-atom note below if the bundle itself earns an atom)
Audit Logging	reuse	Event Log + Audit Trail (the canonical “do not re-invent the audit atom”)
Data Retention Rule	reuse	Retention Window + Defensible Retention (C1)
Provider Credential (authentication sense)	reuse	Credential
Patient Demographics	not-an-atom	a mutable attribute schema; its correction history is Clinical Observation’s amendment-chain shape, not a new concept
Encounter Type	not-an-atom	a reference enumeration (a code)
Billing Encounter Link	not-an-atom	a cross-reference / foreign key — composition-layer state, not an atom
FHIR Resource Export / HL7 Message / Document Import / External System Sync	not-an-atom	serialization / wire formats / integration projections; PHI crossing the boundary is a Selective Disclosure event, message delivery is Notification, idempotent receipt is Duplicate Prevention, document custody is Provenance
Facility Configuration	not-an-atom	deployment configuration

Genuinely-new atom candidates (worth grounding, pending EOS Pass-2)

Candidate	Category	One-line scope	EOS note / composes
Problem / Condition Entry	healthcare	a longitudinal clinical condition with an active → resolved/inactive status lifecycle and an amendment trail; Problem-List entries, diagnoses, and Allergy Records are instances	distinct from Clinical Observation (a point-in-time measurement) — a condition persists and changes status over time; composes Clinical Observation, Provenance, Audit Trail. Highest-leverage healthcare atom on this list.
Fulfillable Order	healthcare / generic	the general order-with-fulfillment lifecycle (placed, in-progress, then completed or cancelled, with a result attachment); Lab Order, Procedure Order, and Medication Order are specializations	the general primitive Medication Order is a specific case of (as Approval Step is to Workflow / State Machine); Pass 2 decides whether to extract the general atom or keep per-domain order atoms
Clinical Administration Record	healthcare	an immutable “substance/treatment X was administered to patient P at time T” event (immunization, medication administration, infusion) with site/dose/lot	borderline — may be Clinical Observation specialized; resolve at authoring whether administration-vs-observation earns its own atom. Consumed by the MAR composition
Record Merge / Identity Reconciliation	resource-lifecycle (generic)	merge two duplicate identity records into a surviving record, with merge provenance and (often) reversible un-merge; Patient Merge, customer dedup, party reconciliation are instances	own state machine (two sources to one merged record, reversible); composes Party Identity + Provenance + Audit Trail
Qualification / Credentialing Record	compliance (generic)	a verifiable professional qualification — license, board certification, clinical privilege — with issuer, scope, expiry, and verification status	the licensure sense of “Provider Credential”, distinct from the authentication Credential atom (name-collision flag); composes Actor Identity, Retention Window. Recurs across healthcare licensure and financial KYC
Ledger Entry / Posting	resource-lifecycle (generic, financial)	an immutable financial posting against an account (debit or credit) with a reference and reversal-by-new-entry discipline	Charge Capture and Payment Posting are instances; the home composition is Immutable Transaction Ledger (C6)
Amendable Document / Signed Note	generic	a narrative record with addendum/amendment history and an author signature; Clinical Note is the canonical instance	likely covered by Clinical Observation’s amendment-chain shape + an Actor Identity signature — resolve at authoring whether a distinct document atom is warranted
Role / Permission Bundle	compliance	a named, reusable set of permission grants assignable to actors (the “role” in RBAC)	borderline — Permissions composes individual grants; a Role atom adds the reusable named bundle + assignment. Decide whether the grouping earns an atom or is a Permissions composition
Time-Slot Schedule	temporal / resource-lifecycle	a recurring time-indexed availability calendar (a provider’s bookable slots over time)	borderline — Capacity Constraint Enforcement covers the bounded-pool side; a distinct atom is warranted only if recurrence / calendar arithmetic recurs widely

Healthcare composition candidates (applications, not atoms)

Patient Record — Party Identity + Problem/Condition entries + Clinical Observations + a Workflow / State Machine encounter lifecycle, under Audit Trail.
Patient Encounter — an episode of care: party references (patient, providers) + a Workflow / State Machine encounter-status lifecycle + the observations and orders recorded during it.
Medication Administration Record (MAR) — Medication Order + Clinical Administration Record + Chain of Custody (C12) for the drug, under Audit Trail.
Prescription Fulfillment — Medication Order + the dispensing event + Chain of Custody.
Insurance Claim Lifecycle — a Workflow / State Machine claim lifecycle (submitted, adjudicated, then paid/denied/appealed) + Ledger Entries + an encounter link, under Audit Trail.
Clinical Trial Data Capture and Immunization Registry Reporting — downstream healthcare compositions noted elsewhere as worked-example targets.

Sequencing note

The recommended first picks when Healthcare Core Expansion begins are the three highest-leverage genuinely-new atoms: Problem / Condition Entry (anchors the longitudinal clinical-record surface; unblocks Patient Record), Fulfillable Order (generalizes Medication Order; unblocks Lab and Procedure orders), and Qualification / Credentialing Record (recurs across healthcare licensure and financial KYC). Every candidate above must still clear the EOS Pass-2 freestanding test before it earns an atom file — the entries flagged borderline are flagged precisely because that test may route them back to an existing pattern rather than a new atom.

Concept-recovery atom backlog — candidates surfaced in reverse (2026-06-13)

Seeded from the reverse concept-recovery exercise (working-ideas/recovery/) — ten runs mining real systems across six languages and six domains plus the FHIR standard (ERPNext, hrms, frappe/crm, Odoo, OpenMRS, Akaunting, Medplum/FHIR, OpenBoxes, and two small libraries), running the routing test and the three gates backwards against deployed code. Same triage discipline as the healthcare backlog above: the dominant result was reuse — the existing atom set recurred as the substrate everywhere — and only genuinely-freestanding concepts the library lacks earn a candidate row. All entries are candidates pending EOS Pass-2; none is grounded, and this section changes no count (grounded counts live only in the Current-state section, per pressure-testing.md §The no-snapshot rule). Evidence is labelled by recovery tier per working-ideas/concept-recovery.md: tier-1 computed, tier-2 inferred from schema, tier-3 read from source — none was runtime-verified (“read, not run”), so a candidate’s invariants are recovered, not executed.

Genuinely-new atom candidates (pending EOS Pass-2)

Candidate	Category	One-line scope	Witnesses (recovery runs)	EOS note / composes
Acyclic Recursive Composition	generic / structural	a record that recursively contains records of its own type under an acyclicity invariant (and, for quantity-bearing forms, a rollup-by-summation invariant); Bill-of-Materials, observation groups, category trees, concept sets, role hierarchies are instances	6 — ERPNext BOM, Odoo `mrp.bom`, OpenMRS `obsGroup`/`ConceptSet`/role-hierarchy, Akaunting `Category`, FHIR `Observation.hasMember`, OpenBoxes `Location`/`ProductComponent` (runs 3, 6–10; all tier-3)	Resolved 2026-06-13 → not an atom. On classification (GPT / Grok / author + the witnesses) this routes to a 4th structural-relation invariant template — acyclicity / well-foundedness (`spec-format.md` §Structural-relation invariant templates) — not a new atom: all six witnesses are self-referential relations on existing concepts’ records (Product, Location, Category, Obs…), so it owns no state, only a relation’s integrity. Tree vs DAG = the relation’s parent-cardinality; the closure/rollup is a derived index. The Workflow-precedent atom case was weighed and declined (Workflow owns state; an acyclic-containment relation does not). Distinct from compositions of compositions (which is spec-artifact nesting — a composition naming another composition); this is a domain-data self-relation one layer down.
Coded Category (+ Terminology Binding overlay)	generic	a typed, coded, often-recursive controlled vocabulary (Coded Category); plus an overlay binding concepts across vocabularies with a typed equivalence (Terminology Binding)	4 — OpenMRS `Concept`/`ConceptMap`, Akaunting `Category` (coded core, no binding), Odoo/ERPNext categories, FHIR `CodeSystem`/`ValueSet`/`ConceptMap` (runs 6–9)	FHIR supplies the structure: CodeSystem (vocabulary) + ValueSet (constrained binding) + ConceptMap (cross-vocabulary map, whose `equivalence` lattice is the load-bearing invariant). Nuances the “a code is not-an-atom” verdict above — a single enum is not, but a vocabulary + mapping system is. May subsume the forthcoming Definition Registry.
Sequential Identifier / Naming Series	resource-lifecycle (generic)	a human-readable, per-scope monotonic identifier with uniqueness and gap/rollover-on-cancel behaviour (`INV-2026-00042`), distinct from the library’s opaque-id discipline	2 — ERPNext `naming_series` (64 DocTypes), Odoo `ir.sequence` (1,481 uses) (runs 3, 6)	Invariants: per-scope monotonicity, scoped uniqueness, declared rollover/gap behaviour. The library gives every atom an opaque id; this is the orthogonal human-facing identifier concept.
Orthogonal / multi-dimensional state	workflow	one entity running concurrent independent sub-lifecycles (Sales Order `delivery_status` ⊥ `billing_status`; an asset’s operational ⊥ financial state)	1–2 — ERPNext (Sales Order, Asset), Odoo (multiple `*_state` fields) (runs 3, 6; tier-2)	Borderline — needs the gates. Workflow / State Machine is single-dimensional (Harel orthogonal regions unmodelled); resolve whether this is a new atom or a composition of several Workflow / State Machines.
Deadline / SLA	temporal / compliance	a commitment to act by a computed time, with breach observable from the records (holiday-calendar-aware)	2 (weak) — frappe/crm SLA (`response_by`/`first_responded_on`) + the regulatory-deadline case; Odoo `crm.lead.date_deadline` is advisory only (runs 5, 6)	Weak recurrence; no strong third witness (Odoo’s deadline is advisory). Time-bound obligation + records-clearable breach detection. Hold pending a stronger witness.

Strengthened existing candidates (cross-reference — no new row)

Ledger Entry / Posting (listed above) — recovery adds the single-entry vs double-entry axis: the double-entry form (Odoo account.move._check_balanced, tier-3) carries a debit = credit binding-bijection invariant; the single-entry form (Akaunting signed transactions, tier-3) does not. Both sit under Immutable Transaction Ledger (C6). The taxonomy distinguishing the two — present in one system, correctly absent in the other — is the cleanest recovery confirmation, not a gap.
Idempotency Result Memo (extraction-pending, 2026-06-10 above) — confirmed in the wild by recovery run 2 (asgi-idempotency-header): the middleware’s response cache is the token → result memo the composition-state audit predicted, with a reproduced bricked-key bug violating its at-most-once invariant. Corroboration of the existing proposal, no change to it.

Composition-pattern candidates (applications, not atoms)

Balance Ledger — append-only ledger + a derived running balance + Capacity Constraint. Five corpora (ERPNext stock/GL, hrms leave, Odoo account/stock, Akaunting transactions, OpenBoxes TransactionEntry; runs 3, 4, 6, 8, 10). Reusable wiring, not a primitive (the balance is a derived index, the bound is Capacity Constraint — no new state). Carries the single/double-entry axis noted under Ledger Entry / Posting.
Reconciliation / Count-and-Adjust (new, run 10) — reconcile a recorded balance against an externally-observed truth (a physical count, a bank statement), record the discrepancy, and post an adjustment so recorded = observed. Two witnesses, two domains: OpenBoxes CycleCount* (inventory) + Akaunting Banking/Reconciliation (bank rec). Likely a composition (Balance Ledger + an observation/count event + an adjusting entry); the Gate-3 question is whether the discrepancy record is an emergent surface of its own. Tier-2 inferred (model names) pending a tier-3 read of CycleCount.groovy. Not to be conflated with conflict / replica reconciliation (offline-first multi-source merge-repair) — a distinct, harder pattern that breaks the single-consistency-domain scope assumption and is staged with the known boundaries in working-ideas/no-global-services.md §Strange-pattern forecast, not here; this count-and-adjust row owns no such boundary.
Cross-document fulfillment rollup — a status derived from the state of downstream documents (“Partly Delivered”, “Partially Received”; ERPNext, run 3). Almost certainly the existing derived-index construct as a recurring cross-document pattern, not an atom.

Sequencing note

First picks: Acyclic Recursive Composition (five cross-language/cross-domain witnesses including the FHIR standard, gate-ready — carry the tree-vs-DAG sub-form distinction into Pass 2) and Coded Category (+ the Terminology Binding overlay, for which FHIR’s CodeSystem/ValueSet/ConceptMap factoring is the proposed structure). Sequential Identifier follows. Orthogonal state and Deadline / SLA stay flagged borderline / weak until the gates — or a stronger witness — settle them. Excluded by author decision (2026-06-13): Invertible Delta / Reversible Change (recovery run 1, pboyer/rec) — a sub-atomic change-with-captured-prior primitive below the library’s granularity; it belongs to utility-spec territory (Undo History’s compensating events already instantiate it), not a freestanding library atom. Every candidate must still clear the EOS Pass-2 freestanding test before it earns an atom file.

The roadmap is a living document. Patterns are added as the library’s content forces resolution of open questions, not on a fixed schedule.

Roadmap

Current state

Planned-sequence atoms — all grounded (roadmap history)

7. Provenance

9. Workflow / State Machine

10. Preference / Personalization

11. Credential

12. Session

13. Capability

14. Invitation

Grounded atoms — short status (formerly atoms #1–#6, #8)

Compositions — current state

Grounded

C11 grounded — the C-numbered backlog closes

C11. Preference-Aware Notification Fanout — grounded on Final Critique 12 — 2026-06-12

Saga (C19) grounded — first of the dream-compositions pipeline

Summary table

Formal model coverage

Shipped

Deferred — recorded in Lineage notes

All other grounded patterns

Convention

Methodology debts — open

Taxonomy question — resolved (2026-06-08)

Q3 2026 – Q2 2027: Year 1 Goal — ~100 Near-Perfect Atoms

Key Initiatives

Healthcare atom backlog — triaged candidate list (2026-06-04)

Already grounded, or covered by reuse (no new atom)

Genuinely-new atom candidates (worth grounding, pending EOS Pass-2)

Healthcare composition candidates (applications, not atoms)

Sequencing note

Concept-recovery atom backlog — candidates surfaced in reverse (2026-06-13)

Genuinely-new atom candidates (pending EOS Pass-2)

Strengthened existing candidates (cross-reference — no new row)

Composition-pattern candidates (applications, not atoms)

Sequencing note

C11. Preference-Aware Notification Fanout — `grounded on Final Critique 12 — 2026-06-12`