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 vision and framing are in why.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.

How to read this file (orientation added 2026-07-06 — navigation only, never state): this is a dated ledger, not a report. §Current state carries the running record, one dated bullet per landing, newest additions at the top of the list; the grounded catalog below it is the registry whose status cells mirror each pattern’s own Status line (the pattern file is the source of truth — a mismatch is a finding). Methodology debts are numbered and permanent; progress and resolution notes ride each debt as dated additions, so a debt’s history reads top to bottom inside its own entry. Candidate backlogs (healthcare, concept-recovery, exhibit-sourced) sit at the bottom and change no counts. This file deliberately carries no summary block — a hand-written “current totals” section is exactly the drift class the no-snapshot rule kills; the counts live inside dated entries where they can never silently lie, and the computed overviews live at graph.md (structure) and status.md (gates).

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.

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 (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 Execute Gated Workflow (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.

Execute Gated Workflow (C10) grounded — 2026-06-04. Immediately after 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 State Machine + Approval Step + Permissions + Assignment + Audit Trail (substrate) and is the first composition to compose the State Machine atom. Its load-bearing emergent property is the precise closure of an atom-level extraction: 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 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.

Propagate Consent Revocation Downstream (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 Customer Onboarding (C8).

Reserve from Pool (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.

Resolve a Person’s Data Rights (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 Final Critique 1). 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 Reserve from Pool’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. 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 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, Customer Onboarding; 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
Customer Onboarding (C8) ✅ landed 2026-06-03	TLA+	High	adverse-trigger-precedes-suspend; open-trigger ⇔ Suspended — `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) — `message-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, 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, Propagate Consent Revocation Downstream, Resolve a Person’s Data Rights, Defensible Retention, External Onboarding, Forensic Recovery, Idempotent Reservation, Immutable Transaction Ledger, Customer Onboarding, Login, Multi-Party Approval, Notification Fanout, Preference-Aware Notification Fanout, Privileged Access Provisioning, Reserve from Pool, Session-Gated Authorization, Shared Todo, Execute Gated Workflow, 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), Resolve a Person’s Data Rights (C7), and 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 Customer Onboarding (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. State Machine

Category: workflow

Status: grounded 2026-06-04 (Alloy model 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 Execute Gated Workflow (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. 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); State Machine is the general case. The two atoms compose into Execute Gated Workflow (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. Execute Gated Workflow (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/message-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 5 — 2026-06-23. Compliance primitive; data subject’s agreement to a specified processing purpose with grant/revoke/expire lifecycle. Unblocked C2 (Propagate Consent Revocation Downstream), C7 (DSAR), C8 (Customer Onboarding).
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 5 — 2026-07-12. Workflow primitive; single approval gate with Pending/Approved/Rejected/Withdrawn lifecycle. Unblocked C4 (Multi-Party Approval, now grounded). First entry in workflow. FC5 (2026-07-12 scheduled rescan) promoted Invariant 9 to an explicit checked predicate in the TLA+ model and surfaced the guard-clock placement revision fixed in execution-contract.md.
Selective Disclosure — grounded on Final Critique 5 — 2026-06-23. 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 5 — 2026-07-12. Compliance primitive; persistent verifiable identity record for an external party with Unverified/Verified/Suspended/Closed lifecycle. Unblocked C8 (Customer Onboarding). Survived foundation round plus Opus Phase 4 clearance gate; six clearance-gate findings closed in-pattern. FC5 (2026-07-12 scheduled rescan) repaired the Invariant-7 erasure carve-out’s capability provenance (scrub re-declared to a forthcoming Erasure Coordination pattern) and specified the read query surface.
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 (Reserve from Pool). 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 Compensable Workflow (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 (Resolve a Person’s Data Rights) 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 (Propagate Consent Revocation Downstream) and C9 (Reserve from Pool) 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 (Execute Gated Workflow), and C12 (Chain of Custody) all grounded 2026-06-04 — C10 immediately after its spine atom 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 Compensable Workflow 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. Propagate Consent Revocation Downstream — 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 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. Resolve a Person’s Data Rights — 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. 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. Reserve from Pool — 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. Execute Gated Workflow — grounded on Final Critique 4 — 2026-06-04. State Machine + Approval Step + Permissions + Assignment + Audit Trail (substrate). Approval-gated transitions — guard evaluation re-converges; first to compose 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 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. Compensable Workflow — grounded on Final Critique 4 — 2026-06-16. 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 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 — Final Critique 4–8 closed 16 foundational; Final Critique 9 returned zero foundational (the first grounding gate, Pass 2 clean from Final Critique 8 on). A post-grounding fresh-reader rescan then reopened the gate — Final Critique 10 surfaced a gate fail-closed/precedence ordering defect, and Final Critique 11 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.

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

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 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: compensable-workflow.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 (compensable-workflow-skip-comp-buggy → Inv 4, compensable-workflow-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 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 on Final Critique 4 — 2026-06-18`	`resource-lifecycle`
—	Actor Identity, Retention Window, Tamper Evidence, Permissions	Atoms	Actor Identity, Tamper Evidence, Permissions: `grounded` 2026-05-13; Retention Window: `grounded on Final Critique 5 — 2026-06-23`	`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 on Final Critique 5 — 2026-06-23`	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 on Final Critique 5 — 2026-06-23`	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	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 on Final Critique 5 — 2026-06-23`	C13 (Login); enriches C16; retires Authentication forthcoming-link in actor-identity.md
12	Session	Atom	`grounded on Final Critique 5 — 2026-06-23`	C13 (Login), C14 (Session-Gated Authorization)
13	Capability	Atom	`grounded on Final Critique 5 — 2026-06-23`	C15 (Capability-Backed Sharing)
14	Invitation	Atom	`grounded on Final Critique 5 — 2026-06-23`	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	Propagate Consent Revocation Downstream	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 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	Resolve a Person’s Data Rights	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	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	Reserve from Pool	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	Execute Gated Workflow	Composition	`grounded on Final Critique 4 — 2026-06-04`	State Machine + Approval Step + Permissions + Assignment + Audit Trail (substrate); approval-gated transitions (guard evaluation re-converges); TLA+ model; first composition to compose State Machine
C12	Chain of Custody	Composition	`grounded on Final Critique 4 — 2026-06-11` (English 2026-06-04; GAP 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	Compensable Workflow	Composition	`grounded on Final Critique 1 — 2026-06-16`	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 is mechanical, not mirrored. Since the 2026-06-03 backlog landing (18 TLA+ and 4 Alloy models, every one shipping a checker-rejected buggy twin — see §Current state above), the shipped set is enumerated by the artifacts themselves: a pattern’s formal models are its sibling .tla / .als files, verified on command by tools/harness/ (node audit.mjs runs every model in the corpus; correct models must hold, buggy twins must be rejected). The per-pattern record lives in each spec’s Lineage notes — the formal-layer vote entry and, where a model shipped, the Formal model entry.

Dated removal note (2026-07-06). A hand-maintained Shipped / Deferred registry previously lived in this section and drifted: it still listed only the six pre-backlog models — and filed Preference / Personalization as Deferred after message-preference.tla and its buggy twin landed (2026-06-03) — weeks after the backlog closed, while the section’s own file recorded the landing under §Current state. Removed under the derive-don’t-mirror discipline (the same rot class as the Summary status mirrors in the 2026-06-12 discoveries entry): the harness and the Lineage entries are the source of truth; this section states the rule, never the roster.

Convention

A vote-yes pattern’s formal layer is discharged when (a) the sibling artifact(s) exist alongside the spec, (b) they clear the model-present bar mechanically via tools/harness/ — correct model green, buggy twin rejected, checks non-vacuous (see pressure-testing.md §The formal-layer vote), and (c) a Formal model entry is recorded in the pattern’s Lineage notes per pressure-testing.md (what the artifact checks, bounds/scope, deliberate exclusions, result). Deferred formal-model candidates land as a Deferred work — formal models item in the pattern’s Lineage notes; they graduate by shipping the artifact, never by editing a registry row here. 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 (Compensable Workflow 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.

Resolved 2026-06-26. The literal trigger — pre-threshold “gate runs again until clean” phrasing in pattern Lineage — no longer exists: a corpus sweep found zero occurrences in atoms//compositions/. Debt #3’s re-gating (the grandfathered cohort given real Final Critique rounds, 2026-06-18/06-23) already moved every pattern onto the threshold, so the pre-threshold rationale was rewritten as a side effect. The only residue was a citation drift — the same canonical passage cited two ways: the actual heading §"What grounded means" (the dominant form) and the bold inline label §"The 92%-good grounding threshold" (which is not a heading). Standardized the two outlier citations (capacity-constraint-enforcement.md) onto the heading form, so all pattern→grounding-criterion references now name the resolvable section. (The anchor named in this debt’s own text above is left as written — it is the description, not a live citation.)

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 (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/ (Compensable Workflow, 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.

Adoption 2026-06-24 — rebuild-failure diagnostic. Operationalize the benchmark’s failure path: when a regeneration diverges, classify the failure — structural/stack gap (the agent cannot start), cross-constituent contract gap (integration divergence), missing decision rationale (business-logic divergence), or passes-tests-but-behavior-differs (test-coverage gap) — and fix in that order, structural first, so a failed rebuild localizes to a spec layer and routes to the specific invariant/action it implicates rather than to a file. Framing borrowed from the Augment Code “rebuild test” (spec-as-source guide, 2026; logged in the prior-art scan).

Adoption 2026-07-06 — backend-swappable generation: the agent behind a seam. The projector’s first generator backend is the Claude Agent SDK (the vendor’s programmatic agent toolkit, run headless) — chosen because the corpus’s seven renders were already produced by that workflow — but the backend is an adapter, never a dependency. Two requirements ride this manifest so the generating AI stays swappable. (a) The generator seam: the projector’s backend interface is one thin per-agent adapter (assemble prompt pack → dispatch → collect candidate artifacts); everything load-bearing — manifest resolution, prompt-pack assembly, the conformance + harness + lint gates, the regen loop — is backend-agnostic, mirroring the conformance validator’s architecture (same manifest, same evaluators, per-render adapters only). The prompt-pack template is tooling and lives with the projector; assembled packs are build artifacts, never committed (per the prompts-stay-out-of-the-repo rule in AGENTS.md). (b) The per-run provenance record: every generation run records, machine-readably — input identity (the spec files with their grounding markers or content hashes, the Execution Contract version, the prompt-pack template version); backend identity (model + version, toolkit version, sampling parameters); output identity (artifact hashes, each file stamped with the debt #13 marker); gate results (conformance percentage, harness verdicts, lint); and platform-sourced token cost (the measurement.md rule — never self-reported). Swapping backends is then a new adapter plus a re-run, and cross-generator agreement — agree.mjs one level up: two backends, same spec, verdict-by-verdict diff — becomes the calibration instrument, exactly as multi-render agreement localizes render defects: a divergence localizes either a backend weakness or a spec under-determination. This discharges the generation half of risks.md §Reviewer-vendor dependence; the review-council half (a cross-vendor control round for grounding gates) remains open there.*

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), Reserve from Pool 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, Compensable Workflow 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 (Compensable Workflow): State Machine + Event Log → Compensable Workflow · advance-or-compensate; footer complement · Undo History (compensating action vs replay-skip) and sibling · Execute Gated Workflow (failure-compensation vs approval-gating). The load-bearing semantic rule: the card renders composition — both constituents are parts of Compensable Workflow — not a dataflow pipeline (an early sketch drew WSM → Compensable Workflow → Event Log, which misreads as Event Log being downstream of Compensable Workflow). 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; Compensable Workflow’s own spec already carries both). Compensable Workflow is the natural first card. Surfaced 2026-06-16.

11. Method-takeaway adoptions from the agentic-formalization prior-art note (arXiv:2604.18228). Reading Towards an Agentic LLM-based Approach to Requirement Formalization (Tagliaferro et al., Politecnico di Milano, 2026) surfaced four method adoptions — full note and rationale at working-ideas/prior-art-agentic-formalization.md — each a touch-triggered edit to a grounded methodology doc: (a) a per-atom verifiability gate as an explicit, traceable field in the spec schema (verifiable? if not, why — unobservable / qualitative intent / model-external — and in which tool), not an implicit consequence of the assurance ladder (spec-format.md); (b) on the ladder, separate “intent-aligned” from “well-formed” so the Checked rung never conflates internal consistency with semantic fidelity to intent (pressure-testing.md); (c) mechanize equivalence, never LLM-judge it — wherever Alloy/TLA+ can decide equivalence it must; an LLM judge is never load-bearing for the Proved rung (pressure-testing.md); (d) decoupled per-stage validation — validate each derivation/render target against the canonical layer independently rather than end-to-end so regressions localize (execution-contract.md; applies to the derivation chain and Evergreen Modernization). The note’s fifth point — LLM extraction reliably drops logical boundaries (termination, completion, failure-detection) and invents unstated domain constraints — is empirical support for the existing grounding-threshold and adversarial-posture discipline, not a change. Each of (a)–(d) edits a grounded doc; batch with the touch-triggered re-pass wave. Surfaced 2026-06-24.

12. CWE weakness-class tags on the security overlay. The security overlay maps invariants to regulations (NIST 800-63B, PCI DSS, GDPR, FDA 21 CFR, SEC, HIPAA, OWASP ASVS) but to no weakness-class taxonomy — there is zero CWE reference in the corpus. Security atoms already enforce the behaviors recognized CWEs name (authorization gating, secret-surface separation, audit-on-mutation); tag the relevant invariants with their CWE IDs so which weakness class an invariant forecloses is explicit and machine-checkable, strengthening the regulator/audit surface. A security-overlay convention add to spec-format.md, landed only where an invariant demonstrably forecloses a named weakness — not blanket annotation. Source: the Augment Code spec-as-source guide’s constitution-pattern CWE mappings (2026). Surfaced 2026-06-24.

13. Inline generation-provenance marker on derived artifacts. Debt #8’s manifest records spec→implementation lineage externally; the complement is stamping each generated artifact itself with a generated — do not edit marker carrying its source spec, the spec’s grounding marker, and the generating model/version. This reinforces the discipline already stated for formal models — never hand-patch a derived artifact (pressure-testing.md) — by making a derived code artifact self-identifying as derived and traceable without consulting the manifest. Lands on the projector (debt #7) and is emitted and CI-checked alongside the manifest (debt #8). Source: the Augment Code spec-as-source guide (2026). Surfaced 2026-06-24.

14. Retire the C-number scheme — names are canonical. Compositions carry legacy Cn identifiers (C1–C19) inherited from the original planned-backlog sequencing (working-ideas/dream-compositions.md) — cryptic and anti-Grace: a human reading “C12” learns nothing, where “Chain of Custody” carries the meaning. Done 2026-06-24: the (Cn) suffix was stripped from the nine composition titles that still carried it, so titles are now name-only, matching the nav. Future goal: retire the Cn shorthand from cross-references too — ~1,500 in-corpus references (C1 alone ≈ 249) rewritten to the composition name/link, so no cryptic identifier survives anywhere. Scope: 19 numbers, C1–C19 — the eighteen-composition backlog plus C19 (Compensable Workflow, the one deliberate extension beyond it); the six compositions that predate C-numbering carry no number and need no rewrite. The roadmap’s composition catalog is the interim number↔name registry to rewrite against. Best done incrementally — one Cn at a time (rewrite that number’s references to the composition name/link, verify, then move to the next), each change riding the touch-trigger re-pass of the compositions it touches, rather than one big-bang sweep; once the last number is retired, a lint check enforces that no bare Cn composition reference remains. Surfaced 2026-06-24.

Progress 2026-06-24 — C1–C6 done; rename recipe, a readability step, and a lint gap recorded. C1 was a pure number-retirement (no rename): 232 cross-references → “Defensible Retention.” C2 was the first rename — number retired and the composition renamed to Propagate Consent Revocation Downstream, file included. The full rename recipe (when a Cn is also renamed, not just de-numbered): (1) git mv the spec file; (2) update its H1 and front-matter title; (3) rewrite the token, the old name (full + short), and every filename link corpus-wide; (4) regenerate atoms/index.md; (5) update the roadmap catalog entry (name + link); (6) rename the formal-model artifacts — the .tla/.als, the buggy twin, and their .cfgs — match the TLA MODULE name to the new filename, fix the old name in the model header comment, and re-run the checker (correct passes, buggy rejected); (7) readability pass — convert the composition’s self-references to “this composition” (subjects → “This/this composition”, possessives → “this composition’s”; the title/H1 keep the name), minding determiner artifacts (“the this composition X” → “this composition’s X”), hyphenated forms, and sentence-initial capitalization. Readability now runs on every retirement, rename or not. C1–C6 done (C3–C6 pure number-retirements; C5 was a no-op — already name-only in the specs, only registry/log tokens left; C6 the first big multi-file retirement, 13 files). Scope (held since C1): only spec bodies — atoms/, compositions/, root spec docs — are de-numbered; the roadmap catalog (interim registry), dated history (changelog, ai-usage-log), the tools/harness/coverage/ matrices, and working-ideas/ notes keep their Cn by design (they still carry C1–C4). Traps seen so far: ID-style false positives (e.g. APA’s “credential C2”, an ID — not the composition); non-breaking-space name doubles; a Cn embedded in a stable finding ID (the MC-Cn-N form) — leave those like the registry, historical labels not live cross-references; and a Cn carrying a leading letter (the then-current FCn form embedded a bare round-number Cn with no boundary after the FC prefix) — invisible to \bCn\b, but a landmine for any looser pattern; and (C6) redundant name+number glosses — Cn (Full Name), (composition Cn, …), [Name (Cn)](link) — collapse to the bare name rather than producing Name (Name), while per-composition round labels (Cn cluster) live in the finding-ID namespace and are left like finding IDs. Lint gap to close: the dangling-link check (A-dangling-link) validates only .md targets, so it did not catch the spec → missing .tla reference the rename briefly introduced; extend it to flag spec→model (.tla/.als) references to absent files — a companion to the no-bare-Cn check above. Finding-ID update: the MC-Cn-N / Cn-N finding IDs and Cn cluster round labels this pass deliberately left in place are now marked for removal under debt #15 — cryptic acronyms, the same anti-Grace problem.

Progress 2026-06-25 — C7 and C8 done. C7 was a rename: “Data Subject Rights Fulfillment” → Resolve a Person’s Data Rights (7 artifacts git mv‘d, 3 MODULE names matched, both twins re-verified; dated history kept the old name per the C2 precedent). C8 was a rename plus a full acronym kill — the first pass where retirement went beyond the number and the composition name. Per directive, “KYC” (not on the naming.md §6 cited-standard whitelist; correction 2 already named the target) was eliminated wholesale from the spec body, not merely glossed: the title/H1 → Customer Onboarding; the action initiate_kyc → initiate_onboarding; the id field kyc_case_id → case_id; the state map party_to_kyc_case → party_to_case; the event namespace kyc.* → customer-onboarding.* (8 event types); the example actor system_kyc_auto → system_verification_auto; and prose “KYC” spelled out to “Customer Due Diligence” / “Know Your Customer” or cut. Identifier rule (reusable): strip the acronym, then ask whether what remains needs a qualifier or already has one from context — travelling action names take it (initiate_onboarding), but in-file state keys do not (the file is the qualifier → bare case_id, party_to_case). The structural identifiers and event names were confined to the one spec (no cross-file or formal-model references — the .tla abstracts to state/openTriggers), so the rename stayed .md + model-header only (MODULE → customer-onboarding, checker re-run: correct passes, buggy twin rejected at 3 states). Scope held: spec bodies de-numbered and de-acronymed; the roadmap registry keeps its C8 tokens (display name updated to Customer Onboarding, .md/.tla links repointed); tools/harness/coverage/ and working-ideas/ left per precedent. Domain “KYC” deliberately left only where it is a generic acronym example in the acronym-policy docs (pressure-testing.md §Pass 1, spec-format.md) and a term-collision teaching example (the-spec-layer.md), plus dated Lineage acronym-gloss finding records — those are debt #15’s acronym-sweep scope, not a composition reference.

Progress 2026-06-25 — C9 done. C9 retired “Reservation Lifecycle” → Reserve from Pool — a clean rename (no acronym), and the first to dogfood the new naming grammar (working-ideas/naming.md §1): “Lifecycle” is exactly the banned category/process-shape head, replaced by the verb-led act head “Reserve” with the load-bearing distinguisher “from Pool” as its modifier (the bounded pool is what separates it from its sibling Idempotent Reservation). 5 artifacts git mv‘d to the reserve-from-pool slug; MODULE names matched, checker re-run (correct passes at 21 states, buggy twin — the non-atomic slot-leak — rejected at 5). No identifier purge: unlike C8, nothing was an acronym, so the domain vocabulary (reserve, confirm_reservation, reservation_to_pool, token_results) stays — “reservation” is the honest subject noun, not a dead token, and reserve now even echoes the verb head. 15 C9 self-refs → “this composition”; cross-files (capacity-constraint-enforcement, provisional-commitment, actor-identity, duplicate-prevention, event-log, idempotent-reservation, preference-aware-notification-fanout, README, TAXONOMY) repointed name + links, (C9) glosses collapsed. Roadmap registry keeps its C9 tokens (display name → Reserve from Pool, catalog link repointed); tools/harness/coverage/ and working-ideas/ left per precedent.

Progress 2026-06-25 — C10 done. C10 retired “Stateful Workflow Execution” → Execute Gated Workflow — the second grammar dogfood, and the sharper one. The old name’s head “Execution” was the marginal act-head flagged in the stress cases, and its modifier “Stateful” failed the word-function test (it restates the substrate — the State Machine atom is the stateful part). The spec’s own headline distinguisher is guard evaluation re-converges (the composition evaluates the approval gates the bare atom leaves caller-asserted), so by the “modifier carries the load-bearing distinction” rule the modifier resolves to Gated, not Stateful — giving the verb-led Execute Gated Workflow, which pairs as Gated Workflow vs Compensable Workflow (same head, modifier marking the real difference). 7 artifacts git mv‘d (note the extra -buggy-unaudited twin isolating the audit-binding invariant); 3 MODULE names matched, checker re-run (correct passes at 25 states, both buggy twins rejected — gate-clearance and audit-atomicity each on its own twin). No identifier purge (nothing was an acronym; start_workflow, gate_binding, decide_gate are honest domain vocabulary). 2 C10 self-refs (both parenthetical self-glosses) removed; cross-files (approval-step, state-machine, assignment, permissions, README, compensable-workflow) repointed name + links, (C10) glosses collapsed. Roadmap registry keeps its C10 tokens (display name → Execute Gated Workflow, catalog link repointed); the measurement.md token-cost ledger left untouched as dated history (it carries Stateful Workflow Execution (C10) rows by date, like ai-usage-log). Up next: C11 (Preference-Aware Notification Fanout) — already a clean name; a borderline four-word case (naming.md §4 flags it a watch item, not a correction), so likely a pure number-retirement.

Progress 2026-06-25 — C11 done. C11 was the first pure number-retirement of this run — the name “Preference-Aware Notification Fanout” stays (naming.md §4 watch item, not a correction; nounier than ideal but no better candidate found), so no git mv, no MODULE/title/slug change, no index regen. Just the number: 6 \bC11\b self-refs → “this composition” (one was the “(C11)” roadmap-row self-gloss, collapsed; the Structural-milestone “C11 marker”/”C11 row” rewritten descriptively), and cross-file C11/(C11) → the name in Preference, README, and Propagate Consent Revocation Downstream. The FCn trap bit here for real: the self-file carries 4 Final Critique 11 labels — the then-current FCn form, whose C11 substring sits behind the FC prefix with no \bC11\b boundary — all preserved at the time (finding/round labels, dated history) and since retired under debt #15, so a substring replace would have mangled them; the audit was done on \bC11\b only. Roadmap registry keeps its C11 tokens (name already canonical, slug unchanged — nothing to repoint). Model untouched (no rename), re-verified green for good measure. Up next: C12 (Chain of Custody) — already a clean, strong name (domain term of art; artifact-led head, legitimate per the §1 grammar), so another pure number-retirement.

Progress 2026-06-25 — C12 done. C12 retired as a pure number-retirement — “Chain of Custody” kept (clean domain term of art, artifact-led head, legitimate under §1). No git mv, no MODULE/title/slug change. The MC-Cn-N finding-ID trap was the live hazard here: the self-file’s 56 \bC12\b included 5 occurrences inside a stable MC-Cn-N finding ID (a \bC12\b match sits inside that ID), so a blind \bC12\b swap would have corrupted the token. Handled by protect-replace-restore (mask the finding ID → placeholder, swap the 51 bare self-refs → “this composition”, restore the finding ID); the 5 finding-ID labels were left intact for the C12 pass (dated finding IDs) and later retired wholesale under debt #15. Cross-files (provenance, README, forensic-recovery, immutable-transaction-ledger) collapsed (C12) glosses, bare C12 → Chain of Custody. Roadmap registry keeps its C12 tokens (name canonical, slug unchanged). Model untouched. Up next: C13 (Login) — clean name, pure number-retirement.

Progress 2026-06-25 — C13 done. C13 retired as a pure number-retirement — “Login” kept (clean one-word act head). No git mv/MODULE/title/slug change. Login is heavily cross-referenced by the auth family, so the work was cross-files: collapsed (C13) glosses and the slashed/bare forms (Login/C13, is C13 (Login)) across credential, session, actor-suspension, authenticated-actor, external-onboarding, and privileged-access-provisioning (whose stale Composition-notes link, pointing at ../roadmap.md, was also repointed to ./login.md); the self-file’s one marker reference de-numbered. One dated-Lineage exception left, by design: atoms/session.md Round-1 Pass-1 record quotes the rejected finding “C13/C14 sigil unexplained” verbatim — it’s a historical finding quote (and names C14, not yet processed), so it’s preserved like finding IDs; the eventual no-bare-Cn lint must whitelist dated-Lineage finding text. demos/ and tools/ reference Login by Cn but are excluded (not spec bodies), as in prior passes. Roadmap registry keeps its C13 tokens. Up next: C14 (Session-Gated Authorization) — clean name, pure number-retirement.

Progress 2026-06-25 — C14 done. C14 retired as a pure number-retirement — “Session-Gated Authorization” kept. No git mv/MODULE/title/slug change. Cross-files (credential, session, external-onboarding, login, privileged-access-provisioning): collapsed (C14) glosses and the bare/listed forms; PAP’s stale ../roadmap.md Session-Gated-Authorization link repointed to ./session-gated-authorization.md; self-file marker de-numbered; one Lineage finding-fold note de-numbered (credential.md “(C14 cross-reference linked)” → the name). The atoms/session.md:390 Round-1 quote “C13/C14 sigil unexplained” is left intact (dated finding quote — it carries both C13 and C14, preserved together). demos/, tools/, and dated history excluded. Roadmap registry keeps its C14 tokens. Up next: C15 (Capability-Backed Sharing) — clean name, pure number-retirement.

Progress 2026-06-25 — C15 done. C15 retired as a pure number-retirement — “Capability-Backed Sharing” kept. No git mv/MODULE/title/slug change. Self-file: 80 bare C15 self-refs → “this composition” (no finding-IDs to protect — trap check clean); artifacts and the self-marker de-numbered. Cross-files (capability, README, privileged-access-provisioning): collapsed (C15) glosses and bare forms → Capability-Backed Sharing; PAP’s stale ../roadmap.md link repointed → ./capability-backed-sharing.md. One dated-Lineage exception left: atoms/capability.md Lineage note quotes a dropped stale peer-status marker “C15 partially resolved” verbatim — preserved like finding labels (debt #15 scope), same call as session.md:390. Roadmap registry keeps its C15 tokens. Up next: C16 (External Onboarding) — clean name, pure number-retirement.

Progress 2026-06-25 — C16 done. C16 retired as a pure number-retirement — “External Onboarding” kept. No git mv/MODULE/title/slug change. Self-file (external-onboarding.md): 2 C16 self-refs → “this composition” / de-numbered marker. Cross-files (customer-onboarding, credential, invitation, privileged-access-provisioning): collapsed (C16) glosses and bare/C16-admitted forms → External Onboarding; PAP’s stale ../roadmap.md link repointed → ./external-onboarding.md. One data-contract change, by decision: customer-onboarding.md’s enrollment_path enum value c16 → external-onboarding (5×), since the value named the admission path by C-number — {direct, external-onboarding} now reads semantically (the prose C16-admitted branch → External-Onboarding-admitted branch to match). One dated-Lineage exception left: atoms/credential.md triage note keeps “C16 = External Onboarding are correct” (registry number↔name mapping, same call as its C8 = Customer Onboarding half). Roadmap registry keeps its C16 tokens. Up next: C17 (Authenticated Actor) — clean name, pure number-retirement.

Progress 2026-06-25 — C17 done. C17 retired as a pure number-retirement — “Authenticated Actor” kept. No git mv/MODULE/title/slug change. Self-file (authenticated-actor.md): 3 C17 self-refs → “this composition”. Cross-files (credential, session, README, actor-suspension): collapsed (C17) glosses, possessives (C17's → Authenticated Actor’s), and bare forms → Authenticated Actor. actor-suspension.md (C18) carried the most (9) — handled by ` (C17) → "" then C17’s/C17 → the name, with its own **C18 self-number left intact** (50 occurrences, for the C18 pass). Roadmap registry keeps its C17` tokens. Up next: C18 (Actor Suspension) — clean name, pure number-retirement; then C19 (Compensable Workflow) is the lone remaining rename.

Progress 2026-06-25 — C18 done. C18 retired as a pure number-retirement — “Actor Suspension” kept. No git mv/MODULE/title/slug change. Self-file (actor-suspension.md): 73 bare C18 self-refs → “this composition” (no finding-IDs to protect); artifacts and the one determiner (a C18 defect → a defect of this composition) cleaned. Cross-files (session, README): collapsed (C18) gloss and the bare C18 wires … form → Actor Suspension. Roadmap registry keeps its C18 tokens. Up next: C19 — the last C-number, and the one genuine rename of the back half.

Closeout 2026-06-26 — lint guards landed. The two checks debt #14 named as its closeout are now in tools/linter/lint.py: check L flags any bare composition C-number (C1–C19) in an atom/composition live body (example credential Cn IDs scrubbed; root policy docs that cite Cn as a teaching example are out of scope; Lineage skipped as dated history), and the dangling-link gap is closed by extending check A to resolve .tla/.als/.cfg markdown links, not just .md — which immediately caught a space-mangled compensable-workflow.cfg link left by the C19 rename. Corpus lints clean.

Progress 2026-06-25 — C19 done; debt #14 COMPLETE. C19 retired as a rename plus a domain-term purge: “Saga / Compensable Workflow” → Compensable Workflow (naming.md §4 correction 5 — “Saga” is jargon that must be looked up, and the slash is two names). Per directive the lowercase runtime noun was purged too: 7 artifacts git mv‘d to the compensable-workflow slug; 3 MODULE names matched and the checker re-run (correct passes; both buggy twins rejected — skip-comp → Inv4, double-apply → Inv7); self-file capital Saga self-refs → “this composition”, and ~120 lowercase runtime saga → “compensable workflow” (the cap/lowercase pattern↔instance distinction the spec relied on is preserved, just renamed). Prior-art kept literal: the Garcia-Molina Sagas citation, the io.temporal.workflow.Saga SDK class, and the “Saga Isolation / Semantic Lock” concept all stay “Saga” (external names, not internal jargon; audit-trail.md’s generic “saga compensation” mechanism term likewise). Cross-files (event-log, undo-history) → Compensable Workflow; roadmap registry display name + .md/.tla/twin links updated with C19 tokens kept; atoms/index.md regenerated (slug saga → compensable-workflow). debt #14 is COMPLETE — C1–C19 all retired; no bare Cn composition reference survives in any spec body. The Cn tokens that remain are the deliberately-kept ones: the roadmap registry, dated history (changelog, ai-usage-log, discoveries, open-questions, measurement), finding IDs (MC-Cn-N, FCn, the C13/C14 Pass-1 quote), tools/, working-ideas/, and demos/ — all debt #15’s deferred acronym-sweep scope. The no-bare-Cn lint check named as debt #14’s closeout can now be added and will pass.

15. Tighten the acronym rule to whitelist-only, and sweep out the internal coinage. The policy already exists from the prior language sweep — spec-format.md (every acronym spelled out and defined at first use, all tiers) and pressure-testing.md §Pass 1 (no undefined acronym anywhere — a reference-graph violation) — with a cited-standard whitelist already drafted in working-ideas/naming.md §6 (HIPAA, GDPR, SOX, PCI DSS, CFR, NIST, FHIR, FRCP, TCPA, FDA, AML — external standards, statutes, or regulatory bodies only; a whitelisted initialism may be cited in a spec but never be a pattern name). The gap: the enforced rule is gloss-at-first-use, which still admits the methodology’s own coined shorthand — FCn (Final Critique n), FCn-N, Fn, Cn-N, MC-Cn-N, Cn cluster / Refactor n, and the borderline GRID / EOS / Pass n — a reader gains nothing from “Final Critique 5” even glossed. Two accepted classes only: (a) the cited-standard whitelist above, and (b) a small whitelist of globally-accepted everyday initialisms (API, URL, ID, EU, US, …), each still defined on first use and kept rare-to-none. Everything else — the internal coinage — is marked for removal: spell the concept out or cut it, don’t merely gloss. Mechanism: generalize naming.md §6 into one corpus-wide allowed-acronym whitelist the Pass-1 check enforces (extending the linter’s standards-proper-noun scrub), then sweep the Status/Lineage labels and the few live-body leaks (one fixed in preference-aware-notification-fanout.md, 2026-06-24). This reverses #14’s interim “leave finding IDs” stance — those labels are on the removal list. Best ridden on the touch-trigger re-pass wave. Surfaced 2026-06-24.

Progress 2026-06-26 — spec bodies swept; regression guard landed; broad whitelist enforcement deferred. The internal coinage is out of the specs: FCn → “Final Critique n”, the MC-Cn-N coverage findings → descriptive (“the Invariant-4 coverage-gap finding”), and the finding-ID schemes Cn-N / Rn-Fn / OG-n / S-n / FC-Fn either dropped (the round/pass is already named in each section header) or rewritten to plain English, across all of atoms/ and compositions/ (prose and .tla/.als model comments). The bare composition C-numbers were taken out of the spec bodies too, per a follow-on directive — including the nameless cross-refs (unlike C7's → unlike Resolve a Person's Data Rights'). working-ideas/naming.md gained “Rule zero” (never coin an acronym/sigil; names for humans, IDs for machines; only cited standards + GRID/EOS excepted), and check M in the linter is the high-precision regression guard for the exact coinage shapes (bare S-n excluded — SEC “S-1” collision). Deliberately scoped/deferred: (a) the broad allowed-acronym whitelist enforcement — a general acronym scanner would false-positive every TLA+/GDPR/WASM and fight a prose pass, so the precise sigil guard stands in its place until a curated whitelist is worth building; (b) the internal docs (roadmap registry, working-ideas/, tools/, demos/, dated history) keep their tokens by decision — the C-number is the registry’s stable key, and the conformance tooling consumes Cn codes functionally. The spec layer is the part that had to be clean, and is.

16. Method-takeaway adoptions from the Augment brownfield spec-driven-development guide. Reading Spec-Driven Development for Brownfield Enterprise Codebases (Augment Code, 2026) surfaced three method adoptions and two positioning contrasts — full note and rationale at working-ideas/prior-art-augment-brownfield-sdd.md: (a) the four-element change-level spec (current behavior / target behavior / invariants-in-adjacent-systems / scope boundary) as the per-change delta container for Evergreen Modernization engagements, with the invariants element resolved to named pattern invariants and the pattern’s Generation acceptance queries run as the regression gate — deltas anchored to grounded absolutes rather than prose, and their migration-spec pattern slotting compositions in as the target state; (b) the specced-vs-unspecced defect-density metric for measurement.md once modernization engagements produce the data — no one has published rigorous brownfield before/after numbers, so the first credible dataset wins the citation; (c) never attempt comprehensive system specification on brownfield entry — the entry move is pattern recognition against the bounded atom set (the concept-recovery routing test), stated explicitly so the guide’s correct critique of full-system specs is never mistaken for a critique of this library. The positioning contrasts (drift-rate metric concedes spec-chases-code where conformance inverts the authority; “machine-checkable contract” meaning schema lint where the conformance validator measures implementation behavior) route to the prior-art/positioning staging note, not to canon. Surfaced 2026-07-06.

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 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	State Machine (a declared status lifecycle)
Appointment Slot / Booking / Cancellation / Provider Schedule	reuse	Capacity Constraint Enforcement + Provisional Commitment + Reserve from Pool (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 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 State Machine encounter lifecycle, under Audit Trail.
Patient Encounter — an episode of care: party references (patient, providers) + a 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 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. State Machine is single-dimensional (Harel orthogonal regions unmodelled); resolve whether this is a new atom or a composition of several 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.

Exhibit-sourced candidate — Branching Undo (2026-07-06)

The third engine of the Undoing Undos exhibit (a Jackson-meeting artifact, linked from The Corpus landing): reversal that preserves every timeline — undo then diverge keeps the abandoned branch reachable, so the shape of the past is a tree and the promise is no state is ever lost. Its two siblings are grounded (Undo History, replay-skip; Compensable Workflow, compensating action); this one has not yet faced the routing test or the freestanding gate.

Use-case triage (2026-07-06). The realistic demand clusters in two places, and both are draft-space, not record-space. (a) Scenario modeling — financial planning, budgeting, actuarial and supply-chain what-ifs: fork a baseline, explore variant assumptions, abandon, return, fork again, with abandoned variants reachable for comparison and audit. The wild implements this badly by hand everywhere it is missing (Budget_v3_FINAL_revised2.xlsx is branching undo by filename); the enterprise-shaped witnesses are Salesforce sandboxes and SAP transport variants, the design-shaped ones Figma branching and CAD alternatives, the editor-shaped ones Vim undotree / Emacs undo-tree, with Git’s commit graph as the limiting case. (b) Agent exploration — the fastest-growing witness class: an AI agent that tries, backtracks, and forks working state traverses an undo tree by construction (checkpoint-and-rewind features, per-agent worktrees).

Adversarial pass on the hypothesis (2026-07-06, external model review). Three findings folded. (a) The naming point strengthens the hypothesis: if the concept renames itself the moment it crosses spaces — becoming “versioning” or “scenario management” in draft-space — that is the purpose test firing: undo’s purpose is recover from my own recent action; the tree’s purpose is hold open possibilities. Different purpose, different concept. (b) The acid test — systems where branches are the record — survives, narrowly: Git’s DAG is canonical but its purpose is coordinating divergent work, not undo; blockchain forks are consensus repair; database branching is ephemeral environments that promote or die. The hard case is regulated considered-alternatives (the road not taken retained for audit) — and record-space handles it by recording that the tree existed as ordinary total-ordered entries: record-space can record a tree without being a tree. The tree’s shape becomes data in the record, never the structure of the record. Pressed harder on Git specifically, the acid test resolves rather than survives: Git’s DAG is structurally a union of linear timelines plus lineage metadata (every branch’s first-parent chain is linear — the Scenario Workspace decomposition, implemented); a merge commit is the promote seam (an ordinary append into the receiving timeline’s first-parent order, carrying the second parent as the lineage reference; fast-forward literally collapses); and Git’s own undo surface confirms the taxonomy (reset linear, revert compensating — while checkout -b is not undo but the start of new work). The boundary in one sentence: the tree is the record exactly when the tree is the subject — a version-control system’s domain objects are timelines, so its record-space is about draft-space (the hypothesis operating one level up); this catalog’s domain objects are deeds, and deeds want total order. (c) The composed-alternative reading (“Undo History with multiple pointers”) mechanically collapses: a pointer picks a position in one log, but a branch needs a divergent future — appends after two different cursors — which a single Event Log cannot hold under its own total-order invariant. Followed honestly, the multi-pointer reading decomposes into per-branch log instances plus a lineage index, which is the Scenario Workspace shape. Promote’s minimal interface is deliberately boring: an ordinary append into the target log’s total order carrying a lineage reference — append plus provenance; content-addressable storage is realization, below the contract.

The draft-space hypothesis (route this at triage). Regulated record-space actively wants the opposite — a single authoritative timeline is Event Log’s total-order invariant, which is precisely why the grounded corpus has never needed branching. The tree plausibly lives above the canonical store: scenarios, drafts, explorations — and the chosen branch promotes through the ordinary seam, collapsing the tree to lineage metadata at commit. If the hypothesis holds, the candidate resolves not to a “Branching Undo” atom but to a composition — working name Scenario Workspace: fork / explore / compare / promote over snapshot state, where promote is the boundary that rejoins Event Log and Provenance. This also draws the sibling boundary crisply: Undo History rewinds a timeline, Compensable Workflow reverses effects on one, Scenario Workspace multiplies timelines in draft-space and reconciles to one on commit. (House witness: the derive-expiry sweep of 2026-06-23 — applied, gated, reverted, with the abandoned branch kept reachable as a dated discovery — is this pattern operating on the spec corpus itself.) Pending witnesses plus the gates — recorded here so the exhibit’s third engine points at a registered candidate rather than a dangling claim.

Witness candidate registered (2026-07-11). Grace Desk (working-ideas/grace-desk-brief.md, staging tier) — a shared plan board and triage desk for the library’s own operations: draft-space plan branches operated by the agent fleet over a Shared Todo record-space, promoting through the ordinary seam, with the human adjudicator holding promote. If built, it is the first instance of the agent-exploration witness class this entry names, and a second witness besides — scenario planning over shared tasks. Route per the hypothesis above: witness first; extraction (or routing to reuse) only after witness data exists.

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

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

Summary table

Formal model coverage

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

Exhibit-sourced candidate — Branching Undo (2026-07-06)

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