diff --git a/AGENTS.md b/AGENTS.md
index 4d3a53e..6a3fa1e 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -41,6 +41,8 @@ When a task uses a fact owned by another package, read that package before using
 - `code.hybscloud.com/sess` for protocol frontiers, branching, endpoint transitions, and session close semantics.
 - `code.hybscloud.com/takt` for runner movement, polling, resumption, completion memory, completion routing, and route-indexed stream carriers.
 
+For broad guide edits, runtime-utilization edits, or review work that changes the cross-package model, read the complete current source of every package whose facts the edited guide relies on. In practice, this usually means `code.hybscloud.com/iox`, `code.hybscloud.com/iofd`, `code.hybscloud.com/sock`, `code.hybscloud.com/kont`, `code.hybscloud.com/cove`, `code.hybscloud.com/takt`, and `code.hybscloud.com/sess` before changing `uring/AGENTS.md` or any file under `uring/agents/`. Extend that set with `code.hybscloud.com/zcall`, `code.hybscloud.com/iobuf`, `code.hybscloud.com/spin`, `code.hybscloud.com/lfq`, or `code.hybscloud.com/framer` whenever the edited guide cites syscall, buffer, spin/yield, mailbox, or framing facts.
+
 Before generating or reviewing code, read every guide file needed by the task. A file is needed when its topic names a fact, action, resource, outcome, frontier, policy, or obligation used by that task.
 
 Read in this order:
diff --git a/agents/boundary/integration.md b/agents/boundary/integration.md
index a348017..9381bbe 100644
--- a/agents/boundary/integration.md
+++ b/agents/boundary/integration.md
@@ -1,12 +1,12 @@
 # Integration Boundary
 
-Using `uring` correctly means using it *with* its neighbours, each in its own lane, and never letting one package's job leak into another's. This file is the map of who owns what. `OwnerMap` assigns every role to exactly one package: outcome and stream vocabulary to `iox`, descriptors to `iofd`, addresses to `sock`, buffers to `iobuf`, suspension and one-shot resumption to `kont`, protocol frontiers to `sess`, route and subscription frontiers to `takt`, and so on. The rules then pin which facts may be projected across the package boundary and which — caller frontier, caller policy, `cove` requirement evidence, resumptions, mailbox policy, and completion-memory policy — must stay strictly in caller code, and require that every action go through the public surface rather than a bypass.
+Using `code.hybscloud.com/uring` correctly means using it *with* its neighbours, each in its own lane, and never letting one package's job leak into another's. This file is the map of who owns what. `OwnerMap` assigns every role to exactly one package: outcome and stream vocabulary to `code.hybscloud.com/iox`, descriptors to `code.hybscloud.com/iofd`, addresses to `code.hybscloud.com/sock`, buffers to `code.hybscloud.com/iobuf`, suspension and one-shot resumption to `code.hybscloud.com/kont`, protocol frontiers to `code.hybscloud.com/sess`, route and subscription frontiers to `code.hybscloud.com/takt`, and so on. The rules then pin which facts may be projected across the package boundary and which — caller frontier, caller policy, `code.hybscloud.com/cove` requirement evidence, resumptions, mailbox policy, and completion-memory policy — must stay strictly in caller code, and require that every action go through the public surface rather than a bypass.
 
 In plain terms, the rules an agent follows here are:
 
-- Every role has exactly one owner, and you read that owner before using its facts. Outcome, stream, datagram, and byte-progress vocabulary belong to `iox`; syscall result and errno to `zcall`; descriptors to `iofd`; socket addresses to `sock`; buffers to `iobuf`; spin, yield, and lock to `spin`; the caller mailbox queue to `lfq`; frame boundaries to `framer`; context, requirement, and safety evidence to `cove`; suspension and one-shot resumption to `kont`; protocol frontiers to `sess`; and route, subscription, runner-movement, and completion-memory vocabulary to `takt`.
+- Every role has exactly one owner, and you read that owner before using its facts. Outcome, stream, datagram, and byte-progress vocabulary belong to `code.hybscloud.com/iox`; syscall result and errno to `code.hybscloud.com/zcall`; descriptors to `code.hybscloud.com/iofd`; socket addresses to `code.hybscloud.com/sock`; buffers to `code.hybscloud.com/iobuf`; spin, yield, and lock to `code.hybscloud.com/spin`; the caller mailbox queue to `code.hybscloud.com/lfq`; frame boundaries to `code.hybscloud.com/framer`; context, requirement, and safety evidence to `code.hybscloud.com/cove`; suspension and one-shot resumption to `code.hybscloud.com/kont`; protocol frontiers to `code.hybscloud.com/sess`; and route, subscription, runner-movement, and completion-memory vocabulary to `code.hybscloud.com/takt`.
 - Only owned boundary inputs may cross into the boundary. The boundary-projectable carriers are the outcome contract, descriptor authority, socket address, buffer fact, spin/yield fact, and frame boundary; nothing else is projected across.
-- Caller frontier and caller policy never cross into the boundary. Context, requirement, and safety evidence from `cove` may guard caller decisions and may justify copied boundary inputs, but the `cove` carriers themselves stay in caller code. Resumptions, mailbox policy, and completion-memory facts and policy also stay strictly in caller code, and projecting any of them into the boundary is rejected.
+- Caller frontier and caller policy never cross into the boundary. Context, requirement, and safety evidence from `code.hybscloud.com/cove` may guard caller decisions and may justify copied boundary inputs, but carriers from `code.hybscloud.com/cove` stay in caller code. Resumptions, mailbox policy, and completion-memory facts and policy also stay strictly in caller code, and projecting any of them into the boundary is rejected.
 - Every action goes through the public surface. An action that bypasses the public surface is rejected.
 
 The block below states these rules formally.
diff --git a/agents/boundary/protocols.md b/agents/boundary/protocols.md
index e5c8c8f..002d07c 100644
--- a/agents/boundary/protocols.md
+++ b/agents/boundary/protocols.md
@@ -6,14 +6,14 @@ The block carries the same discipline onto the Go surface: a `GoHandler` is shal
 
 In plain terms, the rules an agent follows here are:
 
-- Own the protocol; the package only observes. Stream, datagram, outcome, and byte-progress vocabulary belong to `iox`; suspension and one-shot resumption to `kont`; protocol frontiers to `sess`; route, subscription, runner-movement, and completion-memory vocabulary to `takt`; safety evidence to `cove`; spin, yield, and lock to `spin`. The protocol frontier and policy are caller-owned, and the protocol transition taken after an observation is caller-defined and never lives inside the boundary.
+- Own the protocol; the package only observes. Stream, datagram, outcome, and byte-progress vocabulary belong to `code.hybscloud.com/iox`; suspension and one-shot resumption to `code.hybscloud.com/kont`; protocol frontiers to `code.hybscloud.com/sess`; route, subscription, runner-movement, and completion-memory vocabulary to `code.hybscloud.com/takt`; safety evidence to `code.hybscloud.com/cove`; spin, yield, and lock to `code.hybscloud.com/spin`. The protocol frontier and policy are caller-owned, and the protocol transition taken after an observation is caller-defined and never lives inside the boundary.
 - Read multishot completions as frontier facts, using the same four-way decode. A non-negative multishot CQE with `MORE` is a live success that keeps the frontier non-terminal and signals that a successor observation may arrive; a negative multishot CQE with `MORE` is a non-terminal failure. A failure with `MORE` is never `errMore`, never byte progress, and never terminal.
 - Decode zero-copy release separately. A release-ready CQE decodes to a release observation with no control value, carrying the `NOTIF` flag when the release is notification-driven and not when it is the terminal no-notification fallback; a notification that is not release-ready, and an early notification, both produce no outcome and no release.
 - Hand result resources to the caller. A returned descriptor or selected buffer is owned by the caller and never appears on a non-terminal frontier.
 - Treat the package as a shallow handler, never a deep one. A shallow handler handles one visible frontier, resumes at most once per observation, stores no boundary borrow, and leaves policy in the caller; a deep handler that keeps control over successor observations is a hidden runner loop, which is rejected, so repetition is the caller's own explicit loop.
 - Discharge the shallow obligations. A shallow handler must satisfy the outcome, owner, and policy gates and the support-split obligation — defined in [workflow/boundary-gates.md](../workflow/boundary-gates.md) and [workflow/proof-obligations.md](../workflow/proof-obligations.md) — plus the copy-CQE rule.
 - Keep Go handlers, closures, and tables shallow and caller-owned. A Go handler is shallow when it consumes one visible frontier and resumes at most once; a handler closure may capture only copied completion facts or caller-owned state, never a borrowed CQE view; a handler table is keyed by caller-owned event keys, every handler in it is shallow, it is built before dispatch starts, and hot-path dispatch allocates nothing and builds no closures.
-- Keep parser, route, and completion-memory policy in the caller. Parser state and branch policy, route lookup and retirement, completion pool and GC-root policy, and completion-memory facts and policy are all caller-owned (completion-memory facts owned by `takt`), and none of them may hide inside the boundary.
+- Keep parser, route, and completion-memory policy in the caller. Parser state and branch policy, route lookup and retirement, completion pool and GC-root policy, and completion-memory facts and policy are all caller-owned (completion-memory facts owned by `code.hybscloud.com/takt`), and none of them may hide inside the boundary.
 
 The block below states these rules formally.
 
diff --git a/agents/boundary/resources.md b/agents/boundary/resources.md
index c22ca4a..c73582e 100644
--- a/agents/boundary/resources.md
+++ b/agents/boundary/resources.md
@@ -161,7 +161,7 @@ Buffers are resources with a lifecycle of their own — `allocate → own → pu
 
 In plain terms, the rules an agent follows here are:
 
-- A buffer has its own lifecycle, owned by `iobuf`. It moves `allocate → own → publish → select → consume → recycle → release`, and the buffer-shaping facts (pool index, aligned region, iovec view, array copy, typed slice view, reset-without-zero) belong to `iobuf`.
+- A buffer has its own lifecycle, owned by `code.hybscloud.com/iobuf`. It moves `allocate → own → publish → select → consume → recycle → release`, and the buffer-shaping facts (pool index, aligned region, iovec view, array copy, typed slice view, reset-without-zero) belong to `code.hybscloud.com/iobuf`.
 - While the kernel may own a buffer, you may not touch it. Reuse, return, mutate, unregister, and recycle are all disabled for a buffer the kernel may still be reading or writing.
 - Register, provide, select, and consume under explicit preconditions. Registration needs an owned, aligned, stable-address buffer and a valid slot; a provided buffer is published to a valid group and id; a selected buffer comes from a CQE carrying the buffer-select flag and a selected-buffer frontier; after consuming the first `n` bytes the buffer is recycled, copied-then-recycled, or released.
 - Release a zero-copy window exactly once, and only when it is safe. The release fires after both the data and notification frontiers are observed, or through an explicit terminal no-notification fallback, and never more than once; while pending it stays kernel-owned.
diff --git a/agents/formalization/INDEX.md b/agents/formalization/INDEX.md
index 0dcf9c3..1e21602 100644
--- a/agents/formalization/INDEX.md
+++ b/agents/formalization/INDEX.md
@@ -2,9 +2,9 @@
 
 Use these files when the task needs the formal notation behind the public `code.hybscloud.com/uring` agent guide. They cover caller code that directly invokes the package and broader systems built above that caller layer. They also describe abstraction from Go into the guide notation and compilation from checked notation back into Go. The files are ordered from notation basics to verification closure.
 
-The formalization guide family is checked as a composed guide: each topic file states an internal well property, and the topic judgments must remain provably composable under the closure conditions in [uring/agents/formalization/overview.md](overview.md), [uring/agents/formalization/guarantees.md](guarantees.md), and [uring/agents/formalization/verification.md](verification.md).
+The formalization guide family is checked as a composed guide: each topic file is checked by `GuideInternalWell_U(f)`, defined in [uring/agents/formalization/guarantees.md](guarantees.md), and the topic judgments must remain provably composable under the closure conditions in [uring/agents/formalization/overview.md](overview.md), [uring/agents/formalization/guarantees.md](guarantees.md), and [uring/agents/formalization/verification.md](verification.md).
 
-The formal vocabulary stays explicit in `uring` terms. Preserve every group when editing any topic file:
+The formal vocabulary stays explicit in `code.hybscloud.com/uring` boundary terms. Preserve every group when editing any topic file:
 
 ```text
 kernel           := {core, judgment, Ctrl, noHidden, canonicalLevel}
@@ -15,8 +15,8 @@ reify_runner     := {Reify, Reflect, trampoline, runner, Suspension, coalgebra}
 compilation      := {compile_to_go, outcome_compilation, handler_compilation, contextual_compilation}
 sessions_outcomes := {duality, projection, Outcome, Π, Backoff, ErrWouldBlock, ErrMore}
 metatheory       := {soundness, completeness, consistency, preservation, progress}
-abstraction      := {LIFT, SAVE, ANALYZE, FIX, REPORT, UPDATE, formalize, typecheck, reduce, prove, verify}
-middleware       := {middleware, shallow_handler, iox, kont, cove, takt}
+abstraction      := {LIFT, SAVE, ANALYZE, FIX, REPORT, UPDATE, analyze, lift, formalize, typecheck, reduce, prove, verify}
+middleware       := {middleware, shallow_handler, pkg("code.hybscloud.com/iox"), pkg("code.hybscloud.com/kont"), pkg("code.hybscloud.com/cove"), pkg("code.hybscloud.com/takt")}
 properties       := {Structural_Soundness, Conservativity, Composability, Parametricity, extension_admissibility}
 ```
 
diff --git a/agents/formalization/go-mapping.md b/agents/formalization/go-mapping.md
index 7d0eaa9..82709e7 100644
--- a/agents/formalization/go-mapping.md
+++ b/agents/formalization/go-mapping.md
@@ -1,6 +1,6 @@
 # Go Mapping
 
-The model in the other topic files only matters because it maps faithfully to real Go. This file is that bridge, in both directions. *Abstraction* lifts a Go surface up into a judgment so you can reason about it; *compilation* sends a judgment back down to Go and demands that the round trip preserve denotation and never smuggle caller frontier or policy into the boundary. When you change `uring` code, this is the file that says your change still *means* what the model says it means: same outcomes, same release evidence, ownership and epochs intact, nothing hidden in the boundary.
+The model in the other topic files only matters because it maps faithfully to real Go. This file is that bridge, in both directions. *Abstraction* lifts a Go surface up into a judgment so you can reason about it; *compilation* sends a judgment back down to Go and demands that the round trip preserve denotation and never smuggle caller frontier or policy into the boundary. When you change `code.hybscloud.com/uring` code, this is the file that says your change still *means* what the model says it means: same outcomes, same release evidence, ownership and epochs intact, nothing hidden in the boundary.
 
 ## Abstraction: Go To Guide
 
diff --git a/agents/formalization/guarantees.md b/agents/formalization/guarantees.md
index 05cb466..f77f490 100644
--- a/agents/formalization/guarantees.md
+++ b/agents/formalization/guarantees.md
@@ -208,7 +208,7 @@ Completeness_relative(surface) ⇔
 ```
 ## The Properties A Change Must Satisfy
 
-The theorems above are about the system; the properties below are about *your* judgment and *your* Go. Each is a predicate you can check directly: owner unique, resources affine, outcomes separated, policy kept out of the boundary, denotation defined, round trip closed. `Accept(J, go_surface)` bundles them into the bar a change must clear — it is the formal restatement of "this change uses `uring` correctly".
+The theorems above are about the system; the properties below are about *your* judgment and *your* Go. Each is a predicate you can check directly: owner unique, resources affine, outcomes separated, policy kept out of the boundary, denotation defined, round trip closed. `Accept(J, go_surface)` bundles them into the bar a change must clear — it is the formal restatement of "this change uses `code.hybscloud.com/uring` correctly".
 
 ```text
 module = pkg("code.hybscloud.com/uring")
diff --git a/agents/formalization/handler.md b/agents/formalization/handler.md
index 9c42fc0..565bec3 100644
--- a/agents/formalization/handler.md
+++ b/agents/formalization/handler.md
@@ -1,6 +1,6 @@
 # Handler
 
-`uring` is a *shallow* effect handler: it observes one boundary action and hands control straight back to the caller. It never owns the loop, never reinstalls itself to interpret the next completion, and never captures caller policy. This file is the operational heart of that claim. Read it to know exactly how a boundary action steps, what counts as a normal form, and how a suspension is resumed at most once per observation — because the moment a change makes the handler *deep* (a hidden runner loop, a retained continuation, policy baked into the step), every separation the guide promises collapses.
+`code.hybscloud.com/uring` is a *shallow* effect handler: it observes one boundary action and hands control straight back to the caller. It never owns the loop, never reinstalls itself to interpret the next completion, and never captures caller policy. This file is the operational heart of that claim. Read it to know exactly how a boundary action steps, what counts as a normal form, and how a suspension is resumed at most once per observation — because the moment a change makes the handler *deep* (a hidden runner loop, a retained continuation, policy baked into the step), every separation the guide promises collapses.
 
 The three sections move from the small-step calculus, to the reduction that says when stepping is done, to the suspend/resume boundary where a kernel observation is delivered to the caller's continuation.
 
@@ -180,7 +180,7 @@ ReductionSound(J,J_nf) ⇔
 
 ## Suspend, Resume, And The Observation Boundary
 
-This is where one kernel observation crosses into the caller's continuation. A suspension is resumed at most once per observation, the continuation is owned by the caller layer (not the boundary), and the runner loop is the caller's, not the package's. The two rejections at the end — no hidden runner loop, no boundary-owned caller frontier — are what keep `uring` shallow rather than silently deep.
+This is where one kernel observation crosses into the caller's continuation. A suspension is resumed at most once per observation, the continuation is owned by the caller layer (not the boundary), and the runner loop is the caller's, not the package's. The two rejections at the end — no hidden runner loop, no boundary-owned caller frontier — are what keep `code.hybscloud.com/uring` shallow rather than silently deep.
 
 ```text
 module = pkg("code.hybscloud.com/uring")
diff --git a/agents/formalization/kernel-boundary.md b/agents/formalization/kernel-boundary.md
index ccdb6e2..8275da9 100644
--- a/agents/formalization/kernel-boundary.md
+++ b/agents/formalization/kernel-boundary.md
@@ -1,10 +1,10 @@
 # Kernel Boundary
 
-This is the half of the world an agent does not control: what the kernel does, and which stratum owns which fact. To use `uring` correctly you must keep *kernel facts* (an SQE was submitted; a CQE arrived with these `Res` / `Flags` / `user_data`) strictly apart from *caller policy* (whether to retry, back off, or route). The two sections below give you (1) the boundary / below / caller stratum model and the per-package ownership of each carrier, and (2) the exact correspondence between an SQE action you encode and the CQE observation you later decode. If a change lets a kernel fact carry policy, or lets a borrowed CQE outlive its observation, it is wrong here before it is wrong anywhere else.
+This is the half of the world an agent does not control: what the kernel does, and which stratum owns which fact. To use `code.hybscloud.com/uring` correctly you must keep *kernel facts* (an SQE was submitted; a CQE arrived with these `Res` / `Flags` / `user_data`) strictly apart from *caller policy* (whether to retry, back off, or route). The two sections below give you (1) the boundary / below / caller stratum model and the per-package ownership of each carrier, and (2) the exact correspondence between an SQE action you encode and the CQE observation you later decode. If a change lets a kernel fact carry policy, or lets a borrowed CQE outlive its observation, it is wrong here before it is wrong anywhere else.
 
 ## Kernel Facts And Stratum Ownership
 
-The block fixes the kernel boundary `K = below(module)`, the disjoint strata, and `CarrierOwnerPackages` — the packages allowed to own carriers used by the guide. Read it as the authority on *who owns what*: nothing the kernel reports is caller policy, nothing the caller decides is a kernel fact, and `cove` context or requirement evidence guards caller decisions rather than becoming a boundary projection.
+The block fixes the kernel boundary `K = below(module)`, the disjoint strata, and `CarrierOwnerPackages` — the packages allowed to own carriers used by the guide. Read it as the authority on *who owns what*: nothing the kernel reports is caller policy, nothing the caller decides is a kernel fact, and `code.hybscloud.com/cove` context or requirement evidence guards caller decisions rather than becoming a boundary projection.
 
 ```text
 module = pkg("code.hybscloud.com/uring")
diff --git a/agents/formalization/notation.md b/agents/formalization/notation.md
index 7f82aaf..7b0af01 100644
--- a/agents/formalization/notation.md
+++ b/agents/formalization/notation.md
@@ -1,6 +1,6 @@
 # Notation
 
-This is the notation an agent reasons in when changing or reviewing `code.hybscloud.com/uring`. To use `uring` correctly you must read three things precisely: the *judgment* `J` that records what a boundary action does, the *syntactic categories* that name every carrier the kernel and the caller can touch, and the *typing discipline* that decides which carriers are linear (used once) and which evidence must be copied rather than borrowed. None of this is ceremony — every later guarantee (outcomes, ownership, sessions, the shallow handler) is stated against these symbols, so an edit that breaks the notation silently breaks the obligations that depend on it.
+This is the notation an agent reasons in when changing or reviewing `code.hybscloud.com/uring`. To use `code.hybscloud.com/uring` correctly you must read three things precisely: the *judgment* `J` that records what a boundary action does, the *syntactic categories* that name every carrier the kernel and the caller can touch, and the *typing discipline* that decides which carriers are linear (used once) and which evidence must be copied rather than borrowed. None of this is ceremony — every later guarantee (outcomes, ownership, sessions, the shallow handler) is stated against these symbols, so an edit that breaks the notation silently breaks the obligations that depend on it.
 
 Keep the judgment shape in view as you read; every other topic file projects onto one of its slots:
 
diff --git a/agents/formalization/resources.md b/agents/formalization/resources.md
index 1d5e884..cf8b2be 100644
--- a/agents/formalization/resources.md
+++ b/agents/formalization/resources.md
@@ -1,6 +1,6 @@
 # Resources
 
-Every ring context, submission entry, file descriptor, buffer, and zero-copy tracker the kernel touches is a *resource* with one owner and a definite lifetime. Using `uring` correctly means never consuming one twice, never releasing one early, and never letting a borrowed view escape the observation that produced it. This file is the inventory and the discipline.
+Every ring context, submission entry, file descriptor, buffer, and zero-copy tracker the kernel touches is a *resource* with one owner and a definite lifetime. Using `code.hybscloud.com/uring` correctly means never consuming one twice, never releasing one early, and never letting a borrowed view escape the observation that produced it. This file is the inventory and the discipline.
 
 It enumerates every resource kind the boundary can produce, the result resources handed back to the caller (FDs, buffers), and the evidence, frontier, and lifecycle kinds that track their state — together with `OwnerPkg`, which fixes exactly which package owns each kind (`dom(OwnerPkg) = DenotedKind`). The affine frontiers `Θ`/`Θ'` make linear consumption checkable, and the epoch order turns "no early release" into a property you can verify rather than hope for.
 
diff --git a/agents/formalization/sessions.md b/agents/formalization/sessions.md
index 22fb560..6597b61 100644
--- a/agents/formalization/sessions.md
+++ b/agents/formalization/sessions.md
@@ -1,8 +1,8 @@
 # Sessions
 
-A protocol is a caller-side state machine driven by boundary observations, and `uring` correctly refuses to own any of it. This file gives the frontier model: how a session frontier `Σ` steps when a completion arrives, and which steps exist at all. Every observation drives exactly one of six transitions — success (live or terminal), `errMore`, failure (live or terminal), `wouldBlock` (which returns control unchanged), suspension, or runner movement — and the whole stepping relation `ObsStepRel` lives outside the boundary (`ObsStepRel ∉ support(B)`). Parser state, branch policy, and the frontier itself are caller-owned; if a change lets any of them hide inside `B`, the protocol is no longer the caller's.
+A protocol is a caller-side state machine driven by boundary observations, and `code.hybscloud.com/uring` correctly refuses to own any of it. This file gives the frontier model: how a session frontier `Σ` steps when a completion arrives, and which steps exist at all. Every observation drives exactly one of six transitions — success (live or terminal), `errMore`, failure (live or terminal), `wouldBlock` (which returns control unchanged), suspension, or runner movement — and the whole stepping relation `ObsStepRel` lives outside the boundary (`ObsStepRel ∉ support(B)`). Parser state, branch policy, and the frontier itself are caller-owned; if a change lets any of them hide inside `B`, the protocol is no longer the caller's.
 
-Two asymmetries matter for using `uring` correctly: a failure on a live frontier is not terminal and must not carry a terminal frontier fact, and a multishot frontier is advanced by the caller's loop, never by the boundary re-entering itself.
+Two asymmetries matter for using `code.hybscloud.com/uring` correctly: a failure on a live frontier is not terminal and must not carry a terminal frontier fact, and a multishot frontier is advanced by the caller's loop, never by the boundary re-entering itself.
 
 In plain terms, the rules an agent follows here are:
 
diff --git a/agents/lift/INDEX.md b/agents/lift/INDEX.md
index 1b58d22..a13ae2d 100644
--- a/agents/lift/INDEX.md
+++ b/agents/lift/INDEX.md
@@ -8,7 +8,7 @@ When the user does not specify another location, save new or updated lift record
 
 - [uring/agents/lift/boundary-core.md](boundary-core.md): saved lift for the core boundary facts plus SQE encoding, CQE observation, outcome decode, release decode, and zero-copy notification handling.
 - [uring/agents/lift/resources-lifecycle.md](resources-lifecycle.md): saved lift for ownership epochs, pending kernel references, release, recycle, close, stop, and cancellation-adjacent lifecycle checks, together with fixed, provided, and selected buffers and zero-copy buffer carriers.
-- [uring/agents/lift/protocols-runtime.md](protocols-runtime.md): saved lift for multishot frontiers, subscription-style observations, protocol boundaries, stream-route liveness, and the caller-owned `code.hybscloud.com/kont`, `code.hybscloud.com/cove`, `code.hybscloud.com/takt`, and `code.hybscloud.com/sess` carriers around boundary observations.
+- [uring/agents/lift/protocols-runtime.md](protocols-runtime.md): saved lift for multishot frontiers, subscription-style observations, protocol boundaries, stream-route liveness, and the caller-owned carriers from `code.hybscloud.com/kont`, `code.hybscloud.com/cove`, `code.hybscloud.com/takt`, and `code.hybscloud.com/sess` around boundary observations.
 - [uring/agents/lift/policy-separation.md](policy-separation.md): saved lift for separating caller-owned retry, backoff, route, parser, scheduler, cancellation, timeout, and service policy from `code.hybscloud.com/uring` boundary mechanics.
 
 ## Save Rule
diff --git a/agents/lift/protocols-runtime.md b/agents/lift/protocols-runtime.md
index 3ab51c9..8e28982 100644
--- a/agents/lift/protocols-runtime.md
+++ b/agents/lift/protocols-runtime.md
@@ -268,7 +268,7 @@ PO_multishot_protocols =
 ```
 ## Runtime Carriers Lift
 
-This second lift records the runtime carriers — the checked shape that caller-side Go must preserve when it drives operations through `kont`, `cove`, `takt`, and `sess`.
+This second lift records the runtime carriers — the checked shape that caller-side Go must preserve when it drives operations through `code.hybscloud.com/kont`, `code.hybscloud.com/cove`, `code.hybscloud.com/takt`, and `code.hybscloud.com/sess`.
 
 ```text
 topic = runtime_carriers
@@ -301,14 +301,16 @@ J_runtime_carriers =
 complete(lift,J_runtime_carriers)
   → saved(SaveLift(lift,task,J_runtime_carriers))
 
-RuntimeOwner =
+RuntimeOwnerPkg =
   { pkg("code.hybscloud.com/kont")
   , pkg("code.hybscloud.com/cove")
   , pkg("code.hybscloud.com/takt")
   , pkg("code.hybscloud.com/sess")
   }
-support(RuntimeOwner) ⊆ C
-RuntimeOwner ∩ support(B) = ∅
+RuntimeOwnerFact_rc =
+  {runtime_owner_pkg(p) | p ∈ RuntimeOwnerPkg}
+support(RuntimeOwnerFact_rc) ⊆ C
+RuntimeOwnerFact_rc ∩ support(B) = ∅
 
 RuntimeTheoryRoute_rc =
   { pkg("code.hybscloud.com/kont")
@@ -320,14 +322,14 @@ RuntimeTheoryRoute_rc =
   , pkg("code.hybscloud.com/sess")
       ↦ {session_frontier}
 }
-∀ p ∈ RuntimeOwner. RuntimeTheoryRoute_rc[p] ⊆ TheoryConcept
+∀ p ∈ RuntimeOwnerPkg. RuntimeTheoryRoute_rc[p] ⊆ TheoryConcept
 RuntimeTheoryUse_rc =
   {runtime_concept_use(p,c) |
-     p ∈ RuntimeOwner ∧ c ∈ RuntimeTheoryRoute_rc[p]}
+     p ∈ RuntimeOwnerPkg ∧ c ∈ RuntimeTheoryRoute_rc[p]}
 RuntimeTheoryUse_rc ⊆ RuntimeConceptUse
 support(RuntimeTheoryUse_rc) ⊆ C
 project(RuntimeTheoryUse_rc,B) = ∅
-∀ c ∈ ⋃ {RuntimeTheoryRoute_rc[p] | p ∈ RuntimeOwner}.
+∀ c ∈ ⋃ {RuntimeTheoryRoute_rc[p] | p ∈ RuntimeOwnerPkg}.
   concept_utilized_U(J_runtime_carriers,c)
 
 KontCarrier =
@@ -448,6 +450,18 @@ BoundarySuspension(s,op) ⇔
   s ∈ OneShotSuspension ∧ op ∈ boundary_action(B) ∧ pending_op(s)=op
 ∀ s ∈ OneShotSuspension.
   ∀ op. BoundarySuspension(s,op) → identity(s)=user_data(op)
+live_token_rc(token) ⇔ token ∈ dom(PendingTable_rc)
+submit_token_rc(token,op) ⇔
+  one_shot(op)
+  ∧ carrier(op) = Loop(pkg("code.hybscloud.com/takt"))
+  ∧ token_indexes(token,user_data(op))
+submit_token_rc(token,op) ∧ live_token_rc(token)
+  → fail(ErrLiveTokenReuse_rc)
+    ∧ fatal(Loop(pkg("code.hybscloud.com/takt")),
+             ErrLiveTokenReuse_rc)
+    ∧ drain(PendingTable_rc)
+retire_token_rc(token) ⇔
+  token ∈ dom_pre(PendingTable_rc) ∧ token ∉ dom_post(PendingTable_rc)
 ∀ op.
   multishot(op) → reject(carrier(op) = OneShotSuspension)
 ∀ op.
@@ -500,6 +514,18 @@ poll_err(Loop(pkg("code.hybscloud.com/takt")))
   = ErrWouldBlock_rc
   → idle(Loop(pkg("code.hybscloud.com/takt")))
     ∧ no_mutation(PendingTable_rc)
+fatal(Loop(pkg("code.hybscloud.com/takt")),e) ∧ submit_token_rc(token,op)
+  → fail(e)
+fatal(Loop(pkg("code.hybscloud.com/takt")),e)
+  → poll(Loop(pkg("code.hybscloud.com/takt"))) = fail(e)
+drain(Loop(pkg("code.hybscloud.com/takt"))) ∧
+  fatal_pre(Loop(pkg("code.hybscloud.com/takt")))=nil
+  → fatal_post(Loop(pkg("code.hybscloud.com/takt"))) =
+      ErrDisposed_rc
+drain(Loop(pkg("code.hybscloud.com/takt"))) ∧
+  fatal_pre(Loop(pkg("code.hybscloud.com/takt")))≠nil
+  → fatal_post(Loop(pkg("code.hybscloud.com/takt"))) =
+      fatal_pre(Loop(pkg("code.hybscloud.com/takt")))
 stream_completion(SubscriptionLoop(pkg("code.hybscloud.com/takt")), c) ∧ More_rc(c)
   → emit(stream_event(c))
     ∧ live_route_rc(route_rc(c))
@@ -522,10 +548,14 @@ cancel_route_rc(route) ∧
   (route=zero_route_rc ∨ route ∉ dom_pre(RouteTable_rc))
   → fail(ErrUnknownSubscription_rc)
     ∧ no_mutation(RouteTable_rc)
-fatal(SubscriptionLoop(pkg("code.hybscloud.com/takt")),e) →
-  subscribe_route_rc(_,_) = fail(e)
-  ∧ poll(SubscriptionLoop(pkg("code.hybscloud.com/takt"))) = fail(e)
-  ∧ cancel_route_rc(_) = fail(e)
+fatal(SubscriptionLoop(pkg("code.hybscloud.com/takt")),e) ∧
+  subscribe_route_rc(route,op)
+  → fail(e)
+fatal(SubscriptionLoop(pkg("code.hybscloud.com/takt")),e) ∧
+  cancel_route_rc(route)
+  → fail(e)
+fatal(SubscriptionLoop(pkg("code.hybscloud.com/takt")),e)
+  → poll(SubscriptionLoop(pkg("code.hybscloud.com/takt"))) = fail(e)
 drain(SubscriptionLoop(pkg("code.hybscloud.com/takt"))) ∧
   fatal_pre(SubscriptionLoop(pkg("code.hybscloud.com/takt")))=nil
   → fatal_post(SubscriptionLoop(pkg("code.hybscloud.com/takt"))) =
@@ -577,6 +607,12 @@ Preservation_rc =
        → (More_rc(c) ⇔ boundary_more_rc(cqe)))
   ∧ (payload_failure_rc(c) ∧ More_rc(c)
        → live_route_rc(route_rc(c)) ∧ ¬retire_route_rc(route_rc(c)))
+  ∧ (submit_token_rc(token,op) ∧ live_token_rc(token)
+       → fail(ErrLiveTokenReuse_rc))
+  ∧ (drain(Loop(pkg("code.hybscloud.com/takt"))) ∧
+       fatal_pre(Loop(pkg("code.hybscloud.com/takt")))=nil
+       → fatal_post(Loop(pkg("code.hybscloud.com/takt"))) =
+          ErrDisposed_rc)
   ∧ (subscribe_route_rc(zero_route_rc,op)
        → fail(ErrInvalidRouteID_rc))
   ∧ (cancel_route_rc(route) ∧ route ∉ dom_pre(RouteTable_rc)
diff --git a/agents/runtime/cove.md b/agents/runtime/cove.md
index da87964..759e317 100644
--- a/agents/runtime/cove.md
+++ b/agents/runtime/cove.md
@@ -1,13 +1,13 @@
 # Context Evidence Utilization
 
-Because handling a completion is shallow, the world can advance between the moment you submit an operation and the moment you resume on its CQE — so the requirement evidence you relied on must still hold at the point of use. `code.hybscloud.com/cove` is how you carry and re-check that evidence across a suspension boundary. This file is the rule for using `cove` with `code.hybscloud.com/uring`: requirement and safety evidence is caller-owned, epoch-monotone where it may be cached and re-checked at the use epoch where it may not, and never projected into the boundary.
+Because handling a completion is shallow, the world can advance between the moment you submit an operation and the moment you resume on its CQE — so the requirement evidence you relied on must still hold at the point of use. `code.hybscloud.com/cove` is how you carry and re-check that evidence across a suspension boundary. This file is the rule for using `code.hybscloud.com/cove` with `code.hybscloud.com/uring`: requirement and safety evidence is caller-owned, epoch-monotone where it may be cached and re-checked at the use epoch where it may not, and never projected into the boundary.
 
 In plain terms, the rules an agent follows here are:
 
 - Carry context across the shallow gap, and re-check at use. Between observe and resume the world may advance, so cache only monotone facts (capability present, registration done, terminal observed) and re-check non-monotone facts (frontier live, buffer owned, fd open, ring not closed, token live) at the resume or dispatch epoch.
 - Resume does not validate for you. Resuming a suspension view performs no requirement check; guard it explicitly with a requirement (`Need`/`NeedExpr`), and if a requirement fails, the wait, reroute, or abandon decision is the caller's.
 - Copy completion facts into the context, never a borrowed pointer. A context extension carries copied `Res`/`Flags`/`user_data`, metadata, capability, and ownership facts; a borrowed CQE pointer is never in the world or the context.
-- Keep all `cove` carriers in the caller layer. Context, requirement, rule, suspension-view, and Kripke carriers are caller-owned, never projected into the boundary, and never used to mutate the boundary frontiers `Θ`/`Σ`/`Μ`.
+- Keep all carriers from `code.hybscloud.com/cove` in the caller layer. Context, requirement, rule, suspension-view, and Kripke carriers are caller-owned, never projected into the boundary, and never used to mutate the boundary frontiers `Θ`/`Σ`/`Μ`.
 
 The block below states these rules formally.
 
diff --git a/agents/runtime/kont.md b/agents/runtime/kont.md
index eace1fc..ca69558 100644
--- a/agents/runtime/kont.md
+++ b/agents/runtime/kont.md
@@ -1,15 +1,15 @@
 # Suspension Utilization
 
-When you suspend on a pending ring operation, `code.hybscloud.com/kont` is how you do it correctly: one suspension, one resume, matched to one operation identity. This file is the rule for wiring `kont` onto a `code.hybscloud.com/uring` boundary action. A one-shot operation maps to an affine `Suspension` resumed at most once with *copied* completion facts (never a borrowed CQE view); a multishot operation is rejected here and routed through `code.hybscloud.com/takt` instead; and `kont` itself stays entirely in the caller layer, its carriers never projected into the boundary. This is the package-level instance of the shallow handler: resume on one observation, hand control back.
+When you suspend on a pending ring operation, `code.hybscloud.com/kont` is how you do it correctly: one suspension, one resume, matched to one operation identity. This file is the rule for wiring `code.hybscloud.com/kont` onto a `code.hybscloud.com/uring` boundary action. A one-shot operation maps to an affine `Suspension` resumed at most once with *copied* completion facts (never a borrowed CQE view); a multishot operation is rejected here and routed through `code.hybscloud.com/takt` instead; and `code.hybscloud.com/kont` itself stays entirely in the caller layer, its carriers never projected into the boundary. This is the package-level instance of the shallow handler: resume on one observation, hand control back.
 
 In plain terms, the rules an agent follows here are:
 
 - One suspension, one resume, one identity. A one-shot operation maps to an affine `Suspension` resumed at most once; resume consumes both the suspension and the operation identity, and a second resume is rejected.
 - Resume on copied facts, never a borrowed view. The resume value copies `Res`, `Flags`, `user_data`, and selected-buffer metadata; a borrowed CQE view is never stored, and a continuation closure captures only copied facts or caller-owned state.
-- Multishot does not belong here. A multishot operation is rejected from a `Suspension` and routed through `takt`'s `SubscriptionLoop` instead.
+- Multishot does not belong here. A multishot operation is rejected from a `Suspension` and routed through `SubscriptionLoop` from `code.hybscloud.com/takt` instead.
 - Discarding is not cancelling. Discarding a suspension consumes it but does not cancel the pending operation; cancellation is a separate visible boundary action, and the discard decision is the caller's.
 - Step index is proof fuel only. It bounds reasoning, and never changes runtime affinity or creates progress evidence.
-- Keep all `kont` carriers in the caller layer. Effect, computation, suspension, and step carriers are caller-owned and never projected into the boundary.
+- Keep all carriers from `code.hybscloud.com/kont` in the caller layer. Effect, computation, suspension, and step carriers are caller-owned and never projected into the boundary.
 
 The block below states these rules formally.
 
diff --git a/agents/runtime/sess.md b/agents/runtime/sess.md
index 3592b0d..25d53cf 100644
--- a/agents/runtime/sess.md
+++ b/agents/runtime/sess.md
@@ -1,13 +1,13 @@
 # Session Protocol Utilization
 
-A session is a caller-side protocol state machine expressed over completions, and `code.hybscloud.com/sess` is how you build one on top of `code.hybscloud.com/uring` without letting the protocol leak into the boundary. This file is the rule for using `sess`: each protocol step advances on one boundary observation, `wouldBlock` returns control with the endpoint and frontier preserved, duality and post-`Close` terminality are caller checks, and the session frontier and parser state stay caller-owned. The `errMore`-to-`fail` asymmetry from the outcome plane carries through unchanged.
+A session is a caller-side protocol state machine expressed over completions, and `code.hybscloud.com/sess` is how you build one on top of `code.hybscloud.com/uring` without letting the protocol leak into the boundary. This file is the rule for using `code.hybscloud.com/sess`: each protocol step advances on one boundary observation, `wouldBlock` returns control with the endpoint and frontier preserved, duality and post-`Close` terminality are caller checks, and the session frontier and parser state stay caller-owned. The failure-with-`MORE` asymmetry from the outcome plane carries through unchanged.
 
 In plain terms, the rules an agent follows here are:
 
 - One protocol step, one boundary observation. Each `Advance` of an endpoint binds one boundary action; an endpoint has a single owner and a single-producer, single-consumer transport, and concurrent use is rejected.
-- `wouldBlock` returns control unchanged. Transport backpressure surfaces as `ErrWouldBlock` (the backpressure outcome owned by `iox`), makes no protocol progress, and preserves the endpoint and frontier; the wait, backoff, or drive-peer decision is the caller's.
-- `errMore` is outside the session transport domain. `ErrMore` is not a session transport outcome; it preserves the endpoint and is the caller's to classify as a stream frontier (routed through `takt`'s `SubscriptionLoop`) or to fail dispatch — a multishot frontier is never a session carrier.
-- Failure preserves the endpoint, and the asymmetry carries through. Any failure evidence leaves the endpoint preserved, a thrown error in a paired run aborts the session globally, and the `errMore`-to-`fail` asymmetry from the outcome plane holds unchanged.
+- `wouldBlock` returns control unchanged. Transport backpressure surfaces as `ErrWouldBlock` (the backpressure outcome owned by `code.hybscloud.com/iox`), makes no protocol progress, and preserves the endpoint and frontier; the wait, backoff, or drive-peer decision is the caller's.
+- `errMore` is outside the session transport domain. `ErrMore` is not a session transport outcome; it preserves the endpoint and is the caller's to classify as a stream frontier (routed through `SubscriptionLoop` from `code.hybscloud.com/takt`) or to fail dispatch — a multishot frontier is never a session carrier.
+- Failure preserves the endpoint, and the asymmetry carries through. Any failure evidence leaves the endpoint preserved, a thrown error in a paired run aborts the session globally, and the failure-with-`MORE` asymmetry from the outcome plane holds unchanged.
 - Close is a protocol transition, not a kernel close. `Close` advances the protocol frontier; it does not close the fd or stop the ring, and finishing a session service makes cancel/drain, release/recycle, and descriptor close visible.
 - Duality, terminality, and parser state are caller checks. They are caller-owned, never boundary validation, and absent from the hot path; the session frontier and protocol carriers stay caller-owned and out of the boundary.
 
diff --git a/agents/runtime/takt.md b/agents/runtime/takt.md
index 79eb4dd..591de13 100644
--- a/agents/runtime/takt.md
+++ b/agents/runtime/takt.md
@@ -1,10 +1,10 @@
 # Runner Utilization
 
-The loop that drives operations against the ring is the caller's, not the package's, and `code.hybscloud.com/takt` is how you build that loop correctly. This file is the rule for using `takt` with `code.hybscloud.com/uring`: a token *is* the `user_data` operation identity, a one-shot completion routes through `Loop` while a multishot stream routes through `SubscriptionLoop` keyed by a `RouteID` of token and generation, drain corresponds to the stop and drain epoch, and runner movement, completion routing, and completion memory all stay caller-owned and out of the boundary. A reused live token or route is rejected.
+The loop that drives operations against the ring is the caller's, not the package's, and `code.hybscloud.com/takt` is how you build that loop correctly. This file is the rule for using `code.hybscloud.com/takt` with `code.hybscloud.com/uring`: a token *is* the `user_data` operation identity, a one-shot completion routes through `Loop` while a multishot stream routes through `SubscriptionLoop` keyed by a `RouteID` of token and generation, drain corresponds to the stop and drain epoch, and runner movement, completion routing, and completion memory all stay caller-owned and out of the boundary. A reused live token or route is rejected.
 
 In plain terms, the rules an agent follows here are:
 
-- A token is the operation identity. A `takt` token *is* the `user_data` of a boundary operation; reusing a still-live token is rejected (`ErrLiveTokenReuse`), and a completion value must be copied facts, never a borrowed CQE view.
+- A token is the operation identity. A token from `code.hybscloud.com/takt` *is* the `user_data` of a boundary operation; reusing a still-live token is rejected (`ErrLiveTokenReuse`), and a completion value must be copied facts, never a borrowed CQE view.
 - Route one-shot and multishot differently. A one-shot operation runs through `Loop`; a multishot operation runs through `SubscriptionLoop` keyed by a `RouteID = (Token, Generation)`. A multishot completion arriving in a one-shot `Loop` fails as `ErrUnsupportedMultishot`, and reusing a live route is rejected (`ErrLiveRouteReuse`).
 - Distinguish dispatcher-level from completion-level `ErrMore`. `Advance`/`AdvanceSuspension` resume on dispatcher `ErrMore` and return a live frontier; the generic `Loop` rejects completion-level `ErrMore` as unsupported multishot; a stream completion's `More` flag means the route stays live, and its absence means the route may retire.
 - Back off and wait in the caller. On `ErrWouldBlock` or no completion, the park, spin-wait, or backoff decision and its state are caller-owned; the loop never hides them.
@@ -92,7 +92,8 @@ meaning(more_flag_takt(c) = true, SubscriptionLoop(pkg("code.hybscloud.com/takt"
 meaning(more_flag_takt(c) = false, SubscriptionLoop(pkg("code.hybscloud.com/takt"))) =
   route_may_retire_after_event(route(c))
 PendingTable = finite_map(Token, Suspension[A])
-CompletionMemory = loop_slab_storage([]Completion)
+CompletionMemoryStore_takt = loop_slab_storage([]Completion)
+storage_realizer(CompletionMemory, CompletionMemoryStore_takt)
 RouteTable = finite_map(RouteID, RouteState)
 RouteState = {active, canceling}
 current_suspension_takt(token) =
@@ -115,6 +116,9 @@ backend_submit(token,op) =
 live(token) ⇔ ∃cqe op. may_arrive(cqe,op) ∧ boundary_token_correlates(token,op)
 submit(token',op') ∧ live(token')
   → fail(ErrLiveTokenReuse_takt)
+    ∧ fatal(Loop(pkg("code.hybscloud.com/takt")),
+             ErrLiveTokenReuse_takt)
+    ∧ drain(PendingTable)
 completion(token,v) ∧ ∃op. boundary_token_correlates(token,op)
   → BoundaryCompletionValue(v)
 terminal(Completion(token)) → retire(token)
@@ -126,6 +130,18 @@ poll(Loop(pkg("code.hybscloud.com/takt"))) = idle →
 poll_err = ErrWouldBlock_takt
   → poll(Loop(pkg("code.hybscloud.com/takt"))) = idle
     ∧ no_mutation(PendingTable)
+fatal(Loop(pkg("code.hybscloud.com/takt")),e) ∧ submit(token,op)
+  → fail(e)
+fatal(Loop(pkg("code.hybscloud.com/takt")),e)
+  → poll(Loop(pkg("code.hybscloud.com/takt"))) = fail(e)
+drain(Loop(pkg("code.hybscloud.com/takt"))) ∧
+  fatal_pre(Loop(pkg("code.hybscloud.com/takt")))=nil
+  → fatal_post(Loop(pkg("code.hybscloud.com/takt"))) =
+      ErrDisposed_takt
+drain(Loop(pkg("code.hybscloud.com/takt"))) ∧
+  fatal_pre(Loop(pkg("code.hybscloud.com/takt")))≠nil
+  → fatal_post(Loop(pkg("code.hybscloud.com/takt"))) =
+      fatal_pre(Loop(pkg("code.hybscloud.com/takt")))
 
 ⟦Reify(Eff[A])⟧ = Expr[A]
 ⟦Reflect(Expr[A])⟧ = Eff[A]
@@ -229,10 +245,14 @@ cancel_success(route) ⇔ cancel(route) ∧ route ∈ dom_pre(RouteTable)
 cancel_success(route) →
   route ∈ dom_pre(RouteTable)
   ∧ route_remains_live_until_terminal_or_drain(route)
-fatal(SubscriptionLoop(pkg("code.hybscloud.com/takt")),e) →
-  subscribe(_,_) = fail(e)
-  ∧ poll(SubscriptionLoop(pkg("code.hybscloud.com/takt"))) = fail(e)
-  ∧ cancel(_) = fail(e)
+fatal(SubscriptionLoop(pkg("code.hybscloud.com/takt")),e) ∧
+  subscribe(route,op)
+  → fail(e)
+fatal(SubscriptionLoop(pkg("code.hybscloud.com/takt")),e) ∧
+  cancel(route)
+  → fail(e)
+fatal(SubscriptionLoop(pkg("code.hybscloud.com/takt")),e)
+  → poll(SubscriptionLoop(pkg("code.hybscloud.com/takt"))) = fail(e)
 drain(SubscriptionLoop(pkg("code.hybscloud.com/takt"))) →
   ∀ route ∈ dom_pre(RouteTable).
     retire(route)
@@ -304,6 +324,7 @@ reject(hidden_runner_loop(B))
 successor_observation_possible(ctx) → decision_owner(next_observation) = C
 
 support(RunnerCarrier ∪ EffectCarrier ∪ {PendingTable, RouteTable,
+                         CompletionMemoryStore_takt,
                          backoff_policy(Backoff_takt), spin_wait_policy(SpinWait_takt),
                          poll_cadence}) ⊆ C
 support(kernel_boundary_facts) ⊆ B
diff --git a/agents/workflow/boundary-gates.md b/agents/workflow/boundary-gates.md
index f768127..df790b2 100644
--- a/agents/workflow/boundary-gates.md
+++ b/agents/workflow/boundary-gates.md
@@ -4,7 +4,7 @@ Before a change counts as correct, it must pass the gates in this file — the m
 
 Each gate checks one thing, and a gate that fails means the change is wrong:
 
-- `G_read` — read-completeness: you have read the complete `iox` package and the owner package of every package-owned fact the change uses.
+- `G_read` — read-completeness: you have read the complete `code.hybscloud.com/iox` package and the owner package of every package-owned fact the change uses.
 - `G_place` — correct placement: the caller frontier and caller policy both sit in the caller layer, owned by the caller, and neither overlaps the boundary.
 - `G_owner` — single owner: the resource frontiers are affine, every boundary fact has a single-stratum owner, and every resource has a named owner epoch.
 - `G_outcome` — outcome separation: the outcome and release planes are kept apart, the control symbol is one of `ok`/`wouldBlock`/`errMore`/`fail(e)`, and the CQE evidence (`Res`, `Flags`, `user_data`, frontier) is preserved.
diff --git a/agents/workflow/task-checklists.md b/agents/workflow/task-checklists.md
index 501a1c8..d15af94 100644
--- a/agents/workflow/task-checklists.md
+++ b/agents/workflow/task-checklists.md
@@ -20,12 +20,12 @@ Classify the task by shape and add the topic files and lift records for every sh
 - Buffer change: read [uring/agents/boundary/resources.md](../boundary/resources.md) and [uring/agents/formalization/resources.md](../formalization/resources.md); check the lift in [uring/agents/lift/resources-lifecycle.md](../lift/resources-lifecycle.md).
 - Integration point: read [uring/agents/boundary/integration.md](../boundary/integration.md) and [uring/agents/formalization/go-mapping.md](../formalization/go-mapping.md); check the lifts in [uring/agents/lift/boundary-core.md](../lift/boundary-core.md) and [uring/agents/lift/policy-separation.md](../lift/policy-separation.md).
 - Protocol: read [uring/agents/boundary/protocols.md](../boundary/protocols.md) and [uring/agents/formalization/sessions.md](../formalization/sessions.md); check the lift in [uring/agents/lift/protocols-runtime.md](../lift/protocols-runtime.md).
-- Runtime-package integration (`kont`, `cove`, `takt`, `sess`): read [uring/agents/runtime/kont.md](../runtime/kont.md), [uring/agents/runtime/cove.md](../runtime/cove.md), [uring/agents/runtime/takt.md](../runtime/takt.md), [uring/agents/runtime/sess.md](../runtime/sess.md), [uring/agents/formalization/handler.md](../formalization/handler.md), and [uring/agents/formalization/sessions.md](../formalization/sessions.md); check the lifts in [uring/agents/lift/protocols-runtime.md](../lift/protocols-runtime.md) and [uring/agents/lift/policy-separation.md](../lift/policy-separation.md).
+- Runtime-package integration (`code.hybscloud.com/kont`, `code.hybscloud.com/cove`, `code.hybscloud.com/takt`, `code.hybscloud.com/sess`): read [uring/agents/runtime/kont.md](../runtime/kont.md), [uring/agents/runtime/cove.md](../runtime/cove.md), [uring/agents/runtime/takt.md](../runtime/takt.md), [uring/agents/runtime/sess.md](../runtime/sess.md), [uring/agents/formalization/handler.md](../formalization/handler.md), and [uring/agents/formalization/sessions.md](../formalization/sessions.md); check the lifts in [uring/agents/lift/protocols-runtime.md](../lift/protocols-runtime.md) and [uring/agents/lift/policy-separation.md](../lift/policy-separation.md).
 - Reference claim: read [uring/agents/references.md](../references.md); there is no lift record to check.
 
 When the task touches the model — every shape above except a pure reference claim — also read all of the formalization files, starting from [uring/agents/formalization/INDEX.md](../formalization/INDEX.md).
 
-For a broad guide edit or broad caller-side work, read every indexed topic file and check every lift record.
+For a broad guide edit or broad caller-side work, read every indexed topic file, check every lift record, and read the complete current source for every package whose facts the edited guide relies on. When the edit touches the runtime, integration, protocol, ownership, or outcome model, the minimum package-source set is `code.hybscloud.com/iox`, `code.hybscloud.com/iofd`, `code.hybscloud.com/sock`, `code.hybscloud.com/kont`, `code.hybscloud.com/cove`, `code.hybscloud.com/takt`, and `code.hybscloud.com/sess`; add `code.hybscloud.com/zcall`, `code.hybscloud.com/iobuf`, `code.hybscloud.com/spin`, `code.hybscloud.com/lfq`, or `code.hybscloud.com/framer` whenever the edited guide uses syscall, buffer, spin/yield, mailbox, or framing facts.
 
 ## Before you start