diff --git a/AGENTS.md b/AGENTS.md
index 6a3fa1e..b39dd1e 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -104,7 +104,7 @@ Use the caller-layer packages according to the role they own:
 - Use `code.hybscloud.com/takt` when caller code needs runner movement, completion memory, polling, error-aware stepping, or route-indexed stream carriers. `Advance` and `AdvanceSuspension` resume on dispatcher-level `ErrMore`; generic `Loop` rejects completion-level `ErrMore` as unsupported multishot; `SubscriptionLoop` is the carrier for live stream routes.
 - Use `code.hybscloud.com/sess` when protocol branching, endpoint frontiers, paired protocol execution, or error-aware endpoint stepping sits above the completion stream. Its transport backpressure is `ErrWouldBlock` from `code.hybscloud.com/iox`; `ErrMore` is outside the endpoint transport domain, so live multishot routing must be classified before it reaches a session endpoint.
 
-These packages are general caller-layer tools. The obligations in this guide apply when caller code uses them to wrap or drive a `code.hybscloud.com/uring` boundary action. Error-aware forms from `code.hybscloud.com/takt` and `code.hybscloud.com/sess` carry caller protocol policy; they do not change what a `code.hybscloud.com/uring` boundary helper may own. The detailed utilization guides for these packages live under [`agents/runtime/`](agents/runtime/), starting from [`agents/runtime/INDEX.md`](agents/runtime/INDEX.md).
+These packages are general caller-layer tools. The obligations in this guide apply when caller code uses them to wrap or drive a `code.hybscloud.com/uring` boundary action. Error-aware forms from `code.hybscloud.com/takt` and `code.hybscloud.com/sess` carry caller protocol policy; they do not change what a `code.hybscloud.com/uring` boundary helper may own. The detailed utilization guides for these packages live under [`agents/runtime/`](agents/runtime/), starting from [`agents/runtime/INDEX.md`](agents/runtime/INDEX.md); those files also name the package source files and coding obligations used for review.
 
 Protocol stacks built above or beyond `code.hybscloud.com/uring` can treat the package as a shallow boundary handler: it exposes kernel observations and returns control to the caller. Protocol parsing, retries, route state, and terminal policy stay in the caller's protocol or runtime layer. The handler discipline is defined in [`agents/boundary/protocols.md`](agents/boundary/protocols.md) and restated in each file under [`agents/runtime/`](agents/runtime/) for the package it covers.
 
diff --git a/agents/formalization/INDEX.md b/agents/formalization/INDEX.md
index 1e21602..9a6c286 100644
--- a/agents/formalization/INDEX.md
+++ b/agents/formalization/INDEX.md
@@ -4,21 +4,19 @@ Use these files when the task needs the formal notation behind the public `code.
 
 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 `code.hybscloud.com/uring` boundary terms. Preserve every group when editing any topic file:
-
-```text
-kernel           := {core, judgment, Ctrl, noHidden, canonicalLevel}
-syntax           := {NameAtoms, facts, Γ, Δ, Θ, χ, Σ, Μ, Φ, Obs, Rel, Π}
-typing           := {typing, resource, session, effect, coeffect}
-reduction        := {reduction, wouldBlock, errMore, shallow_handler, coeffect}
-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, 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}
-```
+The formal vocabulary stays explicit in `code.hybscloud.com/uring` boundary terms, but this index remains a navigation file. When editing a topic file, preserve the vocabulary group it owns:
+
+- Kernel and judgment vocabulary: core boundary facts, `Ctrl`, `noHidden`, and `canonicalLevel`.
+- Syntax vocabulary: `NameAtoms`, facts, `Γ`, `Δ`, `Θ`, `χ`, `Σ`, `Μ`, `Φ`, `Obs`, `Rel`, and `Π`.
+- Typing vocabulary: typing, resource, session, effect, and coeffect judgments.
+- Reduction vocabulary: `wouldBlock`, `errMore`, shallow-handler reduction, and coeffect reduction.
+- Runner and bridge vocabulary: `Reify`, `Reflect`, trampoline, runner, `Suspension`, and coalgebra.
+- Compilation vocabulary: `compile_to_go`, outcome compilation, handler compilation, and contextual compilation.
+- Session and outcome vocabulary: duality, projection, `Outcome`, `Π`, `Backoff`, `ErrWouldBlock`, and `ErrMore`.
+- Metatheory vocabulary: soundness, scope-relative completeness, consistency, preservation, and progress.
+- Workflow vocabulary: `analyze`, `lift`, `formalize`, `typecheck`, `reduce`, `prove`, `compile_to_go`, and `verify`, together with saved-stage records.
+- Middleware vocabulary: shallow-handler composition across `code.hybscloud.com/iox`, `code.hybscloud.com/kont`, `code.hybscloud.com/cove`, and `code.hybscloud.com/takt`.
+- Property vocabulary: `Structural_Soundness`, `Conservativity`, `Composability`, `Parametricity`, and `extension_admissibility`.
 
 Read the formalization files in this order:
 
diff --git a/agents/formalization/go-mapping.md b/agents/formalization/go-mapping.md
index 82709e7..4364560 100644
--- a/agents/formalization/go-mapping.md
+++ b/agents/formalization/go-mapping.md
@@ -8,6 +8,7 @@ The block lifts a `GoSurface` into a `JudgmentSurface` (`lift = ⟦·⟧⁻¹_U`
 
 ```text
 module = pkg("code.hybscloud.com/uring")
+B = boundary(module)
 A = above(module)
 D = beyond(module)
 C = caller(module) = A ∪ D
@@ -177,24 +178,32 @@ compile_denotation_preserved(J,w) ⇔
 CompileSubmit(J) ⇔
   defined(⟦J⟧_U)
   ∧ action(J)=submit
-  ∧ ⟦J⟧_U = helper(submit)
-  ∧ emits(Encode(req,ctx))
-  ∧ no_loop(helper)
-  ∧ no_retry(helper)
+  ∧ ∃ req,ctx,h.
+      h = ⟦J⟧_U
+      ∧ h = helper(submit)
+      ∧ emits(h,Encode(req,ctx))
+      ∧ no_loop(h)
+      ∧ no_retry(h)
 
 CompileObserve(J) ⇔
   defined(⟦J⟧_U)
   ∧ action(J)∈{wait,observe,decode}
-  ∧ ⟦J⟧_U = helper(action(J))
-  ∧ reads(cqe)
-  ∧ (operation_cqe(cqe) → projects(CQEToObs(cqe,ctx,r,χ(J))))
-  ∧ (release_ready_carrier(cqe,ctx,r) → projects(ReleaseProjection(cqe,ctx,r,χ(J))))
-  ∧ preserves(cqe.Res,cqe.Flags,cqe.user_data)
+  ∧ ∃ cqe,ctx,r,h.
+      h = ⟦J⟧_U
+      ∧ h = helper(action(J))
+      ∧ reads(h,cqe)
+      ∧ (operation_cqe(cqe) → projects(h,CQEToObs(cqe,ctx,r,χ(J))))
+      ∧ (release_ready_carrier(cqe,ctx,r) →
+          projects(h,ReleaseProjection(cqe,ctx,r,χ(J))))
+      ∧ preserves(h,{cqe.Res,cqe.Flags,cqe.user_data})
 
 CompileResource(J) ⇔
-  preserves(Θ(J),Θ'(J))
-  ∧ no_hidden_pool_policy(helper)
-  ∧ no_hidden_gc_root(helper)
+  defined(⟦J⟧_U)
+  ∧ ∃ h.
+      h = ⟦J⟧_U
+      ∧ preserves(h,{Θ(J),Θ'(J)})
+      ∧ no_hidden_pool_policy(h)
+      ∧ no_hidden_gc_root(h)
 
 CompilePolicy(J) ⇔
   defined(⟦J⟧_U)
@@ -212,6 +221,9 @@ compilation_sound(J) ⇔
   ∧ DesignDirection(J)
   ∧ Roundtrip1(J)
   ∧ ∃ w ∈ World_U. compile_denotation_preserved(J,w)
+  ∧ (action(J)=submit → CompileSubmit(J))
+  ∧ (action(J)∈{wait,observe,decode} → CompileObserve(J))
+  ∧ CompileResource(J)
   ∧ CompilePolicy(J)
 
 reject(defined(⟦J⟧_U) ∧ hidden(CallerFrontier ∪ CallerPolicy, support(⟦J⟧_U)))
diff --git a/agents/formalization/notation.md b/agents/formalization/notation.md
index 7b0af01..6ffa3a1 100644
--- a/agents/formalization/notation.md
+++ b/agents/formalization/notation.md
@@ -16,9 +16,11 @@ The block below fixes the module strata (boundary `B`, caller `C = A ∪ D`, bel
 
 ```text
 module = pkg("code.hybscloud.com/uring")
+B = boundary(module)
 A = above(module)
 D = beyond(module)
 C = caller(module) = A ∪ D
+K = below(module)
 
 ASCIIAlpha = { c | "A" ≤ c ≤ "Z" ∨ "a" ≤ c ≤ "z" }
 ASCIIDigit = { c | "0" ≤ c ≤ "9" }
@@ -252,6 +254,13 @@ capital_sort_or_identifier(x) ⇔ x ∈ SortOrKind ∪ IdentifierCapital
 ∀x. bound_instance(x) → x ∉ SortOrKind ∧ x ∉ IdentifierCapital
 ∀cqe. field_access(cqe) ⊆ {cqe.Res, cqe.Flags, cqe.user_data}
 
+PathName = {p | finite_string(p)}
+Path = {path(p) | p ∈ PathName}
+SourceFile = {f ∈ Path | checked_out_source_file(f)}
+read_current_source : SourceFile → Bool
+read_current_source(f) ⇔
+  f ∈ SourceFile ∧ file_exists(f) ∧ read_at_current_revision(f)
+
 capital_allowed(Ctx) ⇔ kind_position(Ctx) ∨ sort_annotation(Ctx)
 capital_allowed(CQE) ⇔ sort_position(CQE) ∨ type_annotation(CQE)
 capital_allowed(R[κ]) ⇔ kind_family(R[κ])
diff --git a/agents/formalization/sessions.md b/agents/formalization/sessions.md
index 6597b61..99402ae 100644
--- a/agents/formalization/sessions.md
+++ b/agents/formalization/sessions.md
@@ -14,10 +14,10 @@ The block below states these rules formally.
 
 ```text
 module = pkg("code.hybscloud.com/uring")
+B = boundary(module)
 A = above(module)
 D = beyond(module)
 C = caller(module) = A ∪ D
-B = boundary(module)
 World_U = { w | world_for(module,w) }
 Denotation_U(w) = { d | denotation_at(module,w,d) }
 
diff --git a/agents/lift/protocols-runtime.md b/agents/lift/protocols-runtime.md
index 8e28982..25d5537 100644
--- a/agents/lift/protocols-runtime.md
+++ b/agents/lift/protocols-runtime.md
@@ -311,6 +311,26 @@ RuntimeOwnerFact_rc =
   {runtime_owner_pkg(p) | p ∈ RuntimeOwnerPkg}
 support(RuntimeOwnerFact_rc) ⊆ C
 RuntimeOwnerFact_rc ∩ support(B) = ∅
+RuntimeSource_rc =
+  { path("kont/effect.go"), path("kont/cont.go"), path("kont/frame.go"),
+    path("kont/bridge.go"), path("kont/step.go"), path("kont/trampoline.go"),
+    path("kont/index.go"), path("kont/affine.go"), path("kont/marker_pool.go"),
+    path("kont/pool.go"), path("kont/dispatch.go"),
+    path("cove/constraint.go"), path("cove/view.go"), path("cove/cmd.go"),
+    path("cove/req.go"), path("cove/req_expr.go"), path("cove/rule.go"),
+    path("cove/rule_expr.go"), path("cove/checked.go"),
+    path("cove/checked_expr.go"), path("cove/step.go"),
+    path("cove/kripke.go"), path("cove/bridge.go"),
+    path("takt/backend.go"), path("takt/takt.go"), path("takt/bridge.go"),
+    path("takt/step.go"), path("takt/error.go"), path("takt/loop.go"),
+    path("takt/option.go"), path("takt/subscription_backend.go"),
+    path("takt/subscription.go"), path("takt/subscription_option.go"),
+    path("takt/completion_memory.go"),
+    path("sess/op.go"), path("sess/session.go"), path("sess/step.go"),
+    path("sess/error.go"), path("sess/run.go"), path("sess/bridge.go"),
+    path("sess/fused.go"), path("sess/fused_expr.go"),
+    path("sess/rec.go"), path("sess/exec.go"), path("sess/serial.go") }
+source_checked(RuntimeSource_rc) ⇔ ∀ f ∈ RuntimeSource_rc. read_current_source(f)
 
 RuntimeTheoryRoute_rc =
   { pkg("code.hybscloud.com/kont")
@@ -358,6 +378,16 @@ current_suspension_rc(c) =
 current_suspension_rc(op) =
   ιs. s ∈ OneShotSuspension ∧ pending_op(s)=op
   if ∃!s. s ∈ OneShotSuspension ∧ pending_op(s)=op
+runtime_resume_value_rc(cqe) =
+  copy({cqe.Res, cqe.Flags, cqe.user_data, selected_buffer_metadata(cqe)})
+BoundaryContextFact_rc(cqe) =
+  copy({cqe.Res, cqe.Flags, cqe.user_data, selected_buffer_metadata(cqe),
+        capability_fact(cqe), ownership_fact(cqe)})
+ContextExtension_rc(ctx,cqe) =
+  extend(ctx,BoundaryContextFact_rc(cqe))
+support(ContextExtension_rc(ctx,cqe)) ⊆ C
+project(ContextExtension_rc(ctx,cqe),B) = ∅
+borrowed_cqe_pointer ∉ BoundaryContextFact_rc(cqe)
 more_flag_rc(c) = c.More
 more_flag_rc(c) ∈ Bool
 More_rc(c) ⇔ more_flag_rc(c) = true
@@ -392,6 +422,8 @@ ErrDisposed_rc =
   err_symbol(pkg("code.hybscloud.com/takt"),"ErrDisposed")
 ErrMore_rc ∈ ErrorSymbol
 ErrWouldBlock_rc ∈ ErrorSymbol
+SessTransportDomain_rc = {nil, ErrWouldBlock_rc}
+ErrMore_rc ∉ SessTransportDomain_rc
 TaktFatalSymbol_rc =
   {ErrUnsupportedMultishot_rc, ErrLiveTokenReuse_rc,
    ErrLiveRouteReuse_rc, ErrInvalidRouteID_rc, ErrDisposed_rc}
@@ -413,12 +445,65 @@ SessCarrier =
    Reify, Reflect, Step, Advance, StepError, AdvanceError,
    Run, RunExpr, RunError, RunErrorExpr,
    Exec, ExecExpr, ExecError, ExecErrorExpr, Loop, ExprLoop}
+SessOp_rc = {Send[T], Recv[T], Close, SelectL, SelectR, Offer}
+BoundaryProtocolStep_rc(step) ⇔
+  defined(bind(step)) ∧ bind(step) ∈ boundary_action(B)
+∀ protocol_io_step_rc.
+  BoundaryProtocolStep_rc(protocol_io_step_rc) →
+    one_boundary_action(bind(protocol_io_step_rc))
 
 Carrier_rc = KontCarrier ∪ CoveCarrier ∪ TaktCarrier ∪ SessCarrier
 support(Carrier_rc) ⊆ C
 project(Carrier_rc,B) = ∅
 support({PendingTable_rc,RouteTable_rc}) ⊆ C
 project({PendingTable_rc,RouteTable_rc},B) = ∅
+CodingObligation_kont_rc(op,s,cqe) ⇔
+  source_checked(RuntimeSource_rc)
+  ∧ BoundarySuspension(s,op)
+  ∧ one_shot(op)
+  ∧ copied_facts(runtime_resume_value_rc(cqe))
+  ∧ borrowed_cqe_view ∉ runtime_resume_value_rc(cqe)
+  ∧ project({s,resume,try_resume,discard},B) = ∅
+CodingObligation_cove_rc(ctx,s,guard,cqe) ⇔
+  source_checked(RuntimeSource_rc)
+  ∧ CoveRequirementGate(ctx,s,guard)
+  ∧ support(ContextExtension_rc(ctx,cqe)) ⊆ C
+  ∧ borrowed_cqe_pointer ∉ ContextExtension_rc(ctx,cqe)
+  ∧ project(CoveCarrier,B) = ∅
+CodingObligation_takt_rc(op,token,cqe) ⇔
+  source_checked(RuntimeSource_rc)
+  ∧ submit_token_rc(token,op)
+  ∧ token_indexes(token,user_data(op))
+  ∧ copied_facts(runtime_resume_value_rc(cqe))
+  ∧ classify_takt_dispatch(ErrMore_rc) ≠ classify_takt_completion_loop(ErrMore_rc)
+  ∧ project(TaktCarrier ∪ {PendingTable_rc,RouteTable_rc},B) = ∅
+CodingObligation_takt_stream_rc(op,route,c,cqe) ⇔
+  source_checked(RuntimeSource_rc)
+  ∧ multishot(op)
+  ∧ carrier(op) = SubscriptionLoop(pkg("code.hybscloud.com/takt"))
+  ∧ route ∈ RouteID
+  ∧ route = route_rc(c)
+  ∧ boundary_stream_completion_rc(c,cqe)
+  ∧ project(TaktCarrier ∪ {RouteTable_rc},B) = ∅
+CodingObligation_sess_rc(ep,op,err) ⇔
+  source_checked(RuntimeSource_rc)
+  ∧ single_owner(ep)
+  ∧ op ∈ SessOp_rc
+  ∧ ∃ protocol_io_step_rc.
+      BoundaryProtocolStep_rc(protocol_io_step_rc)
+      ∧ bind(protocol_io_step_rc) = op
+  ∧ err ∈ SessTransportDomain_rc
+  ∧ classify_sess_transport(err) ∈ {ok,wouldBlock}
+  ∧ classify_sess_transport(ErrMore_rc) = unexpected(ErrMore_rc)
+  ∧ protocol_frontier(session(ep)) ∈ CallerFrontier
+  ∧ support(protocol_frontier(session(ep))) ⊆ C
+  ∧ project(SessCarrier,B) = ∅
+RuntimeCodingObligation_rc =
+  {CodingObligation_kont_rc, CodingObligation_cove_rc,
+   CodingObligation_takt_rc, CodingObligation_takt_stream_rc,
+   CodingObligation_sess_rc}
+support(RuntimeCodingObligation_rc) ⊆ C
+project(RuntimeCodingObligation_rc,B) = ∅
 
 CoveRequirementGate(ctx,s,guard) ⇔
   owner(ctx) = pkg("code.hybscloud.com/cove")
@@ -597,6 +682,8 @@ Preservation_rc =
   ∧ support(BoundaryFacts) ⊆ B
   ∧ project(Carrier_rc ∪ RuntimePolicy,B)=∅
   ∧ project(RuntimeTheoryUse_rc,B)=∅
+  ∧ support(RuntimeCodingObligation_rc) ⊆ C
+  ∧ project(RuntimeCodingObligation_rc,B)=∅
   ∧ classify_takt_dispatch(ErrMore_rc)
        ≠ classify_takt_completion_loop(ErrMore_rc)
   ∧ classify_takt_dispatch(ErrMore_rc)
diff --git a/agents/runtime/INDEX.md b/agents/runtime/INDEX.md
index 4afecad..1a6996c 100644
--- a/agents/runtime/INDEX.md
+++ b/agents/runtime/INDEX.md
@@ -2,7 +2,7 @@
 
 This directory explains how caller-side code combines `code.hybscloud.com/uring` with four caller-layer support packages: `code.hybscloud.com/kont` for suspension and one-shot resumption, `code.hybscloud.com/cove` for explicit context and requirement evidence, `code.hybscloud.com/takt` for runner movement, completion routing, and error-aware stepping, and `code.hybscloud.com/sess` for session-typed protocol frontiers, paired execution, and endpoint stepping. The packages themselves stay in the caller layer. A boundary helper may receive copied facts derived from them, but it must not import their policy, route state, endpoint state, completion memory, or long-lived control logic into `code.hybscloud.com/uring`.
 
-Each file describes one package: which boundary facts it consumes, which caller-owned decisions it carries, and which obligations apply when its carriers wrap a `code.hybscloud.com/uring` boundary action. The packages remain general caller-layer tools; the formulas in this directory constrain their boundary-wrapped use, not every possible use of those packages. The shallow handler discipline defined in [uring/agents/boundary/protocols.md](../boundary/protocols.md) is restated inside each file for the package it covers: every carrier handles one boundary observation and returns control to the caller. Read the package source named by a file before relying on its facts, following the checklist in [uring/agents/workflow/task-checklists.md](../workflow/task-checklists.md).
+Each file describes one package: which boundary facts it consumes, which caller-owned decisions it carries, and which obligations apply when its carriers wrap a `code.hybscloud.com/uring` boundary action. The packages remain general caller-layer tools; the formulas in this directory constrain their boundary-wrapped use, not every possible use of those packages. The shallow handler discipline defined in [uring/agents/boundary/protocols.md](../boundary/protocols.md) is restated inside each file for the package it covers: every carrier handles one boundary observation and returns control to the caller. Each runtime file also names the package source evidence and a `CodingObligation_*` predicate so code review can check the guide against the current public package surface. Read the package source named by a file before relying on its facts, following the checklist in [uring/agents/workflow/task-checklists.md](../workflow/task-checklists.md).
 
 ## Reading Order
 
diff --git a/agents/runtime/cove.md b/agents/runtime/cove.md
index 759e317..c81ba8c 100644
--- a/agents/runtime/cove.md
+++ b/agents/runtime/cove.md
@@ -52,6 +52,13 @@ MonotoneFacts =
   {capability_present, registration_done, terminal_observed}
 NonMonotoneFacts =
   {frontier_live, buffer_owned, fd_open, ring_not_closed, token_live}
+Source_cove =
+  {path("cove/constraint.go"), path("cove/view.go"), path("cove/cmd.go"),
+   path("cove/req.go"), path("cove/req_expr.go"), path("cove/rule.go"),
+   path("cove/rule_expr.go"), path("cove/checked.go"),
+   path("cove/checked_expr.go"), path("cove/step.go"),
+   path("cove/kripke.go"), path("cove/bridge.go")}
+source_checked(Source_cove) ⇔ ∀ f ∈ Source_cove. read_current_source(f)
 World = (MonotoneFactsState, EphemeralFactsState, Requirements, Epoch)
 monotone_facts(w) ⊆ MonotoneFacts
 ephemeral_facts(w) ⊆ NonMonotoneFacts
@@ -92,6 +99,14 @@ GuardedSuspensionView(ctx,s,guard) ⇔
   SuspensionView(ctx,s)
   ∧ guard ∈ Guard
   ∧ guard_holds(ctx,guard)
+CodingObligation_cove(ctx,s,guard,cqe) ⇔
+  source_checked(Source_cove)
+  ∧ GuardedSuspensionView(ctx,s,guard)
+  ∧ support(ContextExtension(ctx,cqe)) ⊆ C
+  ∧ borrowed_cqe_pointer ∉ ContextExtension(ctx,cqe)
+  ∧ ∀ F ∈ NonMonotoneFacts. check_at_use_epoch(F)
+  ∧ ∀ F ∈ NonMonotoneFacts. reject(cache_across(F,suspension_frontier))
+  ∧ project(CtxCarrier ∪ ExprCarrier ∪ KripkeCarrier ∪ {World},B) = ∅
 resume(GuardedSuspensionView(ctx,s,guard),v) →
   requirement_evidence(guard,ctx) ∈ C
 ¬requirements_hold(ctx) → decision_owner({wait, reroute, abandon}) = C
diff --git a/agents/runtime/kont.md b/agents/runtime/kont.md
index ca69558..56b3fb6 100644
--- a/agents/runtime/kont.md
+++ b/agents/runtime/kont.md
@@ -47,8 +47,28 @@ SuspCarrier = {Suspension[A], Affine[R,A], EffectFrame[A]}
 BoundaryObservation =
   {cqe_res, cqe_flags, user_data, selected_buffer, capability_fact,
    ownership_fact}
+Source_kont =
+  {path("kont/effect.go"), path("kont/cont.go"), path("kont/frame.go"),
+   path("kont/bridge.go"), path("kont/step.go"), path("kont/trampoline.go"),
+   path("kont/index.go"), path("kont/affine.go"), path("kont/marker_pool.go"),
+   path("kont/pool.go"), path("kont/dispatch.go")}
+source_checked(Source_kont) ⇔ ∀ f ∈ Source_kont. read_current_source(f)
 BoundaryWrapped(s) ⇔
   s ∈ Suspension[A] ∧ pending_op(s) ∈ boundary_action(B)
+CodingObligation_kont(op,s,cqe) ⇔
+  source_checked(Source_kont)
+  ∧ BoundaryWrapped(s)
+  ∧ pending_op(s)=op
+  ∧ one_shot(op)
+  ∧ affine(s)
+  ∧ resume_value(cqe) =
+      copy({cqe.Res, cqe.Flags, cqe.user_data, selected_buffer_metadata(cqe)})
+  ∧ resume_value(cqe) ∩ borrowed_cqe_view = ∅
+  ∧ closure_capture(continuation_of(s))
+      ⊆ copied_completion_facts ∪ caller_owned_state
+  ∧ project({s,resume,try_resume,discard},B) = ∅
+multishot(op) → ¬CodingObligation_kont(op,s,cqe)
+multishot(op) → route_via(SubscriptionLoop(pkg("code.hybscloud.com/takt")))
 
 ⟦Perform(op)⟧ = suspended(effect_operation_shape(op))
 ⟦ExprPerform(op)⟧ = suspended(effect_operation_shape(op))
diff --git a/agents/runtime/sess.md b/agents/runtime/sess.md
index 25d53cf..834f33a 100644
--- a/agents/runtime/sess.md
+++ b/agents/runtime/sess.md
@@ -51,6 +51,12 @@ ProtocolCarrier = {Eff[A], Expr[A], Either[E,A], Suspension[A]}
 Endpoint = SessionState × Transport × Serial
 Transport = bounded_spsc_queues(capacity=4)
 Op = Send(v) ⊎ Recv ⊎ Close ⊎ SelectL ⊎ SelectR ⊎ Offer
+Source_sess =
+  {path("sess/op.go"), path("sess/session.go"), path("sess/step.go"),
+   path("sess/error.go"), path("sess/run.go"), path("sess/bridge.go"),
+   path("sess/fused.go"), path("sess/fused_expr.go"),
+   path("sess/rec.go"), path("sess/exec.go"), path("sess/serial.go")}
+source_checked(Source_sess) ⇔ ∀ f ∈ Source_sess. read_current_source(f)
 current_suspension_sess(op) =
   ιs. s ∈ type_symbol(pkg("code.hybscloud.com/kont"),"Suspension[A]")
       ∧ pending_op(s)=op
@@ -62,15 +68,29 @@ E_sess ∩ {err_symbol(pkg("code.hybscloud.com/iox"),"ErrWouldBlock"),
 Unexpected_sess = {err_symbol(pkg("code.hybscloud.com/iox"),"ErrMore")} ∪ E_sess
 Unexpected_sess_outcome = { unexpected(e) | e ∈ Unexpected_sess }
 SessTransportCtrl = {ok, wouldBlock}
+SessTransportDomain =
+  {nil, err_symbol(pkg("code.hybscloud.com/iox"),"ErrWouldBlock")}
+q_sess_transport : SessTransportDomain → SessTransportCtrl
 q_sess_transport(nil) = ok
 q_sess_transport(err_symbol(pkg("code.hybscloud.com/iox"),"ErrWouldBlock")) =
   wouldBlock
-q_sess_transport(err_symbol(pkg("code.hybscloud.com/iox"),"ErrMore")) =
-  undefined
-dom(q_sess_transport) =
-  {nil, err_symbol(pkg("code.hybscloud.com/iox"),"ErrWouldBlock")}
+dom(q_sess_transport) = SessTransportDomain
 err_symbol(pkg("code.hybscloud.com/iox"),"ErrMore")
-  ∉ dom(q_sess_transport)
+  ∉ SessTransportDomain
+CodingObligation_sess(ep,op,err) ⇔
+  source_checked(Source_sess)
+  ∧ single_owner(ep)
+  ∧ op ∈ Op
+  ∧ ∃ protocol_io_step.
+      BoundaryProtocolStep(protocol_io_step)
+      ∧ bind(protocol_io_step) = op
+  ∧ err ∈ dom(q_sess_transport)
+  ∧ q_sess_transport(err) ∈ SessTransportCtrl
+  ∧ err_symbol(pkg("code.hybscloud.com/iox"),"ErrMore")
+      ∉ dom(q_sess_transport)
+  ∧ protocol_frontier(session(ep)) ∈ CallerFrontier
+  ∧ support(protocol_frontier(session(ep))) ⊆ C
+  ∧ project(SessCarrier ∪ ProtocolCarrier ∪ CallerCheck,B) = ∅
 
 protocol_frontier(session) ∈ CallerFrontier
 ⟦Reify(Eff[A])⟧ = Expr[A]
@@ -80,7 +100,8 @@ support({Reify, Reflect}) ⊆ C
 project({Reify, Reflect}, B) = ∅
 BoundaryProtocolStep(step) ⇔
   defined(bind(step)) ∧ bind(step) ∈ boundary_action(B)
-BoundaryProtocolStep(protocol_io_step) → one_boundary_action(bind(protocol_io_step))
+∀ protocol_io_step.
+  BoundaryProtocolStep(protocol_io_step) → one_boundary_action(bind(protocol_io_step))
 single_owner(Endpoint)
 single_producer_single_consumer(Transport)
 concurrent_use(Endpoint) → reject
diff --git a/agents/runtime/takt.md b/agents/runtime/takt.md
index 591de13..2337861 100644
--- a/agents/runtime/takt.md
+++ b/agents/runtime/takt.md
@@ -53,6 +53,13 @@ EffectCarrier = {Eff[A], Expr[A], Either[E,A], Suspension[A]}
 
 Completion = {Token, Value, Err}
 StreamCompletion = {RouteID, Value, HasValue, EventErr, More}
+Source_takt =
+  {path("takt/backend.go"), path("takt/takt.go"), path("takt/bridge.go"),
+   path("takt/step.go"), path("takt/error.go"), path("takt/loop.go"),
+   path("takt/option.go"), path("takt/subscription_backend.go"),
+   path("takt/subscription.go"), path("takt/subscription_option.go"),
+   path("takt/completion_memory.go")}
+source_checked(Source_takt) ⇔ ∀ f ∈ Source_takt. read_current_source(f)
 ErrMore_takt = err_symbol(pkg("code.hybscloud.com/iox"),"ErrMore")
 ErrWouldBlock_takt = err_symbol(pkg("code.hybscloud.com/iox"),"ErrWouldBlock")
 ErrUnsupportedMultishot_takt =
@@ -106,6 +113,21 @@ current_suspension_takt(op) =
 BoundaryDispatch(op) ⇔ op ∈ boundary_action(B)
 BoundaryCompletionValue(v) ⇔
   copied_facts(v) ∧ borrowed_cqe_view ∉ v
+completion_value_takt(cqe) =
+  copy({cqe.Res, cqe.Flags, cqe.user_data, selected_buffer_metadata(cqe)})
+CodingObligation_takt(op,token,cqe) ⇔
+  source_checked(Source_takt)
+  ∧ BoundaryDispatch(op)
+  ∧ token_indexes(token,user_data(op))
+  ∧ BoundaryCompletionValue(completion_value_takt(cqe))
+  ∧ ((one_shot(op) ∧ route_via(Loop(pkg("code.hybscloud.com/takt"))))
+     ∨ (multishot(op)
+        ∧ route_via(SubscriptionLoop(pkg("code.hybscloud.com/takt")))))
+  ∧ DispatchErrMore_takt ≠ CompletionErrMore_takt
+  ∧ (multishot(op)
+       → ¬route_via(Loop(pkg("code.hybscloud.com/takt"))))
+  ∧ project(RunnerCarrier ∪ {PendingTable, RouteTable,
+             CompletionMemoryStore_takt},B) = ∅
 
 boundary_token_correlates(token,op) ⇔
   BoundaryDispatch(op)