Provisional Commitment

Atom grounded on Final Critique 4 — 2026-06-18 10 invariants TLA+ model buggy twin ×2 regulated · via 2 composers composed by 2

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

Table of contents

Provisional Commitment

Summary

Provisional Commitment models the everyday business act of “holding” something for someone while they decide whether to go through with it — a credit-card authorization, a hospital bed, an item in a cart, a hotel room, an airline seat. A hold starts when it is placed and stays active for a fixed decision window. It is resolved into one of three recorded end states: Confirmed (the person went through with it), Released (they gave it back), or Expired (the window closed with no decision). The window is a promise in both directions. The system keeps the resource reserved until the window closes. The person must decide before it does, or the hold expires. Resolving exactly once is the core guarantee. After a hold reaches an end state, any further attempt is told it is already resolved. A confirm or release attempted after the window has closed is told the window has elapsed. An expire attempted before the window has closed is told the window has not yet elapsed. Each hold gets a permanent internal identifier. The resource, the requester, and the window are all fixed when the hold is placed and never change. So once a hold settles, it is a clean, unambiguous record of what happened — one an auditor can reconstruct from the records alone. The pattern deliberately leaves out related concepts — making retries safe, keeping a full step-by-step history, and enforcing pool-wide limits like overbooking caps — because each of those is handled by a separate pattern that attaches to this one, which keeps this pattern small and its guarantees clear.

Also known as: a hold, a reservation, a tentative reservation, a two-phase reservation.

Intent

A requester needs a resource whose grant is not yet certain. The system promises to hold the resource for the requester for a known period, during which the requester decides whether to confirm (taking the resource into a binding allocation) or release (returning it to availability). If the requester does neither before the period elapses, the hold expires: the resource returns to availability and the Commitment moves to a terminal Expired state recorded by an Expire event (fired by a scheduler/sweep at the deadline or lazily on the next access). Expiry is a real transition with a side effect — returning the resource (and, in a pool-backed composition, a capacity slot) to availability — which is why it is an explicit recorded event rather than a status inferred at read time.

The pattern addresses a class of needs that recur across virtually every regulated industry: credit-limit holds at banks (pending settlement), bed assignments at hospitals (pending admission), inventory reservations at retailers (pending checkout), room bookings at hotels (pending check-in), seat holds at airlines (pending purchase). The shape is constant — a resource is encumbered for a bounded window, the encumbrance resolves into commitment or release (or its window lapses), and the audit record of the encumbrance is itself a regulated asset.

This is a freestanding atom (can be specified without naming any other pattern) in the EOS (Essence of Software — Daniel Jackson’s framework for specifying software concepts as freestanding, composable units) sense. It has its own state (the Commitment record and its resolution), its own actions (Place Hold, Confirm, Release, Expire), and its own operational principles (single-resolution, the honored-window guard, and the three terminal transitions are absorbing). It does not implement idempotency (submitting the same operation twice produces the same result as once) under retry, the full audit trail of every observation, or aggregate capacity constraints over a resource pool. Each is a separate composable atom; see Composition notes.

Structure

Identity model

Every Commitment known to the system has an Id — an opaque, immutable, assigned on Place Hold from injected id material at the seam. The id is the Commitment’s identity; the Resource binding, Requester, and hold window are immutable properties of the Commitment, not its identity.

Two commitments for the same Resource have different ids — sequential or concurrent commitments are distinct, even when they share a Resource or a Requester. Ids are not reused after a Commitment is resolved (Confirmed, Released, or Expired).

The opaque-id model is load-bearing. Identifying a Commitment by its (resource, requester) pair would muddle re-holds — a requester re-holding the same resource after an earlier release is a different Commitment with its own audit trail. Identifying by hold timestamp would lose precision under concurrent commitments. Opaque ids preserve the one-commitment-one-id discipline that makes per-event audit reconstruction tractable, which is the regulatory expectation in every domain this atom covers.

Inputs

A Resource reference identifying what is being held. The atom treats this as opaque — the implementation defines the resource registry and what availability means.
A Requester reference identifying who the hold is for.
A hold window Duration, supplied at creation. The window opens at Placed At and closes at Expires At = Placed At + Duration.
User- or system-initiated actions. Every action consumes the current clock reading Now as a pipeline-implicit input (the pipeline’s clock_t, supplied at the I/O seam — not read inside the transition, not trusted from the caller, and not shown as a signature parameter). Now is consumed for two clearly separated purposes: stamping immutable timestamps on a transition (execution time), and evaluating the pure honored-window guard. See the Logic-confinement note in Decision points.
- Place Hold — record a new Commitment held for a Requester. (Projected contract: place_hold(resource, requester, duration) → id | rejected(invalid-request | resource-unavailable | storage-failure).)
- Confirm — take a held Commitment into a binding allocation. (Projected contract: confirm(id) → ok | rejected(not-known | not-held | window-elapsed | storage-failure).)
- Release — return a held Commitment’s resource to availability. (Projected contract: release(id) → ok | rejected(not-known | not-held | window-elapsed | storage-failure).)
- Expire — move a lapsed held Commitment to its terminal Expired state and return the resource. (Projected contract: expire(id) → ok | rejected(not-known | not-held | window-not-elapsed | storage-failure).)
Not Held names a terminal Commitment — already Confirmed, Released, or Expired. Window Elapsed is the distinct rejection when Confirm/Release is attempted on a still-Held past the window; Window Not Elapsed is the symmetric rejection when Expire is attempted before the window has closed.
Id material (the source of opaque, unique commitment identifiers) is likewise injected at the seam and not generated internally.

Outputs

The current set of Held commitments.
The current set of Confirmed, Released, and Expired commitments (the three terminal states).
For each Commitment: Id, Resource, Requester, Placed At, Expires At, the state (Held, Confirmed, Released, or Expired), and the timestamp of the most recent transition.
Action acknowledgements — success (returning id for Place Hold, ok otherwise) or rejection with a named reason.

State

Each Commitment carries a state field. The state machine has one non-terminal state and three terminal states:

Held — the resource is encumbered for the requester; the window is open; no resolution has occurred. The only non-terminal state.
Confirmed — the requester confirmed within the window; the resource is taken into a binding allocation. Terminal.
Released — the requester (or a system acting on their behalf) released within the window; the resource returns to availability. Terminal.
Expired — the window lapsed (Now ≥ Expires At) with the Commitment still Held, and an Expire event then fired (by a scheduler/sweep or lazily on access), moving it to this terminal state and returning the resource to availability. Terminal.

There is no Unheld state in the system’s record. Unheld describes the period before Place Hold is called and after a commitment’s effect on the resource has concluded — it is a property of the resource, not of the Commitment. The commitment lifecycle proceeds: Unheld → (Place Hold) → Held → one of {Confirmed, Released, Expired}. All three terminal states are absorbing.

Each Commitment carries:

Id — opaque, immutable, assigned on Place Hold from injected id material at the seam. Never changes.
Resource — the resource reference. Set on Place Hold. Never changes.
Requester — the requester reference. Set on Place Hold. Never changes.
Placed At — set on Place Hold from the implicit Now. Never changes.
Expires At — set on Place Hold as Placed At + Duration. Immutable. Never changes.
state — Held Confirmed Released Expired. Set to Held on Place Hold; immutable once it reaches a terminal.
Confirmed At — set on Confirm, present only in Confirmed. Immutable once set.
Released At — set on Release, present only in Released. Immutable once set.
Expired At — set on Expire, present only in Expired. Immutable once set. (Expires At ≤ Expired At: the expire event fires only once the window has closed.)

Transitions — every transition below stamps its timestamp from the pipeline-implicit Now, and no transition reads the clock internally:

action	from	to	window guard	stamps	result	rejections
Place Hold	Unheld (no record)	Held	—	fresh Id; Placed At = Now; Expires At = Now + Duration	the new `id`	Invalid Request; Resource Unavailable; Storage Failure
Confirm	Held	Confirmed	Now < Expires At	Confirmed At = Now	`ok`	Not Known; Not Held; Window Elapsed; Storage Failure
Release	Held	Released	Now < Expires At	Released At = Now	`ok`	Not Known; Not Held; Window Elapsed; Storage Failure
Expire	Held	Expired	Now ≥ Expires At	Expired At = Now; resource returns to availability	`ok`	Not Known; Not Held; Window Not Elapsed; Storage Failure

Four semantics the cells cannot hold:

The window boundary is exact, and a failed guard writes nothing. Confirm and Release are legal strictly while Now < Expires At; Expire is legal only once Now ≥ Expires At. The boundary at Now = Expires At is the single point where the clock decides which transition may fire — resolution below it, expiry at or above it. When the guard fails, the record is left Held and nothing is written: a late Confirm/Release is rejected Window Elapsed, a premature Expire is rejected Window Not Elapsed. The atom never records a resolution after the window closes, nor an expiry before it.
Expiry may fire eagerly or lazily. The Expire event may be fired eagerly by a scheduler/sweep at the deadline, or lazily on the next access to a lapsed hold — a deployment-shaped choice (see Behavior and Edge cases). Either way the resource (and, in a pool-backed composition, a capacity slot) returns to availability, which is why the lapse is a written transition and not a read-time inference.
The three terminal states are absorbing. There are no transitions out of Confirmed, Released, or Expired; the atom has no unconfirm, un-release, or reactivate surface. A resolving action on an already-terminal Commitment is rejected Not Held (Invariant 3).
Rejection priority is fixed. For each resolving action the order is Not Known → Not Held → the window guard (Window Elapsed for Confirm/Release, Window Not Elapsed for Expire) → Storage Failure; for Place Hold it is Invalid Request → Resource Unavailable → Storage Failure. The full per-action preconditions are in Decision points.

Flow

Place hold. The requester signals intent to use the resource without binding. The system records the Commitment in Held with a fresh id, Placed At, and Expires At. Returns the id. (Start.)
Wait. While the Commitment is in Held and Now < Expires At, the resource is encumbered for the requester.
Resolve, or expire. While Now < Expires At, exactly one of two resolving transitions may occur: Confirm (Held → Confirmed) or Release (Held → Released). If neither fires before the window closes, the Commitment expires: once Now ≥ Expires At, an Expire event (Held → Expired) returns the resource to availability and records Expired At. A Confirm/Release attempted after the window is rejected Window Elapsed; an Expire attempted before the window is rejected Window Not Elapsed.
Settled. The Commitment is in one of three terminal states (Confirmed, Released, or Expired). Its record persists for audit. (End.)

Decision points

Each action carries explicit preconditions. Violations are rejected, not silently absorbed.

Logic confinement (clock and id). The clock and the id are pipeline-implicit, supplied at the I/O seam (Step 3 of the execution contract), never produced inside a transition and not shown as action signature parameters. Now (clock_t) is read once by the pipeline at the seam and consumed by the action; the Id is assigned from injected id_t id material at the seam, not generated internally (per the Logic Confinement Principle, see execution-contract.md). A guard’s window test is a pure function of the record and the implicit Now — state = Held ∧ Now < Expires At for Confirm/Release, and state = Held ∧ Now ≥ Expires At for Expire. The clock is consumed by (a) those pure guards and (b) the immutable timestamp stamps inside a committed transition (Placed At, Confirmed At, Released At, Expired At), each set from the same implicit Now. Each transition is thereby a pure function of its record state, inputs, Now, and id material, with both sources auditable at the deployment layer. Rejection priority for each action: Not Known → Not Held → window guard (Window Elapsed for Confirm/Release, Window Not Elapsed for Expire) → Storage Failure.

At Place Hold — Resource, Requester, and Duration must be well-formed; otherwise Invalid Request. Duration must be positive and within implementation bounds; otherwise Invalid Request. The resource must be available for holding under the registry’s availability rules; otherwise Resource Unavailable. Placed At = Now and Expires At = Now + Duration are computed once from the implicit Now and stored immutably. If the store write fails, the atom returns Storage Failure; no Commitment is created.
At Confirm — Id must reference a known Commitment; otherwise Not Known. The referenced Commitment must have state = Held; otherwise Not Held (it is already a terminal — Confirmed, Released, or Expired). Window guard: if Now ≥ Expires At — a lapsed, still-Held — confirmation is rejected as Window Elapsed; the record is left Held and nothing is written. The atom never writes a resolution after the window closes. If the store write fails, the atom returns Storage Failure; the Commitment remains in Held.
At Release — Id must reference a known Commitment; otherwise Not Known. The referenced Commitment must have state = Held; otherwise Not Held. Window guard: if Now ≥ Expires At, release is rejected as Window Elapsed; the record is left Held and nothing is written. (A caller wishing to return a resource before its window closes calls Release while Now < Expires At; after the window closes the Commitment is Expired instead, which also frees the resource.) If the store write fails, the atom returns Storage Failure; the Commitment remains in Held.
At Expire — Id must reference a known Commitment; otherwise Not Known. The referenced Commitment must have state = Held; otherwise Not Held. Window guard: if Now < Expires At, expiry is rejected as Window Not Elapsed; the record is left Held and nothing is written. The atom never expires a Commitment before its window closes. If the store write fails, the atom returns Storage Failure; the Commitment remains in Held.

Behavior

Observed behavior, derived from how regulated systems use provisional commitments:

Single-resolution is the atom’s central guarantee. Each resolving transition — Confirm, Release, Expire — checks the state as its first operation. If the state is already a terminal (Confirmed, Released, or Expired), the action returns Not Held without modifying any record. The check-and-commit from Held to a terminal must be atomic: under concurrent resolving transitions, exactly one commits and the rest see Not Held. An implementation that writes two terminal states for one Commitment has violated the atom’s core contract.
A hold is not a promise of confirmation. The requester is free to release at any time before the window elapses; release is a normal audited outcome, not a failure mode.
The hold window is a contract with two faces: a commitment to the requester (the resource is theirs to confirm within the window) and a constraint on the requester (decide within the window or the hold expires). Both faces are load-bearing — auditors check both.
Expiry may be eager or lazy, but it is always a recorded transition with a side effect. When Now ≥ Expires At, an Expire event moves a still-Held to Expired and returns the resource to availability. A deployment may fire it eagerly — a scheduler/sweep that calls Expire at (or shortly after) Expires At — or lazily — Expire fired on the next access to a lapsed hold. The eager-vs-lazy choice has audit implications: under lazy expiry a lapsed-but-not-yet-expired Commitment is still Held until something touches it, so the resource is reclaimed at sweep/access time rather than precisely at Expires At. The side effect — returning the resource (and, in a pool-backed composition, a capacity slot) to availability — is why expiry is an explicit event rather than a read-time inference: a side-effect-free lapse could be derived, but this lapse releases a resource and so needs a write. A Confirm/Release attempted on a lapsed hold is rejected Window Elapsed before any expire fires; an Expire attempted before the window closes is rejected Window Not Elapsed.
Concurrent Place Hold calls for the same resource resolve serially under the host environment’s serialization guarantees. Whichever call wins the race produces a Held; the loser receives Resource Unavailable.
The Commitment record persists in its terminal state indefinitely from the atom’s perspective. Retention, archival, and purge (permanent, unrecoverable removal from storage) are composing concepts; the regulated-deployment composition is with Retention Window.
Audit trails read the Commitment record directly. Every transition has a timestamp; every Commitment names a Requester and a Resource. This is the minimum surface a regulator expects.
Now and the id material are pipeline-implicit at the deployment seam, not signature parameters. Every action consumes Now (the pipeline’s clock_t) supplied at the I/O seam, and Place Hold’s id material is supplied by the deployment’s source at the seam — per the Logic Confinement Principle (see execution-contract.md), the core transition neither reads a wall clock nor generates an id internally. Now is consumed only by (a) the pure window guards and (b) the immutable timestamp stamps inside committed transitions (Placed At, Confirmed At, Released At, Expired At), so each transition is a pure function of its record state, inputs, Now, and id material, with both sources auditable at the deployment layer.

Feedback

Each successful action produces an observable, measurable change:

After Place Hold — a new Commitment appears in Held with a fresh Id, Placed At, Expires At. Held count and total count each increase by one. The id is returned to the caller.
After Confirm — the Commitment moves Held → Confirmed with Confirmed At. Held count decreases by one; Confirmed count increases by one; total count unchanged.
After Release — the Commitment moves Held → Released with Released At. Held count decreases by one; Released count increases by one; total count unchanged.
After Expire — the Commitment moves Held → Expired with Expired At; the resource returns to availability. Held count decreases by one; Expired count increases by one; total count unchanged.

Each rejected action produces an observable refusal naming the failed precondition: Invalid Request, Resource Unavailable, Not Held, Not Known, Window Elapsed, Window Not Elapsed, or Storage Failure.

The Held, Confirmed, Released, and Expired sets are queryable — operators can list, filter, and count them at any time. Per-commitment fields are observable to operators and (where appropriate) to requesters.

Invariants

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

Invariant 1 — Membership exclusivity. For every Commitment c known to the system, c is in exactly one of {Held, Confirmed, Released, Expired}, never in two states, never in none.
Invariant 2 — Single-resolution. A Commitment reaches at most one terminal state — Confirmed, Released, or Expired — and no further transition is permitted after that. Any resolving action (Confirm, Release, Expire) called on an already-terminal Commitment returns Not Held. The check-and-commit from Held to a terminal must be atomic, so that under concurrent resolution attempts exactly one commits.
Invariant 3 — Terminal absorption. Once a Commitment enters Confirmed, Released, or Expired, no action transitions it elsewhere. The atom has no unconfirm, un-release, or reactivate surface.
Invariant 4 — Id stability. A Commitment’s Id is set on Place Hold and never changes.
Invariant 5 — Resource and requester immutability. A Commitment’s Resource and Requester are set on Place Hold and never change. Re-holding the same resource for the same requester produces a new Commitment with a new id.
Invariant 6 — Hold window monotonicity. For every Commitment, Placed At < Expires At. The Duration supplied to Place Hold is positive.
Invariant 7 — Confirmation within the window. A Commitment can transition to Confirmed (or Released) only while Now < Expires At. After the window elapses, confirmation and release are rejected Window Elapsed; the only legal terminal transition from Held is Expire (guarded Now ≥ Expires At). This is what guarantees no resolution is ever recorded after the declared window closes, and no expiry before it.
Invariant 8 — Transition timestamps strictly after placement. For any Commitment: if Confirmed At is defined, Placed At ≤ Confirmed At; if Released At is defined, Placed At ≤ Released At; if Expired At is defined, Expires At ≤ Expired At (expiry cannot run before its scheduled time).
Invariant 9 — No id reuse. No two distinct commitments share an Id, across the lifetime of the system.
Invariant 10 — Commitment store durability. Once recorded, a Commitment is never deleted from the store. Confirm, Release, and Expire transition a Commitment to a terminal state; they do not remove the record. The total commitment count is monotonically non-decreasing. Retention, archival, and purge are composing concepts (Retention Window).

Membership exclusivity, single-resolution, and terminal absorption together give the audit-friendly property — once a Commitment settles, its record is a fact about the past, not a candidate for revision. Confirmation within the window (Invariant 7) gives the honored-window property — auditors can verify, structurally, that no Commitment was confirmed or released after its declared window, and none expired before it. Resource and requester immutability gives the one-commitment-one-id property that makes per-event audit reconstruction tractable. Commitment store durability gives the irrevocable-record property — the audit surface cannot be silently reduced by deletion.

Examples

The same atom, five regulated domains, identical mechanic.

Banking — credit-limit hold

A merchant submits a $250 authorization against a customer’s card. The bank calls place_hold(card_resource, cardholder, 7-days) → id = auth_c41 (placed_at = now, expires_at = now + 7 days per scheme rules). The cardholder’s available credit drops by $250. Three days later the merchant captures the authorization — confirm(auth_c41); the window is still open (now < expires_at), so the $250 becomes a settled charge. Alternatively the merchant voids the authorization within seven days — release(auth_c41); available credit restores. If the merchant does neither, on the eighth day the authorization expires — expire(auth_c41) (fired by the scheme’s settlement sweep once now ≥ expires_at); the $250 hold is dropped and available credit restores; any late confirm(auth_c41) is rejected window-elapsed. Each transition is recorded for liquidity reporting under the bank’s BCBS-aligned (Basel Committee on Banking Supervision — the international body that sets bank-capital and liquidity standards) framework.

Healthcare — bed assignment

The emergency department requests a bed for a patient awaiting admission. The bed-management system calls place_hold(bed_resource, patient, 2-hours) → id = bed_h17 (placed_at = 14:00, expires_at = 16:00). The bed shows as encumbered on the unit dashboard. At 14:45 the patient arrives on the unit — confirm(bed_h17); now < expires_at, so the bed becomes officially assigned. Alternatively the patient is discharged from the ED instead — release(bed_h17); the bed returns to available. If neither happens by 16:00, the bed-management system’s sweep fires expire(bed_h17) (now ≥ expires_at); the hold moves to Expired and the bed returns to the available pool. The Joint-Commission-aligned care-coordination audit reads the commitment record directly.

Retail — inventory reservation

A shopper adds a $1,200 laptop to their cart at an online retailer with inventory of one unit. The order-management system calls place_hold(sku_resource, shopper, 15-minutes) → id = inv_r93 (placed_at = 19:14, expires_at = 19:29). The product page shows one in stock, reserved to other shoppers. At 19:18 the shopper completes checkout — confirm(inv_r93); the unit transfers to the order. Alternatively the shopper empties their cart — release(inv_r93); the unit returns. If the shopper abandons the cart silently, the cart sweep fires expire(inv_r93) from 19:29 (now ≥ expires_at); the hold moves to Expired, the unit is returned to available stock for other shoppers, and a late confirm(inv_r93) is rejected window-elapsed.

Hospitality — room booking

A guest reserves a hotel room with a guaranteed-by-credit-card hold for two nights, check-in tomorrow. The property-management system calls place_hold(room_resource, guest, duration) → id = rm_b58 (placed_at = today 11:00, expires_at = tomorrow 18:00 — the property’s standard cancellation cutoff). The room is unavailable to other reservations. The guest checks in at 17:30 tomorrow — confirm(rm_b58); now < expires_at, so the booking becomes a stay. Alternatively the guest cancels by 18:00 tomorrow — release(rm_b58); the room reopens. If neither happens, the property’s sweep fires expire(rm_b58) from tomorrow 18:00 (now ≥ expires_at); the hold moves to Expired, the room reopens, and the property’s no-show fee policy (a separate composing pattern, triggered off the Expired transition) takes effect.

Airline — seat hold

A passenger selects a fare and a seat during booking. The reservation system calls place_hold(seat_resource, passenger, 15-minutes) → id = seat_a22 (placed_at = 09:33, expires_at = 09:48 — the carrier’s standard 15-minute fare-lock per IATA (International Air Transport Association — the airline industry’s global trade body) practice). The seat is unavailable to other booking sessions. The passenger pays at 09:40 — confirm(seat_a22); the seat is ticketed. Alternatively the passenger backs out — release(seat_a22); the seat returns. If the passenger abandons the booking flow, the fare-lock sweep fires expire(seat_a22) from 09:48 (now ≥ expires_at); the hold moves to Expired and the seat returns to availability for other sessions. The attached fare quote is invalidated whenever the hold leaves availability — on a Released or an Expired transition the composing layer observes the terminal state (a composing Fare Quote atom; out of scope here).

The mechanic is identical across all five. What differs: resource semantics, hold-window duration, the regulatory framing of the audit trail, and the composing atoms that handle fare locks, capacity caps, no-show fees, payment idempotency, and the like. In every case the expiry of an undecided hold is a recorded expire transition that returns the resource to availability.

Regulated adversarial scenarios

Three scenarios the atom must survive in regulated contexts, beyond happy-path and rejection-path:

Regulator audit. An auditor asks “show me every credit-limit hold that was confirmed (or released) after its declared window.” The query reads the commitment records, filters where Confirmed At (or Released At) is defined and exceeds Expires At, and returns the empty set. Invariant 7 (confirmation within the window) guarantees this structurally — the Window Elapsed rejection at the Confirm/Release actions makes a post-window resolution impossible to record, and the symmetric Window Not Elapsed guard on Expire makes a premature expiry impossible. The auditor sees a structural guarantee, not a procedural promise.
Data subject request. A customer invokes their GDPR (EU General Data Protection Regulation — the European Union’s data-privacy law) right to erasure on personal data referenced by Requester. The atom on its own cannot satisfy erasure while preserving the structural audit trail — that tension is the same one Event Log names under right-to-be-forgotten. Composing with a Cryptographic Shredding or Erasure Tombstone pattern alongside legal counsel redacts the personal-data field while keeping Id, Placed At, Expires At, state, and transition timestamps intact. The lifecycle — including the Expire transition — remains auditable; the personal data does not persist.
Breach investigation. An incident responder needs the universe of resources committed during a window of suspected unauthorized access — say, 02:00–04:00 UTC (Coordinated Universal Time — the global time standard) on a given date. Each Commitment carries Placed At; the query reads the commitment record set and returns the matching set directly, with no log replay required. For each, the responder reads the terminal state and its timestamp to see which holds were resolved (Confirmed/Released) versus which expired. The Event Log composition adds the per-transition timeline needed to determine the exact ordering of the resolutions during the same window.

These scenarios exercise the atom against the questions regulators actually ask. Happy-path and rejection-path examples cover what users do; adversarial scenarios cover what auditors, data subjects, and investigators do.

Edge cases and explicit non-goals

What this atom does not cover:

Idempotency under retry. If a requester invokes Place Hold twice for the same logical intent (network retry, double-click), the atom on its own produces two commitments. Idempotent reservation composes with Duplicate Prevention, keyed on an idempotency token (a client-supplied token that makes repeated submissions safe) supplied by the requester. See Composition notes.
Full audit trail of state transitions. The Commitment record carries one timestamp per terminal transition (Confirmed At, Released At, or Expired At), sufficient for terminal-state audit. Reconstructing the full sequence of observations — every read, every retry, every observer — requires composing with Event Log. The commitment record is the projection; the Event Log is the journal.
Aggregate capacity constraints. Rules like no more than 110 concurrent holds against a 100-seat aircraft (overbooking limits, fractional reserves, inventory pool caps) belong to a separate Capacity Constraint Enforcement atom — forthcoming. The bare Provisional Commitment atom holds one resource per Commitment and does not opine on pool-level rules.
Partial release. A Commitment is for one resource and resolves in full. Holding ten units and releasing three is two operations against two commitments at the registry’s grain, not a partial transition of one Commitment.
Renewal or extension of the hold window. The atom forbids changing Expires At after placement (Invariant 6). Patterns that need a longer hold must place a new Commitment (a still-Held, not-yet-expired original may be Released first), producing a fresh id and a new audit entry. Mutating Expires At would silently break the honored-window property — and would retroactively change when Expire becomes legal.
Retroactive cancellation of a Confirmed commitment. Once Confirmed, the atom has no unconfirm action — terminal absorption is invariant. Refund, admission reversal, return-to-stock, and similar effects compose this atom with a separate Reversal pattern that produces a new compensating commitment, not a state change on the original.
Resource availability semantics. The atom rejects Place Hold with Resource Unavailable if the registry says the resource is not hold-able, but does not define hold-able. The registry — a separate concept — owns that decision (another active hold, a maintenance lock, an out-of-stock signal, an account-level freeze).
Concurrency and atomicity. State transitions are atomic. A crash mid-transition that leaves a Commitment in neither Held nor a terminal state violates membership exclusivity; the implementor owns the transactional boundary. Multi-commitment transactions belong to a Transaction pattern.
Clock semantics and the implicit clock. Wall-time is accessed at the deployment seam — Now (the pipeline’s clock_t) is supplied to each action by the pipeline rather than read from an internal clock, and the same implicit Now drives the pure window guards. The timestamps Placed At, Confirmed At, Released At, and Expired At are stamped from that implicit Now, never read inside a transition. Skew between the implicit Now and the underlying wall source, monotonicity, and timezone handling are handled at the deployment layer (clock quality is a deployment-layer decision, not part of this atom’s contract); a composed Event Log’s sequence_number is the authoritative order when transitions race. The window’s correctness is best-effort under an adversarial clock; the action-vs-clock boundary at Now = Expires At — confirm/release legal strictly below it, expire legal at or above it — is the one place execution-time clock reads gate which transition may fire.
Eager vs. lazy expiry policy. The atom requires Expire to be invoked to move a lapsed hold to Expired, but does not mandate when. Eager expiry (scheduled sweeps firing at Expires At) produces no observable Held-past-Expires At lag and satisfies strict audit, and reclaims the resource (and any composed pool slot) promptly; lazy expiry (at next observation) is cheaper but lets a Commitment linger in Held past its window in records that have not been read, holding the resource until something touches it. Both are valid; the choice is deployment-shaped with different audit and resource-reclamation implications. (Because the lapse has a side effect — returning the resource to availability — it is a written transition either way, not a read-time derivation.)
The business meaning of confirmation. The atom treats Confirm as a request from the requester (or a system acting on their behalf) and accepts it under preconditions. Confirmation meaning funds settled, patient admitted, item shipped, guest arrived, ticket issued, is host-system policy — not part of this atom. A confirmation later judged premature is the host’s problem to compensate.
Non-repudiation. The atom names a Requester reference on each Commitment but does not require cryptographic, procedural, or authentication-context binding of the action to the named requester. An adversary with write access to the commitment record could place or confirm a Commitment that the named requester did not authorize, and nothing in the atom’s surface would surface the discrepancy. Verifiable attribution — signed authorization, MFA-bound (Multi-Factor Authentication — requiring two or more independent proofs of identity) caller context, witnessed approval — belongs to an Actor Identity composition. See Composition notes.

Where the atom breaks down: when the resource is fungible at a finer grain than per-commitment (a block of 100 seats sold to a travel agent who sub-allocates to passengers — a multi-tier composition, not one commitment); when the hold window must be paused (medical urgency suspending elective procedure holds — a Pause/Resume pattern); when the resource registry cannot supply atomic, serialized place-hold semantics.

Terms

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

Commitment

The record this atom defines: a single resource held for a single requester for a bounded window, then resolved to exactly one terminal state. It carries its Id, Resource, Requester, Placed At, Expires At, the state field below, and a transition timestamp (Confirmed At, Released At, or Expired At); the Id, Resource, Requester, and hold window are immutable from creation. Its state field holds one of Held, Confirmed, Released, or Expired.

Kind: Type Projects: state

Place Hold

The behavior that records a new Commitment. It assigns a fresh Id from injected id material at the seam, sets Resource, Requester, Placed At = Now, and Expires At = Now + Duration, enters the Commitment in Held, and returns the Id (or a rejection naming the failed precondition).

Kind: Operation

Confirm

The resolving behavior that takes a Held into a binding allocation. Permitted only while state = Held and Now < Expires At; it moves the Commitment → Confirmed and stamps Confirmed At. After the window closes it is rejected Window Elapsed; on an already-terminal Commitment it is rejected Not Held.

Kind: Operation

Release

The resolving behavior that returns a Held’s resource to availability before the window closes. Permitted only while state = Held and Now < Expires At; it moves the Commitment → Released and stamps Released At. After the window closes it is rejected Window Elapsed; on an already-terminal Commitment it is rejected Not Held.

Kind: Operation

Expire

The resolving behavior — the side-effecting lapse event — that moves a lapsed Held to Expired and returns its resource (and, in a pool-backed composition, a capacity slot) to availability. Permitted only while state = Held and Now ≥ Expires At; it stamps Expired At. Before the window closes it is rejected Window Not Elapsed. May be fired eagerly by a scheduler/sweep or lazily on the next access.

Kind: Operation

Id

The opaque, immutable identity of a Commitment, assigned on Place Hold from injected id material at the seam and never reused. The Resource, Requester, and hold window are properties of the Commitment, not its identity.

Kind: Field Field of: Commitment Projects: id

Resource

The reference identifying what is being held. The atom treats it as opaque — the implementation defines the resource registry and what availability means. Set on Place Hold, immutable thereafter.

Kind: Field Field of: Commitment Projects: resource

Requester

The reference identifying who the hold is for. Set on Place Hold, immutable thereafter. The atom names the Requester but does not by itself bind the action to a verifiable actor — that is an Actor Identity composition.

Kind: Field Field of: Commitment Projects: requester

Placed At

The wall-time the Commitment was placed, stamped from the implicit Now on Place Hold. Immutable thereafter. The window opens here; Placed At < Expires At always holds.

Kind: Field Field of: Commitment Projects: placed_at

Expires At

The wall-time the hold window closes, set on Place Hold as Placed At + Duration. Immutable thereafter. It is the boundary the window guards read: Confirm/Release are legal while Now < Expires At, Expire once Now ≥ Expires At.

Kind: Field Field of: Commitment Projects: expires_at

Confirmed At

The wall-time the Commitment was confirmed, stamped from Now on Confirm. Present only in Confirmed; immutable once set. Placed At ≤ Confirmed At always holds.

Kind: Field Field of: Commitment Projects: confirmed_at

Released At

The wall-time the Commitment was released, stamped from Now on Release. Present only in Released; immutable once set. Placed At ≤ Released At always holds.

Kind: Field Field of: Commitment Projects: released_at

Expired At

The wall-time the Commitment expired, stamped from Now on Expire. Present only in Expired; immutable once set. Expires At ≤ Expired At always holds — expiry cannot run before its scheduled time.

Kind: Field Field of: Commitment Projects: expired_at

Duration

The hold window length supplied to Place Hold. It sizes the window — Expires At = Placed At + Duration — but is not stored on the Commitment under its own name; the immutable Placed At and Expires At are what persist. It must be positive and within implementation bounds.

Kind: Parameter Parameter of: Place Hold Projects: duration

Now

The current clock reading every action consumes — the pipeline’s clock_t, supplied at the I/O seam, never read inside the transition and never a signature parameter. It is consumed by (a) the pure window guards and (b) the immutable timestamp stamps inside committed transitions (Placed At, Confirmed At, Released At, Expired At).

Kind: Parameter Parameter of: Place Hold Projects: now

Held

The single non-terminal state: the resource is encumbered for the requester, the window is open, and no resolution has occurred. The lifecycle proceeds Held → one of {Confirmed, Released, Expired}.

Kind: Member Member of: the commitment state Role: Outcome

Confirmed

The terminal state a Commitment reaches when the requester confirmed within the window — the resource is taken into a binding allocation. Absorbing: no action transitions it elsewhere.

Kind: Member Member of: the commitment state Role: Outcome

Released

The terminal state a Commitment reaches when it was released within the window — the resource returns to availability. Absorbing: no action transitions it elsewhere.

Kind: Member Member of: the commitment state Role: Outcome

Expired

The terminal state a Commitment reaches when the window lapsed with the Commitment still Held and an Expire event then fired — the resource returns to availability. Absorbing: no action transitions it elsewhere.

Kind: Member Member of: the commitment state Role: Outcome

Invalid Request

The refusal Place Hold returns when Resource, Requester, or Duration is not well-formed, or Duration is not positive or out of bounds. A guard rejection that fails before any store write; no Commitment is created.

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

Resource Unavailable

The refusal Place Hold returns when the registry says the resource is not hold-able under its availability rules. The loser of a concurrent place-hold race for the same resource also receives this. No Commitment is created.

Kind: Member Member of: the Place Hold rejection Role: Outcome Projects: resource-unavailable

Not Known

The refusal Confirm, Release, or Expire returns when the supplied Id references no known Commitment. A lookup miss, distinct from a state or window rejection.

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

Not Held

The refusal Confirm, Release, or Expire returns when the referenced Commitment is already terminal — Confirmed, Released, or Expired. This is the single-resolution guard: a resolving action on an already-resolved Commitment is refused without modifying any record.

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

Window Elapsed

The refusal Confirm or Release returns when Now ≥ Expires At — the still-Held’s window has closed. The record is left Held and nothing is written; the atom never records a resolution after the window closes.

Kind: Member Member of: the resolving-action rejection Role: Outcome Projects: window-elapsed

Window Not Elapsed

The refusal Expire returns when Now < Expires At — the window has not yet closed. The symmetric counterpart to Window Elapsed: the record is left Held and nothing is written; the atom never expires a Commitment before its window closes.

Kind: Member Member of: the Expire rejection Role: Outcome Projects: window-not-elapsed

Storage Failure

The refusal any action returns when the store write fails after the preconditions pass. No Commitment is created (for Place Hold) or the Commitment remains in Held (for the resolving actions); the caller must treat it as definitive.

Kind: Member Member of: the action rejection Role: Outcome Projects: storage-failure

Composition notes

Provisional Commitment is freestanding and is designed to compose with other atoms rather than absorb their concepts:

Duplicate Prevention — for idempotent reservation. The container calls check(idempotency_token) before Place Hold and record(idempotency_token) after a successful Place Hold, mapping the resulting commitment Id to the token. A retry with the same token returns the previously-produced Id rather than creating a second Commitment. Window duration is the implementation’s choice; typical values match the underlying network retry envelope (minutes). This composition is realized as the Idempotent Reservation composition.
Event Log — for the audit-able commitment history. The container appends an event to a log instance on every successful state-changing action (Place Hold, Confirm, Release, Expire), preserving the state-transition sequence for compliance. The commitment record remains the current-state projection; the Event Log is the journal from which the transitions can be replayed and audited.
Retention Window — places terminal-state commitments (Confirmed, Released, Expired) under retention per the host’s regulatory regime. The retention record itself is the audit evidence; what happens to it is the recursive question Retention Window owns.
Capacity Constraint Enforcement (forthcoming) — for aggregate rules over a resource pool. Composes by intercepting Place Hold to consult the pool’s capacity rule; rejects as pool-capacity-exceeded when the rule is violated. The Expire transition returns the pool slot to availability — the side effect that the Reserve from Pool composition relies on (it drives ProvisionalCommitment.expire(id) and returns the slot to the pool atomically).
Hold Window with Expiry (forthcoming) — may extract window-management concepts (eager-expiry sweepers, deadline notifications, grace periods) into a separate atom. The window is intrinsic to this atom because the window is the contract; if window-management policy proves to recur generically across other resource-lifecycle atoms, extraction will be revisited.
Reversal (forthcoming) — produces a compensating commitment that offsets a Confirmed one (refund, admission reversal, return-to-stock). Composes by referencing the original commitment id; does not mutate it.
Actor Identity — binds each action against the atom to a verifiable actor, producing the non-repudiation guarantee regulators expect (signed authorization, MFA-bound caller context, witnessed approval). Provisional Commitment names Requester as a property of the Commitment; Actor Identity is the contract that says the named requester actually authorized the action and cannot later deny it.

Standards references

Provisional Commitment is the first regulated-business atom in the library; its standards inheritance is correspondingly richer than the productivity primitives.

ISO 9001:2015 §8.5.2 (Identification and traceability) — the minimum anchor. Resources under provisional commitment must be identifiable and traceable through every state transition; the atom’s identity model and per-commitment audit fields satisfy this directly.
ISO 9001:2015 §8.5.4 (Preservation) — the resource is preserved in its committed state for the requester during the hold window; the atom’s hold-window monotonicity invariant is the operational form.
Basel III liquidity framework (BCBS 238 LCR) — banks’ credit-limit holds and intraday liquidity reservations follow the same lifecycle. The atom’s terminal-absorption invariant matches Basel’s expectation that settlement events are facts about the past, not subject to silent revision.
The Joint Commission, Provision of Care, Treatment, and Services — healthcare bed-management and capacity-coordination standards require resource encumbrance to be auditable and time-bounded. The atom’s audit-friendly property is the structural correlate.
IATA Resolution 830a (and related ticketing-time-limit rules) — airline reservation systems’ fare-lock and seat-hold semantics formalize the hold-window contract this atom abstracts; the atom is vocabulary-neutral, IATA is one instantiation.
PCI DSS (Payment Card Industry Data Security Standard — the card networks’ mandatory security rules for handling cardholder data) Requirement 10 (logging and monitoring) — for retail and payment commitments touching cardholder data, every state transition must be logged. Composes with Event Log to deliver this directly.
GDPR Article 30 (records of processing activities) — for commitments whose records contain personal data (named guests, identified patients, ticketed passengers, account holders), the commitment record is itself a processing activity subject to Art. 30’s controller-records obligation. The atom’s per-commitment audit fields (Requester, Placed At, Expires At, transition timestamps) supply the data points Art. 30 expects; what counts as a processing purpose per commitment is host-system policy.
Sarbanes-Oxley §404 (internal control over financial reporting) — where confirmed commitments are material to financial reporting (the banking credit-limit example most clearly; any retail or hospitality commitment whose Confirmed transition flows to the books), the controls around the Held → Confirmed transition are §404-scope. Composes with Event Log to produce the auditable evidence §404 attestations require; the atom is implementation-independent on the specific control framework chosen.

For healthcare commitments touching protected health information, HIPAA’s (Health Insurance Portability and Accountability Act — US federal law governing healthcare data privacy and security) audit-controls requirement (45 CFR (Code of Federal Regulations — the codification of US federal agency rules) §164.312(b)) applies to the composing Event Log instance rather than to the commitment record itself; the atom is implementation-independent on this point. The same separation applies to GDPR Art. 30 in EU contexts where the composing Event Log carries the full processing history.

It inherits from:

Daniel Jackson, The Essence of Software — the freestanding-atom posture and the discipline of composing capacity, idempotency, audit, and reversal as separate concepts.
Eiffel’s design-by-contract — preconditions on each action; named rejection reasons.
Linear temporal logic — terminal absorption, single-resolution, and confirmation-within-the-window expressed as temporal properties.
Two-phase commit and reservation protocols (distributed systems) — the prepare/commit pattern this atom abstracts; here the prepare phase is the visible business state rather than an implementation hidden under transactional semantics.

Generation acceptance

A derived implementation of Provisional Commitment is acceptable — in the regulator-acceptance sense MUSE’s (the v1.1 completeness framework whose nine nodes GRID is drawn from) Proof node requires — when an external auditor, given the commitment record set plus the composed Event Log instance, can do all of the following without recourse to source code, runbooks, or developer narration:

Reconstruct the lifecycle of any commitment. From Place Hold to its terminal transition (Confirmed, Released, or Expired), with every timestamp, the resource and requester references, and the recorded state at each step.
Confirm single-resolution for every commitment. For every record, confirm that at most one terminal timestamp is non-null (Confirmed At, Released At, or Expired At) — never two. A record with two non-null terminal timestamps is evidence of a double-resolution defect (Invariant 2). A record with none is still Held.
Verify all ten invariants hold over the record set. Membership exclusivity, single-resolution, terminal absorption, id stability, resource and requester immutability, hold-window monotonicity, confirmation within the window, transition timestamps strictly after placement, no id reuse, and commitment store durability. Each invariant is checkable by a query over the records.
Observe every rejection reason at its action site. The seven named reasons (Invalid Request, Resource Unavailable, Not Held, Not Known, Window Elapsed, Window Not Elapsed, Storage Failure) are surfaced on the action interface and visible in the audit trail when rejection events are logged.
Identify the composing patterns active in this deployment. Whether idempotency (Duplicate Prevention), full audit history (Event Log), pool capacity (Capacity Constraint Enforcement), reversal of confirmed commitments (Reversal), retention of terminal records (Retention Window), and verifiable attribution (Actor Identity) are wired in, and with what configuration.

This is the generator’s contract: any code generated from this atom must produce records and a runtime surface that pass the checks above. The bar is the regulator’s question, not the developer’s intuition.

Status

grounded on Final Critique 4 — 2026-06-18 — the 2026-06-21 “derive expiry at read time” refactor (and its Final Critique 5 regrounding) has been withdrawn for this atom, returning it to its already-gated Final Critique 4 surface: expiry is once again a stored terminal Expired reached by an explicit expire(id) event, restoring the expired_at field, the window-not-elapsed rejection, and confirm’s window-elapsed guard. The reason the derive-at-read change does not apply here is that this atom’s lapse has a side effect — the expire event returns the resource (and, in a pool-backed composition, a capacity slot) to availability, relied on by the Reserve from Pool and Idempotent Reservation compositions, which call ProvisionalCommitment.expire(id). Derive-at-read applies only to a side-effect-free lapse; a side-effecting lapse needs an explicit expiry event. Because the content now matches the form that was already cleared at Final Critique 4, no new gate is required — this is a revert to a previously-grounded surface, not a new round; the meaning-preserving clock change from the withdrawn work (the clock is pipeline-implicit, not a now signature parameter — Final Critique 4 signatures had none either) is retained. The formal model was restored to the Final Critique 4 stored-Expired shape and re-verified green in the harness with both buggy twins rejected (resolution hazard and window hazard; see Lineage). Final Critique 4 (the first AI-conducted adversarial round, fresh-reader Opus, 2026-06-18) closed 1 foundational finding — now/id material supplied at the seam; formal-layer vote stood YES; the pattern was grandfathered at the legacy grounded — 2026-05-20 token until that round. See Lineage §AI adversarial round — Final Critique 4 and §Derive-expiry refactor reverted.

Lineage notes

This atom is the result of two iterations of pressure-testing.

First iteration — three-pass review during authoring. All three passes from pressure-testing.md run during the initial drafting; findings recorded below.

Pass 1 — Structural completeness (GRID — the nine-node completeness framework: Intent, System, Friction, Flow, Decision, Feedback, State, Behavior, Proof). Clean after one revision. The initial draft conflated Unheld with a system state, which would have left State malformed (a commitment cannot be Unheld and have an id at the same time). Resolved: State names four states (Held, Confirmed, Released, Expired); Intent and Flow frame Unheld as a property of the resource before and after the commitment’s effect, not of the commitment record. All nine GRID nodes resolved with their references intact.

Pass 2 — Conceptual independence (EOS). Clean. Four concerns were candidates for absorption and all four are correctly named as composing patterns rather than folded in:

Idempotency under retry — generic across messaging, payments, form submission. Composes with Duplicate Prevention.
Audit trail of state transitions — generic across every regulated domain. Composes with Event Log.
Aggregate capacity constraints — generic across overbooking, fractional reserves, inventory pools. Composes with a forthcoming Capacity Constraint Enforcement atom.
Reversal of a Confirmed commitment — generic across refunds, chargebacks, admission reversals. Composes with a forthcoming Reversal atom.

Each was tempting to absorb because all five example domains care about all four. EOS discipline holds: a concern that recurs across many concepts belongs to its own concept, not to the host. Provisional Commitment stays small.

Pass 3 — Adversarial scrutiny (Linus mode). Five findings, all closed in-pattern:

Identity model ambiguity. The first draft was unclear whether (resource, requester) could serve as identity. Resolved: explicit opaque-id model, with a defended-in-line paragraph naming the risk of (resource, requester) (re-holds and concurrent commitments would collide) and the mechanism that defuses it (one commitment, one id).
Confirmation after window elapsed. The first draft did not say whether confirm(id) was allowed when now ≥ expires_at but expire(id) had not yet run. Resolved: explicit window-elapsed rejection on confirm; Invariant 7 names confirmation-within-the-window as load-bearing; Edge cases names eager-vs.-lazy expiry as a deployment-shaped choice with audit implications.
Expiry semantics. The first draft treated expiry as automatic. Resolved: explicit expire(id) action with its own preconditions and a transition timestamp expired_at. Behavior names the eager-vs.-lazy choice; Edge cases enumerates the trade-off.
Hold-window mutation. The first draft was silent on whether expires_at could be extended. Resolved: explicit non-goal in Edge cases; the only path to a longer hold is release-and-re-place, producing a fresh id and a new audit entry. Mutating expires_at would silently break the honored-contract property.
Examples were happy-path only. Resolved: each of the five domain examples names all three terminal transitions (Confirmed, Released, Expired); Edge cases enumerates the rejection paths (invalid-request, resource-unavailable, not-held, not-known, window-elapsed, window-not-elapsed).

Three deferred concerns are named as explicit out-of-scope rather than fixed in-pattern: concurrency / atomicity, clock semantics, and the business meaning of confirmation. Each is deployment-shaped or belongs to a composing pattern.

The three passes together exercise the architecture as designed: GRID catches structural gaps (the Unheld conflation); EOS catches over-absorption (idempotency, audit, capacity, reversal); Linus catches hidden decisions (identity model, expiry semantics, window mutation). The atom is stronger because all three checks happened.

Second iteration — post-authoring adversarial review. A separate adversarial pass focused on regulated-domain coverage surfaced four further gaps. All four were closed in-pattern.

Standards inheritance was thinner than the atom’s regulated framing required. The first iteration named ISO 9001, Basel III, the Joint Commission, IATA, PCI DSS, and HIPAA but omitted two cross-cutting regulatory frameworks that apply across the example domains. Resolved: Standards references now include GDPR Article 30 (records of processing — applies wherever a commitment record contains personal data) and Sarbanes-Oxley §404 (internal control over financial reporting — applies where confirmed commitments are material to the books, the banking example most clearly).
Adversarial scenarios were missing. Examples covered happy-path domains and rejection paths but not the questions auditors, data subjects, and incident responders actually ask. Resolved: Examples now includes a sixth subsection — Regulated adversarial scenarios — walking regulator audit (querying for late confirmations and seeing Invariant 7 enforced structurally), data subject request (GDPR erasure composing with Cryptographic Shredding), and breach investigation (querying placed_at directly for time-windowed forensics).
No explicit generation-acceptance criterion. The first iteration’s success criteria were implicit — invariants hold, rejection reasons surface. For a regulated atom, the bar should be explicit and use the regulator’s language. Resolved: a new Generation acceptance section names four checks an external auditor must be able to perform against the records alone (reconstruct the lifecycle, verify the nine invariants, observe every rejection reason, identify composing patterns active in the deployment). This is the generator’s contract — the bar derived code must clear.
Non-repudiation was unaddressed. The atom names requester as a property of each commitment but did not say anything about whether the named requester actually authorized the action. Absorbing cryptographic binding into the atom would be an EOS over-absorption (it recurs across every regulated record). Resolved: Edge cases names non-repudiation as an explicit non-goal and points to the composing pattern; Composition notes adds Actor Identity as the contract that binds each action to a verifiable actor. (Subsequently drafted; the link resolves.)

The second iteration confirms the recursive property the methodology claims: Lineage notes themselves are pressure-testable, and a fresh adversarial pass surfaces additional gaps even after the three-pass authoring review reaches grounded. Each fresh application of the methodology adds evidence the architecture is doing real work.

Subsequent to this atom’s publication, two of the second-iteration fixes — Regulated adversarial scenarios and Generation acceptance — were promoted to canonical status in contributing.md and pressure-testing.md. This atom’s second-iteration record is the historical origin; the methodology docs are now the canonical source.

Refinement round 1. Four findings, all closed in-pattern. Conventions inherited from the methodology directly.

Action signatures used rejected(reason) placeholders; storage-failure absent from all four. All four action signatures named rejected(reason) with the reason taxonomy living only in the Feedback and Decision points prose. Resolved: signatures expanded — place_hold returns rejected(invalid-request | resource-unavailable | storage-failure), confirm returns rejected(not-known | not-held | window-elapsed | storage-failure), release returns rejected(not-known | not-held | storage-failure), expire returns rejected(not-known | not-held | window-not-elapsed | storage-failure). Feedback updated to include storage-failure.
storage-failure missing from Decision points. All four actions write to the commitment store; none previously named the write-failure path. Resolved: each Decision point extended — if the store write fails, the atom returns rejected(storage-failure) and the commitment is unchanged (for confirm, release, expire) or not created (for place_hold). Decision points for confirm, release, and expire also restructured to separate the not-known check from the not-held check explicitly.
No durability invariant. Nine invariants existed; none stated that commitments are never deleted. The Behavior section said “The commitment record persists in its terminal state indefinitely from the atom’s perspective” — correct as prose, but not an invariant. Resolved: Invariant 10 — Commitment store durability — added: confirm, release, and expire transition commitments to terminal states without removing records; total count is monotonically non-decreasing; retention and purge are composing concerns (Retention Window). The summary paragraph updated to name the irrevocable-record property this invariant gives.
Generation acceptance referenced “nine invariants” — stale after Invariant 10. Resolved: updated to “ten invariants”; durability added to the enumeration of checkable properties.

Scheduled rescan: 2026-05-20. Pass 1 GRID clean. Pass 2 EOS clean. Pass 3 Linus (fresh-reader) — one refining finding: Generation acceptance check 3 listed “six named reasons” and omitted storage-failure, which is a named rejection reason in all four action signatures and correctly listed in the Feedback section. Fixed: updated to “seven named reasons” with storage-failure added to the enumeration. No other findings.

Formal-layer vote — 2026-06-03: YES (model pending). Invariant 7 (confirm rejected if now ≥ expires_at) is a timing claim; Invariant 8 (transition timestamps after placement) and Invariant 3 (terminal absorption) form a temporal reachability surface. Load-bearing temporal/ordering/safety claims a derived formal model would verify; none exists yet, so the pattern is downgraded to grounded (English) — formal layer pending until the model is authored and verifies (findings flow back into this English spec per the conflict protocol). Vote per pressure-testing.md §Formal models — The formal-layer vote.

Formal-layer vote — reconsidered 2026-06-03: KEPT YES. This pattern was one of the five clock/precedence candidates reviewed in the 2026-06-03 bar reconsideration. Unlike Retention Window / Session / Consent (downgraded to English-only), Provisional Commitment was kept because confirm-within-window is a genuine action-vs-time race: as the clock advances, a confirm must not slip past expires_at while an auto-expire is also enabled. That is exactly the class a model exhausts and prose cannot. Model authored same day (below).

Formal model — 2026-06-03: TLA+ authored and verified; pattern promoted to grounded. Derived model provisional-commitment.tla + config provisional-commitment.cfg, checked by tla-checker via tools/harness/check.mjs. What it checks: one commitment, an advancing bounded clock, fixed ExpiresAt = 2, MaxClock = 3. The load-bearing claim — a commitment reaches Confirmed only if confirm fired strictly within the window — is checked via a ghost confirmedAt (the clock value at confirm time): Inv_ConfirmWithinWindow == state = Confirmed ⇒ confirmedAt < ExpiresAt. confirm (guard clock < ExpiresAt) and expire (guard clock ≥ ExpiresAt) have mutually exclusive time-guards. Exhaustive: 17 states, holds. Buggy twin provisional-commitment-buggy.tla drops the clock < ExpiresAt guard on confirm; rejected at 10 states (tick to clock = 2 = ExpiresAt, then confirm → confirmedAt = 2 ≥ ExpiresAt). The twin mechanizes the window-elapsed rejection: without the guard, confirm-after-expiry is reachable. Out of model scope: id discipline, storage-failure, multi-commitment place_hold serialization. Conflict-protocol outcome: none — the model corroborates the English; canonical English unchanged.

Formal model — 2026-06-04: Invariant 8 (transition timestamps strictly after placement) coverage closed. Coverage cross-check identified a partial GAP: Release and Expire had no ghost timestamps, so the release/expire halves of Inv 8 were unchecked. Fix: (1) Added PlacedAt = 1 constant (commitment placed at clock=1; sentinel value 0 is strictly below PlacedAt, giving the check real teeth). (2) Added ghost variables releasedAt and expiredAt; Release stamps releasedAt = clock, Expire stamps expiredAt = clock. (3) Added Inv8_TransitionsAfterPlacement asserting confirmedAt ≥ PlacedAt, releasedAt ≥ PlacedAt, expiredAt ≥ PlacedAt in their respective terminal states. (4) Updated buggy twin: Release and Expire stamp 0 instead of clock (simulating a recorder that hard-codes zero instead of reading wall-clock); Confirm window guard restored so only Inv 8 fires in this twin. The Inv 7 confirm-within-window hazard is retained as a second isolated twin, provisional-commitment-buggy-window.tla (ConfirmBuggy admits at clock = ExpiresAt; rejected at 6 states on Inv_ConfirmWithinWindow, with Inv 8 holding). The two isolated twins give Inv 7 and Inv 8 each their own dedicated counterexample; both are auto-discovered and required-to-reject by tools/harness/audit.mjs. Correct model: 15 states, all invariants hold. Buggy twin: rejected at 4 states — Init → Release produces releasedAt = 0 < PlacedAt = 1, violating Inv8_TransitionsAfterPlacement. Saturation note: state count grows with MaxClock (15 at MaxClock=3, 24 at MaxClock=4) because each additional clock tick extends the integer domain; all distinct behavioral interleavings (confirm within window, release at any clock, expire at or after window) are present at MaxClock=3 — semantically saturated. Conflict-protocol outcome: none — model corroborates the English; canonical English unchanged.

AI adversarial round — Final Critique 4 (first real AI round) — 2026-06-18. This atom grounded 2026-05-20 under the early process — foundation plus refinement, with no fresh-reader AI adversarial round — and carried the legacy grandfathered token. This round is that missing AI-conducted adversarial round (fresh-reader Opus, Happy-Torvalds-X2); it is the atom’s Final Critique 4 (Rounds 1–3 the foundation/refinement baseline, per pressure-testing.md §Round structure). One foundational finding closed: F1 Logic Confinement — now and the id material are now injected inputs supplied at the deployment seam (was an ‘implicit clock’ with = now inside the transitions and ‘system-generated’ ids); the confirm-vs-expire boundary at now = expires_at is unchanged. Caller signatures unchanged and the invariant set held at 10, so the fixes are additive with no constituent-change cascade. Formal-layer vote stands YES (strong model: the checker already treats the clock as an advancing input and the id as out of scope), so F1 does not reopen it. Confirming fresh-reader Opus clearance gate (2026-06-18): CLEAR, 0 foundational, no new surface. Compositions affected — confirming check only, NOT a re-pass: Idempotent Reservation, Reserve from Pool. Grounds at Final Critique 4.

Execution/render-time refactor — 2026-06-21 (touch-triggered; status downgraded to partially resolved). Direction (Scott): derive expiry at read time; reduce execution-time clock dependence; clearly mark the residual. This atom is part of the corpus-wide sweep of clock-gated atoms for which invitation.md is the worked reference case. Changes:

Stored Expired removed; expiry derived. Stored terminals are now Confirmed and Released. Expired is a derived effective_status projection — Expired ⟺ state = Held ∧ now ≥ expires_at — computed at read time from the immutable expires_at and the injected clock. New Invariant 11. Applies the “derive the idealization, do not lag it with a flag” pitfall (pressure-testing.md §Formal-model authoring pitfalls) to the canonical English.
expire action, expired_at field, and the window-not-elapsed rejection removed. The expire(id) action’s only job was to write the stored Expired terminal; with expiry derived, it is gone, and so is the window-not-elapsed reason that only guarded it. Expiry never writes. A read of the record set plus the read-time clock recovers every lapsed hold.
Kept guarantee — no resolution after the window. confirm/release retain the pure window guard reading the injected now and rejecting window-elapsed when now ≥ expires_at — no write. This is the surviving (and deliberately confined) execution-time clock dependence: the action-vs-clock boundary at now = expires_at now gates the resolving writes directly, rather than racing an auto-expire. The reword folds the old Invariant 7 (confirmation within the window) into Invariant 7 (resolution within the window, covering both confirm and release) and absorbs the old Invariant 8’s expired_at half into the derivation.
Clock surfaced as an explicit injected input in the signatures (subsequently reverted — see below). Every action took now explicitly — place_hold(resource, requester, duration, now), confirm(id, now), release(id, now) — consumed only by (a) pure window guards / the read projection (no write) and (b) immutable timestamp stamps inside committed transitions. This matched the worked reference (invitation.md threads now into signatures); it deviated from the corpus convention of leaving clock_t pipeline-implicit. Flagged for the re-pass; subsequently resolved by the signature revert below.
Sections updated: summary blockquote, Intent, Summary, Identity model, Inputs/Outputs (+ a read surface with effective_status, signatures threaded), State (stored Held/Confirmed/Released; “Expired is derived, never stored”; transitions = writes only), Decision points (+ Logic-confinement note and rejection priority; expire block and window-not-elapsed removed), Behavior, Feedback, Invariants 1/2/3/7/8/10 reworded and 11 added, Examples (all five threaded; expire examples converted to derived-expired; adversarial scenarios reworded), Edge cases (clock-derivation residual note; eager-vs-lazy-expiry bullet replaced — expiry is derived, not swept), Composition notes (Retention Window cascade reconciliation; Event Log/Hold Window updated), Generation acceptance, Status.
Constituent-change cascade. Removing the expire action, the stored Expired value, and the window-not-elapsed reason is a breaking change to Provisional Commitment’s surface; every composition naming it requires a touch-triggered re-pass:
- Idempotent Reservation — exposes expire(id, idempotency_token) delegating to ProvisionalCommitment.expire(id), and lists not-held/window-elapsed pass-throughs; its Invariant 2 names confirm/release/expire. The delegated expire no longer exists; the composition must either drop its expire wrapper (a lapse needs no write) or re-home it as a notification/derivation. Re-pass required (not edited here — compositions are out of scope for this touch).
- Reserve from Pool — exposes expire_reservation(...) that drives ProvisionalCommitment.expire and returns the slot to the pool atomically, guarded by window-not-elapsed; its examples and invariants (e.g. the confirm/expire race, “No lapsed confirmation”) lean on the expire write. With expiry derived, the slot is free at now ≥ expires_at with no write; the slot-return must be re-expressed as a derivation (or a Capacity Constraint release triggered by the derived status). Re-pass required (not edited here).
- Retention Window — its Composition notes place “terminal-state commitments (Confirmed, Released, Expired) under retention.” Since Expired is now derived, the composing layer places retention based on the derived effective status (retain stored Confirmed/Released directly; treat a lapsed Held reading Expired as a retention candidate via effective_status). retention-window.md is not edited by this refactor (composing pattern, out of scope); the reconciliation is recorded in this atom’s Composition notes and here. The Customer Onboarding composition also names this atom and rides the same confirming re-pass.
Formal model re-derived. provisional-commitment.tla + the two buggy twins re-derived to the new shape: state ∈ {Held, Confirmed, Released} (no stored Expired); now an advancing injected clock; Lapsed(c) / EffStatus(c) the derived read-time projection; resolving writes (Confirm, Release) guarded state = Held ∧ now < ExpiresAt; no Expire action. Checks: Inv_SingleResolution (single-resolution by write over the two stored terminals, via ghost resolution), Inv_NoStoredExpired (the store never holds an Expired value), Inv_DerivedExpiryCoherent (a stored terminal reads back as itself), Inv_ConfirmWithinWindow (the KEPT residual — a Confirmed commitment was confirmed strictly within the window, via ghost confirmedAt), and Inv8_TransitionsAfterPlacement (stored timestamps ≥ PlacedAt). Constants unchanged (PlacedAt = 1, ExpiresAt = 2, MaxClock = 3). Re-run through tools/harness/check.mjs: correct model PASS (9 states, all invariants hold); -buggy (RESOLUTION hazard — ConfirmBuggy drops the state = Held guard, re-resolving an already-Released commitment) PASS = violation (8 states, Inv_SingleResolution); -buggy-window (WINDOW hazard — ConfirmBuggy admits at clock ≤ ExpiresAt, confirming a lapsed hold) PASS = violation (6 states, Inv_ConfirmWithinWindow). Each twin’s violation was confirmed isolated to its target invariant (the other load-bearing invariants hold in each twin). The full coverage cross-check (a matrix over Invariants 1–11) and the bound-saturation review ride the pending re-pass; note now is modeled as an advancing clock, so the raw state count grows with MaxClock while the behavior space saturates once now crosses ExpiresAt.

Final Critique 5 — 2026-06-23 — clean (fresh-reader re-gate; council-run). Closing fresh-reader Final Critique (Pass 1 GRID / Pass 2 EOS / Pass 3 Linus at X2) over the execution/render-time refactor batch returned zero foundational findings. Formal model re-verified green in the harness, buggy twin(s) rejected, coverage cross-check clean (no GAP rows), bound saturated. This atom was already clean at the first Final Critique; its only change since was the meaning-preserving signature revert (clock returned to pipeline-implicit), classified editorial under the recalibrated touch trigger (pressure-testing.md §Touch triggers re-pass), so it regrounds with the batch. Regrounded at Final Critique 5.

Signature revert — now returned to pipeline-implicit per the FC council; the now-explicit experiment is reverted; clock/id injection is stated in prose (the Logic-confinement note), not in signatures.

Derive-expiry refactor reverted — 2026-06-23. The 2026-06-21 “derive expiry at read time” change (entry above) and its Final Critique 5 regrounding are withdrawn for this atom. Expiry is restored as a stored terminal Expired reached by an explicit expire(id) event — with the expired_at field, the window-not-elapsed rejection, and confirm’s window-elapsed guard all back — because this atom’s lapse has a side effect: the expire event releases the resource (and, in a pool-backed composition, returns a capacity slot to a Capacity Constraint pool). That side effect is relied on by the Reserve from Pool and Idempotent Reservation compositions, which call ProvisionalCommitment.expire(id) and map its not-known/not-held/window-not-elapsed/storage-failure rejections. The corpus-wide “derive expiry at read time” initiative (invitation.md is its worked reference) applies only to a side-effect-free lapse — a status that can be inferred at read time because nothing is released when the window closes. A side-effecting lapse cannot be a read-time derivation: returning a resource is a write, so it needs an explicit expiry event. This atom is therefore excluded from that initiative and returns to its already-gated Final Critique 4 surface.

Status / grounding. The Status token returns to grounded on Final Critique 4 — 2026-06-18 (its grounding before the withdrawn refactor). Because the restored content is byte-for-meaning the Final Critique 4 form that was already cleared, no new gate is required: this is a revert to a previously-grounded surface, not a new adversarial round. The two prior Lineage entries (the 2026-06-21 refactor and the 2026-06-23 Final Critique 5 regrounding) are kept above as dated history of the withdrawn experiment.
What is kept from the withdrawn work. Only the meaning-preserving clock treatment: now (clock_t) is pipeline-implicit, supplied at the I/O seam, never a signature parameter — which is also exactly what the Final Critique 4 signatures had (none of place_hold/confirm/release/expire ever took a now parameter), so no signature changes back. No now parameter was re-added to any signature.

Restored surface. State machine Held → Confirmed Released Expired (all three stored terminals, all absorbing). Actions place_hold, confirm, release, and expire(id) → ok | rejected(not-known | not-held | window-not-elapsed | storage-failure). Invariant set back to the Final Critique 4 10 invariants (the derive-expiry Invariant 11, the effective_status read projection, the “Expiry is not a transition” framing, and all “no expire action” language are removed).

Formal model restored and re-verified. provisional-commitment.tla and the two buggy twins were reverted to the Final Critique 4 stored-Expired shape: state ∈ {Held, Confirmed, Released, Expired}; Confirm/Release guarded state = Held ∧ clock < ExpiresAt; an Expire transition (Held → Expired) guarded state = Held ∧ clock ≥ ExpiresAt; ghost resolution for single-resolution over the three terminals; ghost confirmedAt/releasedAt/expiredAt for Inv 8; the confirm-within-window invariant (Inv_ConfirmWithinWindow). Constants unchanged (PlacedAt = 1, ExpiresAt = 2, MaxClock = 3). Harness results re-run through tools/harness/check.mjs: correct model PASS (12 states, all invariants hold); provisional-commitment-buggy.tla --buggy — RESOLUTION hazard (ConfirmBuggy drops the state = Held guard, re-resolving an already-Released commitment) — PASS = violation (9 states, Inv_SingleResolution); provisional-commitment-buggy-window.tla --buggy — WINDOW hazard (ConfirmBuggy admits at clock ≤ ExpiresAt, confirming a lapsed hold) — PASS = violation (6 states, Inv_ConfirmWithinWindow). Each twin’s violation was confirmed isolated to its target invariant.
Compositions. Idempotent Reservation and Reserve from Pool are not edited — they already call ProvisionalCommitment.expire(id) and become consistent automatically now that it is restored; the constituent-change cascade the withdrawn refactor flagged for them does not fire.

Annotation conversion — 2026-06-29 (annotation.md second-batch rollout, foundations-first with Actor Identity, Retention Window, Tamper Evidence, Permissions, Session). Converted every concept reference to a [Term] marker and added the per-page Terms registry, applying the resolved four-kind ontology — Type, Operation, Field (a datum a Type carries — what does it carry?), Parameter (a value an Operation needs — what does it need?), and Member. Inventory: one Type (Commitment, whose state state-field name is the Type card’s Projects: token); four Operations — Place Hold, Confirm, Release, Expire (kramdown anchors #place-hold, #confirm, #release, #expire, the exact anchors Actor Identity links to); eight Fields stored on the Commitment — Id, Resource, Requester, and the five timestamps Placed At, Expires At, Confirmed At, Released At, Expired At (the time-window Fields, stored-as-themselves, exactly as duplicate-prevention’s recorded_at was a Field); two Parameters consumed but never stored under their own name — Duration (supplied to Place Hold, sizes the window via Expires At = Placed At + Duration) and the injected Now (the pipeline’s clock_t clock reading) — the same duration/clock split duplicate-prevention drew between its window/now Parameters and its stored timestamp, placed by the discriminator stored-as-itself → Field, consumed → Parameter; and the Members — the four states Held, Confirmed, Released, Expired (pure state Members, no Projects: line, mirroring personal-todo’s Pending/Done) and the seven rejection reasons Invalid Request, Resource Unavailable, Not Known, Not Held, Window Elapsed, Window Not Elapsed, Storage Failure. The collision watch is clean: the Expire Operation (#expire) and the Expired Member (#expired) are distinct anchors, as are Confirm/Confirmed, Release/Released, and Expires At/Expired At. Casing left the prose into each card’s Projects: line; every target’s lowering is derived by tools/harness/term-adapter.mjs. The four Operation contracts (place_hold(resource, requester, duration) → …, confirm(id) → …, release(id) → …, expire(id) → …) are kept once each in Inputs as the labeled projected contract; the concrete example invocations in Examples (e.g. place_hold(card_resource, cardholder, 7-days) → id = auth_c41, confirm(auth_c41)) and their literal returns (id, ok, auth_c41) are left verbatim as illustrative wire-level calls. Cross-page references: Duplicate Prevention’s wiring calls check(idempotency_token)/record(idempotency_token) and the qualified ProvisionalCommitment.expire(id) stay backticked as concrete invocations; pool-capacity-exceeded (the forthcoming Capacity Constraint atom’s reason) and Event Log’s sequence_number field stay backticked — their owners are not converted (Capacity Constraint forthcoming; sequence_number is Event Log’s Field, not this atom’s); the pipeline type-names clock_t/id_t stay backticked as verbatim pipeline tokens. Expression only — the expiry formula is the identical relation (Now ≥ Expires At for Expire, Now < Expires At for Confirm/Release, the same boundary at Now = Expires At), all ten invariants hold their exact claims (Invariant 7’s confirm-within-window and Invariant 8’s Expires At ≤ Expired At are the identical relations), the invariant set stays at 10, and Invariant numbering is untouched. The .tla model and its two buggy twins are UNTOUCHED and still PASS / rejected — provisional-commitment.tla PASS, provisional-commitment-buggy.tla --buggy correctly rejected (RESOLUTION hazard, Inv_SingleResolution), provisional-commitment-buggy-window.tla --buggy correctly rejected (WINDOW hazard, Inv_ConfirmWithinWindow); no .tla/.cfg changed. Re-verified, not re-grounded: Status stays at grounded on Final Critique 4 — 2026-06-18. Gates: linter 0 (incl. the O-term-resolver, resolving all of this page’s markers against its registry); the derived manifest projects an identifier kind (Field) and an enumerated kind (Member); the harness re-run green with both buggy twins rejected; git status clean for all model files; diff read line-by-line against the same-claim-or-weaker test.

Showcase pass — 2026-06-29. Brought to the full showcase standard, matching the duplicate-prevention.md exemplar, on top of the already-applied annotation conversion. Changes are representational only: (1) Summary/blockquote merge — the plain Tier-1 prose.md cut-#4 Summary moved to the very top (before Intent), the descriptive top blockquote folded out as redundant (this removed the last stale raw casing on the page — the blockquote still carried now < expires_at / expires_at / confirm / release / expire while the body was already casing-free), and an also-known-as italic line added. (2) Lineage collapse — the Lineage notes wrapped in the collapsed <details> block mirroring the exemplar. (3) prose.md cut #1 (one idea per sentence) — the two densest run-on sentences in the Summary (the three-clause resolution-rejection sentence and the identity/immutability/audit sentence) split into short declaratives, lossless. (4) prose.md cut #5 (prose→structure) — the State section’s Transitions: prose list rendered as a transition table (action · from · to · window guard · stamps · result · rejections), with four semantics kept in prose beside it per the cut-#5 caveat: the exact window boundary at Now = Expires At and the fail-closed writes-nothing on a failed guard; eager-vs-lazy expiry firing with the side-effect rationale; terminal absorption; and the fixed rejection priority (cross-referenced to Decision points, where the full per-action preconditions stay). Cuts #2 (glossary) and #3 (cross-ref footer) were assessed and skipped: acronyms are already spelled-out-once inline per the corpus convention here, and provenance already lives in the invariants’ supporting prose and Composition notes rather than being re-cited mid-sentence. Expression only — every invariant and its number, the Now < Expires At / Now ≥ Expires At window relations and the Now = Expires At boundary, all four projected-contract signatures, every guarantee, and the invariant count (10) are unchanged in force; every [Term] marker still resolves to its card and the Terms registry is intact. Re-verified, not re-grounded: Status stays at grounded on Final Critique 4 — 2026-06-18. Gates: linter 0 (incl. the O-term resolver — all markers resolve); the .tla model and both buggy twins untouched and still PASS / correctly-rejected; the derived manifest projects cleanly; git status shows no model files modified; diff read line-by-line against the same-claim-or-weaker test.