Pressure Testing

Table of contents

Pressure Testing
Pressure Testing (The Crucible)

Pressure Testing (The Crucible)

The foundation review every Grace Commons pattern survives before being considered grounded (fully reviewed, complete, and reliable). Minimum standard: a 3×3 baseline — three rounds of three passes (structured review sweeps) each, nine passes — followed by a Final Critique, an AI-conducted adversarial (Torvalds) round that reruns all three passes in strict fresh-reader mode and repeats until the pattern grounds. Round 1 is the foundation (Pass 1 → 2 → 3, author-led); the remaining baseline rounds are human or council refinement, continuing until a complete round surfaces no new findings; the Final Critique then runs as the closing AI round (starting at Round 4) and carries the pattern to grounded on Final Critique N. The baseline is a floor, not the finish: a pattern that looks clean after the foundation still completes its refinement rounds before the Final Critique — the clean result is the confirmation, not a reason to skip ahead. See §Round structure and naming for the canonical counting, and §What “grounded” means for the formal-layer vote and Opus clearance gate that also gate grounding.

A pattern’s spec is incomplete in three different ways at once. Each of the three passes below catches a different class of incompleteness. None substitutes for the others. Together they constitute the mandatory foundation for atoms (in atoms/) and compositions (in compositions/).

The foundation passes are not a single-shot quality bar. Fixing a Pass 1 gap changes the document, and the changed document has new surface area for Pass 3 to find. A spec that passes all three cleanly on the first attempt has either been authored with extraordinary care or has not been reviewed adversarially enough. Refinement passes — re-running the same three passes after each round of fixes — are expected, not exceptional. There is no fixed number of refinement passes; the loop runs until a complete pass surfaces no new findings.

The three passes are recursive in a useful way: applying them to a pattern produces a commit whose message records the round, and that reasoning can itself be pressure-tested by re-running the same three passes. Each fresh use becomes evidence the architecture is doing real work.

Pass 1 — Structural completeness (GRID)

What it checks. For each of GRID’s nine nodes (GRID is a nine-checkpoint completeness framework — each node is one checkpoint) — Intent, System, Friction, Flow, Decision, Feedback, State, Behavior, Proof — is the node specified? Does the spec satisfy the node’s completeness rule? Are the node’s references to other nodes resolved?

What it catches. Missing pieces. Nodes that aren’t addressed at all. Friction items that don’t reference a Flow step. Decisions that aren’t linked to a State or Behavior. Intent claims that aren’t testable.

How to run it. Mechanical. Walk the nine nodes one by one with their MUSE v1.1 (the completeness framework GRID is built on) rules:

Node	Completeness rule
Intent	Must be testable — falsifiable by observable behavior
System	Must reference real components, not hypothetical ones
Friction	Must reference a specific system node or behavior
Flow	Must have a defined start, end, and at least one branch
Decision	Must be linked to a State or Behavior node
Feedback	Must be measurable — tied to a specific signal or metric
State	Must name what changes and under what condition
Behavior	Must be observable — not inferred
Proof	Must be measurable and defined before development begins, and must name its verification surface — records-alone checks, and/or a derived formal model where the formal-layer vote requires one (see Formal models below)

Then check the reference graph: every Friction links to a Flow step; every Decision links to State and Behavior; every Proof links to Intent. Orphaned references (links that point to something not defined in the spec) are violations. The same check extends to invariant dependencies: every Rests on: clause must resolve to a declared capability (see Capability provenance) — a dependency on an undeclared substrate or constituent capability is an orphaned reference of the same class.

Then check accessibility completeness — two structural checks that are mechanical, not adversarial, and belong in Pass 1:

Summary is Tier 1 clean. Does the Summary contain any unexplained acronym, undefined jargon, or technical term that is not everyday English? Every such term must be defined inline. A Summary that a non-engineer with domain knowledge cannot read without a glossary is a Pass 1 structural gap, not a stylistic preference.
No undefined acronym anywhere in the spec. Does any acronym or initialisation (HIPAA, GDPR, EOS, GRID, NFC, FATF, BSA/AML, KYC, CDD, PCI DSS, etc.) appear without being spelled out and briefly glossed at its first use in the document? First-use definition is required globally — in any section, not just the Summary. An undefined acronym is an implicit “you know where to look” cross-reference and is treated as a reference-graph violation.

For compositions that define a named semantics subsection (Replay semantics, Evaluation rules, Provisioning cascade, or similar): every action wiring step that defers execution to that subsection — by saying “recompute”, “evaluate”, “apply”, “cascade”, or equivalent — must name the subsection explicitly. An action wiring step that says “recompute the derived state” without citing the Replay semantics section is an intra-document orphaned reference and is a Pass 1 finding.

Then run the reference-graph checks the frozen rules of 2026-08-29 add, each mechanical and each a resolved-or-orphaned question:

Every reconciliation leg names both edges. Its lower edge resolves to a Configuration entry (a completion bound) and its upper edge to the retention policy of the audit instance it reads — §A reconciliation is bounded at both ends.
Every pairing names its field, and every payload carries it. A check or sweep that says pair, match, join, or the corresponding names invocation_id, and every outcome payload the action can write — success, refusal, void — carries it — §Intents pair with outcomes.
Every transcribed rejection arm keeps its declared payload, and every landed code is in the signature. recording-failure(step), never bare, on the left of a mapping arrow; a code the prose lands appears in the action’s signature block — §A transcribed rejection arm keeps its payload (linter check S-recording-step).
Every seal presentation is keyed by sequence_number. An original_event_payloads map keyed by an identifier is an orphaned reference to a covering range it cannot present — §A seal presentation is keyed by log position (linter check T-seal-key).
Every derived-index element states its past-horizon classification, and a truth-bearing half names its atom. The named atom resolves to a file or a *(forthcoming)* marker — §A derived index splits at the horizon.

And the ones the frozen rules of 2026-08-30 add:

Every retry loop names its terminus, and every leg names its serialization key. Retry until it lands resolves to a completion bound at which the invocation yields; two legs over one act resolve to one key they serialize on — §A compensator is exclusive.
Every verdict class in a verdict table resolves to a producing step. A failed-verification(purged) the table promises has a step that reaches it before any composition-side membership check — §Lawful destruction is answered before absence.
Every set-valued outcome field resolves to a cardinality cap. Non-empty is not a cap — §An outcome is sized before the intent.
Every liveness window resolves to its inequality. Bound, cadence, and latency are three Configuration entries and the strict inequality is on the page — §Liveness is arithmetic.
Every cross-seam comparison names its offset allowance. A composition stamp compared to a constituent stamp resolves to a clock_offset_allowance entry or to a pass-through — §A stamp from another seam never decides a write alone.
Every exported rejection code carries the payload the prose distinguishes. A token landed on both sides of the commit carries the position in the signature — §A composition’s own rejection arm carries the retry bit (linter check U-retry-bit).
Every exercised constituent capability resolves to a declared source. The six tells for uses under §Capability provenance — a read keyed by an un-indexed field, an enumeration the store does not offer, durability the constituent disclaims, a multi-call critical section, a clock the constituent has none of, a uniqueness scope wider than the constituent’s — are each an orphaned reference.

Time: 15–30 minutes for an atom; longer for a composition with multiple constituents.

Personal Todo example. First pass surfaced five gaps: actor (Behavior was incomplete — who acts?), description mutability (State + Decision were silent on edit), temporal metadata (State omitted timestamps), observability (Feedback didn’t say what’s queryable), identity policy (Decision punted on duplicate handling). Four were closed in-pattern; the fifth was extracted to Duplicate Prevention by Pass 2.

Pass 2 — Conceptual independence (EOS — Essence of Software)

What it checks. For each responsibility the spec names, does it belong to this concept, or to a different concept that ought to compose with it?

What it catches. Over-absorption (when a spec takes on more than it should — grabbing responsibilities that belong to a different concept). A spec absorbing a responsibility that is generic, recurs across many concepts, and deserves its own freestanding atom. In EOS’s frame these are concepts hiding inside a host — not properties of the host concept; concepts in their own right.

How to run it. For each responsibility, ask:

Does it recur across many domains? (Identity stability, recency guards, audit logging, time windows, ordering, retention, tamper-evidence — usually a separate concept.)
Does it have its own state machine, distinct from the host concept’s? (If so, almost certainly its own concept.)
Could the host concept be specified without it, with the functionality composed in? (If yes, extract.)
Would another concept that needs this functionality reinvent it? (If yes, extract.)

Two classification questions the frozen rules of 2026-08-29 add, both about where a fact lives:

Of the records a recovery path writes, which are re-derivable and which are not? A re-derivable record is derived state, rebuilt from the constituent stores or the sealed trail; a record that is not re-derivable is not re-emitted by the recovery — the act is re-run or abandoned. A recovery that “remembers” is holding state no classification admits — §Recovery commits under a declared service identity.
What is each derived element past its horizon? Still derived from an independent failure domain, not needed, or truth-bearing — and a truth-bearing half is an unnamed atom to extract: a purge’s destroyed key (Erasure Tombstone), a record owed for a committed act (Outbox), a composition’s own log (Event Log). A composition-owned middle is the tell — §A derived index splits at the horizon.

The composition-layer extraction gate — one level up. The four questions above are written against atoms: they catch a responsibility that should be its own freestanding atom. As the composition catalog grows, the dominant over-absorption risk moves up a level. It is no longer a responsibility absorbed into one spec, but the same emergent invariant or wiring decision recurring across many compositions — binding bijections, cascade gates, attribution-coverage variants — with no canonical rule for when that recurrence should be retired into a shared substrate composition or atom. The rule below is that trigger, and it is deliberately not a recurrence count: no fixed N is defensible, because two forced recurrences of a real concept warrant extraction while a dozen co-occurrences of the same atoms do not. The trigger is a conjunction of gates — extraction fires only when Gates 1 through 3 all hold; the tie-breaker that follows orders borderline candidates but never opens or closes the decision by itself. Without the rule the choice gets made ad hoc, one round at a time, and the corpus accumulates parallel re-derivations of the same emergent rule.

Gate 1 — recurrence is at the invariant level, not the atom-set level. Count recurrence as the same emergent invariant independently forced across compositions — never as co-occurrence of the same constituent atoms. Similarity is not recurrence: shared constituent lists, parallel wiring shape, and naming conventions are surface similarity, while identical wiring can force different invariants and a genuinely cross-domain instance of one invariant can look nothing alike in two specs. This gate rejects recurrence-inflation — the false count that admits cosmetic twins.
Gate 2 — the recurrence has an emergent invariant surface of its own. The recurring thing must be a must-be-true that no constituent owns alone, not the co-location of constituents that each already hold their own invariants. Gate 1 asks is it the same invariant recurring; Gate 2 asks is it an emergent invariant at all — distinct failures, so the two gates are not redundant: Gate 1 rejects the same atoms wired twice for different reasons, while Gate 2 rejects a recurrence whose “invariant” is merely the conjunction of constituent invariants (zero emergent yield — a recipe, not a substrate).
Gate 3 (decisive) — the recurrence names a freestanding concept, not wiring. This is Jackson’s wiring-not-primitive rule: wiring freestanding concepts together does not mint a new primitive. The discriminator that makes the gate decidable rather than a matter of taste: does the recurring invariant introduce state or behavior the constituents do not already carry — a state machine of its own — or is it the mechanical consequence of wiring them, adding no state beyond what the constituents hold? The operative test is new state, not the looser “is something emergent here”: mere emergence is present in any non-trivial composition and decides nothing, whereas new state the constituents lack is checkable by inspection. Only the former is a concept worth extracting; the latter is wiring dressed as a primitive, and promoting it makes every composition that names it inherit a dependency that buys no new guarantee. Gates 1 and 2 can both read yes on surface evidence and this gate still settles it — which is why it is decisive, not co-equal with the other two.
Tie-breaker (a weight, not a gate) — would a substrate retire forthcoming-debt? If the recurring invariant has already seeded forthcoming atoms or composition-introduced surfaces across the affected specs — each naming the same not-yet-extracted home — a substrate that collapses them into one declared owner retires that standing debt at once. This raises a candidate’s priority among those that already clear Gates 1 through 3; it never substitutes for them. A recurrence that would retire debt but fails Gate 3 is still wiring, and is not extracted.

Worked case — running the gates. Immutable Transaction Ledger’s Final Critique 5 (its Pass 2 EOS extraction-candidate review) considered the strongest candidate it found — a standalone binding-bijection / dual-store atomic commit atom — and declined it. Run through the gates, that decline is determined by the gates, not reached by instinct. Gate 1 holds: the binding-bijection invariant genuinely recurs — the same disclosure-record-to-audit-event atomicity recurs in Chain of Custody and Forensic Recovery, both named in Immutable Transaction Ledger’s commit history as carrying the binding-bijection model shape, not merely the same atoms co-occurring. Gate 2 holds: it is an emergent must-be-true no single constituent owns. But Gate 3 fails — the bijection has no state machine of its own; it is the mechanical consequence of committing two stores under one atomicity obligation, introducing no state the constituents do not already carry, so it names wiring, not a freestanding concept. Gate 3 turns the decision, exactly as the rule predicts a recurring-but-mechanical invariant should resolve. The council reached this answer by instinct, against one spec, with nothing to make the next such decision repeatable; the gates make it repeatable — and, run here, they reproduce the council’s verdict for a stated reason rather than merely re-describing it after the fact.

The higher-order composition test (2026-08-30). The three gates say when a recurrence names a concept; they were written for atoms, and applied one level up they say nothing about whether the concept is worth its own page. The test below is the acceptance bar for a composition of compositions — a substrate a composition adopts through a declared contract without exposing its constituents — and it was written the day the corpus proved it needed one: twenty compositions independently re-deriving the same invariant-bearing machinery (an intent and outcome record, a serialized section, a recovery terminus, a bounded reconciliation, a positioned rejection code), each local copy accumulating slightly different fixes, and each fresh-reader round finding the next defect in the copy the previous round had just repaired. That is not duplication; it is a missing compound. The risk on the other side is the false abstraction — a layer created because it might be reusable rather than because the corpus has shown it is — and the test is what keeps abstraction evidence-driven. A higher-order composition earns its existence under all of the following:

No abstraction without recurrence. Extract only after the same invariant or protocol shape has appeared repeatedly in real compositions. The floor is five exact instances — instances of the same problem, not the same syntax; a pattern whose recovery, durability, trust, or failure semantics differ does not count toward the five. (A rule on this page freezes on three; a compound costs more to be wrong about, because un-extracting one means re-deriving the protocol in every adopter, so its floor is higher. This does not amend the no fixed N sentence above: the count is a floor the evidence must clear, and the three gates still decide.)
The abstraction must remove more complexity than it introduces. If callers still need to understand or restate the protocol’s internals, the extraction failed.
It must own a real invariant. Helper behaviour is not enough; the compound centralizes something every caller would otherwise have to re-prove.
Callers bind parameters, not behaviour. Adoption replaces protocol prose with a small declarative dependency plus caller-specific bindings — the act’s key, the constituent commit call, the bound, the pairing field, the identity or none.
Responsibility becomes clearer, not more distributed. One invariant family has one obvious owner.
Do not abstract away meaningful differences. Similar syntax is not sufficient where recovery, durability, trust, or failure semantics differ; those are separate compounds, or declared deviations, never a wider contract.
Require deletion as evidence. A new compound materially removes duplicated prose, state, checks, models, and recovery machinery from its adopters — measured, in bytes, by tools/survey/protocol_prose.py, before and after.
Keep deviations explicit. A caller that needs behaviour outside the common contract declares the deviation rather than expanding the abstraction until it is universal and vague.

Stated simply: a higher-order composition earns existence when several compositions repeatedly implement the same invariant-bearing protocol, and extracting it makes those compositions materially smaller while moving the invariant and its proof burden to one place. This is not a class hierarchy. Composition is recursively closed — a composition may itself be composed through a declared contract without exposing its internal atoms — and the principle is closer to chemistry than to object-oriented design: discover a recurring stable compound, name it, specify its properties, reuse it; do not invent one because several things happen to look alike.

Worked evidence — the recoverable invocation (2026-08-30). The survey the seventh rule names, run the day the test was written: twenty compositions carry three or more of the six components, the protocol prose totals roughly 920 kilobytes, and its share of a body runs from 8% (Privileged Access Provisioning) to 55% (Actor Suspension); nine carry all six. The exactness clause splits them. Fourteen share one problem exactly — an act committed in a constituent store and journaled through the Audit Trail substrate, attested, sealed, and retained under a purge horizon, with a recovery identity that writes when the human is gone — and clear the floor nearly three times over; their extraction is a decision the gates make, not a question of evidence. Four share a different problem — the same act shape journaled through a bare Event Log, with no attribution and no horizon (Authenticated Actor, Compensable Workflow, Idempotent Reservation, Preference-Aware Notification Fanout) — and sit one short of the floor, which is where they belong: their legs differ (one evicts, one redisposes, one reports, one has no leg at all), and whether they share a problem or a shape is what the fifth instance will say. Audit Trail is neither: it is the first group’s journal, and its own reconciliation is the one instance that cannot adopt what it provides. The two atoms that carried the shape (Clinical Observation, Medication Order) closed it by refusing to have a leg at all, and are not adopters. The compound is stable enough to specify now because its three revisions in one day — where the lease starts, what a non-lease host does, whether expiry stops writes — were each forced by a closure check rather than chosen; it is specified once, modeled once (two processes over one act), gated once, and adopted by one caller before the other thirteen, so the deletion count is measured on a real adopter rather than estimated. Roadmap methodology debt #20 carries the candidate.

A sibling boundary error EOS also owns is capability mis-attribution: an invariant or action that pins a capability on a constituent which does not expose it. The capability is real and emergent, but it belongs to a composition-introduced surface or a not-yet-extracted atom — not the constituent it is named on. Treat it like over-absorption in reverse: surface the real owner and declare the dependency there (see Capability provenance).

Time: 10–20 minutes once familiar with the existing atom catalog. Faster as the catalog grows — a quick scan against existing atoms surfaces most over-absorptions.

Personal Todo example. First-pass identity policy was absorbed in-pattern as a 24-hour deletion record. Pass 2 caught it: the same responsibility appears in comment double-post, payment idempotency, newsletter double-subscribe, form submission. It is not a property of Personal Todo — it is its own concept. Extracted as Duplicate Prevention. Personal Todo got cleaner; three other concepts now have a place to compose from.

Pass 3 — Adversarial scrutiny (Linus mode — named after Linus Torvalds, creator of Linux, known for blunt and unsparing code reviews)

What it checks. Read the spec like someone with low patience for hand-waving. Look for muddled thinking, decisions deferred dressed up as deliberate ambiguity, marketing claims without justification, examples that exercise only happy paths, invariants that aren’t actually invariant.

What it catches. Hidden decisions and sloppy thinking. The load-bearing decisions that have been pushed below the surface where they don’t have to argue for themselves.

How to run it. Adopt the posture of a senior reviewer who is allergic to abstraction-as-evasion. Sample questions to ask of every spec:

Identity. What concretely is the identity model? Is identity an opaque id, or is it a property like name or description? What happens if the identity-property changes — is that the same entity or a different one? Pick a side. State it.
Action signatures. What does each action return on success? On failure? What are the rejection reasons, named?
Primitive policies. For every string, number, date, identifier in the spec — what are the rules? Empty allowed? Whitespace? Unicode normalization? Length cap? Trim? Case-sensitivity?
Invariant precision. Are invariants (rules that must always be true, no matter what) stated with proper conditional structure when terms are optional? A chain inequality a ≤ b ≤ c is wrong if any term may be undefined.
Examples. Do they exercise rejection paths, edge cases, and the explicit non-goals — or only the happy path?
Deferred responsibilities. Are concurrency (multiple operations happening at the same time), atomicity (an operation either fully completes or fully fails — no in-between), clock semantics (rules about where timestamps come from and whether they can be trusted), and persistence named explicitly as out-of-scope, or implicitly assumed away?
Marketing. Does the spec claim it extends or is informed by or is built on something? Is the claim accurate, or sleight-of-hand papering over a different model?
Atomicity. Are state transitions atomic? What about a crash mid-transition — is an invariant violated? Whose problem is that?
Time. Where does now come from? Whose clock? What about skew, monotonicity, timezone?
Cross-references. Does every step, invariant, or claim that depends on content defined elsewhere name that section explicitly? Does every section that defines a mechanism used by another section get named by those users? Implicit “you know where to look” is a finding — all references must be explicit in both directions.
Logic confinement. Does any action embed async work, IO, crypto, or clock reads inside the core transition? Time, identity, and cryptographic material must be injected inputs, not internal calls. A transition that generates now or a random id inside itself is non-deterministic — flag it. See Logic Confinement Principle in execution-contract.md.
Relations. Does every relation a composition introduces across its constituents (containment, ownership, membership, hierarchy) declare its cardinality — one-to-one, one-to-many, or many-to-many — and the modality of each side (mandatory / optional)? Modality is asserted at quiescence, modulo declared compensation and the retention horizon: a binding’s orphan may be reachable-but-surfaced under partial failure (state it as safety + liveness, not a static “always both sides”), and may degrade to bound-or-honest-destruction past the horizon. Is the relation’s state classified per execution-contract.md §Composition state — a derived index (the default; the inverse is rebuilt from the forward references) or extraction-pending (state carrying truth no constituent replays — an unnamed atom to extract; there is no composition-owned middle)? An undeclared cross-constituent relation is where orphans, dangling references, and drifting inverses hide. A relation may also be self-referential — a constituent related to its own kind (a containment hierarchy, a bill-of-materials, a grouping) — which additionally requires acyclicity / well-foundedness: no record is its own ancestor under the transitive closure (the cycle a cross-constituent relation cannot even form). The required-invariant forms this pass checks for — referential integrity, orphan-freedom, inverse consistency, and acyclicity — are the canonical templates in spec-format.md §Structural-relation invariant templates: this pass owns the check (declare the relation’s shape; carry the templates that shape requires), spec-format owns the forms.
Sweeps. For every reconciliation leg: what does it do to an invocation that committed its first write one second ago, and to one whose events have aged past the audit horizon? Is the correction it fires reversible by the constituent it fires against? — §A reconciliation is bounded at both ends.
Pairing. Given two invocations of this action against one subject, which intent record answers for which outcome? What does the sweep do when it cannot tell? — §Intents pair with outcomes.
Recovery. Who writes each recovery record, under what identity, from what source — and what happens when the source is gone? Does re-invocation reach the step that failed, or die on an already-* arm before it? — §Recovery commits under a declared service identity.
Arms. For each mapped rejection arm, which constituent step failed and what is on disk when it did? Is the retry safe on every step the arm covers? Is any arm declared unreachable by an argument that names fewer steps than the constituent has? — §A transcribed rejection arm keeps its payload.
Cadence. Which seal cadence does the example assume, and what does the verification return under the other one? — §A seal presentation is keyed by log position.
Horizon. For each derived element, what reads it after the purge, and does that reader know the element is no longer derived? — §A derived index splits at the horizon.
Writers. What does this invocation do at bound + 1, when the leg has already read its act as an orphan? What do two runs of the leg do at once? — §A compensator is exclusive.
Purged. Present this action a record the substrate purged yesterday and read the step list: which step answers, and is it the constituent’s? — §Lawful destruction is answered before absence.
Envelope. Which is larger, the intent or the outcome, and which was sized against the cap? What does the caller do when the outcome is refused after the commit? — §An outcome is sized before the intent.
Arithmetic. Pick a bound, a cadence, a latency and a window that pass the check as written; does an orphan created at t close inside the window? — §Liveness is arithmetic.
Clocks. For each comparison in a sweep or a resume arm, whose clock stamped each side, and what does a skew of one bound do to the decision? — §A stamp from another seam never decides a write alone.
Caller. For each code the signature exports, what does the caller do next, and is that safe at every step that lands the code? — §A composition’s own rejection arm carries the retry bit.
Provenance of uses. For each read, enumeration, durability claim, critical section, clock, and uniqueness scope the steps exercise, which line of the constituent’s contract grants it? — §Capability provenance.

Adversarial postures (run all three). The questions above check topics; these check the spec from a hostile stance, and catch what a topic-checklist misses:

The cheapest-compliant implementer. “Read this as someone trying to ship the cheapest possible implementation that still technically satisfies every sentence.” Whatever they could get away with is an under-specification — close it.
Two engineers who dislike each other. “Find any sentence two senior engineers who want each other to be wrong could read two different ways.” Each such sentence is a determinism leak — pin the reading.
The unstated-assumption hunt. “Name every implicit assumption about clocks, ordering, or identity the spec relies on but does not state.” Each one is a hidden load-bearing decision — surface it or name it out-of-scope.

Time: 30–60 minutes for a thorough pass. The most labor-intensive of the three.

Personal Todo example. Surfaced five gaps in the simplified post-Pass-1-and-2 spec: identity model muddled, add return value unspecified, description rules unspecified, timestamp monotonicity (the requirement that timestamps always move forward, never backward) malformed (chain inequality with optional terms), examples were happy-path only. All five fixed in a third revision; three additional responsibilities (concurrency, atomicity, clock semantics) named as explicit out-of-scope rather than fixed in-pattern.

Formal models — the parallel verification surface

The three passes above operate on structured English. They catch ambiguity, incompleteness, over-absorption, and hidden decisions — the classes of gap a careful reader can frame as a question. They cannot catch the class of gap no reader thought to look for. That class is what formal models exist to catch.

A pattern may carry one or more formal-model siblings — .als for Alloy, .tla + .cfg for TLA+ — in the same directory as its canonical .md. Alloy checks structural invariants via bounded exhaustive search; TLA+ checks behavioural sequences via exhaustive interleaving under TLC. Both run at design time, before any implementation exists. Both treat the canonical English as the source — the formal artifact is a validator of the spec, not a replacement for it.

Formal models complement the three passes; they never replace them. Whether one is a prerequisite for grounded is no longer left implicit — it is decided by the formal-layer vote (below), cast and recorded for every pattern. When a model exists it is a first-class artifact in its own right. The Alloy model for Attributed Permissions Admin surfaced Invariant 7 (Attestation Exclusivity) after sixteen prose-review findings had already closed, because no human reviewer thought to ask could an attestation be used twice? That is the load-bearing contribution: the formal layer asks questions the prose layer cannot frame.

Findings from formal models are recorded in the commit message that lands the model, in the same arc as Pass 1–3 findings; the Ledger’s formal: line names the files and the verification date. The entry must carry plain-English summary sufficient for a reader who does not know the tool — what the artifact is, where it lives, what invariants it checks (named, not by syntax), the bounds or scope used, any deliberate scope exclusions and why, and the result. See contributing.md §Formal-model artifacts for the full convention: location and tier discipline (spec-layer artifacts; not in demos/ or build folders), base TLA+ as the default flavor (PlusCal only when intra-action protocol semantics genuinely warrant it, and defended in the commit message where used), and the human-readability requirement (every formal construct annotated in plain English). The artifact-side annotation and the commit-message summary together discharge the minimum-formalism principle’s accessibility contract — the formal layer is free to use the most expressive tool that earns its keep precisely because the canonical English carries the bridge to every other reader.

The English/formal SSOT contract

The canonical English spec is the single source of truth. A formal model is a derived artifact — the same ontological status as generated code in the library’s thesis (code is a build artifact; the spec is canonical): the model is a second build artifact, lowered from the same English source, whose job is to prove the source’s load-bearing claims hold under exhaustive search or interleaving. It is a validator and a discovery instrument, not a second source of record. This holds along the library’s compile-to-binary roadmap, where the pipeline is English (source) → formal verification (gate) → binary (output): both the model and the binary are derived from the one English source, and the formal layer is the type-checker of the compiler — the proof-carrying gate that refuses to emit a binary when the source’s stated invariants do not hold. Compiling meaning directly to a binary reinforces English-as-SSOT (one source compiles) and requires the formal layer (the source must be provably deterministic enough to lower). It is both, never either.

Where the protocol lives (2026-08-30). The contract above says what each layer is; the campaign of 2026-08-29 and 2026-08-30 said where the boundary between them had drifted. Twenty-five fresh-reader gates and closure checks ran in two days, none returned clean, and of the forty-five foundational findings a second reader confirmed, most were not wrong semantics — they were interleavings: a second writer landing an outcome beside the invocation’s own, a stalled invocation waking after the reconciliation had compensated, a lease edge, a zero-match landing, a purged verdict reached after a membership check. That is the class a formal layer exists to find, and it found none of them, because the models had been handed a protocol with the leg absent, the invocation as one atomic step, and no crash — debt #19’s the model proved what it was told, seen from the other side. The English layer was not too large because it held too much semantics; it was too large because it held the protocol, where the interleaving space is unbounded and every fix adds surface (the files grew fifteen to thirty percent per round). The correction is a boundary, not a rule: the protocol — the intent and outcome pair, the section and its lease, the bound, the reconciliation with its edges, the positioned code — belongs in the formal layer, carried there by a compound specified once with a model that has two processes over one act, the invocation and the leg. What stays in an adopter is bindings and the semantic judgment only a human can make: what the act means, which store is authoritative, what a caller may rely on, what must be retained. The measurable is the protocol prose per adopter (tools/survey/protocol_prose.py), falling to bindings. The first result, the same day: the compound’s model landed — five components over one act, two sweep runs, time explicit — held, rejected three twins, and corrected the prose in two places five fresh readers had passed: the section host must not release on a holder’s death, and the closure window must budget one dead run. The model also found the sweep’s lower edge is not what forbids the second writer — the section is — which no reader had questioned because the prose asserted it. And then the boundary was tested properly. The gate that followed the model — written to a success criterion fixed before the model existed, so it could not be fitted afterwards — returned three foundational findings, all of them timing, which the criterion had named as the shape of failure. Every one was a place where the model had been more disciplined than the page: it fused the lease check with the write, so the pause the page itself admits could not occur; it held the section until a write had landed, where the page releases on return; it gave the sweep the act’s bound as a lease, where the page gives it the longer of two. The correction was to the model, not to the prose — and the corrected model reproduced all three defects unaided, then found a fourth nobody had asked about: the remaining gate the page had leaned on for two rounds carries none of the one-writer invariant, and the fence carries all of it. The lesson is not that the boundary is wrong. It is that moving the protocol into the formal layer only helps to the extent the model is audited against what the page actually says, which is now a pitfall in its own right below. The refining tail did move as the criterion predicted — five semantic, six structural, and no binding findings at all: the adopter-facing surface, which is the compound’s whole purpose, held.

The dialect (2026-08-30). The same campaign made visible what the passes and the linter have been building: a structured English whose semantic core is gradually formalized. A construction becomes part of the language by one pipeline — stated as a rule on this page, given its tells, given a mechanical slice, landed in the linter advisory, promoted to gating when the sweep empties it — and the freeze discipline is what makes the pipeline work, since no grammar check can be written for a phrase that is still moving. The constructions that crossed that line in two days: recording-failure(step), (intent | outcome), <x>_completion_bound, between two edges, intent_event_candidates, proceed as landed, recovery_intended, one writer per act, the lease whose expiry is the terminus. The three checks that converged to zero (S-recording-step, T-seal-key, U-retry-bit) are syntactic slices of that dialect; the next slices can be structural — a <x>_completion_bound must exist wherever a leg does; an exported code landed on both sides of a commit must carry a position — and are writable only because the vocabulary is now fixed. The prose that remains after the protocol moves is the high-value layer, and its errors will look different from this campaign’s: fewer two writers and more this store was not the authoritative one — the ones worth a fresh reader’s full effort. That difference is the test of the boundary, and it is stated here before the first model that could pass it exists: a fresh gate run after a compound’s model lands should return mostly semantic and binding findings — meaning, authority, what a caller may rely on — and not another crop of lease, clock, and interleaving defects. A gate that still returns several foundational timing defects after the model has landed says the model absorbed too little of the protocol and the boundary sits in the wrong place. The first candidate to face the test is the Recoverable Invocation (roadmap debt #20), whose five prose gates on 2026-08-30 showed the category of finding change from protocol shape to timed concurrency — the phase change that says prose review has done its job and the model’s has begun.

The one carve-out. A property that cannot be stated in English without loss — true liveness, fairness, certain temporal conditions only crisp in LTL/TLA+ — is canonical in the formal assertion, and the English carries an explicitly-labelled gloss that points to it (precise statement: see assertion L3). That is the only place “English and formal together” is literally true. Everywhere else — the overwhelming majority of every spec — English is canonical and the formal model is derived.

The conflict protocol. A disagreement between the English and a derived artifact (a model counterexample, or two artifacts that lowered differently) is a diagnosis trigger, not an auto-fix. Three cases, three different repairs:

The model found a real counterexample the English permits. The English has a genuine logic gap — a missing precondition, an ordering that does not hold under interleaving. Fix the English, regenerate the model, re-verify. This is the model earning its keep; the finding lands in the commit message and is written back into the canonical English.
The model was mis-derived — wrong predicate, wrong bound, an action omitted from the translation. The English is correct; the encoding is wrong. Fix the derivation; the English is untouched. Never edit the English to match a buggy validator.
The English was ambiguous enough that two derived artifacts (model and binary) lowered it differently. Neither derived artifact is wrong — the source was under-specified. Disambiguate the English, regenerate both. Under the compile-to-binary target this becomes the dominant and most valuable signal: the compiler telling you the source is ambiguous before it ships.

The invariant across all three: you only ever edit the English to change meaning; you only ever edit the derivation to fix translation; and you never hand-patch a model to silence a counterexample. Triage which artifact holds the defect, then repair the right one. (Today some models are hand-authored, so “regenerate” is partly manual; the roadmap’s endgame makes the model and the binary both build targets off the English, at which point regeneration is a button and hand-maintained models are a transition-phase artifact to be eliminated.)

Why composition models do not import constituent models

Composition models sit beside their constituents’ models in the repo and never reference them — no .als opens another pattern’s module, no .tla instances one. That is architecture, not oversight, and not performance:

Formal models are derived per-pattern: each is lowered from its own pattern’s English and verifies only what that pattern owns. A composition’s model verifies the emergent surface against its constituents’ contracts — their named invariants and action signatures, assumed as abstracted structure — while each constituent’s own model (where its formal-layer vote is yes) discharges those contracts independently, with its own bounds and its own buggy twin. This is assume-guarantee layering. A derived artifact importing a derived artifact would build a shadow dependency graph that can drift from the canonical one in the English (§The English/formal SSOT contract: the spec graph, not the artifact graph, is the source of record); it would couple per-pattern tool choices the library deliberately keeps free — the flavor is picked per property class, so a constituent and its composition legitimately differ (Attributed Permissions Admin’s operational model is TLA+ while its Permissions constituent’s model is Alloy, and a .tla cannot instance an .als); and it would fail outright where a constituent’s vote was no and no model exists (Actor Identity grounds English-only, yet is composed by patterns whose models verify fine against its prose contract). Change propagation runs through the spec layer instead: a breaking constituent change triggers the constituent-change cascade (touch-triggered re-passes on every composition naming the atom) and the affected models are re-derived, in the multi-file refinement order — atoms before the compositions that name them. The state-space economics — abstracted contracts instead of multiplied constituent state machines — are a consequence of this architecture, not its reason.

The residual this leaves is rendering fidelity: a composition model re-declares simplified constituent structure, and if that rendering drifted from the atom’s spec, the composition model would verify against a phantom. The dependency-ordered refinement rule, the cascade, and §The coverage cross-check are the guards that own that residual. (Surfaced by issue #1, the library’s first external question; canonicalized 2026-06-12.)

The formal-layer vote

Before any pattern may declare grounded, it casts an explicit formal-layer vote, recorded on the Ledger’s formal: line and argued in the commit: does this pattern carry load-bearing temporal, ordering, concurrency, or safety claims that a formal model would verify — yes or no, with a one-line rationale? The vote is mandatory; the model is not. The vote enforces explicit-over-implicit on the methodology itself — the same information-management discipline the library applies to specs — so that no pattern grounds without the formal layer having been considered, even when the considered answer is no.

Vote = no. The pattern grounds English-only. The recorded vote is the evidence the formal layer was weighed and judged unwarranted (the minimum-formalism principle — do not put Alloy on Personal Todo). The English remains the sole SSOT and carries the full proof burden in prose, which is why an English-only pattern’s prose must be correspondingly rigorous and verbose: nothing downstream is checking it.
Vote = yes. A derived formal model becomes a grounding prerequisite for that pattern. Until it exists and verifies, the pattern is grounded (English) — formal layer pending: the three-pass baseline and Final Critique may be clean, but the load-bearing temporal claims have not yet been discharged on the surface best suited to them. The model’s findings are written back into the English per the conflict protocol; only then does the pattern reach unqualified grounded.

What “the model exists and verifies” means — the “model present” bar. A model file existing is not the formal layer being discharged. The phrase “model present” on a formal: line or in a vote means all of the following, on the record:

It runs green in the reproducible harness. The model passes tools/harness/ mechanically — not “ran once in the Alloy GUI,” not “a sibling Python checker agrees.” The committed artifact verifies on command. (A model that does not typecheck, or that a TLA+ checker reports NoInitialStates for, has not run — treat a typecheck/parse error or empty initial-state set as a hard failure, never a skip.)
It ships a buggy twin the checker rejects. Every model carries a deliberately-wrong sibling (<name>-buggy.tla / -buggy.als) that re-introduces a real hazard the spec defends against; the harness must reject it (TLA+: an invariant violation; Alloy: at least one check finds a counterexample). The twin is the vacuity guard — without it, a model that passes proves nothing, because a check can pass simply because its antecedent is never satisfiable. The twin proving the checker can fail is what makes the correct model’s green meaningful.
Its checks are non-vacuous. Every Alloy check is accompanied by a satisfiable run that exercises the same predicate (so the guarantee is quantified over a non-empty set, not vacuously true); every TLA+ model explores a state space that saturates at the chosen bound (raise the bound until the state count stops growing, then keep headroom — a passing run at an arbitrary low bound is not coverage). The tell to refuse: a check that holds while its paired run is vacuous — that guarantee is unenforced.

These three are the bar that the capability.als typecheck error, its vacuous transition layer, and privileged-access-provisioning.tla’s unrunnable request_to_chain all slipped past historically — each was recorded as “model present” while the artifact was not actually verifying anything. The bar exists to close that loophole: until a vote-yes pattern clears all three, it stays grounded (English) — formal layer pending, never grounded.

This vote replaces the prior rule that formal models were simply “not prerequisites for grounded.” That rule predated the shift toward the formal layer as the load-bearing verification surface; it left the decision implicit, which allowed a pattern with heavy temporal claims to ground without anyone deciding whether prose review was the right gate for it. The vote closes that gap without over-correcting into a blanket formal-for-everything mandate.

Formal-model authoring pitfalls

These are the recurring traps that surfaced authoring the formal layer across the library. Each one produced a model that looked verified while checking nothing, or a model that diverged from the spec it was meant to validate. They are authoring discipline, not tooling trivia; the tool-specific and operational specifics (checker dialect, harness provisioning) live in tools/harness/README.md. The single thread connecting them: a model that passes is worthless unless you have established it could have failed.

An action that fuses a guard with its effect cannot find a check-then-act defect (2026-08-30). If the model evaluates remaining >= write_bound and performs the write in one atomic step, no time can pass between them, and “a write issued inside the lease lands inside it” stops being a fact the model derives and becomes one it defines. The first Recoverable Invocation model did exactly that, held over 38,394 states, rejected three twins — and a fresh reader then found that the gate it had validated is check-then-act, which the spec itself says of relative timeouts two sections away. Split every lease, deadline, freshness and liveness gate into two actions, with time free to pass between them, and budget the pause rather than forbidding it. The corrected model reproduces the defect on its own and, with the remedy as a constant, says which mechanism actually carries the invariant: the fence does, and the gate — the thing the page had leaned on for two rounds — carries none of it.
Where the model is more disciplined than the spec, it is validating a better spec than the one anybody will implement (2026-08-30). This is the general form of the trap above and of debt #19’s the model proved what it was told: not a model told too little, but a model that quietly supplies the care a careful implementer would supply. The first Recoverable Invocation model held its section until its closing write had landed; the page releases it when record_action returns. It gave the sweep the act’s completion_bound as a lease; the page gives it max(completion_bound, closure_latency). Neither divergence is visible as an error — each reads as a sensible modelling choice — and each hid a real defect. Audit a model against the spec’s stated discipline, clause by clause, asking of every guard and every ordering: does the page say this, or am I supplying it? Where the model must be more generous than the page to stay tractable, say so and say why the gap cannot matter.
A property that is really liveness, checked as time-indexed safety, needs the stall budgeted (2026-08-30). A window (“closed within compensation_window”) stated as a safety property over an explicit clock is checkable — but in a model without fairness, “pause for ever” is always an available behaviour, and it starves the act at every window. Read naively that looks like an unmeetable bound; it is a statement about fairness. Give the pause an explicit budget, so exceptional pauses stay reachable (the safety counterexamples need them) while the arithmetic becomes measurable. Then derive the bound by controlled variation — hold everything fixed, move one term, measure the smallest window that holds — rather than reading it off the prose.
STANDING ROUND DISCIPLINE: the diff-derived obligation sweep (2026-09-10). This is a procedure every repair round runs, not a lesson to remember. Before a round is delivered, take the round’s own diff and list every obligation it introduced or removed — each new must, each inequality, each new key or argument, each new exemption, each deleted source, each renamed token, each newly declared piece of state. For each one, write down the sites that now have to honour it and check them: the worked examples that must satisfy a new inequality; the acceptance checks that must carry a new key; the modes the page already declares which need an exemption from it; the totality claims (“these four are the whole of it”, “six clocks meet here”) a new element falsifies; the signatures still exporting a code whose last producing source the round deleted; the sibling surfaces a rule was stated at one of. The list is short — a round introduces perhaps ten obligations — and it is derived from the diff rather than from the corpus, which is what makes it tractable and what makes it find things. A numeric subset is mechanical and worth automating first: every worked example’s bound values satisfy every inequality the page declares. Run this sweep in addition to the token sweep, never instead of it, and expect it to find more.
Sweep obligations, not tokens (2026-09-10). A repair round should end with a sweep, and this campaign has been sweeping the wrong thing carefully. The token sweep — is this identifier spelled two ways, is this code declared and never landed, does this registry entry have a marker — runs clean and is worth keeping, and it is blind to the defect that actually recurs. The recurring defect is an obligation introduced in one place and not carried to the places that must honour it. Supersession made transitive at one action and left pairwise at the three surfaces the same paragraph names. A duplicate key added without exempting the mode the page itself says produces duplicates by design. A configuration floor added, and the worked example eight lines below it breaching the floor. An acceptance check re-keyed onto a record only one of its two branches has a producer for. Sixteen of one gate’s nineteen self-inflicted findings were that one shape, and every one of them survived a token sweep that reported nothing. So the sweep to run is derived from the round’s own diff, not from the corpus: for each normative statement the round introduced — every must, every inequality, every new key, every deleted source — enumerate the sites that have to honour it and check each. It is a checklist, it is short because a round introduces few obligations, and it is the only sweep that looks where the defects are. A numeric subset is even mechanical: every worked example’s bound values satisfy every inequality the page declares is pure parsing and would have caught the floor breach outright.
The sweep finds neighbours, not only the diff’s own sites (2026-09-10). The discipline says the list of obligations is derived from the round’s diff, which is what makes it short enough to run. That is still right, and it undersells what the run produces. Enumerating an obligation forces you to name the sites that must honour it, and naming a site means reading it — at which point defects that have been sitting there for rounds become visible, because you are for once reading that passage with a specific question rather than for general sense. One round’s sweep, checking whether a new count reached the Summary, found the Summary and the Ledger both saying the formal model has five components and both then listing six, an operator having been added two gates earlier without the count moving. Nothing in that round touched either sentence. So do not narrow the sweep to a diff-versus-site test. The diff decides which passages to open; what you find once they are open is the sweep’s second yield, and on this evidence it is not small.
A delegated obligation needs a discharge record, or it is not delegated — it is dropped (2026-09-10). This corpus is scrupulous about admitting what it will not decide. An atom that will not settle a question says so and hands it to the composing layer; a composition that will not settle it says so and hands it to the deployment. Both halves are honest and both are load-bearing — and nothing tracks whether the last party in the chain ever decided. The instance: a permissions atom stated that duplicate active grants on one (subject, scope) pair are permitted and that “composing systems that intend to issue a single authoritative grant should guard against concurrent issuance”; the composition wiring it acknowledged that and re-delegated, naming the failure mode exactly — “accidental (a UI double-click before the first request returned)”; the deployment never picked it up, and a user reported an actor holding the same permission eleven times. No spec was wrong and the generated code was conformant the whole way down. That is a fourth class of finding, distinct from the three the frame metric carries — not an uncaptured requirement, not a transcription failure, not silent completion, but correctly captured, correctly delegated, never discharged. Its mirror is the render-local notes file whose findings about other renders never travel upward; together they say the return path is broken in both directions, and neither direction has a mechanism. The remedy is an artifact, not a check, and the third triage question is why: the decidable form — every delegated obligation is acknowledged by every composition that composes it — passes on the instance that motivated it, because acknowledging and re-delegating is acknowledgement. The hop that fails is composition → deployment, and the deployment is not in the corpus. So generate the transitive set of delegated clauses for a wiring as a deployment obligation sheet and make answering it part of shipping. The population is already there and nearly formulaic: 159 clauses across 40 files corpus-wide, 51 for one demo’s wiring.
A check is only as reliable as the surface it parses, and this corpus has measured that (2026-09-10). Eleven checks have been through the promotion pipeline. Sorted by what surface they read rather than by what they check, the outcome is unanimous: six of six promoted checks parse a place where the language was already controlled — the Ledger block, the Status line, the Terms registry, the signature fence, numbered steps, a bolded count claim — and five of five rejected checks were reading ordinary English. Each rejection was argued on its own terms at the time, and one sentence predicts all five. So the triage questions this page already carries — can a finding be dismissed without reading a claim, does the shape recur, does the decidable form cover the defect — have a cheaper predecessor: is the thing being read already written in a controlled form? If not, the honest options are to reject the check or to control the surface first, and the second is usually the better trade, because a controlled surface pays every future check as well as this one.

The corollary is a design instruction, not just a triage one. Where an obligation matters enough to check, make its sentence shape fixed before writing the checker. The corpus’s most reliable check is the one reading its most rigid container, and its most embarrassing near-misses were checkers built to infer intent from paragraphs. Control the surface, then check it — in that order, because the reverse produces a check that runs, passes, and lies.
Introducing a form is riskier than discovering one, so introduce it at one site (2026-09-10). The rule for a controlled vocabulary is that forms are discovered: a construction appears in prose, survives pressure testing, acquires a stable meaning, gets recognizable tells, becomes mechanically checkable, and only then becomes canonical. That rule has an exception and it is worth naming so it is not taken silently. Sometimes the concept is thoroughly earned — proven by findings across several rounds — while the phrasing never stabilized, because each round said it differently. Authoritative ownership of an obligation is the case here: three consecutive gates were about it, a frozen rule depends on it, and the corpus says it in those words eleven times in seven files out of fifty-seven. The words have to be introduced rather than found. When that happens, introduce the form at exactly one site — one spec, 2026-09-10 — and let it be used before it is propagated, because nothing has pressure-tested the phrasing and a form spread to forty sites before its first real use is forty sites to re-edit. A discovered form arrives already tested by the prose that produced it; an introduced one has to earn the same standing the slow way.
Where a claim lives in both a controlled form and a prose form, the prose is the half that rots (2026-09-10). This campaign now has two clean instances from a single round, and they point the same way. A page declared a configuration floor in prose as run_bound ≥ 2 × closure_latency + journal_write_bound, while the schedule enumerator that had refuted two earlier forms of the same inequality was filtering on max(completion_bound, closure_latency + journal_write_bound) + closure_latency — the correct form, since the holder a run waits out may be an invocation and not a sweep. The two disagreed for two rounds. Re-run under each, the prose floor admits 324 of 432 tuples and the window inequality breaches on 15 of them; the enumerator’s admits 288 and breaches on none. In the same round a fresh reader found that a duplicate-detection key had no exemption for the mode the page itself instructs to produce duplicates — while the formal model’s corresponding invariant had been written ServiceIdentity => ~secondOpened since the gate that added it, with the branch in it all along. In both cases the machine-readable artifact was right and the sentence was wrong, and in both cases the sentence was the newer of the two. The instruction is cheap: when a claim exists in a model, a checker, an enumerator or a fixture as well as in prose, diff them deliberately at the end of every round — not to see whether the code implements the page, which is the usual direction, but to see whether the page still says what the code checks. And the deeper reading is the one the controlled-language work is built on: the prose did not rot because anyone was careless with it. It rotted because nothing was reading it.
Measure the form, not the word — and say which you measured (2026-09-10). A count reported seven candidate controlled forms as earned, 45–57 of 57 files each, and a grammar proposal was drafted on it. The count measured English words two ways at once: it ignored case, so must, before and after counted, and it matched fragments and synonyms, so derived from (48 of 57 files) stood in for IS DERIVED FROM (7) and never for MUST NOT. Re-measured over the 56 files of atoms/ and compositions/ (the first count’s 57 also included the Recoverable Invocation draft), for the uppercase token in its controlled role, MUST is in 3 files, MUST NOT in 1, and every other candidate in none — while the same words in any case run from 6 to 55. The concepts are pervasive; the forms are absent. Both are true and they are claims about different things, and only one of them is evidence that a form has been discovered rather than invented. So a vocabulary measurement states its match pattern, its case rule and its file set, or it is not a measurement of a form — a rule about case alone would not have caught the fragment match. The deeper consequence is that earned cannot mean the token already appears in its controlled role — that is circular, since a controlled form exists to replace the free-prose expression of an idea and its token appears only once someone admits it. It has to mean the concept recurs and its free-prose expression has drifted or produced findings; recurrence alone is not a case, because the commonest words in this corpus are the ones carrying the least obligation. The failure here was mine and it was the campaign’s own signature shape at one remove: a number was produced, believed, and propagated into a roadmap entry and a language proposal without anyone asking what it had counted.
Extend an earned form’s field set before inventing a new one (2026-09-10). A round that needs to state four parallel facts about each of three things reaches naturally for a table. Before doing that, look at what the page already has: this corpus’s term entrys are aligned key-value blocks, a controlled surface that has been through the promotion pipeline and carries a passing check. Re-using that shape with a different field set — Instant / Minted by / Judged by / Value / Bound at beside the existing Kind / Member of / Role / Projection — costs a reader nothing to learn, keeps the parse surface the checker already understands, and does not spend the risk budget that §Introducing a form is riskier than discovering one is about. A new field set inside an established shape is a discovery; a new shape is an introduction. Reserve introductions for the cases where no earned shape fits.
Ownership has levels: extracting a rule leaves its bindings behind (2026-09-10). An extraction moves the rule to one owner and, by design, leaves the composing pattern its bindings — which key, which holder, how long, which arm maps to which code. That is correct and it is the whole reason the extraction shrinks so little. But a binding is an obligation too, and it can be owned in as many places as the rule was. One page bound a fence three times: one passage minted the instant with the allowance, a second said the fence carried the bare instant “which is where the first puts it” — an assertion about a passage that says the opposite — and a third cited the second. The atom was faithful, the rule was unambiguous, and a generator reading any one of the three built something different. So run the ownership count twice: once on the rule, once on each binding of it, and consolidate the bindings on the composing page even after the rule has left it. A rule with one owner and a binding with three is a defect wearing the composing pattern’s clothes.
Consolidating is a change like any other, and needs the obligation sweep run on it (2026-09-10). Creating a single owner for a scattered rule feels like the end of a repair, and it is the beginning of one. Three of one gate’s six foundational findings were the residue of two consolidations done the round before: an exemption that one of the old owners carried and the new owner did not, so the page went on mandating a state three surfaces report as a failure; a classification every sibling element carries that the new element was not given; and a binding never consolidated at all. The sweep’s question at a consolidation is not the usual one. What must change because of this is the question for a new obligation. For a new owner it is: what did the old owners say that the new one must now say? Walk each site the consolidation emptied and check that every clause it carried — the exemptions, the classifications, the degradations, the pointers — arrived at the new owner or was deliberately dropped. A clause that was in one of four owners and none of the citations is the most likely thing to be lost, because the three that lacked it look like agreement.
DRY on responsibility, not on nouns — and extraction is not the only cure (2026-09-10). The rule that decides what to pull out of a document is not this word appears a lot. It is: one authoritative owner per obligation. A repeated use of a concept is composition and is exactly what a library is for; a repeated ownership of an obligation is duplication, and it is the thing that propagates badly, because a rule stated in four places is a rule that four rounds of repair must each find four times. The test is concrete: when this obligation changes, how many passages have to change with it? One is healthy at any frequency. Four is the defect whatever the word count.

That test has two cures and this library had been reaching for only one. Where the obligation is owned by several patterns, extract it to an atom they cite — which is what happened with lease semantics, and the small size of the resulting shrink is the correct outcome, not a disappointment: most of the page’s remaining lease references are bindings and uses, and those are supposed to stay. Where the obligation is owned by several sites inside one pattern — a rule stated at an action, restated at a read, restated at an invariant, restated at an acceptance check — the cure is a single normative statement the other sites cite, and it needs no new file. One review round found a rule made transitive at one of its four owners and left pairwise at the other three; no atom would have prevented that, and one owner with three citations would have.

So triage an extraction candidate by counting owners first and files second: owners in more than one pattern → an atom; owners in more than one place in one pattern → consolidate and cite. Both are the same rule applied at different scales, and confusing them either leaves the defect in place or mints an atom nobody else needs.
Choose an extraction by where the obligations are now, not where they have been (2026-09-10). An extraction removes future propagation, so the evidence for it has to be forward-looking, and the cumulative record is a backward-looking measure that quietly recommends the wrong candidate. A concept was extracted from one composition on exactly the right kind of evidence — recurrence, four rounds of it, the largest single source of obligations across the page’s whole review history. Classifying every foundational finding by the obligation behind it showed the share was real and declining: two of three at the first gate, three of seven at the second, and by the sixth gate one of nine, because the rounds in between had argued that concept out. The concepts that had taken its place — a findings surface with a state machine no atom names, and the duplicate-detection machinery — were each producing two or three findings a gate and had no extraction planned. The cumulative record measures what has already been fixed; the current round measures what is still costing. So rank extraction candidates by the obligation sources in the last one or two rounds, and treat a candidate whose share is falling as one the review has already handled by hand.
Say a measurement is underpowered before you run it, not after (2026-09-10). An extraction removed 1.9% of a document’s body. At the document’s measured defect density — one foundational finding per nineteen kilobytes — that predicts removing 0.19 findings, which is noise. The next review could not possibly detect the change, and a result at the old level would have been read, by someone hoping, as evidence that extraction does not work. The arithmetic that says so takes one line and is available before the review runs, which is the only time it is worth anything: afterwards it reads as an excuse. When a change is too small for the metric you were going to judge it by, either make the change bigger before measuring, or change the measure to something the change can move — here, findings classified by which obligation source they come from, which is directly attributable and needs no volume at all. A metric that cannot see your intervention is not a neutral metric; it is a metric that will report failure.
A flat defect density means the repairs are growing the denominator (2026-09-10). Four consecutive gates on one page returned 6, 7, 8 and 9 foundational findings while the body grew from 119 KB to 164 KB. Divide and the picture changes completely: 19.8, 19.7, 19.1, 18.2 KB per foundational finding — flat. The page has a stable defect density and each round of repair adds surface, so the absolute count rises with the size and the effort is invisible in the number. That is worth checking on any long-running review, because the raw count reads as getting worse and the density reads as treading water, and they call for different responses. The one that follows from a flat density is that a page gets better only by getting smaller. Every finding’s fix is an obligation, every obligation has a propagation cost across the whole document, and past some size that cost exceeds what a round can pay — at which point the right move is not another repair round but an extraction: move the machinery the obligations are about into atoms the page cites, so that each round propagates across a smaller surface. Measure the density before deciding that a rising count means a worsening page.
Before building a check, ask whether its decidable form would have caught the instances that motivated it (2026-09-10). This is the third triage question and it belongs after the other two, because a shape can pass both and still be worthless. Two shapes had recurred often enough that the recurrence rule said build them, and both were built far enough to measure and then rejected — one of them by the sharpest result this pipeline has produced. A declared partition must add up had cost three hand-fixes and escalated to foundational, so the recurrence was undeniable. Its decidable form — every name in an a + b + c = d expression is a field of that action’s declared return — runs clean on the one instance that motivated it. The defect was never that a name was undeclared; it was that a path fell into no bucket, which is not visible to any parser. The check would have been built, would have passed, and would have prevented nothing, while carrying the authority of a gating check. The second shape, a retired token surviving at a call site, was decidable as a token and a token extending it across an underscore both live on one page: 178 instances across fifty-six files, of which one is the defect — the rest are the corpus’s ordinary naming convention (event_id and intent_event_id, actor_ref and acting_actor_ref), and telling those from a stale name is a question about what the names mean. So the full triage is three questions, and the order matters: can a finding be dismissed without reading what a sentence claims; does the shape recur often enough to be worth checking; and does the mechanical shadow of the shape actually cover the defects that made you want it? The third is the one that catches a check which would run, pass, and lie. Measuring it costs what the first two cost — one script, run against the instances already in hand — and it is the only one that can be answered before the check exists and not after.
A plausible remediation from a fresh reader is still only a hypothesis until the model distinguishes it from its siblings (2026-09-09). Four consecutive gates have now identified a real defect and prescribed the wrong repair, and the failure mode is consistent rather than careless: a reader who has found a genuine hole reasons from the sentence in front of them to the mechanism that would close it, and the mechanism they reach is the plausible one, not necessarily the load-bearing one. A window inequality was short by one term and the prescribed second term still breached on 396 of 432 parameter tuples. A read failure wanted its own code at one action and the prescription put it at four. A late-landing intent write looked like a missing lease gate, and the model shows the gate-off configuration holds under a fence while the gated configuration violates without one — the fence is the mechanism and the gate is neither necessary nor sufficient. So a prescribed fix is a hypothesis with a shape: it names a mechanism, and a named mechanism has siblings. Build the configuration where the prescribed mechanism is off and everything else is unchanged, and the configuration where its sibling is off, and let the checker say which one the property depends on. If the prescribed one holds with it removed, the prescription was aimed elsewhere. This costs two runs and it has changed the repair in four rounds out of four, which is the strongest argument this campaign has produced for the formal layer owning protocol mechanics outright: the model is no longer only verifying the specification, it is verifying the fixes the verification process proposes.
Splitting an action redefines every phase label it touches (2026-09-09). Raising a model’s fidelity is usually safe and this is the exception. An action that was atomic carried phase labels whose meaning came from the atomicity — “opened” meant the intent is in the journal, because issuing and landing were one step. Split that action into issue and land and the label silently keeps its old name and loses half its meaning: “opened” now means the intent was issued, and every guard that read it as landed is quietly wrong. In this campaign that produced an invariant failure attributed to the protocol for a full round of analysis before it was recognised as the model’s own. The earlier version could not have made the error, which is what makes it easy to miss: the regression is introduced by the improvement. So when an action is split, re-derive every guard that mentions its phases before running anything, and prefer renaming the old label to keeping it — a label that survives a split unchanged is a claim that nothing about it changed, and that claim is usually false. Increasing fidelity can introduce an abstraction bug, and the bug will look like a finding.
A model’s claim is bounded by its horizon, and the twin suite is what measures whether that bound is enough (2026-09-09). “All invariants hold” is never a statement about the protocol; it is a statement about the protocol within N ticks at these constants. That is usually harmless and becomes dangerous the moment the horizon moves — and it moves whenever fidelity rises, because more phases cost states. When a model that ran at seven ticks will only finish at five, the honest report is holds within five, and the temptation is to say holds and move on. There is a cheap empirical substitute for the monotonicity argument nobody wants to write: a twin that still fails at a horizon proves the horizon covers that property’s witness, because the twin exhibits the violation and the chain producing it therefore fits. So re-run the whole twin suite at every horizon change and treat the results as the vacuity evidence they are; a property attacked by no twin is checked at the horizon and claimed at the horizon, and should be written that way. Where a property’s witness demonstrably does not fit — one here needs a take, a read, a write landing past the lease, an expiry and a second take — give it its own configuration with a horizon that covers it, rather than stretching the main one until nothing finishes.
Count a shape’s population in recurrences, not in instances (2026-09-09). The population rule below stopped two checks by measuring how many times a construct appears in the corpus, and the measurement was right both times. The conclusion drawn from it was wrong for one of them, and the correction is worth more than the original rule. A declared partition — these five counts sum to that one — appeared once in fifty-six files, so it was triaged out as a hand-fix wearing a tool’s clothes. It has since been hand-fixed in three consecutive rounds and escalated from refining to foundational, because each round added a path to the thing being counted and the identity is only correct with respect to the paths that existed the day it was written. A retired token surviving at a call site went the same way: triaged out on one instance, then recurred, and the second time the round’s own sweep printed the offending line and the reader looked past it. So a shape that appears once in a static corpus but is rewritten every round on the page under active development has a population of one file and a population of four events, and it is the second number that decides whether a check pays. The test costs one extra question and no extra tooling: how many instances are there, and how many times has this shape been repaired before? A shape with two prior repairs needs no further argument. The deeper point is that the corpus is the wrong denominator for a document still being written — most of a check’s value accrues while a page is changing, and by the time the page is stable the check has little left to catch.
Write the probe for the second occurrence, not just the first (2026-09-09). Reachability probes stop a model from passing because nothing happened. They have a blind spot of their own, and it showed up one gate after they were introduced. Three probes asked whether a newly modelled writer ever holds the section, ever writes, and ever writes over an existing record; all three were rejected, so the component was reachable and its invariants were not vacuous. The next gate then found a defect the model could express and the configuration had switched off — a budget of one call, where the defect needs two, because it is a chain: a record superseded by a record superseded by a record. Neither the model nor the probes were wrong; the question was. Does it ever happen and does it ever happen twice are different questions, and in a concurrency model the interesting failures are almost never the first occurrence — they are the second one interleaving with the first, or the correction of a correction. So budget constants deserve the same treatment as remedy constants: raise the budget by one and probe for the second occurrence, or write down why one is enough. And when a probe holds, the question is not “did the configured limit change” but “WHAT IS ACTUALLY PREVENTING THE BEHAVIOUR?” — and the answer is rarely the knob named in the configuration. A probe for a supersession chain held twice: the first time because the configuration had pushed the sweeps out and removed the only thing that triggers the operator, the second because the operator’s phase machine was terminal — it never returned to idle — so the budget constant the round had carefully raised was never the binding constraint at all. Both times the report would have read “raised the budget, still holds”, and both times that sentence would have been false about the reason. This also names a third way a formal result can mislead — beside the behaviour never happened and the violation came from something other than the twin’s constant, there is the behaviour is expressible and a configuration constant excluded it, which reads as a clean pass and is the hardest of the three to see.
A new component earns its invariants only after a deliberate falsehood about it fails (2026-09-08). A model that adds a process, a writer or a path can pass on the first run for the worst reason: the new thing is unreachable in the configuration, so every invariant mentioning it is vacuously true and the run says only that nothing happened. This campaign was already caught this way once — a window invariant whose antecedent needed a horizon several times the one configured — and caught it by arithmetic rather than by method. The method is cheap: alongside the twins, write reachability probes, each a deliberate falsehood about the new component (it never holds the section; it never writes; it never writes over an existing record), and require the checker to REJECT each one before reading the main run as evidence. Three probes cost three configurations and one line of definition each. Pair it with the twin’s own guard: a twin whose constant is flipped inside an unusual configuration needs a PASSING SIBLING in that same configuration, differing by exactly that constant, or its violation is attributable to the configuration rather than to the constant. Between them the two rules answer the only two ways a formal result lies — the behaviour never happened, or the violation was caused by something other than what the twin claims.
When a model will not terminate, ask whether the excess behaviour is behaviour the spec actually admits (2026-09-08). The first instinct on a state explosion is to buy the space back: shorten the horizon, cut a budget, drop a process. Sometimes that is right. But an explosion is also evidence, and it is worth one question first: is the model letting this component act in situations the specification does not? Bringing an operator into a protocol model made it non-terminating, and the cause was that the operator could race the sweep to any open past-the-edge act — which the page admits in exactly one deployment, the report-only one where the sweep writes nothing. Making that deployment a modelled dimension both shrank the space and corrected the model, and the two were the same edit. A budget shrinks the space and leaves the model wrong; a fidelity correction shrinks it and makes the model right. The tell is whether the narrowing can be stated as a sentence from the specification. If it can, it is fidelity. If the only justification is “otherwise it does not finish”, it is a budget, and it belongs in the configuration with a comment saying what it costs.
An outside-the-frame finding names the instrument you are missing, not the model you should grow (2026-09-08). The frame metric sorts a formal-layer campaign’s findings into outside the model’s frame, inside and the model was wrong, and inside and the transcription was wrong. The second and third buckets have obvious responses. The first looked, for two rounds, like a standing argument for a bigger model — and it is not. A gate found that the closure window’s inequality under-charged a sweep death by a whole run; the finding was outside the frame because the model carries leases, fences and a window but has no backlog, and therefore has no term for a run’s own elapsed pass. Extending it to carry one would have multiplied the state space to re-derive a bound that is pure arithmetic over a schedule. What settled it instead was forty lines of Python that enumerate the schedules the page’s own timeline admits and report the worst landing instant. It took an hour, it rejected the correction the gate had prescribed (still wrong on 396 of 432 parameter tuples), and it produced a configuration obligation nobody had asked for: the corrected inequality breaches on exactly the tuples where the disclosed run bound is smaller than one lease plus one closure, so that obligation is load-bearing rather than hygiene — a fact discovered by the instrument, not decorated on afterwards. So read the outside-frame bucket as a shopping list of small instruments. A model is one instrument, not the instrument; a bound over a schedule wants an enumerator, an arithmetic claim wants a checker, and reaching for the biggest tool because it is the one already built is how a campaign spends a week to learn what an afternoon would have told it.
Fixing an instance of a shape is not the same as knowing the shape (2026-09-08). A gate found that one of this page’s actions returned a code the page’s own rule reserved for a different diagnosis — two unrelated meanings on one token, with opposite caller actions. The repair gave the second meaning its own code. The new code collided with a constituent’s code named two paragraphs away in the same document, and it took a hand sweep rather than a check to notice. The round had just written a paragraph explaining why two meanings on one token is a defect. A repair that closes an instance while re-committing the error a sentence later is the ordinary case, not an embarrassment, because the reviewer’s attention is on the finding’s site and the shape lives everywhere else. Two things follow. Sweep the shape across the whole document after every repair, not the site — one grep per token introduced. And treat the shapes a repair round re-commits as the strongest candidates the promotion pipeline will ever see, since they come with a demonstration that a careful reader misses them while actively thinking about them. (Both new candidates from this round were nonetheless rejected — one on population, zero instances in fifty-six files, one on the CONTAINS/CLAIMS boundary — which is the population rule doing its job against a shape that felt urgent.)
A check needs a population, not just a rule (2026-08-30). Decidability is necessary and not sufficient. Two more shapes from the same gate were triaged before any effort went into them, and both were rejected on frequency rather than on decidability. A declared partition adding up is decidable in a narrow form — every name in an a + b + c = d expression must be a field of that action’s return — but the expression occurs exactly once across fifty-six files, in the draft that produced the finding; a gating check for a construct with one instance is a hand-fix wearing a tool’s clothes. A retired abbreviation surviving at a call site is worse placed: the retirement is declared in prose (“written (kind, act_key) here and abbreviated act_key nowhere”), so reading it as a declaration is a question about what a sentence claims, and the check is blocked on a convention the corpus does not have rather than on parser cleverness. So triage a candidate on two questions before building it: can the rule be stated without the word claims, and does the shape occur often enough that a check beats fixing the instances? Measuring the second costs one grep and has now stopped two checks; it is the cheapest step in the pipeline and the one most likely to be skipped, because by the time a shape has been named it already feels like a rule.
The boundary’s real test is the dismissal, not the rule (2026-09-08). The CONTAINS/CLAIMS rule below is right and was stated one level too shallow. A later candidate passed every test it names — a code an action’s signature declares that the action’s own prose never lands — and it is as mechanical as a check gets: a delimited code fence against a delimited section, five self-test cases holding in both directions against a deliberately broken variant, and the largest corpus population any candidate in this campaign has had, twenty-seven findings across ten files. It was still rejected. Every one of the twenty-seven had the token elsewhere on the page, and every dismissal therefore required deciding whether a sentence written somewhere else covers this action: one composition lands a credential rejection for four actions in a single shared wiring paragraph that names all four; another lands a code in its term entry and nowhere near the action. Those are legitimate conventions, and no parser can tell them from the real defect the same check correctly found. So ask of a candidate not “can the rule be stated without the word claims” but “can a FINDING be dismissed without reading what a sentence claims”. A rule can be perfectly mechanical and still be a claims question in disguise, and the population measurement will not catch it — this candidate had the best population of any so far and the worst dismissal cost, which are not independent: a shape common enough to be worth checking is usually common enough that the corpus has grown conventions around it.
The linter can ask what a document CONTAINS; only a reader can ask what a sentence CLAIMS (2026-08-30). Three checks were prototyped against gate 8’s mechanically-decidable findings, and the line between the one that promoted and the two that did not turned out to be sharp and reusable. V-signature-alternation asks is there a separator between these two items — a question about the document’s contents, decidable with no notion of assertion, promoted the day it landed. W-step-reference asks does that action have a step 5 — the same kind of question, promoted (preventive; it has never fired). The two that failed both need to know what a sentence is asserting: E-code-not-in-signature cannot tell a code this action exports from a constituent’s code it is transcribing before mapping, and the mechanism check — does step 2 carry the thing the page says step 2 carries — cannot tell a sentence that claims step 2 does X from one that mentions step 2 and separately mentions X. On this page’s draft the second found the real defect it was built for, buried in a dozen false positives, which is exactly the trap: a heuristic that finds a true thing is still a heuristic. So the promotion test is not “did it find something real” but “can the rule be stated without the word claims”. Anything needing that word stays with the fresh reader, and that is the boundary’s real definition — not the topic of the finding, but whether deciding it requires reading a sentence as an assertion.
A checker’s finding being true does not make its rule correct (2026-08-30). The E-code-not-in-signature prototype reported that customer-onboarding’s initiate_onboarding lands invalid-credential without declaring it. The finding pointed at a real defect and the stated rule was wrong: the code is in the signature, and what is actually broken is that the block is missing a |, so invalid-request and invalid-credential sit on consecutive lines and the alternation reads as one malformed code. Correct result, invalid proof path — which is the same failure the formal layer had just spent a campaign fixing, in a new place. So a check earns promotion on its rule being right, never on a finding happening to be real; and where the two diverge, the right response is to split the check into the rule that actually holds (here, a pure-syntax alternation check, which promoted the same day) and the one that does not yet (own-export versus transcribed-constituent-code, which needs a semantic distinction the parser cannot yet draw).
A fixture pins nothing until you have watched the check fail with it (2026-08-30). Writing V-signature-alternation’s fixtures took three attempts to pin one guard. The first nested fixture passed under both the correct check and a deliberately broken one, because its groups each sat on a single line and were separated anyway; the second passed under both because the guard before the one under test already excluded it. Only the third — a nested group spanning lines whose continuation follows a line ending in neither ( nor | — made the broken check fail. Break the check on purpose and confirm the suite goes red, naming the fixture, before believing a green suite means the logic is held. A synthetic fixture that cannot fail is the vacuity trap wearing a test’s clothes.
Three layers, and a promotion pipeline between them (2026-08-30). The Recoverable Invocation campaign ran eight fresh-reader gates and two model rewrites, and what it converged on is a division of labour rather than a better prose discipline. The formal model owns concurrency, timing, crash and recovery, leases, fences and bounds — everything whose interleaving space is unbounded. The linter owns mechanically decidable internal consistency: whether a code an action lands appears in its signature, whether a mechanism a page names exists where it says, whether a declared partition adds up, whether an abbreviation an entry retires survives at a call site, whether two sections state the same rule. The fresh reader owns semantics: authority, meaning, trust assumptions, whether a binding really represents the adopter’s domain. Using a reader as a type checker is the most expensive way to run one, and for three gates that is largely what this campaign was doing.

The measurement that forced the third layer out: after each repair round, count the findings the previous round’s fixes caused — text the repair wrote, or text the repair made wrong. Across gates 7 and 8 that rate ran 35% and then 67%. A repair pass generating two findings for every three it closes is not converging; it is exploring a state space by hand. But the character of the caused findings had inverted by gate 8 — protocol defects in the first round, bookkeeping in the second, with ten of twelve mechanically decidable. A rising caused-rate on judgement-free defects is a tooling gap, not a discipline gap, and a rule the author already half-follows is evidence that it should stop being a rule.

So a finding is promoted rather than merely fixed, on the same path a language takes from convention to compiler error: fresh-reader finding → recurring mechanically decidable shape → linter check → corpus sweep → zero → gating. The sweep is the load-bearing step and the one that is skipped: a check that is not run across the whole corpus and driven to zero is a check nobody can turn on. Two cautions earned immediately. First, verify the instrument against a case whose answer you already know before its output is evidence — the first E-code-not-in-signature prototype reported thirteen findings of which ten were an artifact of a lazy regex, and noise gets waved through where a hard failure would not. Second, a check that fires for the wrong reason is still worth reading: the same prototype’s two surviving corpus findings were both false as described, and one of them was concealing a real defect — a signature block with a missing |, so an alternation silently read as one item.
A model’s NOT MODELED list is a prediction surface, not a disclaimer (2026-08-30). What a model excludes is exactly where the prose is still carrying protocol risk alone, and that is where the next fresh reader’s foundational findings will be. Measured: the gate after the Recoverable Invocation model was corrected returned seven foundational findings, and five sat verbatim on the model’s own exclusion list — skew, the lost-reply retry, retention purge, the bindings table’s lifecycle. So the list is maintained as a live artifact, written to be read as a forecast: each round, what the model newly excludes is what the next round is expected to find. Two consequences follow. Widen the frame selectively, at the exclusions the last gate actually hit, rather than trying to model everything. And record, per gate, where each foundational finding sat relative to the frame — three buckets, not two: outside the frame (widen it), inside and the model was wrong (the correspondence is failing — the serious one), and inside and the transcription was wrong (the model proved it and the prose failed to carry it, which needs discipline in the transcription rather than a better model). A gate returning more findings than the last is not a regression if they have moved from the middle bucket to the first; that is the boundary doing its work.
A remedy introduced into a page must be specified to the standard of its nearest established analogue (2026-08-30). A new mechanism added to fix a finding is itself unreviewed, and the page usually already contains a fully worked instance of the same concept. Recoverable Invocation gained a journal_fence in one paragraph while commit_fence sat three sections away with a declared conveyance, a named clock, and an edge widened by one allowance; the new fence had none of the three and produced three of the next gate’s seven foundational findings by itself — including a contradiction with a sentence in its own paragraph. Find the analogue first and write the remedy against it clause for clause, and then ask what the analogue did not need: here, the margin had to be minted into every instant the fence produces rather than only the lease’s, which the checker established only after the first correction still let the defect through.
Vacuity is the silent killer. A check passes whenever its antecedent is unsatisfiable — it then constrains nothing while reporting success. This is the failure mode behind most false confidence. Defend against it structurally, not by inspection: every guarantee gets a satisfiable companion (an Alloy run that exercises the predicate; a TLA+ buggy twin that the checker rejects). The diagnostic tell is a holds check paired with a vacuous run — when you see it, the guarantee is unenforced. (See the “model present” bar above; this is why criteria 2 and 3 exist.)
Static models lie about transitions. In a static structural model (Alloy snapshots), a “transition” is a pre/post pair representing one entity across a step — but a global identity-or-uniqueness fact (all disj r1, r2 | r1.id != r2.id) treats pre and post as two co-existing records and forbids them from sharing the id, making every transition unsatisfiable. The result is both vacuous demonstration runs and vacuously-passing transition checks (the capability.als defect). Fix: scope identity/uniqueness facts to the records co-existing in a store snapshot (a Store { records : set Rec } sig), so free pre/post transition atoms are exempt. A pre/post pair is the same entity at two times, not two entities at one time.
Derive idealizations; do not lag them with a flag. Specs idealize — membership auto-expires the instant a window passes; visible state is the replay of non-undone events. Modeling such an idealization as a separate variable that you remember to update creates a transient the spec forbids (the flag lags the clock), and the checker correctly rejects your correct model (the Duplicate Prevention case-2 mis-encoding). Fix: model the idealization as a derived predicate computed from the underlying state (Seen == everRecorded /\ now - recordedAt < Window), not as a tracked flag with its own update rule.
Do not beg the question. It is tempting to track the load-bearing invariant as state, updated by the same rule as the action guard — then the check is a tautology and the buggy twin can’t break it. Fix: derive the load-bearing predicate from the actual history (the log, the records, the insertion order), then assert against that. Then a buggy twin genuinely produces a violating history the check catches — which is the only evidence the check has teeth.
Saturate the bound; a low-bound pass is not coverage. A model that passes at an arbitrary small bound may simply be truncating the reachable state space before the interesting interleavings occur (the external-onboarding MaxClock=3 truncation to 44 of 172 reachable states). Fix: raise the bound until the explored-state count stops growing (the space has saturated), then keep headroom. Record the saturation point in the model config so the next reader knows the bound is deliberate, not arbitrary.
Conflate nothing between “exists” and “verifies.” A .tla/.als file in the directory, a model that ran once in a GUI, or a sibling checker in another language that “agrees” are all not the formal layer being discharged. Only a green run of the committed artifact in the reproducible harness, with a rejected buggy twin, counts. This is the discipline the “model present” bar encodes; the pitfalls above are the specific ways an artifact silently fails it.

The coverage cross-check (formal-layer rescan sub-step)

The “model present” bar establishes that a model verifies what it checks and that what it checks is non-vacuous. It does not establish that the model checks the right and the whole load-bearing surface. That residual — did a load-bearing invariant go unchecked, or get silently scoped out? — is the dominant property-fidelity risk, and it is the one the harness cannot catch on its own: a model can be green, twin-rejected, and non-vacuous while quietly omitting an invariant the spec calls load-bearing.

The coverage cross-check closes it. It is a structured read-and-diff, not new tooling or heavier search — deliberately cheap, so it rides the existing scheduled-rescan cadence rather than requiring a separate effort (inductive theorem-proving and large-scope blow-up are the expensive levers, and they chase smaller, lower-probability residuals; do not reach for them to discharge this one). A fresh-context reviewer (a fresh-reader AI is ideal — it surfaces the gaps the model’s author rationalized past) is the right executor; it is parallelizable across patterns.

Procedure. For each pattern carrying a vote-yes model, produce a coverage matrix: one row per invariant in the spec’s Invariants section (and per load-bearing claim named in the formal-layer vote), each classed into exactly one verdict:

covered — a named check/invariant in the model asserts it (cite the construct).
by-construction — the model makes it structurally impossible to violate rather than asserting it (e.g. an append-only log modeled with no remove action). Acceptable, but recorded as an assumption, not a verified property — because the model cannot catch a regression that a future edit introduces. Flag for promotion to a real check if the property is load-bearing.
out-of-scope (named reason) — deliberately not modeled, with the reason stated: a within-action atomicity claim (not an interleaving), a structural/relational property better suited to the other tool, a best-effort clock property, etc.
GAP — load-bearing, uncovered, and with no defensible out-of-scope reason. A GAP is a finding, routed through the standard channel (Pass-3-shaped) and blocking unqualified grounded until closed.

Add one bound-saturation line: raise the model’s scope once (N or MaxClock + k), confirm the explored-state count does not grow and the invariant still holds, and record the saturation point. This is the cheap guard against a low-bound pass that truncated the reachable space before the interesting interleavings.

Worked example — Party Identity. The formal-layer vote named Invariants 4 and 6 load-bearing.

Spec invariant	Verdict
2 — State membership exclusivity	covered (`Inv2_StateExclusivity` / `TypeOK`)
3 — Closed is absorbing	covered (`Inv3_ClosedAbsorbing`, history-flag form)
4 — Verified requires a passed verification after the most recent suspend	covered (`Inv4_PassedAfterSuspend`, derived from the log) — load-bearing, verified
6 — Append-only in insertion order	GAP → resolved. Was by-construction (the model only appended, never removed — an assumption, not an asserted check) despite being load-bearing per the vote. Promoted 2026-06-03 to an explicit check, `Inv6_AppendOnlyPrefix` (the log is a contiguous filled prefix); now covered.
1, 5, 7 — record permanence / event & field immutability	out-of-scope (immutability is structural; the relational/Alloy surface, not this interleaving model)
8 — state-change events auditable	out-of-scope (records-shape property, discharged in prose + Generation acceptance)
9, 10 — id stability / no id reuse	out-of-scope (structural identity; Alloy-class, not TLC-class)
11 — action atomicity	out-of-scope (within-action, not an action-vs-action interleaving)

Bound saturation: at MaxEvents = 6, 532 states; MaxEvents = 7 holds at 532 → saturated. ✓

Note what the cross-check surfaced on the very first pattern: Invariant 6, named load-bearing by the vote, was only by-construction in the model, not asserted — exactly the kind of silent partial-coverage the green checkmark hides. That is the finding the cross-check exists to produce, and it was closed the same way: Invariant 6 was promoted to an explicit checked predicate (Inv6_AppendOnlyPrefix) in both the model and its twin, the correct model still holds (532 states) and the twin is still rejected. Surfaced and closed on the first real run — the worked example is the cross-check earning its keep.

A blank fill-in matrix lives at tools/harness/coverage-matrix.template.md; one filled matrix per vote-yes pattern is the rescan artifact, and any GAP row is a routed finding.

Defending each claim in-line

The three passes are review tools — they catch gaps. Authoring well in the first place reduces what the passes find. The strongest writing discipline for architectural specs: every claim is defended in-line by the same paragraph that introduces it.

The four-step rubric (rubric: a structured guide for evaluating something):

State the principle. The architectural claim, expressed cleanly.
Name the likely objection or barrier. What would a senior reviewer push back on? What historical objection attaches to this claim?
Show the mechanism that resolves it. What specifically defuses the objection — a counter-argument, an architectural choice, a tooling capability?
Land the result. The principle stands, and the reader’s likely objection has been addressed without them needing to raise it.

Readers bring objections; in-line answers are more persuasive than principles that let objections surface unanswered. A claim that survives this discipline rarely needs Pass 3’s adversarial review to defend it — the defense is built in.

Worked example (from the-spec-layer.md):

Verbosity is the architecture of the bridge. Compress the language and one side loses access; preserve it and both sides — humans and machines — traverse the same canonical artifact. AI removes the historical barrier of too-long-to-read: the canonical text stays long because it must be verifiable; AI-generated summaries stay short because they only need to orient; diagrams support summaries without replacing the canonical text underneath. Readers choose the detail level appropriate to the task; the canonical layer keeps all levels consistent with each other.

Tracing the rubric through it:

Principle: verbosity is structural, not stylistic.
Objection: “long specs go unread.”
Mechanism: AI summarizes on demand; diagrams orient; canonical text stays verifiable.
Result: readers choose detail level; consistency preserved.

Apply to every architectural claim. Atomic-pattern specs, composition specs, methodology documents, and outreach material all benefit from this discipline. Where an architectural claim does not yet have a defended-in-line form, that is a writing gap to fix in the next revision — not a structural gap that needs a pass.

Capability provenance — a spec may claim, and use, only declared capabilities

FROZEN — 2026-08-30. The oldest rule on this page still open, stated 2026-06-08 and widened 2026-08-27 to reach uses. It is frozen from the third fresh-reader gates, which returned six foundational findings of this shape across five patterns — none a Rests on: line, every one a use — and mapped each to a surface the widening had already named. The rule’s text is complete for the evidence in hand; what the corpus lacked was the discipline of applying it as written, which a frozen rule supplies and an open one does not. The six shapes are recorded below as the tells for uses, added with the freeze; after it, a round that finds the rule inconvenient applies it or records a finding against the pattern, and reopening requires a case none of its sources or tells covers, recorded first.

An invariant is only as sound as the authority it quantifies over. The strongest form of the reference-graph discipline, applied to invariant dependencies: every clause an invariant rests on must trace to an explicitly declared capability — never to an implicit assumption that a constituent or substrate “can” do something it does not declare. This is no ambient authority — the core tenet of capability-based security — lifted to the invariant layer: an invariant may rely only on authority explicitly held somewhere in the spec graph.

A legitimate invariant dependency traces to exactly one of four declared sources:

a named constituent invariant or action — Audit Trail Invariant 3, AuditTrail.verify_record, a Tamper Evidence seal — something the constituent’s own spec states it has;
a deployment-declared configuration capability — a named, deployment-set obligation such as tamper_evidence_supports_partial_disclosure;
a composition-introduced surface — an emergent action the composition itself defines and owns (a verify_disclosure specified at the composition’s own layer); or
a declared dependency on a named peer pattern — an atom or composition the spec does not compose but explicitly names, where that peer genuinely declares the capability and the spec states the deployment’s obligation to wire it (a conditional invariant whose antecedent is “the named peer is wired”). This differs from an undeclared dependency precisely in being named: the owner is real and stated, not an ambient “the substrate can…”.

An invariant resting on anything else — “the substrate can produce…”, “the mechanism supports…” with no declaring source — carries an undeclared dependency, a foundational finding. The invariant’s Rests on: line is the provenance record where this is enforced: every entry must resolve to one of the four sources.

Declared is not verified. The rule governs provenance, not soundness. An invariant may rest on a declared-but-unverified capability — a deployment-asserted obligation the records cannot confirm — provided it is stated as an obligation with its verification routed to an externally-clearable check (see Generation acceptance). The rule forbids undeclared dependencies, not unverified ones; conflating the two would forbid every legitimately conditional invariant — one whose antecedent is a declared capability the deployment supplies, stated with the antecedent inside the invariant rather than as an after-the-fact weakening clause.

The rule reaches uses, not only claims — widened 2026-08-27, and the widening corrects a mistake this section made about itself. As first written, the rule policed the Rests on: line: the place where an invariant says what it depends on. That is where a mis-attributed capability is declared, but it is not where most of them are exercised. A composition consumes constituent capabilities at four surfaces that carry no Rests on: line and do not look syntactically like calls:

Rebuild procedures — “traverse the trail and take these fields from each payload” claims the payload is readable when it is read, which the substrate may lawfully deny past its retention horizon.
Generation acceptance checks — “for every X, confirm Y” claims the auditor can enumerate X, which the constituent may expose no surface for; and “confirm verify_record returns verified” claims a call shape and an outcome the constituent’s contract may not offer.
Enumeration and traversal logic — a read over a store keyed only by identifier, or over an index whose declared semantics are keyed lookup with rebuild-on-miss, where an enumeration has no miss to detect.
Atomicity and presentation contracts — “these writes commit together or not at all” claims a withdrawal capability over every member of the set, including members the constituent declares it cannot withdraw.

The test is unchanged; only its subject widens. A use is legitimate when the capability it exercises traces to one of the same four declared sources above. A use that traces to none is an undeclared dependency exactly as a claim would be, and a foundational finding of the same kind — the difference is only that nothing on the page announces it, which is why it survives longer.

The tells for uses (2026-08-30). Six shapes, each a foundational finding in the third gates, each an exercised capability the constituent’s own text declines:

A read keyed by a field the constituent does not index. “Enumerate the trail by data.record_id“, “select action_ref = X and this invocation_id” — Audit Trail declares a sequence-range read and routes payload-field selection to a forthcoming Reverse Index. The composition may filter a range in its own code and must say so; it may not call the filter the substrate’s read.
An enumeration over a store keyed by one identifier. Provenance is keyed by chain_id and declares no lookup by artifact_ref; a genesis orphan that must be found by artifact cannot be, and the leg that says it will is resting on a host index nobody declared.
Durability the constituent disclaims. Event Log: “persistence across process restarts is handled at the deployment layer.” A journal the composition rebuilds from after a crash is durable only under a host obligation the Configuration names.
A critical section spanning several constituent calls. Capacity Constraint serializes each call; a composition that reads, allocates, and reads again “under the pool’s serialization” has attributed a multi-call section the constituent’s own edge case sends to a Transaction composition.
A clock from a constituent that has none. now “injected by the Audit Trail substrate” — the substrate exposes no clock output; the reading is the composition’s own seam’s, and saying otherwise mislocates every stamp the composition writes.
A uniqueness scope wider than the constituent’s. Credential bounds effective-Active per (principal_ref, credential_type); a step that revokes “the actor’s active credential” has read per-pair as per-principal and leaves the second type authenticating.

A clean rescan is not evidence when the rule was pointed at the wrong surface. The 2026-06-08 corpus rescan below found zero undeclared dependencies across eighteen compositions, and that result was honestly obtained: every Rests on: line did resolve. Two months later, eleven fresh-reader gates run for an unrelated reason returned undeclared-capability findings in most of the patterns that rescan had cleared — constituent invariant and check counts that do not match the contracts, acceptance checks quantifying over records the constituent cannot enumerate, atomicity asserted over un-withdrawable writes, rebuilds sourced from payloads the substrate destroys. The rescan was not wrong; it was narrow. Treat a clean sweep as evidence about the surface swept, and record which surface that was — a result whose scope is not stated cannot later be told apart from a result that was simply mistaken.

Which pass owns it. Detection belongs to Pass 2 (EOS): attributing a capability to a constituent that does not expose it is a boundary error of the same family as over-absorption — the capability is mis-housed, belonging to a composition-introduced surface or a not-yet-extracted atom rather than the constituent it is pinned on; the fix names the real owner. The mechanical form is a Pass 1 reference-graph check: every Rests on: entry resolves to a declared source, exactly as every relative link must resolve to a real file. The mechanical slice of this has landed as tools/linter/lint.py’s check F-invariant-ref: an exact pattern name followed by “Invariant N” where N exceeds that pattern’s real invariant count is flagged (and the linter runs as a continuous-integration gate as of 2026-06-11). A second mechanical slice landed 2026-08-24 as tools/linter/lint.py’s check F-constituent-call: every qualified constituent call site in a composition body (Constituent.action(args), above the Status section) must name an action the constituent’s projected contracts declare, and every keyword argument passed must appear in that action’s declared parameter list — the drift class where an atom re-grounds, its contract moves, and the composers’ call sites silently go stale (see roadmap.md methodology debt #17 for the motivating findings). Positional-arity drift, renamed rejection reasons, and parenthesis-free prose citations of removed actions stay with the fresh reader. The fuller dangling-capability check — parsing each invariant’s Rests on: clause and flagging any referenced capability that names no declaring constituent invariant/action, configuration knob, or composition surface — remains future; capability-level mis-attribution stays the fresh-reader Pass 2 check described in the corpus-rescan paragraph below.

The mechanical slices the widening makes available (2026-08-27). Both were prototyped as corpus sweeps before being proposed as checks, and both police a use rather than a claim: (1) an all-or-nothing sentence whose member set names an audit write — the test that isolates the atomicity class from the nine patterns that use the phrase benignly; (2) a rebuild procedure that reads an event payload with no stated bound on its own totality. A third — distinguishing a keyed lookup from an enumeration over the same index — needs a parse rather than a match and is not yet available. The sweeps live in tools/survey/ and their results are recorded in roadmap.md methodology debt #19; the rule’s text widens first and the checks follow, so that a finding a check produces is attributable to a rule that already covered it.

Worked origin. Surfaced by the fresh-reader council on Immutable Transaction Ledger (Final Critique 5, finding Final Critique 5): Invariant 2 (verifiable partial disclosure) rested on “the Audit Trail substrate’s Tamper Evidence surface” producing a subset inclusion proof — but the Tamper Evidence atom verifies only whole record-sets, so the capability was pinned on a constituent action that does not exist. The fix re-declared the dependency at two of the legitimate sources (a composition-introduced verify_disclosure surface resting on a deployment-declared mechanism capability) and seeded a forthcoming Subset Proof atom as the eventual named-constituent home. An author reviewing their own work is structurally prone to this miss: the assumed capability feels declared because the author knows what they meant — the fresh-reader EOS seat, lacking that context, reads only what the spec actually grants. The rule is the generalization that makes the miss catchable before a fresh reader is available.

Corpus rescan (2026-06-08). A fresh-reader sweep of all eighteen then-grounded compositions against this rule found zero undeclared dependencies — the substrate-composition template the library already uses attributes capabilities to named constituent actions/invariants, so Immutable Transaction Ledger’s Final Critique 5 was the unique instance, closed when it landed. The sweep did pressure-test the rule itself: Privileged Access Provisioning’s Invariant 4 (cascading revocation) rests on Login’s revoke_sessions_for_credential — a peer composition PAP names but does not compose — which the original three-source list (written from the Immutable Transaction Ledger case) did not cover. The capability is real and the dependency is declared, so it is sound; the fourth source above was added to name the peer-pattern case explicitly. The rescan also surfaced one mechanical nit the lint.py check below cannot catch — Forensic Recovery cited “Event Log Invariant 1 (total order preserved)” when total order is Event Log Invariant 3 (Invariant 1 is append-only); the number was in range, so only a name-aware reader catches it. The division of labor is the lesson: the linter catches out-of-range invariant numbers; the fresh-reader Pass-2 catches name/number mismatches and phantom capabilities.

Durability boundaries — an atomic set may not contain a write the host cannot take back

FROZEN — 2026-08-29. Stated 2026-08-27 after the transactional atomicity over an append-only substrate class closed (three instances, three rounds, one protocol repair), and held open while methodology debt #19’s two remaining classes ran, in case either returned a case it did not cover. Neither did; both closed the same day. It is frozen with the other two #19 rules and the six rules stated 2026-08-29 from the second fresh-reader gates, under §Authentication precedence’s discipline: a round that finds it inconvenient applies it as written or records a finding against the pattern, and reopening requires a case none of its arms covers, recorded first.

The rule. Never place an independently durable write inside a host transaction’s atomic set. A write is independently durable when the store that accepts it declares it cannot be withdrawn and offers no synchronous rollback — an append-only audit log is the canonical case, and in this corpus every AuditTrail.record_action is one. A host transaction cannot enlist such a write, so it cannot roll it back, so a set containing it does not commit together or not at all. Where the append cannot participate, specify three things instead and specify them explicitly: the ordering across the durability boundary, the reachable partial states that ordering admits, and the recovery for each.

This is the fourth use surface of §Capability provenance stated at full strength. “These writes commit together or not at all” claims a withdrawal capability over every member of the set. Where a member is an append the substrate declares un-withdrawable, the claim is an undeclared dependency — and unlike most undeclared dependencies it is not merely unproven. It is false, and the composition’s own text usually contains the refutation.

Why this is not “state the guarantee more carefully”

An all-or-nothing claim over a durability boundary fails in one of two ways, and they need different treatments. The distinction is the campaign’s main result, because the two look identical on the page.

	The claim	The wiring	The treatment
Manifestation A	impossible to prove	the execution order already preserves safety; the reachable partial is the recoverable one	restatement — safety plus liveness, plus the mechanism that makes liveness dischargeable
Manifestation B	false	rollback makes a forbidden state reachable, and it is a state nothing can repair	protocol repair — move the durable write out of the atomic set, then restate

The discriminator: does anything durable end up asserting a fact the canonical state denies? A missing record is recoverable — append the seal, write the propagation event, retry. A false one is not: the append cannot be withdrawn, and manufacturing the missing canonical record afterwards fabricates the very evidence the record exists to protect. A composition cannot honestly restate its way out of a reachable state it has no way to leave. Where the reachable partial is a missing record, restate. Where it is a false one, rewire first.

Practically the question reduces to write order: if the durable append is last, the partial is a missing record; if the append can land while an earlier write is still revocable — including inside a transaction that may yet abort — the partial is a false record. That is why manifestation B is the one that hides: the wiring looks stronger, because it wrapped more in the transaction.

The three tells

1. An argument that reasons about the wrong member of the set. The most convincing instance in the corpus did not assert its atomicity, it argued for it: it observed correctly that one member was a recoverable store write the transaction could undo, and concluded the whole set was atomic. Sound about that member, silent about the append. Showing its work made it more persuasive, not less. When a spec defends an atomicity claim, check that the defence covers every member, especially the one it does not mention.

2. An escape hatch dressed as a caveat. “Where the stores cannot co-transact…”, “in the conforming case…”, “where the host cannot provide that atomicity…” — each reads as a deployment-specific edge and each names the universal case, because an append-only substrate never co-transacts. Qualifying a false claim makes it read as defended. In one instance a gate finding had actively pushed a spec deeper in, adding a conforming-case qualifier for symmetry with a sibling invariant, hardening a claim that was wrong on both sides.

3. The refutation already present elsewhere in the spec. In all three instances the pattern stated the fact that falsifies its own claim — in an edge case, a constituent’s contract, or the treatment of its intent record — a section or two away from where the claim was made. The principle is rarely missing; it is applied to one durable write and dropped for another. Before concluding a composition lacks the insight, search it for the sentence that already has it.

What the restatement costs, and the two ways to pay

Stating liveness raises the question the atomic claim suppressed: compensate with what. The material the failed write carried — a disposition set, a scope enumeration, a disclosure descriptor — commonly exists nowhere else, since it lived in the write that did not land and in the process that died. A restatement that stops at the sentence produces a liveness claim no deployment can discharge and no auditor can test, which is a worse artifact than the overstatement it replaces: the overstatement was at least falsifiable.

Carry the material if it is a computed verdict; carry the boundary if it is derivable from an append-only log. A verdict — a per-record disposition, a determination — is not in any log, so the intent record must carry it (or its digest with the universe cardinality). A set that is derivable — an enumeration over recorded events — needs only a fixed point to be derived at, and a durable write that already exists can serve as that point. The boundary form is strictly better where available: it costs no new field and no second copy, and a boundary cannot drift out of agreement with the thing it bounds.

Either way the liveness arm needs a declared window. “Eventually” is not an auditable guarantee, and a retry with no terminus is indistinguishable, from the records, from an orphan nobody is working on. A compensation_window configuration entry is what makes at quiescence checkable and gives the retry somewhere to escalate to; a reconciliation_cadence bounds detection, and a cadence longer than the window makes the window unmeetable by construction. Both are capability-provenance obligations of the composition’s own — the declaring source for what its liveness arm spends.

And the partial must be findable. The failure that returns surfaces itself; the failure that cannot return — a crash between the two writes — surfaces nothing, and that is the case the no unsurfaced partial arm is actually about. It requires a reconciliation scan that is mandated rather than implied, with a restart trigger and a declared cadence, and a join key it can run on. Check that the key exists before claiming the scan: in one instance the disclosure record carried no identifier tying it to its request, so the invariant named a scan that could not run.

What this does to the formal layer

A model that encodes the claim cannot falsify the claim. In all three instances the model committed every sub-write in one action, so the state that made the wiring unsafe was not merely unverified — it was unrepresentable. That is how the sharpest of the three passed a formal-layer vote, an author gate, a fresh-reader council and a clearance gate without anyone seeing it. When a model’s central action sets several variables at once, ask what interleaving that action forbids and whether the deployment can actually forbid it.

Two consequences for twins. A twin should be the composition’s own previous wiring where one exists — a repair whose necessity cannot be demonstrated is indistinguishable from a preference, and such a twin is also a permanent regression guard against the wiring being folded back. And a twin must be a plausible mis-implementation of this composition: where a safety arm is earned by a constituent’s guarantee (an earlier write that is terminal by the atom’s own invariant) no wiring of this composition can violate it, so it is a frame property here and correctly has no twin. The same claim is a frame property in one pattern and a reachable defect in another, and which it is depends entirely on whether the earlier write can be taken back — the discriminator again, arriving from the formal layer instead of the prose.

The mechanical slice

tools/linter/lint.py check P-atomic-audit: an all-or-nothing sentence whose member set names an audit write, with no acknowledgement in the enclosing block that an appended event cannot be withdrawn. The phrase alone is not the signal — nine patterns use it benignly over constituent-store writes only. It landed advisory, measured the class, and was promoted to gating on 2026-08-27 when the last instance closed and it fired zero times corpus-wide: a check becomes gating at the moment it stops measuring a backlog and starts defending a property.

Its regression guard is worth copying. The check’s first draft treated a hedge word as an acknowledgement marker, which silenced it on the two sites that motivated it — both their pattern’s declared formal-model subject, because a hedge word clusters around a pattern’s most careful claims, so a hedge-word suppressor is biased toward silencing the findings that matter most. That regression was pinned to those corpus sites, and the pins had to be retired as the sites were repaired — a corpus-derived pin is perishable by construction, dying exactly when the finding is fixed, and it creates a bad incentive besides, since the cheapest way to make it pass is to delete it. It is now pinned to synthetic fixtures instead: a decoy block that must fire and an honestly-restated block that must stay silent, neither tied to any corpus file, verified by reintroducing the original bug. Where a check’s regression can be stated without a victim, state it without a victim.

Which pass owns it

Detection is Pass 3 (adversarial) in practice — the question “what is the sequence in which this fails?” is what surfaces it — but the classification is Pass 2 (EOS): whether the reachable partial is a missing record or a false one is a question about where a capability lives, and the answer decides whether the round edits a sentence or moves a boundary. The mechanical form is the linter check above.

Worked origins (all 2026-08-27). Resolve a Person’s Data Rights Invariant 1 — manifestation A; order already correct; restated, with the disposition set carried in both intent records because a verdict is in no log. Capability-Backed Sharing Invariants 2 and 3 — manifestation B; the append sat inside the transaction, so an abort after it left a sealed disclosure event for a disclosure that never committed; rewired to durable intent → transactional domain mutation → durable outcome. Propagate Consent Revocation Downstream Invariant 3 — manifestation A, and the purest instance: both members irreversible, so there was never a transaction to enlist anything in; restated, with the propagation set’s boundary moved onto the existing intent event at no new field. Per-round detail lives in each pattern’s commit history and the class record in roadmap.md methodology debt #19.

A derived index is trustworthy only where a miss is observable

FROZEN — 2026-08-29. Stated 2026-08-27 when methodology debt #19’s enumeration anchoring class closed on all five known instances, and frozen with the rest of #19 on 2026-08-29. Written after §Durability boundaries rather than with its own class, which was an oversight worth keeping on the page: a rule that lives only in a roadmap debt entry is a rule on its way to being lost, and this one had been left there for two classes’ worth of rounds.

The rule. rebuild-on-miss is a keyed-lookup contract. It repairs a gap because a lookup that finds nothing is an observable signal — and every other read shape steps outside that contract, silently. A Contract classification of derived index, rebuild-on-miss invites a reader to conclude that losses are self-healing. They are, at the shape the contract names, and only there.

The shapes that step outside it, all observed:

enumerating the index — no lookup, so no miss; a lost entry is indistinguishable from a fact that never existed;
counting its entries — the same, with the loss expressed as a number that looks like evidence;
quantifying an acceptance check over it — the auditor’s own surface inherits the blindness, and worse, the check often quantifies over the very record whose absence defines the thing it is looking for;
reading a list under a key — the contract is honored at key granularity and violated at element granularity: a short list is not a miss, so the lookup succeeds and the answer is silently truncated;
rebuilding it while something depends on its current contents — the repair mechanism running over a window in which the index is the only record.

The treatment: anchor the read in the authoritative record, and use the index as a cache probed per element with rebuild-on-miss before concluding anything. That restores the keyed-lookup shape the contract is written for, one element at a time, inside a read anchored where the losses cannot occur. The in-corpus exemplar is Audit Trail’s unretained-event sweep, which says why in its own words: “a scan that read a lost entry as no retention exists would misdiagnose an index gap as a compliance finding — and then compensate it, placing a second retention over an event that already had one.”

But anchor carries an assumption, and both halves of it fail in this corpus. “Rebuild from the authoritative record” assumes that record is complete and current with respect to the index. Forensic Recovery’s index outlives its source, because a retention purge destroys the payload field the source enumeration is keyed on. Multi-Party Approval’s index precedes its source, because a chain record exists before its initiation event lands. Replacing the index with the enumeration loses real data in both directions.

Reconcile, never replace — and never let the repair mechanism outrank the record it is repairing. On the read side: compute both directions and report each divergence for what it is (an index gap the rebuild closes; a lawfully-purged payload, which is a fact). On the write side: a rebuild must be additive over the surviving store while any truth-bearing window is open. Anchoring is the special case that is safe only when the completeness-and-currency assumption holds.

Three tells, each seen in three or more of the five instances

1. The principle is already in the pattern, applied to one site and not its neighbour. Forensic Recovery anchors its residue collection correctly at step 6 and reads the raw list at step 4. Capability-Backed Sharing carries a four-case residue triage for one action and none for the other. Execute Gated Workflow’s keyed lookups rebuild correctly while its enumeration does not. Before concluding a composition lacks the insight, search it for the sentence that already has it — and when you find one, the repair is usually to extend a discipline rather than to invent one.

2. A check that verifies an index against its own source. For every entry, confirm its record exists finds dangling references and, by construction, cannot find omissions — so a clean pass is not evidence of completeness, and reporting it as such is how an audit surface acquires a blind spot it will keep. The direction that finds omissions runs the other way, from the source to the index.

3. A claim strengthened by an earlier campaign, resting on a set a later class shows to be incomplete. Execute Gated Workflow’s moot-gate plan was argued exact on the strength of a serialization rule — sound about serialization, silent about the enumeration that built the set. A correctness argument is only as strong as the completeness of the set it quantifies over, and an under-reported set is exact-looking and unfalsifiable, because the omission appears in neither side of whatever comparison the check performs.

What this does to the formal layer

A twin must be a plausible mis-implementation of this composition. Where a safety arm is earned by a constituent’s guarantee — an earlier write that is terminal by the atom’s own invariant — no wiring of this composition can violate it, so it is a frame property here and correctly has no dedicated twin; a twin that broke it would be asserting that a constituent breaks its own contract, which guards nothing. The same claim is a frame property in one pattern and a reachable defect in another, and which it is depends on whether the earlier write can be taken back. Record that reasoning where isolate.mjs reports an invariant as by-construction; the tool asks for the confirmation and the confirmation is the interesting part.

Which pass owns it, and why there is no linter check

Detection is Pass 3 (adversarial) — what does a lost entry do here? — and classification is Pass 2 (EOS), since whether the reachable partial is silent or loud, safe or unsafe, decides whether the round edits a sentence or moves a boundary.

No mechanical check was built, and that is a decision on evidence. Telling a keyed lookup from an enumeration over the same map is a parse rather than a match, and the closed class confirms the cost: two of the five instances are not enumerations at all — a list read under a key, and a rebuild colliding with a write window — so a test keyed on read syntax would have found three and pronounced the class clean. The classification sweep found five and reclassified the shape. What is mechanizable and worth building later is narrower and honest about being so: flag a Composition-state element classified derived index / rebuild-on-miss that is also declared truth-bearing in any window, which is the collision Multi-Party Approval’s instance was.

Derived state has a validity duration — say what it is, and what reads it

FROZEN — 2026-08-29. Stated 2026-08-27 when methodology debt #19’s retention horizon class closed on all sixteen known sites across ten patterns, and frozen with the rest of #19 on 2026-08-29. Its Tier 3 is restated as a rule of its own below (§A derived index splits at the horizon), because the second fresh-reader gates kept finding elements that had been given Tier 0 or Tier 1 and needed Tier 3.

The rule. A derived element’s recovery procedure is valid for a bounded interval; a claim that reads it has a lifetime; the spec is sound only where the first exceeds the second — so both belong on the page. A Contract classification of derived index, rebuild-on-miss says how a fact is recovered and never for how long, and a spec can be perfectly conformant to that vocabulary while asserting a derivability that lapses on a schedule it does not control.

What a purge actually leaves, because the class turns on it — corrected 2026-08-27 by a fresh-reader gate on Defensible Retention, verified against the substrate, and the correction is instructive. This section first asserted that a purge leaves “event_id and sequence_number, and nothing else”, reasoning from Event Log’s append(data) → event_id contract that action_ref and actor_ref ride inside the destroyed payload and go with it. That is wrong about the substrate, and it was wrong in the direction that tells an implementer to abandon a recovery path that exists. Audit Trail captures a destruction record carrying the (event_id, attestation_id) pair before the delegation runs, exactly so a purged event stays answerable, and the attestation carries action_ref, actor_ref and attested_at, of which all three survive readable — only its proof does not. The event’s own recorded_at is likewise a stored field the cascade never touches.

So the corrected statement, which is narrower and sharper. A purge destroys the payload, in its entirety — Event Log’s data field is the whole constructed object, so every binding a composition wrote into it is gone and no enumeration replays it. But the event’s identity survives: it can still be told that it was this composition’s, what action kind it recorded, who attested it and when. Identity survives; binding does not. The standard move — enumerate and filter by action_ref — is therefore not dead past the horizon; it must change surface, joining destruction records to attestations rather than reading payloads. What it recovers is the fact that the events existed and what kind they were, never what they bound.

Why the error is worth keeping on the page rather than quietly fixing. The overstatement made the class look more severe and was therefore comfortable — it argued for the treatment this section prescribes. A wrong fact that supports the conclusion you already hold is the hardest kind to notice, and this one survived a corpus-wide sweep, ten pattern rounds, and its own landing in this document, because at every site it was doing rhetorical work. It was caught by a cold reader who checked the claim against the constituent’s text instead of against the argument it served.

The four treatments, cheapest first

Ask them in order; the first that applies is the answer.

	Ask	If yes	Cost
0	Does the claim’s lifetime already sit inside the recovery’s validity?	State the comparison and stop.	a sentence
1	Is the recovered fact needed at all past the horizon? If not —	State the bound and why it suffices for the element’s one job.	a clause
2	Is there a second declared source, and is using it permitted?	Name it as the past-horizon fallback, and say which claim degrades.	a paragraph
3	Otherwise the fact is needed and nothing else holds it —	Split the classification by retention state (derived index while the payload survives, extraction-pending beyond) and carry the durability obligation that follows. Where the index does not already hold the fact, capture it at destruction time, before the delegation runs, and name the forthcoming atom that will own it.	a mechanism

Tier 0 is not a formality, and it is the most common answer. Login’s session map looks like every other instance until you ask who reads it: the cascade skips every non-Active session, so the only pairs whose recovery can change an outcome belong to sessions still inside their own TTL. The rebuild must stay valid for one session lifetime, not for the life of the credential or the trail — hours against years. Nothing further is owed, and the comparison is what proves it rather than what excuses it.

Tier 2’s two questions are genuinely two. Is there a second source is not may I use it. Defensible Retention falls back to Retention Window’s own records and gains a fallback that over-includes, which on a destruction gate can only refuse a purge — the loss direction is safe, so Invariant 9 survives and only Invariant 2’s scope claim degrades. Propagate Consent Revocation Downstream has the identical fallback available and forbids it: a store-sourced rebuild would resolve the bypassed identifier that audit-first resolvability must leave unresolvable, and the traversal/enumeration disagreement is the bypass detector. Taking it would delete a security property rather than degrade a scope claim. Where the traversal’s exclusivity is itself the guarantee, the fallback shape is unavailable.

And check that a second source is a source. Privileged Access Provisioning’s binding is recoverable from the approval substrate’s chain store — but that store is itself a derived index over audit events, so where the two compositions share one Audit Trail instance they share one horizon and both sides are erased by the same purge. A second source is only a second source if it is an independent failure domain. A constituent whose state is a derived index over the same substrate is not one — where both are erased by the same purge, you have two names for one failure domain, and it is the more dangerous mistake precisely because it reads as coverage.

Tier 3 is not the default. Audit Trail reaches it because nothing else holds its purged entries’ pair, so the pair is captured into the destruction record before the delegation runs. Forensic Recovery needs only the durability half, because the event_id is already written into its list at commit time — where the index already holds the fact before the destruction, the treatment is a durability obligation rather than a capture mechanism.

The deployment obligation none of the tiers supplies — it is orthogonal, not a fifth tier

Tiers 0–3 govern what the spec says, and whichever one applies, this is owed as well — it is not an alternative to them and not the second rung of the ladder. None of the tiers makes the horizon long enough. A composition whose claims read a payload must declare the ordering its deployment has to satisfy, name the invariant that spends it, and route the half it cannot read to the externally-clearable set. The recurring tell: a horizon recommendation stated for one reason while a load-bearing claim silently depends on it for another. Defensible Retention advised keeping the trail as long as the record for litigation defensibility; Invariant 9 depended on it because the trail is that invariant’s rebuild source. Propagate Consent Revocation Downstream advised the same thing for the same stated reason; three of its maps depend on it because the traversal is their only permitted source. When converting, give both reasons and say which one is load-bearing.

Ask what stops working, not only what evidence is lost. The sharpest consequence this class produced is not an audit gap. Past its horizon, Propagate Consent Revocation Downstream cannot resolve a consent_id whose grant event has aged out, so [Withdraw Consent] answers not-known for a consent that is still Granted: a live consent becomes un-withdrawable because the record of its grant aged out before the consent did — a GDPR Article 7(3) failure reached with no partial failure, no bypass, and no bug. Defensible Retention’s is a destruction gate reading a sibling set it can no longer rebuild. Availability and safety are both on this list, not just evidence.

The interval has two edges. Expiry is the common one. Multi-Party Approval is the mirror: its store is truth-bearing before its event exists, so a rebuild running too early destroys the only record. The general form is a validity interval, and both ends have produced real defects — a gate reading a set it could no longer rebuild, and a repair mechanism deleting the record it was repairing.

Which pass owns it

Detection is Pass 1 (GRID) in its mechanical form — a rebuild procedure that reads a payload is a reference into a store whose contract bounds it, and the reference graph is where a dangling one is caught. The classification is Pass 2 (EOS): whether a fact is derived or extraction-pending is a question about where it lives, and the answer changes at the horizon. The mechanical slice is tools/linter/lint.py’s Q-rebuild-bound, gating since 2026-08-27, with a recorded recall gap (it is line-scoped and keys on the literal *Rebuild procedure:* marker) that is the reason a classification sweep still runs before the check’s count is trusted: this class’s sweep found sixteen sites where the check saw fourteen, and two of the four treatment shapes came from instances the check cannot see.

A reconciliation is bounded at both ends — an age bound below, the audit horizon above

FROZEN — 2026-08-29. Stated when the second fresh-reader gates — gates run after a pattern’s open foundational findings had all been closed — returned the same defect shape in three of the first eight patterns sampled, each gated independently and each carrying a reconciliation the previous round had accepted. It is frozen on the day it is stated rather than left open, because the evidence it rests on is not one pattern’s archaeology but recurrence across independently gated patterns, and because a rule stated open is a rule the next round edits instead of applying. Unfreezing follows the same discipline as §Authentication precedence: a case none of its arms covers, recorded first.

The rule. Every reconciliation leg — a sweep, a scan, a comparison of one record class against another — declares the interval it runs over, and the interval has two edges the leg must name: an age bound below, excluding invocations that may still be in flight, and the audit horizon above, past which the record class it is looking for has been lawfully destroyed. A leg with neither edge does two wrong things at once, in opposite directions: it reads work that has not finished yet as an orphan and corrects it, and it reads history whose events have aged out as a crash and re-runs it.

The two edges have different sources and are declared differently. The age bound is a deployment obligation of the composition’s own — a Configuration entry naming the longest an invocation of the action may take between its first committed write and its last, read against the seam clock the invocation began under — and a leg examines nothing younger than it. The horizon is inherited: it is the retention policy of the audit instance the leg reads, and above it the leg’s missing half is not missing, it is purged, so the survivors on the other side are the truth-bearing class §A derived index splits at the horizon governs, not candidates for repair.

The tells

1. A correction fired from a comparison. “For every issuance with no completion, revoke.” “For every chain with no initiation event, treat as a crashed initiation and quarantine.” A leg that does something to the records it finds is the leg whose window matters, because a wrong window is not a wrong report, it is a wrong act — and the act is usually irreversible by the constituent’s own invariant. Read the comparison and ask what happens to an invocation that committed its first write one second ago.

2. “At quiescence” doing the work of a window. The phrase is correct and it is not a bound: an auditor cannot tell quiescence from a slow invocation without a declared duration. Where an invariant’s liveness arm says at quiescence and no Configuration entry says how long quiescence takes to reach, the arm is asserted, not checkable — the same defect §Durability boundaries names for compensation_window, arriving at the reconciliation instead of the compensation.

3. A check quantified over “all” of a purgeable class. “For every X event, confirm a Y event exists” is false on a schedule the composition does not control, because X and Y are purged on the same policy and not necessarily on the same day. The check needs the horizon in its own text, and a stated answer for the pair whose members straddle it.

What it costs

One Configuration entry per bounded action (a completion bound), a stated relation between the leg and the audit instance’s retention policy, and each leg restated in three arms: below the bound, examine nothing; between the bound and the horizon, the leg as written; above the horizon, the survivors are truth-bearing and the leg reports rather than repairs. A check that reads the leg widens its window by whatever read latency the deployment discloses — a subscriber read that lags the dispatch by a bounded interval is not a coverage failure, and the check that says so needs the interval on the page.

Which pass owns it

Detection is Pass 3 (adversarial) — what does this sweep do to an invocation that has not finished, and to one whose events have aged out? — and the mechanical form is a Pass 1 reference-graph check: every leg’s lower edge resolves to a Configuration entry and its upper edge to the retention policy it reads under. No linter check; the leg’s shape is prose.

Worked origins. Login (second gate, 2026-08-28) — the issuance-reconciliation sweep revoked in-flight logins, because nothing told it how long a login takes; fixed with a declared login_completion_bound below which the sweep examines nothing. Multi-Party Approval (second gate, 2026-08-29) — the initiation leg had no horizon, so every lawfully purged chain read as a crashed initiation and was quarantined; fixed by bounding the leg and the additive rebuild’s quarantine to chains whose initiated_at lies inside the horizon. Notification Fanout (second gate, 2026-08-28) — fired_at was claimed as the instant the subscriber set was fixed, which nothing takes or observes; restated as a lower bound, with check 1’s window widened by a disclosed max_read_latency on the subscriber read.

Intents pair with outcomes by an invocation identity the seam injects

FROZEN — 2026-08-29. Same evidence, same freeze discipline as the section above: four of the eight second-gate patterns returned a pairing defect, in four different disguises.

The rule. Where a composition writes an intent record and later an outcome, both carry one invocation_id — minted nowhere inside the composition, injected at the same seam as now (the Logic Confinement Principle), fresh per state-changing invocation — and every sweep join, every acceptance check, and every audit question that pairs an intent with its outcome pairs on that field. Where the pairing is nonetheless undecidable from the records — older records written before the field existed, a marker the deployment lost — the sweep names the candidate set rather than choosing a member, and closes the others as abandoned.

This is the generalization of a rule §Authentication precedence already states for bindings: whenever a check is claimed to verify an ordering or a binding, name the field on the record that makes it recomputable. What the second gates showed is that naming a field per check is not enough, because the field named is usually the wrong one — a per-case key on an action that is repeatable against the case, a per-subject serialization on a scan that can see a concurrent sibling’s records, an intent event id carried on some outcome kinds and not others. One key, injected, on everything, is what makes the join the same question everywhere.

The tells

1. The definite article. “The intent record” in a sweep, where the action can run twice against one subject. One stale intent then satisfies the check for an unbounded number of later acts.

2. A key that is narrower than the act. A join on case_id, record_ref, subject_ref, or (subject, initiator, scope) where two invocations can share it. The tell is a serialization argument — serialized per chain_id — offered as the reason the join is exact, when the scan the join feeds runs under a different key than the serialization does.

3. A recovery emission that matches on the subject. A sweep that re-emits an outcome with recovery = true because a record for that subject is missing pairs an intent with whatever outcome it finds, and under retry or concurrency it emits records that are false as written.

4. An outcome kind without the key. Where an action has several outcome payloads — the success, the refusal, the void — and the acceptance check’s join names a field, read every payload and confirm each carries it. One origin pattern had the field on its main path and on none of three branch payloads its own check joined over.

What it costs

One field on every intent and outcome payload, injected at the seam, and a join clause in each check that names it. No Configuration entry. Where the composition’s serialization is keyed by something the scan can distinguish — a chain’s own id carried as the constituent call’s reason — the same key serves both.

Which pass owns it

Detection is Pass 1 (GRID) in its mechanical form — a check that says pair, match, join, or for the corresponding names the field, and every outcome payload the action can write carries it — and Pass 3 (adversarial) for the two-identical-acts question: given two invocations of this action against one subject, which record answers for which? No linter check yet; the mechanical form is a payload-field presence test the linter could carry once payloads are written in one shape.

Worked origins. Defensible Retention (second gate, 2026-08-28) — intent/outcome pairing undefined, so the sweep re-emitted false recovery = true records under retry and under concurrency; fixed with a seam-injected invocation_id on every audit record and a sweep that lists attributed_to candidates where the pairing is undecidable. Customer Onboarding (second gate, 2026-08-29) — check 6’s join key intent_event_id was absent from three of the outcome payloads it joined over. Multi-Party Approval (second gate, 2026-08-29) — the sibling-safe scan withdrew a concurrently initiating sibling’s step, because the scan’s key and the serialization’s key differed; fixed by carrying the invocation’s chain_id as the submit’s reason. Capability-Backed Sharing (second gate, 2026-08-29) — the intent carried no disclosure_id and the disclosure record no token, so an unmatched intent could not be joined to its disclosure at all; the honest answer there was not a key but a downgrade — escalated, never sealed.

Recovery commits under a declared service identity behind its own intent record, and what cannot be re-derived is re-run

FROZEN — 2026-08-29. Stated from the second gates and from two first-round findings the same week that reached the same shape from the other side. The rule is the conjunction of three things the corpus already says separately — §Authentication precedence’s binding half, §Durability boundaries’ carry-the-material rule, and the Execution Contract’s classification of derived state — applied to the one action every regulated composition has and few had written down: the one that runs when the original invocation is dead.

The rule. Any constituent commit made outside the original invocation — a retry after restart, a sweep’s compensation, a cascade’s recall, a re-invocation on an already-* arm — runs under the composition’s declared service identity (a registered application_actor_ref and application_credential in the substrate’s Actor Identity registry), is preceded by its own recovery-intended record naming the invocation it repairs (the key of the section above) and what it is about to do, and writes only what it can re-derive from the constituent stores or the sealed trail. What it cannot re-derive it does not re-emit: the act is re-run through the action’s own idempotent re-entry arm, or escalated.

The three clauses each close a hole the others leave. Without the identity, the recovery record is attested under a human who was not present (the binding defect). Without the recovery-intended record, the composition’s own trail cannot show that the recovery was occasioned by a repair rather than by a direct call (the provenance defect). Without the re-derivability test, the recovery remembers — from process memory, from a presumed value, from the intent alone — and what it writes is evidence of an act whose content nobody can check (the fabrication defect, which the sealed record then protects forever).

The tells

1. “Re-emit the owed record” with no source named. Ask where the payload comes from. If the answer is the intent record, ask whether the outcome owns a datum the intent must not carry (§Authentication precedence, when the intent record should carry its plan) — a minted id, a verdict computed after the intent. If it does, the recovery cannot write the outcome; it can only re-run the act or say the act was abandoned.

2. Recovery attributed to the human. A sweep step that calls record_action(actor_ref = <the requester>, …) on a path where the requester’s credential is not in hand. The substrate will refuse it or, worse, a cached credential will let it through.

3. A re-invocation that dies on already-* before it reaches the step that failed. The action’s step list commits at step 5 and fails at step 6; the retry re-enters at step 1, hits already-closed at step 5, and stops. Every action whose later steps can fail after an earlier irreversible commit needs a re-entry arm that recognizes its own prior commit and continues.

4. A guard that rests on a transient. A provisioning step gated on an in-memory Approved that no rebuild reproduces means the recovery either cannot fire the step or fires it twice. The guard must be readable from a store the recovery can reach.

What it costs

Two Configuration entries (the service identity), one action_ref per composition for the recovery-intended record, an idempotent re-entry arm on every action with a post-commit failure step, and — the expensive part — an honest sentence per recovery leg saying whether its record is derived or re-run. Where a re-run is impossible and the record is not re-derivable, the leg emits an abandoned record under the service identity and the pattern’s liveness arm degrades to surfaced, which is what the records can actually support.

What this does to the formal layer

The recovery is its own action in the model, with its own actor, or the model cannot distinguish a recovery that repairs from a recovery that fabricates. A model in which the sweep sets the outcome variable directly encodes the fabrication as correct behavior.

Which pass owns it

Detection is Pass 3 (adversarial) — who writes this record, under what identity, from what source, and what if the source is gone? — and classification is Pass 2 (EOS): which of the recovery’s records are derived (re-derivable, rebuild-on-miss) and which are not is a question about where the fact lives, and the not-derivable ones are the ones that must be re-run.

Worked origins. Customer Onboarding (second gate, 2026-08-29) — the post-closure floor had no compliant recovery when the retention placement failed after the party was closed: cross-invocation constituent commits were the thing the action’s own text forbade, and re-invocation died at already-closed; fixed with the declared service identity, a customer-onboarding.recovery-intended record, and a re-entry arm. Login (second gate, 2026-08-28) — the recovery claimed to re-derive every owed record and could not re-derive the cascade’s own; fixed by writing the cascade’s join key into the Session record it revokes and, where a cascade died before completing, emitting credential_revocation_cascade_abandoned and re-running rather than re-emitting. Resolve a Person’s Data Rights (second gate, 2026-08-29) — the scan compensated intents that had no disclosure behind them, writing a sealed event for a disclosure that did not exist; fixed by conditioning the compensation on the disclosure’s existence. Execute Gated Workflow (2026-08-27) reached the same rule from a first-round finding: committed-but-unrecorded work is re-derived from the constituent stores, never remembered by the process.

A transcribed rejection arm keeps its payload and its reachability

FROZEN — 2026-08-29. Stated from four second-gate findings in three patterns, and from refining lines two other patterns already carried for the bare token (every substrate-arm transcription, five rejection sites). The refining lines were right and were being closed one at a time; the second gates showed the defect is foundational when the dropped payload decides whether a retry is safe.

The rule. When a composition maps a constituent’s rejection into its own, the mapping carries the arm’s declared payload — recording-failure(step), cascade-failure(step), mechanism-failure(reason) — and lands every arm the constituent’s contract can reach, including the ones the composition believes it has made unreachable. A bare recording-failure is not an abbreviation; it discards the one fact the caller needs to decide what is on disk.

The substrate makes the point concrete, and it is the substrate every regulated composition here writes to. Audit Trail’s record_action fails at step 2 (attestation) with nothing committed, at step 3 (append) with an orphan attestation, and at step 4 (retention placement) with the event already appended — so recording-failure(step-4) means your record exists; read its id back and clear whatever pending marker you hold, and a retry re-appends. Only the step-2 and step-3 arms are retry-safe. A composition that maps all three to one bare token has written a retry loop that duplicates outcome events under the failure it was written for. The same step is why invalid-request is never unreachable from record_action: step 4’s invalid-policy and policy-not-found arrive as invalid-request, and they come from the substrate’s own retention Configuration, not from the caller’s payload — a deployment fault, reached with the event appended. A composition that argues invalid-request cannot occur here because the payload is composition-built has reasoned about step 1 and step 3 and forgotten step 4.

The tells

1. A bare token on the left of a mapping arrow. `recording-failure` → `rejected(recording-failure)` transcribes the substrate’s arm and drops its payload in the same stroke. The linter finds this one.

2. “Unreachable here because …”. Every such sentence names the steps it reasoned about. Check the ones it did not.

3. A retry that does not ask which step failed. “On recording-failure, retry until the write lands” — correct for two of the three steps and a duplicate-event generator for the third.

4. A code in the prose and not in the signature. The signature block is the surface a caller switches on (§Authentication precedence, the signature block is where attention does not land). A landing described in an edge case for an arm the signature does not declare is a landing the implementer never sees.

5. Validation after the intent. An intent record written before the composition’s own commit-free checks means every rejection path the spec describes as leaving no trace leaves an open marker. Checks that need no commit run first; the intent record is the first write, not the first step.

What it costs

(step) on every transcription; one landing per arm, usually two sentences — step-4: the event is appended; read the id back through the declared read and continue; alert on the retention configuration — and the code added to the signature. The limit-shaped arms need one more thing: where the substrate caps a field (reference_length_cap on actor_ref and action_ref), the composition validates every reference it will pass — including ones it reads from its own store, such as an approver’s — before the intent, or one over-long reference makes every decision on the chain refuse.

The mechanical slice

tools/linter/lint.py check S-recording-step: in a composition that composes Audit Trail, a bare `recording-failure` on the left of a mapping arrow (→), on a line that also names record_action, above the Status section. A bare token in that position is a transcription of the substrate’s arm with its payload dropped; the same token elsewhere — in a signature block naming the composition’s own code, in an example, in prose — is not flagged, because a composition may lawfully declare a recording-failure of its own over a non-substrate write (Reserve from Pool’s recording-failure(post-commit) is one). The same-line condition was added on 2026-08-29 when the check’s first draft, which assumed only Audit Trail emits the token, fired on Privileged Access Provisioning’s transcription of Multi-Party Approval’s arm: compositions re-export recording-failure bare at their own caller boundary, so a composer transcribing a peer’s arm is transcribing it correctly, and the rule reaches the peer’s own transcription of the substrate one level down. It landed advisory on 2026-08-29 measuring twenty-three sites across six patterns (twenty-two across five after the same-line correction), and was promoted to gating the same day, when the sweep under this rule closed the last of them and it fired zero times corpus-wide — the same promotion discipline P-atomic-audit followed. Its regression guard is synthetic: a mapping that drops the step must fire; the same mapping carrying (step) must stay silent; a bare token in a signature block must stay silent.

Which pass owns it

Pass 1 (GRID) — the reference graph: every mapped arm resolves to the constituent’s declared shape, and every code the prose lands appears in the signature — with the reachability argument left to Pass 3 (adversarial): for each arm, which step failed, and what is on disk when it did?

Worked origins. Capability-Backed Sharing (second gate, 2026-08-29) — dropping (step) made the retry duplicate outcome events, and invalid-credential / invalid-request were unlanded at two redemption steps; fixed with a uniform (step) rule, a step-4 read-back, and both codes in the signature. Login (second gate, 2026-08-28) — invalid-request declared unreachable at four steps that the substrate reaches by deployment fault. Multi-Party Approval (second gate, 2026-08-29) — reference_length_cap on an approver’s reference made every decision on the chain refuse; fixed by validating each reference before the intent. Defensible Retention (second gate, 2026-08-28) — the intent record preceded the commit-free checks, so rejection paths said to leave no trace left an open marker.

A seal presentation is keyed by log position over the covering range

FROZEN — 2026-08-29. Stated from two first-round findings of 2026-08-27 that closed the same way in two patterns, and from a third pattern the linter check below finds still carrying the shape. It is the narrowest rule on this page and the one with the cleanest mechanical form.

The rule. The payload set presented to AuditTrail.verify_record is the covering range read_record names for the event — every payload in the seal’s coverage, in ascending sequence_number order — and a composition that passes the caller’s presentation through keeps it as a map keyed by sequence_number, never by its own identifier. The record set a seal commits to is a sequence range (Audit Trail Invariant 7), and under any cadence but per-event that range spans events the composition did not write and has no id for. A map keyed by event_id, entry_id, or disclosure_id can hold at most one payload per event, so under the interval cadence the substrate recommends every verification returns a seal-record-set mismatch — and an acceptance check built on it reports tampering on an intact log.

Two corollaries the same rounds produced. An entry whose covering range is not wholly present in the map is reported unverifiable(payload-not-supplied(missing)), naming the absent sequence numbers, rather than failed — partial verification of the entries whose ranges are supplied is still worth having. And a replay that must be ordered is ordered by the log position of the record that fixes the order — the intent event’s sequence_number, where the intent precedes the act — not by the outcome’s, and not by a per-record list whose order is the order of writes that landed.

The tells

1. original_event_payloads[event_id]. The subscript says what the author thinks a seal covers.

2. The singular. “The payload”, “its original payload”, one verify_record(event_id, payload) per event in a walkthrough. The substrate’s own parameter name is singular and its Invariant 7 is not; the composition inherits the invariant.

3. A per-event cadence assumed where the Configuration recommends interval. The walkthrough’s arithmetic — one seal, one event, one payload — is the healthy special case, and the rule is the range.

The mechanical slice

tools/linter/lint.py check T-seal-key: an original_event_payloads map subscripted or described as keyed by an identifier ([event_id], [entry_id], “keyed by disclosure_id”) in a composition body. It landed advisory on 2026-08-29 at one site and was promoted to gating the same day, when the sweep under this rule closed that site and it fired zero times corpus-wide. Bare-payload verify_record calls are not flagged — the substrate’s own contract uses the singular name, so a match on it would fire on the exemplar — and that recall gap is recorded here rather than closed by loosening.

Which pass owns it

Pass 1 (GRID) — mechanical, above — with the cadence question left to Pass 3 (adversarial): which seal cadence does this example assume, and what does the verification return under the other one?

Worked origins. Chain of Custody (2026-08-27) — original_event_payloads re-keyed by sequence_number, [Verify Custody] assembling each entry’s presentation from the range read_record names, and unverifiable(payload-not-supplied(missing)) for an entry whose range is incomplete. Forensic Recovery (2026-08-27) — the same re-keying, and the replay ordered by the intent event’s position, carried in the index as intent_position. Immutable Transaction Ledger — still keyed by event_id at [Verify Ledger] when this rule was stated; the check above found it, and the sweep under the frozen rules closed it the same day.

A derived index splits at the horizon, and the truth-bearing half names its atom or is declared unrebuildable

FROZEN — 2026-08-29. This is §Derived state has a validity duration’s Tier 3, promoted from the last row of a table to a rule of its own, because the second gates kept finding patterns that had taken Tier 0 or Tier 1 for an element that needed Tier 3 — and one that had written “all six elements are derived indexes” over a store it elsewhere called truth-bearing three times.

The rule. Every Composition-state element classified as a derived index says what it is past the horizon of the store it derives from, and the answer is one of three: still derived, from a second source that is an independent failure domain; not needed, with the claim that reads it bounded to say so; or truth-bearing under a durability obligation — in which case the element is extraction-pending against a named forthcoming atom, and until that atom lands the durability is a declared deployment obligation with a Configuration entry that spends it. A fourth answer is honest and rare: the element is unrebuildable past the horizon and every claim reading it degrades explicitly. There is no fifth. A blanket sentence — all elements are derived — is not an answer, it is the tell.

The truth-bearing half has three recurring shapes and each has a home. What a purge destroyed and how it was keyed — the binding key that lived in a payload the cascade destroys and survives only where the composition wrote it while the event was live — is the Erasure Tombstone atom the substrate itself names. A record owed for a committed act — a marker written transactionally beside a domain write, standing until the sealed outcome lands, from which a seal may be built and without which it must never be — is the Outbox atom. A composition’s own log — an element that is a list of events no constituent replays, written by the composition, read by its checks — is Event Log, absorbed and mis-classified, and the fix is to say so rather than to keep the middle.

The tells

1. A durability obligation referenced and not declared. “Under the durability obligation stated in Composition state” three times, and Composition state says derived. Grep for the phrase; count declarations.

2. “Rebuild from the trail” for a fact the trail’s payload destroyed. The rebuild procedure reads data.<key>; the horizon destroys data. Past it the element is not derived from anything, and calling it derived is the blindness §A derived index is trustworthy only where a miss is observable describes — a lost entry indistinguishable from a purged one.

3. A marker sealed from the intent alone. Where the outcome’s authoritative datum (a disclosure_id, a minted token) exists only in the marker, a recovery that seals from the intent when the marker is lost fabricates the datum. The marker is the truth-bearing half; the seal is built from it or not at all.

4. A composition-owned middle. An element that is neither rebuildable from a constituent nor named as an atom to extract — a <pattern>_event_log, a history list the composition appends to — is the no composition-owned middle rule of the Execution Contract, violated by omission.

What it costs

A sentence per element stating its past-horizon classification; a Configuration entry where the answer is truth-bearing (the durability the deployment owes, stated as an ordering against the store the element keys — as durable as the Selective Disclosure store, at least the audit instance’s retention); and a named forthcoming atom with its *(forthcoming)* marker, which the linter’s stale-forthcoming check will retire when it lands.

Which pass owns it

Classification is Pass 2 (EOS) — the truth-bearing half is an unnamed atom, and naming it is extraction — with the mechanical form in Pass 1 (GRID): every derived element’s past-horizon sentence exists, and every named atom resolves to a forthcoming marker or a file. The collision check §A derived index is trustworthy only where a miss is observable names — an element classified derived that is also declared truth-bearing in some window — is the linter check this rule would carry, and it is still not built; the sweep under this rule is what will say whether it is worth building.

Worked origins. Multi-Party Approval (second gate, 2026-08-29) — the chain store’s past-horizon durability was referenced three times and declared nowhere; fixed with a chain_store_durability Configuration entry and the blanket sentence amended. Immutable Transaction Ledger (2026-08-27) — disclosure_to_event’s purged half is truth-bearing, extraction-pending against the Erasure Tombstone atom. Capability-Backed Sharing (second gate, 2026-08-29) — the pending marker is truth-bearing under a durability obligation, extraction-pending against an Outbox atom, and the seal is built only from it. Login (second gate, 2026-08-28) — login_event_log was a composition-owned middle; reclassified extraction-pending against Event Log. Execute Gated Workflow (2026-08-27) — the consumed flag is durable past the horizon and the consumption test fails closed without it.

A compensator is exclusive — one writer per act, and the invocation yields at its bound

FROZEN — 2026-08-30. Stated from the third fresh-reader gates — the eight patterns the 2026-08-29 freeze had not yet gated, plus one re-grounding — which returned forty-seven foundational findings, forty-five of them confirmed by a second reader given the full record. Three patterns returned this shape, each gated independently, each carrying a reconciliation the sweep under §A reconciliation is bounded at both ends had just extended. Frozen on the day it is stated, under the same discipline as that section: recurrence across independently gated patterns is the evidence, and a rule stated open is a rule the next round edits instead of applying.

The rule. For every act a composition can compensate, exactly one writer may land the outcome — the invocation or a reconciliation leg, never both — and the invocation’s own retry has a terminus: at the completion bound it yields, and everything after the bound belongs to the leg. Two legs that can see the same act serialize on the act’s key, and the look-then-write pre-check every compensator runs is re-read under that serialization, not before it. An age bound alone guards one side: it keeps the leg off work younger than the bound. It does nothing about an invocation that is still retrying past the bound, and nothing about two legs — restart and cadence, two nodes — that run the same comparison at once. Each of those is a second writer, and a second writer lands a second outcome for one act, which the sealed trail then protects.

The frozen §A reconciliation is bounded at both ends presumes an invocation stops at its bound; nothing in the corpus said so, and the three origin patterns each said the opposite — retry until it lands with no terminus, beside a leg that starts at the bound.

The tells

1. “Retry until it lands” with no terminus. The phrase names a loop whose exit is success; it does not name the bound. Ask what the loop does at bound + 1, when the leg has already read the act as an orphan.

2. A pre-check that looks, then appends. “Traverse the log for an existing outcome carrying this key; if none, append.” Two compensators run it at once and both find none. The pre-check is correct only under a serialization that the spec names.

3. Two legs and no lock. A scan “at restart and on reconciliation_cadence” with no per-act mutual exclusion is two legs; on two nodes it is four. The frozen substrate closes its own version of this with a closed-state marker on the act (compensated_attestations); a composition’s leg needs the same or an equivalent.

4. A stalled invocation resuming after the leg. A step that is a bare append — no pre-check of its own, no lease — will land its outcome beside the leg’s when the process it belongs to wakes. Per-key locking that prevents interleaving does not prevent sequencing.

What it costs

One sentence per action with a post-commit failure step: the invocation attempts the outcome write until <x>_completion_bound, then yields; a later success is the leg’s. One serialization statement per leg naming the act’s key (the same invocation_id §Intents pair with outcomes carries), under which the pre-check is re-read. Where the invocation cannot be made to yield — it holds no clock past its first read — the outcome step itself runs the pre-check under the act’s key and adopts an existing outcome as its own (proceed as landed). And a check that reads the pair widens from at most one outcome per intent to exactly one writer per outcome, named: the outcome carries recovery = true or it does not, and the pair is exact.

What this does to the formal layer

The model needs the invocation and the leg as two processes over one act, with the bound as the point at which one of them stops being able to write. A model in which the invocation is a single atomic step cannot exhibit the second writer, and passes.

Which pass owns it

Pass 3 (adversarial) — what does this invocation do at bound + 1, and what do two runs of this leg do at once? — with the mechanical form in Pass 1 (GRID): every retry loop names its terminus, and every leg names its serialization key. No linter check; the loop’s shape is prose.

Worked origins. Chain of Custody (third gate, 2026-08-30) — Invariant 4’s liveness arm retried the outcome write with no terminus while the scan started at the bound; both ran the same look-then-append pre-check with nothing between them. Forensic Recovery (third gate) — the restart scan and the cadence scan, and an invocation past its bound, could each compensate the same intent; the scan’s place in the replay was fixed, its multiplicity was not. Immutable Transaction Ledger (third gate) — [Disclose Subset] step 4 was a bare append, so a stalled invocation resuming after the scan had compensated it landed a second ledger.disclosed; the Configuration entry admitted the direction and named no remedy.

Lawful destruction is answered before absence — the constituent’s purged verdict precedes any composition pre-check

FROZEN — 2026-08-30. Stated from two third-gate findings that closed the same way in two patterns whose verification actions had each been reworked under §A seal presentation is keyed by log position three days earlier. The rework added a composition-side membership check to the step list and put it ahead of the constituent call; the constituent’s purged short-circuit, which the composition’s verdict table promised to relay, became unreachable in both. Frozen with the other rules of this date.

The rule. Where a composition presents a record to a constituent that answers purged before it answers anything else — Audit Trail’s verify_record reads retention state first and returns failed-verification(purged) before it looks at a payload — every composition-side check that could fail on the same record runs after the constituent’s answer, or branches on the retention state the composition already read. A record the substrate has lawfully destroyed is not missing, not unsupplied, and not unverifiable; it is purged, and the verdict class the composition promises for that case is reachable only if the purged answer comes first.

This is §Derived state has a validity duration’s Tier 2 arriving at the step list: the composition knows the element’s validity is bounded by retention, says so in its verdict table, and then writes a membership check that cannot tell a purged member from a lost one. The blindness §A derived index is trustworthy only where a miss is observable names is here in the ordering rather than the index.

The tells

1. A verdict class with no producer. The Overall Verdict table lists failed-verification(purged) as consistent with Complete; walk the step list and find the step that produces it. If every path to it first passes a check that fails on a purged member — “any entry whose payload is not in the presented map → unverifiable(payload-not-supplied)” — the class is promised and unreachable.

2. “Payload not supplied” for a payload the substrate destroyed. The caller cannot supply what the purge removed. A verdict that asks them to has mistaken destruction for omission.

3. A retention state read and not branched on. A step that reads retention_state “for the record” and then proceeds identically for Retained and Purged has read it for nothing.

What it costs

One reordering per verification action — retention state first, then the constituent’s own verdict, then any composition-side membership or presentation check on the survivors — and one per-entry outcome for the purged case (not-applicable(purged), or the constituent’s own failed-verification(purged) relayed) that the completeness verdict counts as consistent. The check that quantifies over the entry set says which members it examined and which it reported purged.

Which pass owns it

Pass 1 (GRID) — every verdict class in the table resolves to a producing step — with the reachability argument in Pass 3 (adversarial): present this action a record the substrate purged yesterday, and read the step list.

Worked origins. Chain of Custody (third gate, 2026-08-30) — [Verify Custody] step 3c’s absence check ran before the purged short-circuit, so a lawfully purged entry landed unverifiable(payload-not-supplied) and the chain could never reach [Custody Proof Complete] after its first purge. Forensic Recovery (third gate) — [Recover History] step 5b reported a purged transition as payload-not-supplied and history-complete became unreachable with one purged event in the sequence.

An outcome is sized before the intent — the cap is checked against the largest record the act can write

FROZEN — 2026-08-30. Stated from two third-gate findings and one refining line of the same round, in three patterns that each argued the substrate’s invalid-request was foreclosed by construction at the outcome position because the payload was composition-built. The argument was about the intent; the outcome is a superset of it, and a compensation record is larger still.

The rule. A composition that writes an intent record before an irreversible commit sizes, at its commit-free validation step, the largest record the act can write — the outcome payload, and the compensation payload a reconciliation would write for it — against the substrate’s payload_cap, and refuses invalid-request before the intent when either would exceed it. Every set-valued field an outcome carries — the entries disclosed, the scopes affected, the credentials revoked — has a declared cardinality cap, in Configuration or in the field’s own policy, or the argument that the cap is unreachable is false. Foreclosed by construction means the construction is bounded; an unbounded set is not a construction, it is an input.

The consequence of getting this wrong is the one §Durability boundaries names: the constituent’s record exists, the outcome that would bind it cannot be written, and the binding is un-writable for as long as the payload stays over the cap — which, for a set that only grows, is forever.

The tells

1. “Foreclosed by construction” / “the payload is composition-built”. Ask which payload. If the sentence was written about the intent, read the outcome’s field list and find the one the intent does not carry.

2. A set-valued field with no cap. disclosed_entry_ids — non-empty; affected_scopes — the complete set; revoked_credentials — every effective-Active credential. Non-empty is a lower bound. The cap is the upper one, and the caller can reach it.

3. A compensation larger than the outcome. A recovery record that carries the outcome’s fields plus intent_event_candidates, recovery = true, and the acting human. If the outcome fits the cap by one byte, the compensation does not.

What it costs

One sizing step at validation — construct the maximal envelope, or bound it arithmetically from the declared caps — and one cardinality cap per set-valued field. Where the set is genuinely unbounded (a long-lived consent’s registrations), the composition declares a chunked shape with every consumer of the field restated against it, or bounds the set by policy; a digest in place of the set is not a shape, because nothing that reads the set can read a digest.

Which pass owns it

Pass 3 (adversarial) under the Arms question — which step failed, and what is on disk? — with the mechanical form in Pass 1 (GRID): every set-valued outcome field resolves to a cap.

Worked origins. Immutable Transaction Ledger (third gate, 2026-08-30) — disclosed_entry_ids had no cardinality cap; the intent passed, the Selective Disclosure record committed, and the outcome could be refused by the cap with no exit. Forensic Recovery (third gate) — the uniform arm rule admitted an outcome-stage invalid-request orphan it then declared unclearable, against Invariant 4’s claim that every orphan is bound. Propagate Consent Revocation Downstream (third gate) — affected_scopes grows without bound, and the escape offered was a digest no processor can act on.

Liveness is arithmetic — bound plus cadence plus latency, strictly less than the window

FROZEN — 2026-08-30. Stated from one third-gate foundational finding and three refining lines in the same round that each corrected the same inequality. The corpus had been writing cadence no longer than the window since §Durability boundaries introduced compensation_window; the sweep under §A reconciliation is bounded at both ends added a lower edge to every leg and did not re-derive the inequality the edge changes.

The rule. Where a liveness arm promises closure within a window, the Configuration states the inequality that makes the promise true — the completion bound the leg waits out, plus the cadence between runs, plus the write latency of the closure, strictly less than the window — and the check that confirms the deployment meets its window confirms that inequality, not a fragment of it. An orphan created at t is invisible to the leg until t + bound; the next run is at most cadence later; the closure lands latency after that. cadence ≤ window is satisfied by a deployment that breaches the window on every orphan.

The tells

1. “Cadence no longer than the window.” Two of the three terms are missing.

2. Equality admitted. No longer than is ≤. At equality the closure lands exactly at the window’s edge, after the latency the inequality did not count.

3. A check that reads Configuration for one knob. Confirm reconciliation_cadence ≤ compensation_window. The check is true and the promise is not.

What it costs

One inequality per liveness arm, written out in Configuration with its three terms, and the sentence checked at instance start — a deployment whose knobs do not satisfy it refuses to start rather than starting to breach. The check that confirms the window reads all three.

Which pass owns it

Pass 1 (GRID) — mechanical: the inequality is on the page and its terms resolve to Configuration entries — with Pass 3 (adversarial) doing the arithmetic on a concrete triple.

Worked origins. Actor Suspension (third gate, 2026-08-30) — check 6 confirmed cadence ≤ completion_window while the sweep skipped entries younger than suspension_completion_bound; a fifteen-minute bound, a ten-minute cadence and a ten-minute window breach on every suspension with the check passing. Propagate Consent Revocation Downstream, Forensic Recovery, Chain of Custody (third gate, refining) — the same fragment.

A stamp from another seam never decides a write alone

FROZEN — 2026-08-30. Stated from two third-gate foundational findings and two refining lines, in patterns that had each stated the Logic Confinement Principle correctly for their own seam and then compared their own reading against a constituent’s.

The rule. A timestamp the composition wrote from its seam and a timestamp a constituent wrote from its own are two readings of two clocks. They may be compared only under a declared offset allowance — a Configuration entry — and the comparison may narrow a decision, never make one: no pairing, bypass verdict, enrollment, compensation, or refusal rests on it alone. Where the composition needs equality, it passes its own reading through to the constituent (disclosed_at = now, revoked_at = now), so that the stamp on the constituent’s record is the composition’s and equality is by construction. A constituent that calls its own range read best-effort under skew has told the composition the read is advisory; a composition that gates a write on it has overruled the constituent’s own contract.

The tells

1. “Inside the bound before the record’s granted_at.” The bound was declared against the composition’s seam; granted_at was stamped by the constituent. The inequality has a sign that skew can flip.

2. A constituent’s advisory read used as a gate. Party Identity: “an [Enrolled At] range … under clock skew its result set is best-effort.” A resume arm that decides enroll again on that read’s emptiness has made the constituent’s caveat load-bearing.

3. A pass-through on one side and not the other. The withdrawal side passes revoked_at = now and pairs exactly; the grant side does not pass granted_at and pairs on before. The asymmetry is the finding.

What it costs

One Configuration entry (clock_offset_allowance), symmetric windows widened by it wherever two seams meet, the pass-through wherever the constituent’s contract accepts the stamp, and — where it does not — the decision downgraded from a verdict to candidates or an escalation. The Generation acceptance standing rule most patterns already carry for checks is the same allowance; this rule carries it to the writes.

Which pass owns it

Pass 3 (adversarial) — the Time question: whose clock stamped each side of this comparison? — with the mechanical form in Pass 1 (GRID): every cross-seam comparison names the allowance it runs under.

Worked origins. Propagate Consent Revocation Downstream (third gate, 2026-08-30) — the grant-side scan paired an intent to a Consent record by intended_at before granted_at and landed bypass, write nothing on the result; a three-second skew made a real orphan un-withdrawable forever. External Onboarding (third gate) — the resume arm’s duplicate-freedom rested on Party Identity’s enrolled_at range read, which Party Identity declares best-effort, with no margin. Forensic Recovery, Propagate Consent Revocation Downstream (third gate, refining) — the composition’s now handed to a constituent whose own future-bound guard runs on its own clock, an invalid-request reachable after the intent.

A composition’s own rejection arm carries the retry bit

FROZEN — 2026-08-30. Stated from two third-gate foundational findings that §A transcribed rejection arm keeps its payload does not cover and was written not to: that rule governs the transcription of a constituent’s arm, and its linter check’s own note records that a composition lawfully re-exports recording-failure bare at its own boundary. Two patterns showed the re-export is not lawful when the bare token covers two dispositions — the case that rule’s arms do not name, recorded here first as its unfreezing discipline requires, and closed by a rule of its own rather than an amendment.

The rule. A rejection code a composition exports at its own signature carries whatever the caller needs to decide whether a retry is safe. Where one token would land at a position before the act’s irreversible commit and at a position after it, the token carries the position — recording-failure(intent | outcome), or two codes — and the signature block declares the payload. The composition boundary is a transcription too: of the composition’s own steps, to a caller who cannot see them. A caller who receives a bare token after an outcome-position failure and retries has been told, by the signature, that nothing was committed.

The tells

1. One token at two steps, one on each side of the commit. The linter finds this one.

2. “The collapse happens only at the caller boundary.” Written as reassurance; it is the defect. The caller is the one who retries.

3. A retry rule the signature does not carry. “Retry only on the intent-position arm” in an edge case, with recording-failure bare in the signature.

The mechanical slice

tools/linter/lint.py check U-retry-bit: within one action’s step list in a composition that composes Audit Trail, a bare `rejected(recording-failure)` landed at a numbered step before the action’s first qualified constituent commit call and at a numbered step after it. Read calls (read, read_record, check, verify_*, history_for, active_for, and the like) do not count as the commit; AuditTrail.record_action does not count as the commit, because the intent record precedes the act by design and its own arm is retry-safe. It landed advisory on 2026-08-30 measuring ten actions across five patterns, two of them patterns the second gates had already closed, and was promoted to gating the same day, when the sweep under this rule closed all ten and it fired zero times corpus-wide — the third check to follow P-atomic-audit’s promotion discipline. Its regression guard is synthetic: two bare landings straddling a commit must fire; the same two with (intent) and (outcome) must stay silent; two bare landings both before the commit must stay silent.

Which pass owns it

Pass 1 (GRID) — every code the prose lands appears in the signature with the payload the prose distinguishes — with Pass 3 (adversarial) asking, for each exported code, what does the caller do next, and is it safe at every step that lands the code?

Worked origins. Immutable Transaction Ledger (third gate, 2026-08-30) — the spec stated the collapse in its own words: two dispositions, retry the whole action and do not retry, a disclosure record exists, shared one token at the caller boundary. Forensic Recovery (third gate) — three lifecycle actions exported the same bare code from a step that had committed nothing and from a step that had committed the transition and owed the audit record; the hard alert and compliance finding Invariant 4 said the outcome carried appeared in no signature.

Authentication precedence — no authority-bearing transition may rely on an unauthenticated principal

FROZEN — 2026-08-27. This rule and everything below it are closed to amendment. It was stated 2026-08-26, carried into eleven patterns over the two days that followed, gated by a fresh reader on every one, and revised eight times over those rounds. It is now fixed: a round that finds this rule inconvenient applies it as written or records a finding against the pattern, and does not edit this section. The freeze is not a claim that the rule is complete — it is the condition under which the next campaign’s findings can be attributed, since a rule still in flight cannot be told apart from the corpus archaeology running beside it (roadmap methodology debt #18’s operating rule, and #19’s sequencing note).

What the freeze does not do. It closes no routed finding: every pre-existing foundational finding those eleven gates returned stays open in its pattern’s Lineage entry, and the formal-layer extensions several of those patterns owe stay undischarged and recorded as such. The live tally lives in roadmap.md, not here (The no-snapshot rule). It also does not exempt the one remaining round — Privileged Access Provisioning’s incomplete template — which applies the frozen rule rather than changing it.

Unfreezing is a deliberate act with a stated cause. The rule reopens only when a round produces a case none of its three answers covers, and the reopening records that case first. Discomfort is not a case.

An invariant is only as sound as the authority it quantifies over (Capability provenance, above); this is the same discipline applied to identity rather than capability. No consequential state transition may rely on an actor identity that has not yet been authenticated — and, the half that does the real work, the authenticated principal must be the principal whose authority the guarantee asserts.

The rule is stated at the seam, not the implementation, and deliberately so. It does not say “every pattern taking a credential must call Credential.verify first” — that would be mechanical, and it would wrongly convict patterns where the attestation is the load-bearing write, with no prior consequential commit to protect. It asks one question at every credential seam:

Whose authority is this state transition relying on, and where is that identity established as authentic before the transition?

Three answers are sound, and they are the only three:

Nothing commits first. The credential-consuming call is itself the load-bearing write, so no state depends on an unverified claim — the substrate case (Audit Trail, where attest is the first and only write), and the single-write action generally.
Verification precedes the commit. The composition verifies the presented credential against the acting principal before any constituent call, with a declared rejection arm that writes nothing — the Privileged Access Provisioning form: Credential.verify(actor_ref, credential_type, credential) early, a deployment-declared credential_type, a named credential-invalid rejection, an invariant that states it, and a Generation acceptance check that tests it.
The transition does not rely on that actor’s authority at all. A bearer-token redemption that takes no actor claim, a system-initiated sweep acting under its own identity with no human authority asserted. This answer is only available when the pattern’s guarantees are correspondingly silent about a human.

A declared deployment obligation is not a fourth answer. Stating that an upstream pre-check is “a deployment obligation, not an option” records the hazard honestly, and is better than silence, but it discharges nothing: it leaves the composition’s own records unable to show the check ever ran, which forfeits precisely the records-alone standard the regulated patterns exist to meet. Where the composition can enforce the seam at its own boundary, it must; the deployment obligation is the residue for what genuinely cannot be enforced there, stated with its verification routed to an externally-clearable check, never the default escape hatch.

The binding half is the sharper half, and it is a different class of defect from ordering. A pattern that verifies the service actor while its guarantee speaks about a human has not made an ordering mistake — it has made a binding mistake, and re-ordering will not fix it. This is the shape that recovery machinery produces by construction: a record re-emitted outside the original invocation is attested under the composition’s own credential, with the human demoted to a payload field, so the substrate verifies the service and says nothing about the person. “The credential is verified inside the audit write” is true of the substrate and false as an inherited claim about the human actor — a composition may state it only about the identity the composition actually passed. Where a guarantee names a person, that person’s authority needs its own authentication binding, and a nested composition does not inherit one merely because some inner layer eventually verifies some actor.

Which pass owns it. Detection belongs to Pass 3 (adversarial): it is the “who checked that the caller was real, and when” question, and it is found by walking an action’s numbered steps and comparing the position of the first verification against the position of the first commit. The mechanical slice is a Pass 1 reference-graph check of the same shape as the Rests on: discipline — for every action taking a credential, either a verification step precedes the first constituent write, or the pattern names which of the three sound answers applies. The binding half stays with the fresh reader: matching each guarantee’s asserted principal against the principal the wiring actually authenticates is a reading task, not a position comparison.

What verified does and does not establish — required wherever the second answer is used, because the guarantee inherits exactly this much and no more. A successful verification establishes that material matching the principal’s registered verifier was presented at that instant. It does not establish that the presenter is the principal (a stolen credential verifies), that the presentation is bound to a channel or session, or that it cannot be replayed. Patterns needing more compose the atoms that provide it; patterns that do not must not claim it.

The insertion hazard — a changed write order invalidates explanations, not just references. Applying this rule to an existing pattern means inserting a write before one that was previously first, and that changes a global fact about the spec: which write comes first. Three consecutive rounds each shipped the same defect, and it was never a step-number error — a mechanical renumber catches those. What goes stale is every paragraph that reasons from the old global fact, and those sit at a distance from the step lists: a “uniform rejection-mapping rule” concluding that a rejection code is unreachable because the constituent writes first; a primitive-policy paragraph explaining that credential failures always surface post-commit; an atomicity claim asserted “without qualification” on the path that just acquired a precursor. Each was internally coherent and each contradicted the new wiring. So: after changing the write order of a composition, re-audit every invariant, rejection mapping, guarantee, recovery description, and explanatory paragraph whose truth depends on ordering — not merely the references to the changed steps. State that audit as a distinct step; it is not a proofreading pass, and a reviewer brief that asks only for renumbering integrity will not find it.

The ordering guarantee must be structurally available before it can be claimed. The sharper form of the same lesson, and the one that produced a false invariant rather than stale prose: an action whose loop interleaves resolution with commitment has no point at which “before the first irreversible act” exists. A rights-fulfillment path that resolved each record’s disposition and destroyed it in the same per-record pass could not host a pre-state intent record anywhere, and placing one after the loop satisfied the step numbering while inverting the guarantee. The fix was to make the read-only phase separable — resolve the whole universe, then authenticate, then execute — and the general rule is that an ordering guarantee is a claim about the shape of the action, not only about the position of a call. Where the shape does not admit the ordering, the shape is what changes.

Stated for the reviewer rather than the author: a temporal guarantee cannot be established from textual step ordering when the runtime execution shape interleaves iterations. A step list is a static artifact and a loop is not; step n precedes step n+1 on the page while executing after every iteration of the loop inside step n−1. This is the failure a careful review is most likely to miss, because it survives every check that reads the document as written: the numbering is consecutive, every cross-reference resolves, and the invariant that is false cites the step that is genuinely there. Reviewing an ordering claim means asking what the runtime does, not what the list says.

Causal provenance: authenticate at every boundary, and record what occasioned the act. Where one composition performs its irreversible act through another that has also adopted this rule, both write an intent record and both verify the same caller credential. That redundancy is cost, not ambiguity, and it must not be optimized away: the inner composition’s surface is independently callable and cannot know it sits inside an authenticated outer context, so a version that trusted such a context would be unsafe on the direct-call path — the inner verification is that path’s only defence. Authentication is not inheritable across a composition boundary. What the outer layer owes instead is provenance: where the two layers share one audit substrate, their intent records land in one sequence, and without a link a reader cannot tell an inner act occasioned by an authorized outer process from a direct call that bypassed it — the question a regulator actually asks. The outer intent record therefore carries the plan: what it is about to occasion, across every leg including the ones that bypass the inner composition entirely. State the resulting join at its true strength — an inner act with no preceding plan is certainly direct, which is the sound and useful discrimination; attribution to a particular outer invocation is exact only where that invocation completed, and presumptive otherwise.

The distinction the name carries is worth keeping sharp, because it is easy to think the problem is already solved. A distinct action_ref per record kind settles the identity of the evidence — which record is the authentication, and for which layer. It says nothing about the identity of the causal process — which invocation occasioned this one. Two intent records can be perfectly distinguishable as records and still leave an auditor unable to say whether an act was occasioned by an authorized process or by a direct call, and that second question is the regulated one.

Two rules about the rule’s own boundaries, learned late and worth stating where the rule is rather than where its appliers are.

A delegated exclusivity check is a flag for this rule, not evidence against it. Two compositions — Execute Gated Workflow and Multi-Party Approval — deliberately carry no authorization gate on their decision actions, because the constituent’s own exclusivity invariant is the authorization: only the named approver may approve, only the submitter may withdraw. Both spelled that out as a design decision, and it survived nine and eleven critique rounds respectively. It is also where each pattern’s foundational claim quietly stopped being about people: an exclusivity invariant compares a supplied actor reference against a recorded one, and until this rule was applied neither reference had been verified, so the named approver approved was a comparison of two strings and anyone who knew an approver’s reference could move a regulated workflow. Delegating authorization to a constituent’s exclusivity check also delegates away the moment a credential would have been consumed — and because the delegation reads as more rigorous than a redundant local gate, it is the last place a reviewer looks. Treat the sentence no redundant permission check is added here as a flag for this rule wherever it appears.

A third-answer carve-out must be checked against the constituent’s record, not only against the composition’s own trail. An exemption argued as this transition relies on no actor’s authority is only true if no constituent it calls requires an actor’s authority to perform it. Multi-Party Approval’s round got this wrong in a way worth preserving: two recovery paths that authenticate nobody were carved out as relying on no principal, and both call a constituent whose invariant admits the call only on the initiator’s reference — so the atom’s immutable record permanently states that the initiator withdrew a step at a moment when the initiator had not authenticated and, on one path, was not present at all. The composition’s own audit record was scrupulously honest (composition actor, recovery = true); the constituent’s record was not, and could not be, because the atom exposes no composition-actor surface. The two records can disagree, and the constituent’s is the one a later reader finds first. Where they must disagree, say so in the invariant and name the records-alone disambiguator; do not let the composition’s own honesty stand in for the constituent’s.

Four failure modes of the applier, not the rule — observed repeatedly enough to be a checklist rather than a caution.

Evidence sufficiency: a binding is only as good as what the record carries. Twice in one campaign the mechanism was wired correctly and the evidence left insufficient, in ways a reader of the wiring would not notice. In one pattern the intent-to-outcome join was specified over a key that was per-case while three of the actions were repeatable against one case, so a single stale intent record would have satisfied the check for an unbounded number of later acts. In another, the attestation’s action reference was correctly composed per-invocation — and no record carried the field needed to recompute it, so an implementation binding one proof to a whole category of act would have passed every declared check. Both were caught by a gate; neither would have been caught by re-reading the step list, because the step list was right. So: whenever a check is claimed to verify an ordering or a binding, name the field on the record that makes it recomputable, and confirm that field is written by the wiring and survives as long as the check must run. A guarantee whose verification depends on state that is evicted, or on a key that does not distinguish the thing being bound, is asserted rather than witnessed — which is the exact defect the rule exists to remove.

The signature block is where attention does not land. Three consecutive rounds shipped the same omission: the touch makes a new rejection reachable — invalid-credential, cleanly returnable now that verification precedes commitment — the preamble says so, an invariant says so, the wiring maps it, and no action signature declares it. The action contract is the surface a caller switches on and a generator consumes, so a code that is reachable and undeclared is either flattened into a neighbour (erasing the distinction the change was made to create) or emitted undeclared. After any change that makes a new outcome reachable, re-read the signature blocks specifically — they are the last place a reviewer looks and the first place an implementer does.

The invariant’s opening sentence must carry its own scope, because that sentence travels alone. An invariant that covers some of a pattern’s actions and not others is routinely drafted as an unrestricted quantifier followed by a paragraph of exceptions — “no call that commits is reached on any path before the caller’s credential has validated”, then a block explaining which action is outside it and why. The block is correct and the sentence is false, and the sentence is what gets quoted: into a status line, a roadmap row, an acceptance check, a generator’s prompt, a reviewer’s summary. In the case that produced this entry, the excluded action was the pattern’s load-bearing one, and the unrestricted opening therefore asserted, on its own, precisely the thing the pattern exists to refuse. Name the covered actions inside the sentence that states the invariant, and let the following block explain why the others are outside rather than that they are. The test is mechanical: quote the invariant’s first sentence with nothing after it and ask whether it is true.

An inheritance claim must be routed through a record that is authoritative, not one that is derived. Where a guarantee is not established at the act itself but inherited from an earlier, verified act, the applier must say how a reader gets from one to the other — and the natural route is whatever index the pattern already maintains for that lookup. That index is usually derived: rebuildable from the same event trail the claim is being verified against, which makes the verification a comparison of a reconstruction with itself, and makes the claim fail exactly when the trail is damaged, which is when it is needed. The authoritative carrier is nearly always already available — a sealed event whose payload holds the same keys — and the fix is to name it and say why the derived route was not taken. This is the same hazard as the check-over-a-rebuildable-index case above, arriving through a different door: there it corrupts a check, here it corrupts a claim in the prose, where no acceptance bar is looking for it.

When the intent record should carry its plan, and when carrying it is a hazard. The causal-provenance rule says an intent record names what its invocation will occasion. Applying it produced the opposite answer in two patterns within a day, and the discriminator is worth stating because both answers looked obviously right at the time.

Carry the plan when the plan and the outcome are separately recorded and their divergence is diagnostic. One composition’s transition firing occasions a burst of withdrawals of human approvals, emitted under the composition’s own service identity, that the caller never sees and that have their own per-item outcome events. Recording the intended set before the act makes both directions of divergence checkable: an item the outcome events name that the plan did not is a conformance failure — the composition acted beyond what it declared — and an item the plan named with no outcome event is an owed compensation. Neither is visible without the plan on the record, and the check that reads them is the only cross-check the cascade has.

Do not carry it when the outcome record is the single authoritative carrier of that datum. Another composition’s withdrawal occasions a propagation set that its load-bearing invariant makes bijective with one outcome event, and whose acceptance check verifies that set against the events it was derived from. A copy on the intent event would be a rival rebuild source for the one datum the pattern exists to make authoritative — and a reader who rebuilt from it would be verifying a reconstruction rather than the record. The same reasoning excludes minted identifiers from every intent record in the corpus: a consent_id, a capability_token, an instance_id, a step_id did not exist when the intent was written, and an intent event carrying one would make an act that never committed resolvable to a reader who traverses for it.

The test is therefore not is this datum interesting? but does the outcome already own this datum authoritatively? If it does, the intent must not restate it. If it does not — if the plan’s only other trace is a set of separately-recorded side effects, or nothing at all — the intent record is the correct and often the only place it can live. A useful sharpening: an intent record may name what the invocation decided to do; it must not name what the act produced.

A related discipline the same rounds argued for: cross-references that leave a section should name the step, not number it. Every round in this campaign spent its most expensive errors on distant paragraphs citing step numbers that an inserted write had shifted — and the worst of them carried correct numbers while describing an order that no longer held, which no numeric check can catch. Inside an action’s own step list a number is fine and reads well. Crossing into an invariant, a rebuild procedure, an acceptance check, an example, or an edge case, prefer the step’s name and role — [Open Gate]’s submit, [Fire Transition]’s gate-state read, the outcome record — with the number in parentheses if it helps. Named references survive insertion; numbered ones silently rot. This is a coupling reduction, not a style preference: it is the cheapest available fix for the representation-level defect debt #19(c) exists to measure.

Worked origin (2026-08-26). Surfaced by the fresh-reader gate on Execute Gated Workflow (Final Critique 9, F1), in a form that shows why the rule is worth stating rather than adjudicating per pattern: the finding was created by a fix. That composition’s prior round gave the deterministic invalid-credential arm a terminal landing — composition-actor re-emission with the human named in the payload — which was correct as a recovery move and which, as a side effect, converted a loud unresolvable alert into a quiet acceptance of an act committed on an unverified actor claim. A landing is only as good as the check that ran before the thing landed. The triage of all eighteen credential-taking patterns that followed found the corpus had reached four different answers to the identical structural question — one pattern verifying, three declaring the obligation in identical words, four naming an upstream pre-check as an option some deployments may want, the rest silent — with no stated rule to choose among them, and with Chain of Custody having closed a word-for-word identical foundational finding by declaration where Privileged Access Provisioning had closed it by verification in its first draft and was never asked to justify the difference. Two live falsehoods fell out of the same triage: a pattern whose prose claimed it “records whoever calls it with a valid credential” on a path where irreversible destruction commits a step before the credential is touched, and a nested erasure path with two unverified layers under a guarantee naming the operator. Unreconciled precedent, not ignorance, is what the rule is for: without it each round picks an answer locally and the corpus drifts.

The no-snapshot rule — library-state facts live in ROADMAP

(Ownership moved here 2026-06-11 from the session-bootstrap index — now AGENTS.md, reached via the CLAUDE.md shim; the rule itself was generalized 2026-06-10, Refactor 1.) roadmap.md is the single source of truth for the library’s current state — grounded counts, per-category lists, sequencing. The six core docs — readme, the-spec-layer, this document, spec-format, contributing, execution-contract; the rule-owning documents in the first six positions of the bootstrap reading order — carry no library-state snapshots: no pattern or composition counts, no present-tense corpus enumerations (“all current compositions are…”), and no “anticipated” or “forthcoming” framing for patterns that have already landed (the landed-but-forthcoming case is also caught mechanically by the linter’s D-stale-forthcoming check). Library-state facts are stated by reference to ROADMAP. Dated historical records (“the 2026-06-08 sweep of all eighteen then-grounded compositions…”) conform — they are self-dating and cannot drift; present-tense corpus claims do not. A snapshot found in a core doc is a finding, not a preference. The rule earned its generality the usual way: a mirrored count in the session-bootstrap file read “twenty atoms and eight compositions” long after ROADMAP had moved past both; worked instances removed 2026-06-10 included spec-format’s Status line carrying the same stale count and the Execution Contract filing Notification Fanout as “in the roadmap” after it had landed. This document is one of the six and is subject to its own rule (see §The methodology applied to itself).

Regulated-pattern conventions

Two structural conventions emerged as Pass 3 findings on the first regulated atom in the library and have stabilized as required sections for any pattern with external acceptance bars. Both are structural fixes to recurring Pass 3 gaps — not optional polish.

Regulated adversarial scenarios

The Pass 3 gap. Early-draft examples are almost always happy-path biased: they walk what users do, not what auditors check. Pass 3 catches this routinely. The historical fix was to add rejection-path examples — what the system refuses. That helps, but it still misses a third class: what external evaluators ask. A regulator querying “show me every commitment confirmed after its declared window” is exercising the invariant from the outside, in the language they use, against the records they can see.

The structural fix. A dedicated Examples subsection — Regulated adversarial scenarios — walking three canonical adversarial reads: regulator audit (a query against the records that must return the expected result by virtue of an invariant), disputed transaction or data-subject request (an external party challenges the system’s claim and the records must answer), and breach or incident investigation (an investigator queries during or after an anomaly). The three classes exercise different invariant surfaces: audit checks structural guarantees, dispute exercises the contract under hostile interpretation, breach exercises forensic queryability.

Worked examples. Provisional Commitment’s adversarial scenarios walk regulator-audit-of-confirmation-window, GDPR-erasure-on-personal-data (GDPR is Europe’s data protection law — it gives people the right to have their data deleted), and breach-window-forensics. Actor Identity’s walk regulator-audit-of-attribution, disputed-transaction-by-actor, and compromised-credential-discovery. Idempotent Reservation’s walk regulator-audit-for-double-charges, disputed-double-charge, and replay-attack — exercising the emergent invariants of the composition rather than the constituents’ invariants.

Generation acceptance

The Pass 3 gap. Success criteria for derived implementations are almost always implicit — the “the invariants hold and rejections surface” assumption. For regulated atoms, that assumption fails to specify what an external auditor reading the records must be able to do. The MUSE Proof node (the “Proof” checkpoint in GRID’s nine-node framework — requires success criteria be testable and defined upfront) requires success criteria be “measurable and defined before development begins,” but the bar is rarely written down; it lives in the architect’s head.

The structural fix. A standalone Generation acceptance section naming what a derived implementation must produce, framed as the bar an external auditor must be able to clear from the records alone, with no recourse to source code, runbooks, or developer narration. Typically four-to-six checks: reconstruct lifecycles from records, verify every invariant from records, observe every rejection-outcome class, identify composing patterns in use, trace ids across boundaries. The framing is “any code generated from this atom must produce records and a runtime surface that pass the following checks” — the generator’s contract.

Worked examples. Provisional Commitment’s Generation acceptance names four checks an external auditor performs against the commitment record set plus the composed Event Log. Actor Identity’s names five checks against the attestation store plus the actor registry’s public material. Idempotent Reservation’s names five checks that span the composition — including the token-to-commitment tracing that neither constituent atom owns alone.

When the conventions apply

Both conventions are required for patterns carrying the regulated overlay, patterns elsewhere whose examples invoke regulated domains (banking, healthcare, payments, hospitality with personal data, airline reservations), and compositions that compose any of the above.

Regulated adversarial scenarios are optional for non-regulated primitives — Personal Todo’s would be contrived. Use judgment; the test is whether an external evaluator with no developer access would have a meaningfully different verification surface from the atom’s existing structure.

Generation acceptance is no longer optional for anything, and the amendment has a cause (2026-09-14). The old rule made it optional for non-regulated primitives on the argument that their bar reduces to the invariants hold and rejections surface — which is true and is not a reason to leave the page silent, because optional and absent read alike from one layer up. A census on 2026-09-14 found three atoms carrying no acceptance surface at all, all three from the earliest migration wave, composed between them by eleven of the corpus’s compositions; Undo History rested thirteen Check rules on two constituents that audited none of their own rules, and nothing reported it, because a considered decline and an unconsidered silence are the same absence.

So presence is mandatory for every migrated spec, and the posture is what must be discoverable. A spec satisfies this in one of exactly two ways: it carries a Generation acceptance section with at least one Check or External check rule, or it declines by delegation — audit declined on its own Term qualifiers line, naming the pattern that owns the audit surface instead. Silence is the only thing outlawed. The point is not that every atom owes checks; it is that a composition resting its own acceptance on a constituent can discover that constituent’s posture mechanically rather than by reading the file and inferring from an absence. tools/linter/lint.py’s Y-acceptance-surface enforces both shapes and is pinned to synthetic fixtures; the bar each section must clear is unchanged and stays this section’s.

Where a section is written for a primitive, it is written from the spec’s own rules and invents no obligation — the atom’s existing claims become testable, which is what the old implicit in its invariants argument was really asserting and never made checkable.

The conventions are inherited rather than reinvented in each new pattern. Each new regulated atom or composition that lands lists “conventions inherited from prior work” in its landing commit and either points back to this section or to the worked examples it most closely follows.

Order and iteration

Phase 1 — Foundation: runs 1 → 2 → 3, once each. Pass 1 is mechanical and produces a list of structural gaps. Pass 2 looks at the in-pattern resolutions and asks whether they belong elsewhere. Pass 3 attacks what survives. All three must run before any refinement begins; the foundation is not optional and cannot be skipped.

Phase 2 — Refinement: re-run 1 → 2 → 3 as many times as needed. Each round of fixes changes the document and can surface new findings in any of the three passes. Pass 2’s extractions can re-introduce Pass 1 gaps. Pass 3 fixes can expose gaps that Pass 1 should have caught. The refinement loop has no fixed count — it runs until a complete pass across all three surfaces no new findings. This is expected: a complex atom with a novel structure may require two or three refinement rounds; a simpler atom closely following a prior pattern may need none. Both outcomes are normal.

Multi-file refinement order. When running refinement rounds across a library — all atoms and compositions in a single sweep — process in dependency order: atoms before any composition that names them. Compositions depend on their constituents’ APIs (rejection reasons, invariant counts, action signatures); refining a composition before its constituent forces guesses about the constituent’s details, and guesses introduce errors.

The corollary follows immediately: when a constituent’s refinement round changes its API — adds a rejection reason, corrects a reason name, adds an invariant — every composition naming that constituent needs a follow-up pass to absorb the change. This propagation is structural, not optional. An invariant count that was accurate at authoring time becomes stale the moment its constituent gains an invariant.

The motivating evidence is from the library’s own first refinement sweep. Shared Todo and Undo History were refined before Personal Todo; both used invalid-request for Personal Todo’s description-validation rejection, which turned out to be invalid-description. The error was only discoverable when Personal Todo was refined last and the correct name was confirmed. Strict dependency order — Personal Todo before any composition naming it — would have surfaced the discrepancy in-round rather than requiring retroactive correction. The same sweep also produced stale invariant counts in Shared Todo (referencing “nine Assignment invariants” after Assignment gained a tenth during its own refinement round), again a consequence of refining the composition before its constituent had fully settled.

The practical rule: before beginning a library-wide refinement sweep, topologically sort the files (order them so that each atom comes before any composition that depends on it). If a composition’s refinement reveals that a constituent’s details are needed but not yet confirmed, pause the composition and refine the constituent first. This is not a performance optimization — it is a correctness requirement for the cross-reference surface the library accumulates.

Reference-first for cross-cutting changes — gate the reference before the sweep. The dependency-order rule above governs independent refinements. A different and more expensive failure appears when one design decision is applied across many patterns at once — a corpus-wide refactor, not N unrelated touches. Here the rule is: apply the change to a single reference pattern, run the closing fresh-reader round (Phase 3) on that reference, and only sweep the rest once the reference clears. Principle: a cross-cutting decision is gated once, on the reference, before it is replicated. Likely objection: “the reference is obviously right; the sweep is mechanical.” Mechanism: the fresh-reader round exists precisely because author confidence is not the bar — running it on one pattern is cheap; running it on the reference after replication is not. Result: the blast radius of a wrong cross-cutting call is one pattern, not the corpus. Worked instance (2026-06-23): the derive expiry at read time initiative threaded the injected clock into action signatures across eight atoms before the reference was gated; the closing round rejected the signature form and the change was reverted across all eight — a cost the reference-first rule bounds to the single reference. This is the multi-file order rule lifted one level: settle-and-gate the decision before replicating it, exactly as you settle the constituent before the composition that names it.

Phase 3 — Final AI adversarial round: mandatory before grounded. After human refinement rounds have settled, one complete round of all three passes is conducted by a high-functioning AI reviewer before the pattern can declare grounded. This is not a repeat of Phase 2 — it is a structurally different kind of scrutiny. A human author who has written and revised a spec has emotional investment in the choices, accumulated blind spots from having reasoned through each decision, and a mental model that paper over gaps the written text does not actually close. An AI reviewer has none of these: it reads only what is written, applies the same pass questions without fatigue or sympathy, and has no stake in the outcome.

The AI round runs all three passes, not Pass 3 alone. Pass 1 and Pass 2 benefit from the same fresh-reader quality: the AI checks GRID completeness against what the spec actually says, not what the author knows it means; and it applies the EOS extraction test without the author’s sense of “we already talked about this.” Pass 3 is where the AI’s adversarial posture is most distinctive — it will surface muddled identity, sloppy invariants, and happy-path-only examples that a sympathetic human reviewer may rationalize past.

What counts as a high-functioning AI reviewer. The bar is not model-specific — it is prompt discipline and structured question coverage. The AI must be given the full pass question sets from this document, the pattern under review in full, and no additional context about the author’s intent beyond what the spec itself states. The reviewer’s job is to surface findings, not to guess what the author meant. A review that paraphrases the spec back is not a pass — it is a read. A pass produces findings, named as findings, or a clean result with explicit confirmation that each question was applied and no gap was found.

Recording the AI round. AI-conducted rounds are recorded in the commit message in the same format as human rounds, but distinguished: the entry notes “AI-conducted round” and names the model used. This is not for model attribution — it is for reproducibility. A future reader who wants to re-run the round knows what prompt discipline and reviewer type produced the original findings. Findings closed in the AI round are recorded the same way as findings closed in human rounds: what was found, how it was resolved.

Fresh-reader discipline, defined operationally. Fresh-reader is the structural property that makes Phase 3 different from refinement Pass 3, not the human/AI distinction. A reviewer satisfies fresh-reader discipline when, for the round in question, the reviewer receives: (a) the full pass question sets from this document; (b) the pattern under review in full; and (c) nothing else — no author intent, no rationale, no prior-round findings from this pattern, no summary of what the author thinks the spec says. A reviewer who reads prior-round findings before applying Pass 3 is conducting refinement Pass 3, which is also valuable but is not Phase 3. The discipline forecloses two specific failure modes: the reviewer rationalizing past a gap because a prior round noted and resolved an adjacent one (“the author addressed this nearby issue, so this nearby gap is probably intentional”), and the reviewer pattern-matching to prior findings instead of attacking the text on its own terms. Refinement rounds can use findings context to drive convergence; the closing Phase 3 round cannot.

Automated councils satisfying Phase 3. Phase 3 may be conducted by a single AI reviewer in one session or by an automated council that decomposes the three passes across agents (typically one agent per pass plus a consolidate step). The Phase 3 discipline applies uniformly to Pass 3: Pass 3 always runs in fresh-reader mode, in every round, regardless of whether the round is refinement or final. Pass 1 and Pass 2 findings drive document changes between rounds (applied by a human, an apply-agent, or whatever the council provides); Pass 3 then reads the resulting document with no findings context. Every Pass 3 invocation is structurally a Phase 3 candidate; the invocation that surfaces no findings — i.e., a clean Pass 3 in a round where Passes 1 and 2 were also clean — grants grounded eligibility. There is no mode switch, no “final round” detection, no escalation logic. The rule chooses simplicity and discipline over convergence speed: redundant findings during refinement (Pass 3 surfacing the same gap across rounds before the document fully absorbs the fix) is a small cost; priming Pass 3 with prior findings is the exact failure the fresh-reader discipline exists to foreclose. Pass 1 and Pass 2 may flow findings forward within a round (Pass 2 may read Pass 1’s findings; Pass 1 has no prior to read) — those passes are structural and conceptual rather than adversarial, and findings context does not undermine their job. The commit message records the council pattern used (which model per agent, which formula) and confirm that Pass 3 ran in fresh-reader mode throughout.

Phase 4 — Readiness check: Opus at Happy Torvalds X2. (Opus is Anthropic’s most capable AI model; “Happy Torvalds X2” means applying Opus’s full intelligence to confirm the spec is generation-ready — not to achieve perfection, but to clear the bar for shipping.) After the nine-pass minimum has been satisfied and Phase 3 returns clean, one additional mandatory pass runs before the pattern may declare grounded. This pass is conducted by Opus — the most capable available model — at twice the analytical depth of standard Pass 3 (Linus mode). It is not a fourth round in the same sense as Phases 1–3; it is a single-pass readiness check whose job is to confirm the spec is good enough to generate from. Code can be regenerated at any time as the spec improves; the goal here is to ship fast and good, then iterate.

Why a separate check, and why Opus at X2. A pattern that has survived nine passes has been iterated and defended. Standard Phase 3 uses “a high-functioning AI reviewer” with structured question coverage and fresh-reader discipline; that bar is correct for the closing AI round of a refinement sequence. Phase 4 applies Opus’s full intelligence to answer one question: is this spec ready to generate reliable code from? Opus at X2 depth catches anything that would produce bad generated output — gaps in the identity model, invariants that break under real conditions, concept boundaries that would cause generation to go wrong — while staying focused on generation-readiness rather than theoretical perfection. The safety net is regeneration: because code is derived from the spec, any future improvement to the spec is immediately realizable. A grounded spec is the starting point for that cycle.

What X2 depth means operationally. The reviewer receives the full pass question sets, the pattern in full, and nothing else — fresh-reader discipline still applies. Pass 1 and Pass 2 run at standard intensity. Pass 3 runs at X2: the reviewer brings full intelligence to bear on whether the spec is generation-ready. Every concept boundary is tested — is it real, or would it cause generated code to absorb the wrong responsibility? Every invariant is tested for conditionality gaps — does it hold under real conditions, not just the happy path? Every example is tested for coverage — would a regulator or a real user find a scenario the spec doesn’t handle? The posture is not “achieve perfection” but “confirm this is good enough to ship from, knowing iteration will follow.”

Recording the clearance gate. The commit message notes “Opus clearance gate — Happy Torvalds X2” and the model version used. Each finding is classified at the time it is recorded — foundational (missing methodology-required content; blocks grounding until closed), refining (sharpens content the spec already has; closed in-pattern but does not block), or rhetorical (prose-only attack on sound content; recorded with classification but does not block). A routed finding’s Ledger line is id · class · where · defect → fix. If foundational findings remain after the round’s fixes land, the gate runs again; the pattern remains partially resolved until the gate returns with zero foundational findings (the 92%-good threshold — see §”What grounded means”). A gate result that meets the threshold is the Ledger’s last gate: line when grounded is declared.

The minimum standard stated plainly. Three rounds × three passes = nine passes minimum, plus one Opus clearance gate (Phase 4), plus the formal-layer vote (and, where the vote is yes, a verifying derived formal model before unqualified grounded). Round 1 is the foundation (Pass 1 → 2 → 3, once each). Rounds 2 through N−1 are human or council refinement, running until a complete round surfaces no new findings. Round N is the final AI adversarial round (Phase 3), running all three passes with fresh-reader discipline — single-reviewer or automated-council, the discipline is what counts. After Round N returns clean, the Opus clearance gate (Phase 4) runs as the tenth and final step. A pattern that has not cleared the Phase 4 gate has not met the minimum standard and should not declare grounded, regardless of how many refinement rounds it has survived.

Round structure and naming — the canonical grounding marker. The phases above describe what runs; this paragraph canonicalizes how rounds are counted and named, because two numbering schemes circulated before it was written down. The 3×3 baseline is three rounds of the three passes — Round 1 runs Pass 1 / Pass 2 / Pass 3; Round 2 runs Pass 1 / Pass 2 / Pass 3; Round 3 runs Pass 1 / Pass 2 / Pass 3. Pass numbering resets per round, so “Pass 3” always means the Linus adversarial pass, never the third pass-of-nine. After the baseline, Final Critique runs as the AI-conducted closing round starting at Round 4 — in current practice the Phase 3 final adversarial round and the Phase 4 Opus clearance gate run together as this single Opus round (fresh-reader discipline throughout, X2 depth on Pass 3, findings classified foundational / refining / rhetorical). If Final Critique 4 closes clean, the pattern is grounded on Final Critique 4; if it surfaces findings, a refinement round absorbs them and the pattern grounds on Final Critique 5, then 6, and so on until the threshold clears — foundational findings at zero; refining and rhetorical findings may remain (the 92%-good threshold, §”What grounded means”). grounded on Final Critique N is the canonical grounding marker recorded in the pattern’s Status line and Ledger. Older patterns that used cumulative Pass 1–9 numbering (Defensible Retention is the worked example) carry a retro-mapping note explaining the relabel; the unified convention is per-round Pass 1/2/3 + Final Critique.

Skipping is not an option. Each pass catches a different class of gap. A pattern that has only survived Pass 1 is structurally complete but probably absorbs responsibilities it shouldn’t and contains hidden decisions. A pattern that has only survived Pass 3 is precise but may be missing entire GRID nodes. Either is incomplete. Refinement passes do not substitute for the foundation — they extend it. The AI round does not substitute for human refinement — it concludes it.

What “grounded” means

A pattern reaches the grounded status — the state declared in its Status section — when:

All nine GRID nodes are resolved (Pass 1 clean).
Every responsibility belongs to the pattern it’s in; no over-absorptions remain (Pass 2 clean).
No muddled identity, sloppy invariants, happy-path-only examples, or hidden load-bearing decisions remain (Pass 3 clean).
All three conditions above have been confirmed by a final AI-conducted round (Phase 3), with findings recorded in the Ledger (open) or the commit (closed).
The Opus readiness check (Phase 4 — Happy Torvalds X2) has returned at-or-above the 92%-good threshold (see below), with the gate result recorded on the Ledger’s last gate: line.
The formal-layer vote has been cast and recorded on the Ledger’s formal: line (see Formal models — The formal-layer vote). If the vote is yes, the derived formal model exists and verifies; until it does, the pattern is grounded (English) — formal layer pending, not grounded.

grounded is a launch point, not a finish line. The spec is ready to generate from; further refinement rounds will continue to improve it; and because code is derived from the spec, every improvement is immediately realizable by regenerating.

The 92%-good grounding threshold. A pattern grounds when the Phase 4 readiness check’s foundational findings reach zero, even if refining and rhetorical findings remain. “92%-good” is the colloquial label: foundationally complete, generation-ready, no methodology-required content missing. The threshold is intentionally not 100% for two reasons. First, X2 depth has no convergence ceiling — a sufficiently thorough reviewer can always find prose to sharpen regardless of whether the underlying content is sound, and demanding zero refining or rhetorical findings would mean a spec never ships. Second, perfection isn’t required: code is a derived artifact that regenerates from the spec. Any improvement to the spec after grounding is immediately realizable. The goal is to ship a spec that generates reliable code today and keep improving it — not to spend indefinite refinement rounds chasing a spec that will never run.

Each gate finding is classified into one of three classes, recorded with the finding in Lineage notes:

Foundational — the spec is missing content the methodology’s pass questions require: a state-machine gap, an unstated invariant, an unaddressed pass question, a regulated-overlay section missing despite the required-when clause applying, a composing concept silently absorbed or silently absent, a deployment-obligation not named anywhere. The fix adds previously-absent content. Foundational findings block grounding — they must be closed in-pattern before the gate counts as clean.

Refining — the spec contains the required content but a section overstates a claim, two sections disagree, a fix from a prior round didn’t propagate everywhere it should, a primitive policy is too thin to defend, a deployment obligation is named in one place but missing from the obligations list. The fix sharpens content the spec already has. Refining findings do not block grounding — they are closed in-pattern alongside foundational ones (the fix is cheap and improves the spec) but the load-bearing surface was already present.

Rhetorical — the spec’s content is sound and the methodology’s pass questions are answered, but the reviewer at X2 intensity has attacked the phrasing the spec uses to defend a claim. The fix is a prose rewrite that says the same thing in different words. Rhetorical findings do not block grounding — they are recorded with classification visible and either closed (rewritten) or accepted (recorded as-is with rationale) per the author’s call.

The threshold operationally. A clearance gate counts as clean for grounding purposes when its foundational finding count is zero — regardless of how many refining or rhetorical findings the same gate surfaced. If foundational findings remain after the round’s fixes land, the pattern remains partially resolved and another round runs. The grounding bar is foundational completeness, not absence-of-all-reviewer-findings.

The “~92%, not 100%” framing recognizes that complex patterns produce refining and rhetorical surface area as a side effect of their defenses; demanding zero of either at X2 is demanding the prose and cross-section consistency be unattackable, which is a different bar than demanding the content be correct. Round 1 of any pattern is typically 100% foundational by classification (foundation gaps). Round 2 typically surfaces a mix as the foundational surface fills in. Subsequent rounds shift the mix toward refining and rhetorical with diminishing returns. The pattern grounds when foundational density reaches zero — empirically the second-or-third round for richly-surfaced atoms, the first round for simpler primitives.

The classification is the reviewer’s call. The Ledger’s per-finding format is: id · class · where · defect → fix, one line, the class one of the three above.* Future readers can audit the classification by inspection.

Status line format — the canonical grammar (pinned 2026-06-11). Every pattern carries a ## Status section (the container is required by spec-format.md; a top-of-file **Status:** line is a shape deviation, not an alternative placement). The section’s first line is the status line: exactly one backticked status token, optionally followed by prose. All explanatory content — round history, model references, gate results, glosses — lives in the prose, never inside the backticks: a Tier-1 gloss inside the token is unparseable by the mechanical checks that mirror it. Before this grammar was pinned, the corpus carried at least six surface shapes for the same statuses, which made the roadmap’s status mirror un-lintable by hand or machine — that is the failure this grammar exists to close. The tokens:

`draft` — freshly authored; the foundation round has not run.
`unresolved` / `partially resolved` — per the taxonomy above.
`grounded on Final Critique N — YYYY-MM-DD` — the canonical grounded form. N is the grounding critique (§Round structure and naming); the date is the most recent complete three-pass round, updated by every touch-triggered re-pass and scheduled rescan.
`grounded (English) on Final Critique N — YYYY-MM-DD — formal layer pending` — vote-yes, derived model not yet verifying (§The formal-layer vote). This state is referred to throughout this document by its short prose name, grounded (English) — formal layer pending; an actual Status line carries the full token with its Final Critique number and date.
`grounded on Final Critique N — YYYY-MM-DD — <named item> pending` — the bounded-qualifier form for a routed finding blocking one named surface (the worked precedent: formal coverage of Invariant 4 pending on Forensic Recovery and Chain of Custody, 2026-06-10 → closed 2026-06-11); the prose names the finding id. <named item> never names the formal layer — the formal-pending state is the previous form’s exclusively, so the two forms cannot collide on the same line.

The status token is the surface the roadmap’s status cells mirror — the pattern file is the source of truth, and a roadmap cell that disagrees with the pattern’s token is a finding (the status-mirror lint check). A pattern whose rescan date is significantly older than the current date — particularly one that predates atoms it now composes with — is a candidate for the next scheduled sweep.

Patterns that have survived only one or two passes should not declare grounded. Patterns that have completed human refinement but not the AI round should declare partially resolved. A pattern whose formal-layer vote is yes but whose verifying model does not yet exist declares grounded (English) — formal layer pending — the prose review is complete and clean, but the temporal claims await discharge on the formal surface. Honest partial completion is more useful than false confidence. Touch triggers re-pass — for load-bearing touches. A load-bearing edit to a grounded pattern — a change to an invariant, a state, an action signature, a rejection reason, a decision rule, or any content the pass questions verify — requires a full three-pass round (the AI round included) before the pattern may retain its grounded status; a pattern so touched is downgraded to partially resolved until the round completes. This is not punitive; it is what keeps grounded meaningful as the library grows.

Editorial touches do not trigger a re-pass. A purely editorial edit — a prose rewrite that changes no load-bearing content, a typo or comment fix, a Decisions entry, or a cross-reference whose target moved while its meaning did not — is recorded in its commit but does not downgrade the pattern or require a fresh round. The test is the constituent-cascade test (breaking vs additive) applied to the pattern itself: does the edit change what a conforming implementation must do, or what a reviewer’s pass questions would check? If not, it is editorial. The earlier formulation — which counted any edit, including a corrected cross-reference, as a re-pass trigger — made the cheapest upkeep as costly as a semantic change and so discouraged the very maintenance that keeps the corpus consistent; calibrating the trigger to load-bearing content removes that disincentive without lowering the bar for changes that actually alter meaning. (Doc-structure consequence: re-pointing cross-references after a file move is editorial, which softens one argument in §The methodology applied to itself against splitting this document — the split’s other costs stand on their own.)

Batch a cross-cutting change through one re-gate. When the reference-first rule (§Multi-file refinement order) has gated a cross-cutting decision and the change is then swept across a batch of patterns, the batch earns one closing round over the touched set — not an independent full cycle per pattern. The assurance lives in the gate, and one fresh-reader gate over the consistent batch is the unit; re-passing each pattern separately multiplies reviewer cost without adding assurance. Reground the batch together once the round is clean. The distinction is load-bearing for cost: the scheduled cadence is calibrated for confirming stable patterns (cheap clean rescans that ratchet confidence), while propagating a cross-cutting design change is this other workflow — reference-first, then swept, then one batched gate. Conflating the two is what makes a single improvement feel like it re-passes the whole corpus.

Constituent-change cascade. A breaking change to a grounded atom — an invariant removed, an action signature incompatibly altered, a state machine transition removed — triggers a touch-triggered re-pass on every grounded composition that names that atom in its Composes section. Each affected composition is downgraded to partially resolved until its re-pass completes. An additive change (new invariant, new edge case, new example, editorial correction) does not trigger a cascade downgrade; the “all invariants from [Atom]” cross-reference form means the composition’s claim is already forward-compatible with constituent growth. Additive atom changes should note “Compositions affected: [list]” in the commit message so the next scheduled sweep can prioritize them.

Scheduled rescan. Grounded patterns are also re-passed on a regular schedule — a weekly or weekend batch is the working default — regardless of whether anything has touched them. A scheduled rescan is the same complete three-pass round as a touch-triggered re-pass; it is not a lighter check. Its purpose is not to find regressions (the spec hasn’t changed, so the spec itself can’t have regressed) but to ratchet confidence in the pattern as the library’s surrounding context evolves. Each clean rescan is independent corroborating evidence that the pattern still holds against the current state of the library’s vocabulary, the current state of the constituent atoms it composes with, and (for AI rounds) the current state of reviewer models. A pattern that has survived five scheduled rescans without findings is materially more reliable than one that has survived one — the number of clean rescans is part of what grounded means in practice, even though the status word is the same.

The default executor is the automated council. A scheduled rescan is council-run by default: the §”Automated councils satisfying Phase 3” machinery conducts the round — typically one agent per pass plus a consolidate step — with Pass 3 in strict fresh-reader mode throughout (the pass question sets and the pattern under review, nothing else). Pass 1 and Pass 2 agents may verify cross-references against the constituent specs the pattern names; that is structural checking, not findings context. For a vote-yes pattern, the same round carries the formal-layer portion below, riding tools/harness/ mechanically. Human attention goes to triage of council findings — classifying, folding fixes, routing extractions — never to conducting rounds. This is not a weakening of the discipline; it is what keeps the cadence executable. A rescan discipline that exceeds the review attention actually available does not degrade gracefully — it silently stops running, and the Status lines’ rescan dates become quiet fiction, which is precisely the false-confidence failure this methodology exists to prevent. A human-conducted rescan remains valid (it is the same three-pass round), but it is the exception, not the load-bearing default. The Ledger’s last gate: line names the executor: a clean council-run rescan records “Scheduled rescan: YYYY-MM-DD — clean (council-run).”

The cost model — parameterized, never snapshotted. The rescan economics are stated as parameters, not arithmetic: per the no-snapshot rule, this section carries no corpus-size math — the corpus and the costs both move; the parameters, not their current values, are canonical. Two parameters govern the cadence:

The weekly rescan budget — a deployment-set number of full council rounds funded per week. It is set explicitly and revisited as measured costs or the corpus change; the measured per-pattern cost of each rescan is recorded on the rescan’s own evidence trail (the commit message, or the deployment’s usage log), so the budget rests on observed cost rather than guessed cost.
Risk-weighted ordering when the budget is short. When the budget covers fewer patterns than the grounded corpus, rescans run oldest-rescan-date-first — staleness is the dominant risk signal, because the longest-unreviewed pattern has accumulated the most unexamined drift in the library context around it — tie-broken by composition fan-in: the count of grounded compositions naming the pattern in their Composes sections. Fan-in breaks ties toward the patterns whose staleness propagates furthest; a stale atom named by six compositions is a bigger liability than an equally stale leaf. Patterns carrying open routed findings are not rescan candidates — their next round is the touch-shaped round that folds the fix, and it rides its own trigger, not the rescan queue.

A scheduled rescan can surface findings for reasons the prior round could not have caught. Three of the common cases:

A constituent atom has been refined since the last rescan, gaining a new invariant or renaming a rejection reason; the composition’s cross-references are now stale. This is the multi-file refinement order rule operating at the timescale of weeks rather than within a single sweep.
Methodology conventions added since the last rescan apply retroactively. The two regulated-pattern conventions (Regulated adversarial scenarios; Generation acceptance) and the Audit-Trail-traversal-clearable / externally-clearable split from Multi-Party Approval’s Round 3 are examples; both were applied retroactively to earlier patterns once codified.
The reviewer (human or AI) has improved. An adversarial pass conducted today by a sharper reviewer than the prior round can surface a finding the prior round missed without the spec having changed.

A scheduled rescan that closes with no findings updates the rescan date in the Status token and the Ledger’s last gate: line, naming the executor: “Scheduled rescan: YYYY-MM-DD — clean (council-run)” for the default, “— clean” for a human-conducted round. A scheduled rescan that surfaces findings is treated identically to a touch-triggered re-pass — open lines in the Ledger for what is routed, the fixes and their reasoning in the commit, status preserved at grounded only if the round closes clean across all three passes. Findings from a scheduled rescan are not a failure of the prior round; they are the rescan doing its job.

For a pattern carrying a vote-yes formal model, the rescan’s formal-layer portion is three cheap mechanical steps, all of which ride this same cadence: (1) re-run the model and its buggy twin through tools/harness/ (the twin must still be rejected); (2) run the coverage cross-check (see §”The coverage cross-check”) — emit the coverage matrix, route any GAP row as a finding; (3) take the one bound-saturation bump. None of these requires new tooling or heavier search; the coverage cross-check in particular is the highest-yield-per-minute step for closing the property-fidelity residual, which is why it belongs in every formal-layer rescan rather than in an occasional special pass.

The cadence is deployment-shaped. The working default is weekly with weekends as the batch window, but a library churning slowly may rescan less often, and a library under active multi-author refinement may rescan more often. The discipline is that the cadence is fixed and externally driven, not “when somebody remembers.” The whole point is to ratchet confidence on a rhythm independent of any particular author’s attention — and the council-as-default-executor is what makes that independence real: the schedule fires the council and the budget bounds the batch, so the cadence holds whether or not any human had review hours that week. Human hours are spent where they are irreplaceable — triage.

Where the journey gets recorded

Each pattern carries two sections after its Status, and nothing else about its history: a Ledger and a Decisions list. The narrative of every round — what a pass surfaced, what was fixed, what was argued — lives in the commit that made the change, and git log -- <file> is the per-pattern index of it. This replaced the prose Lineage notes on 2026-08-27, when fifty-two Lineages totalling close to two million characters had become the corpus’s largest reading cost and its least reliable record: closures were recorded in some patterns inline and in others in later entries, aggregate counts went stale within a day, and a health census took a day’s reading and was wrong when done.

The Ledger is the countable single source of truth for a pattern’s health, in a fenced block with a fixed grammar the linter parses (R-ledger-* checks; python3 tools/linter/lint.py --census derives the corpus tally from it):

status: partially resolved
formal: verified — login.tla, no twin, 2026-05-23
last gate: 2026-08-27 — fresh reader — 7 foundational, 10 refining, 5 rhetorical

open:
- 2026-08-27-a · foundational · Action wiring, cascade step 4 · `failures` is consumed and initialized nowhere → initialize at step 4; increment on 5b's failure arm

Five fields per open line — id, class, where, defect, fix — with → between defect and fix. Ids are date-based (YYYY-MM-DD-x), never gate-based, so a finding does not need to know which round found it. Classes are foundational, refining, rhetorical per §The 92%-good grounding threshold. When a finding closes, its line is deleted; if the closure carried a directional decision, that goes in Decisions; the fact that it was found and closed is in git. The linter refuses by construction: a grounded token with an open foundational line, a Ledger status that disagrees with the Status line, and every grammar fault. formal: states the model files and their verification date, pending with a reason, or not applicable with the vote — and it states what is on disk, not what an entry claims.

Decisions are directional changes only — the turns a future reader must know the pattern took — in three fields, no narrative: - **YYYY-MM-DD — title.** *Chose:* … *Over:* … *Because:* …. An implementation choice is not a direction; it is in the commit. A gate’s roster is not a direction. A choice a Hard invariant of GRACE-lang.md forbids is not a direction either: a Decisions entry cannot make it lawful, so the review that finds one repairs the spec and corrects the entry rather than letting the entry stand as its justification — Provenance’s renumbering was recorded as a choice for four days before a citation broke on it (council read 95). The test is whether the pattern would be a different pattern had it gone the other way; a mature pattern has two or three entries, and many have none.

Which makes the commit message load-bearing. A commit that changes a spec carries the why in its message; the spec carries the what, and for directional changes, the why. A round whose commit message would not let a future reader reconstruct its reasoning has not finished. The corpus’s rule stands — never commit; propose the message in chat — but the message is no longer a courtesy summary.

The methodology applied to itself

The methodology applied to a pattern produces a Ledger, a Decisions list and a commit history. That record can itself be pressure-tested by re-running the three passes — does the recorded reasoning hold up under structural, conceptual-independence, and adversarial scrutiny?

The methodology document itself is subject to its own three passes. This file has been written through the same arc that produced Personal Todo: name the structure, check for over-absorption, attack the remaining vagueness. If you find this document hand-waving anywhere, that is a Pass-3 finding against the methodology, and it should be fixed here the same way it would be fixed in any other spec.

A recorded Pass-2 self-finding — the split, considered and declined. Run against this document, Pass 2 surfaces a real over-absorption candidate: the file carries both the three-pass process every pattern walks and the formal-layer machinery that only vote-yes patterns exercise in full — the vote, the model-present bar, the authoring pitfalls, the English/formal SSOT and conflict protocol, the coverage cross-check — so a contributor authoring a simple vote-no atom reads past all of it. The remedy proposed was a split: a lean process document here, a formal-layer.md taking the formal machinery, capability provenance routed to that document or to spec-format.md, embedded change-history to changelog.md. The split was considered and declined; the reasoning is recorded here rather than lost, because the next reader will feel the same pull and deserves the argument, not a silent absence:

Every cut splits a single rule across the seam. The formal layer interlocks with the three-pass process at point after point, and each place the split would sever lands one rule in two files — the exact one-SSOT-per-rule violation the spec-format.md / Execution Contract ownership seam was assigned to end, reintroduced for a weaker reason. The sharpest instance is the grounding gate: the formal-layer vote is mandatory for every pattern, vote-yes or vote-no, and carries the model-present bar by reference (a vote-yes pattern stays grounded (English) — formal layer pending until it clears the bar), so “the three passes plus grounding semantics” and “the vote plus the bar” cannot live in separate documents without one rule spanning both. The same cut recurs throughout: Pass 1’s Proof node names the formal model; Pass 3’s logic-confinement question is the model’s determinism precondition; the coverage cross-check is a scheduled-rescan sub-step, not freestanding formal machinery; “what grounded means” is stated in terms of the vote and the bar.
The corpus links section-into-file, and re-pointing is not free. Patterns across the grounded corpus cite this document’s §Formal models — The formal-layer vote, §Capability provenance, and the regulated conventions as file-level references that name the section in prose. A split re-points every one of them — and a corrected cross-reference is itself a touch-trigger (see §Touch triggers re-pass), so the mechanical fix would brush a partially resolved downgrade across the grounded corpus to relocate the weakest finding in the set. The cure costs more than the disease.
The change-history that looks extractable mostly is not — the first reason, applied to the cut that looks safest. The “canonicalized in Round N” and retro-mapping sentences read like changelog in canonical space, but most are worked examples discharging this document’s own defend-each-claim-in-line discipline — the capability.als typecheck error justifying the model-present bar, Defensible Retention’s relabel explaining the round-naming convention. Moving them to changelog.md would strip the in-line defense the methodology requires of every architectural claim.

The over-absorption is real, and the benefit is worth naming plainly: a contributor authoring a simple vote-no atom does read past the entire formal-layer machinery, and a split would spare them that. But the benefit is bounded — a vote-no author already skips those sections in practice, so the cost they pay is reading-order, not correctness — while the remedy’s cost is not: a document seam to maintain in perpetuity, much of the grounded corpus touched, both halves owed a fresh adversarial read under this very section’s applied-to-itself rule. Weighed at the same resolution, the cost exceeds the benefit. The condition that would re-open the decision is concrete and falsifiable: when the formal layer grows surface that no three-pass process step references — whether a second formal tool or a standalone model-authoring guide, the test being that no process step depends on it — it will have earned its own document, and the split becomes worth executing. Until then the single document holds.

Each fresh use of the methodology becomes evidence the architecture is doing real work — both for the pattern under review and for the methodology itself.

Three classes of gap, three classes of fix

Phase	Pass	Class of gap	Lens	Typical fix
1–3	1 — GRID	Missing pieces	Structural completeness	Specify the missing node; resolve dangling references
1–3	2 — EOS	Over-absorption	Conceptual independence	Extract the over-absorbed responsibility as its own atom; document the composition
1–3	3 — Linus	Hidden decisions	Adversarial scrutiny	State the load-bearing decision explicitly; tighten invariants; add rejection-path examples
4	Clearance gate	Foundational / refining / rhetorical findings	Opus — Happy Torvalds X2	Close foundational gaps (blocks grounding); close refining findings in-pattern (does not block); record rhetorical findings with classification (does not block). Ground at zero foundational — the 92%-good threshold; see §”What grounded means”

A pattern is grounded when rows 1–3 are clean and row 4’s foundational-finding count is zero. Until then, the pattern is in process — and that is a respectable state to be in, provided the actual state is declared honestly.

The shortest path to a grounded pattern is to run all three passes early and iterate through as many refinement rounds as the pattern needs. The longest path is to declare grounded prematurely — whether after one pass or after three passes that were not adversarial enough. Premature grounding means the spec, the implementations that depend on it, and the contributors who reviewed it must all be revisited together when the gaps surface later. Refinement passes are cheaper before grounded than after.