diff --git a/PolyFun.lean b/PolyFun.lean
index 55153ac..52a346d 100644
--- a/PolyFun.lean
+++ b/PolyFun.lean
@@ -193,6 +193,7 @@ public import PolyFun.PFunctor.Free.Resumption
 public import PolyFun.PFunctor.Free.Universal
 public import PolyFun.PFunctor.Handler
 public import PolyFun.PFunctor.Handler.Free
+public import PolyFun.PFunctor.Handler.Instrumentation
 public import PolyFun.PFunctor.Handler.Normalization
 public import PolyFun.PFunctor.Handler.Normalization.Attr
 public import PolyFun.PFunctor.Handler.Stateful
diff --git a/PolyFun/Interaction/Basic/Sampler.lean b/PolyFun/Interaction/Basic/Sampler.lean
index 4478ec0..393cd06 100644
--- a/PolyFun/Interaction/Basic/Sampler.lean
+++ b/PolyFun/Interaction/Basic/Sampler.lean
@@ -74,6 +74,40 @@ def samplePath {m : Type w → Type w'} [Monad m] :
       let tr ← samplePath (rest x) (sampRest x)
       return ⟨x, tr⟩
 
+/-- Sampling a completed interaction returns its unique empty path. -/
+@[simp]
+theorem samplePath_done {m : Type w → Type w'} [Monad m]
+    (sampler : Sampler m .done) :
+    samplePath .done sampler = pure ⟨⟩ := by
+  rfl
+
+/-! The raw and `TypeTree`-facing node equations are both public so callers can
+rewrite without depending on which transparent representation Lean exposes. -/
+
+/-- Sampling a raw free-monad node first samples its head value and then its
+dependent tail path. -/
+@[simp]
+theorem samplePath_lift_bind {m : Type w → Type w'} [Monad m]
+    {X : Type w} (rest : X → TypeTree.{w})
+    (sampler : m X) (samplerRest : ∀ x, Sampler m (rest x)) :
+    samplePath (@PFunctor.FreeM.lift TypeTree.basePFunctor X >>= rest)
+        ⟨sampler, samplerRest⟩ = do
+      let x ← sampler
+      let tr ← samplePath (rest x) (samplerRest x)
+      return ⟨x, tr⟩ := by
+  rfl
+
+/-- Sampling a `TypeTree.node` first samples its head value and then its
+dependent tail path. -/
+theorem samplePath_node {m : Type w → Type w'} [Monad m]
+    {X : Type w} (rest : X → TypeTree.{w})
+    (sampler : m X) (samplerRest : ∀ x, Sampler m (rest x)) :
+    samplePath (TypeTree.node X rest) ⟨sampler, samplerRest⟩ = do
+      let x ← sampler
+      let tr ← samplePath (rest x) (samplerRest x)
+      return ⟨x, tr⟩ := by
+  rfl
+
 /--
 Combine a scheduler sampler with two per-branch samplers into a sampler
 for the binary-choice interleaving tree
diff --git a/PolyFun/Interaction/Concurrent/Fairness.lean b/PolyFun/Interaction/Concurrent/Fairness.lean
index 8afb727..922880e 100644
--- a/PolyFun/Interaction/Concurrent/Fairness.lean
+++ b/PolyFun/Interaction/Concurrent/Fairness.lean
@@ -46,11 +46,23 @@ forever. -/
 def EventuallyAlways (P : Nat → Prop) : Prop :=
   ∃ N, ∀ n, N ≤ n → P n
 
+/-- Characterize eventual persistence by a cutoff after which the property
+holds at every later index. -/
+theorem eventuallyAlways_iff {P : Nat → Prop} :
+    EventuallyAlways P ↔ ∃ N, ∀ n, N ≤ n → P n :=
+  Iff.rfl
+
 /-- `InfinitelyOften P` means that `P` holds at arbitrarily late time
 indices. -/
 def InfinitelyOften (P : Nat → Prop) : Prop :=
   ∀ N, ∃ n, N ≤ n ∧ P n
 
+/-- Characterize infinite recurrence by the existence of a witness at or
+after every requested index. -/
+theorem infinitelyOften_iff {P : Nat → Prop} :
+    InfinitelyOften P ↔ ∀ N, ∃ n, N ≤ n ∧ P n :=
+  Iff.rfl
+
 theorem always_mono {P Q : Nat → Prop} (himp : ∀ n, P n → Q n) : Always P → Always Q :=
   fun hP n => himp n (hP n)
 
diff --git a/PolyFun/Interaction/Multiparty/Observation.lean b/PolyFun/Interaction/Multiparty/Observation.lean
index e37bc06..4f08edb 100644
--- a/PolyFun/Interaction/Multiparty/Observation.lean
+++ b/PolyFun/Interaction/Multiparty/Observation.lean
@@ -163,6 +163,7 @@ variable {X : Type u}
 
 Every `Observation X` refines `Observation.top X`.
 -/
+@[expose]
 protected def top (X : Type u) : Observation X := ⟨X, id⟩
 
 /--
@@ -187,6 +188,12 @@ observers using `k₂` learn. This is the natural ordering in which
 def Refines (k₁ k₂ : Observation X) : Prop :=
   ∃ f : k₂.1 → k₁.1, ∀ x, k₁.2 x = f (k₂.2 x)
 
+/-- Observation refinement holds exactly when the first observation factors
+through the second by an explicit map. -/
+theorem refines_iff {k₁ k₂ : Observation X} :
+    k₁.Refines k₂ ↔ ∃ f : k₂.1 → k₁.1, ∀ x, k₁.2 x = f (k₂.2 x) :=
+  Iff.rfl
+
 @[refl] theorem Refines.refl (k : Observation X) : k.Refines k :=
   ⟨id, fun _ => rfl⟩
 
diff --git a/PolyFun/Interaction/UC/OpenProcess.lean b/PolyFun/Interaction/UC/OpenProcess.lean
index 70e7e06..17fb9e7 100644
--- a/PolyFun/Interaction/UC/OpenProcess.lean
+++ b/PolyFun/Interaction/UC/OpenProcess.lean
@@ -657,6 +657,48 @@ def OpenNodeContext.boundaryTrace {Party : Type u} {Δ : PortBoundary} : (spec :
   | .node _ rest, ⟨node, next⟩, ⟨x, tr⟩ =>
       node.boundary.emit x * OpenNodeContext.boundaryTrace (rest x) (next x) tr
 
+/-- A completed open node contributes no boundary actions. -/
+@[simp]
+theorem OpenNodeContext.boundaryTrace_done {Party : Type u} {Δ : PortBoundary}
+    (semantics : Decoration (OpenNodeContext.{u, w} Party Δ)
+      (TypeTree.done : TypeTree.{w}))
+    (path : TypeTree.Path (TypeTree.done : TypeTree.{w})) :
+    OpenNodeContext.boundaryTrace (Party := Party) (Δ := Δ) TypeTree.done semantics path =
+      (1 : PFunctor.TraceList Δ.Out) := by
+  rfl
+
+/-! The raw and `TypeTree`-facing node equations are both public so callers can
+rewrite without depending on which transparent representation Lean exposes. -/
+
+/-- A raw free-monad node emits the head boundary action and continues along
+the chosen tail. -/
+@[simp]
+theorem OpenNodeContext.boundaryTrace_lift_bind {Party : Type u} {Δ : PortBoundary}
+    {X : Type w} (rest : X → TypeTree.{w})
+    (semantics : Decoration (OpenNodeContext.{u, w} Party Δ) (TypeTree.node X rest))
+    (x : X) (path : TypeTree.Path (rest x)) :
+    OpenNodeContext.boundaryTrace (Party := Party) (Δ := Δ)
+        (@PFunctor.FreeM.lift TypeTree.basePFunctor X >>= rest) semantics ⟨x, path⟩ =
+      semantics.1.boundary.emit x *
+        OpenNodeContext.boundaryTrace (Party := Party) (Δ := Δ)
+          (rest x) (semantics.2 x) path := by
+  rcases semantics with ⟨node, next⟩
+  rfl
+
+/-- A `TypeTree.node` emits the head boundary action and continues along the
+chosen tail. -/
+theorem OpenNodeContext.boundaryTrace_node {Party : Type u} {Δ : PortBoundary}
+    {X : Type w} (rest : X → TypeTree.{w})
+    (semantics : Decoration (OpenNodeContext.{u, w} Party Δ) (TypeTree.node X rest))
+    (x : X) (path : TypeTree.Path (rest x)) :
+    OpenNodeContext.boundaryTrace (Party := Party) (Δ := Δ)
+        (TypeTree.node X rest) semantics ⟨x, path⟩ =
+      semantics.1.boundary.emit x *
+        OpenNodeContext.boundaryTrace (Party := Party) (Δ := Δ)
+          (rest x) (semantics.2 x) path := by
+  rcases semantics with ⟨node, next⟩
+  rfl
+
 /--
 The open-world specialization of `StepOver`.
 
@@ -674,6 +716,12 @@ def boundaryTrace {Party : Type u} {Δ : PortBoundary} {P : Type v}
     (step : OpenStep Party Δ P) (tr : TypeTree.Path step.tree) : PFunctor.TraceList Δ.Out :=
   OpenNodeContext.boundaryTrace step.tree step.semantics tr
 
+/-- The boundary trace of an open step is the trace of its decorated interaction tree. -/
+theorem boundaryTrace_eq {Party : Type u} {Δ : PortBoundary} {P : Type v}
+    (step : OpenStep Party Δ P) (tr : TypeTree.Path step.tree) :
+    boundaryTrace step tr = OpenNodeContext.boundaryTrace step.tree step.semantics tr := by
+  rfl
+
 end OpenStep
 
 /--
diff --git a/PolyFun/PFunctor/Handler/Instrumentation.lean b/PolyFun/PFunctor/Handler/Instrumentation.lean
new file mode 100644
index 0000000..7648fc1
--- /dev/null
+++ b/PolyFun/PFunctor/Handler/Instrumentation.lean
@@ -0,0 +1,184 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma, Quang Dao
+-/
+
+module
+
+public import Mathlib.Control.Monad.Writer
+public import PolyFun.PFunctor.Handler
+
+/-!
+# Instrumenting Monadic Handlers
+
+This module provides effect-generic constructions for polynomial-functor
+handlers. `liftTarget` changes the target monad through `MonadLiftT`, while
+`preInsert` and `postInsert` add a side effect before or after each handled
+operation. The writer specializations record response-independent or
+response-dependent traces without depending on any oracle-specific API.
+-/
+
+public section
+
+universe u v w uA
+
+namespace PFunctor
+namespace Handler
+
+variable {P : PFunctor.{uA, u}}
+variable {m : Type u → Type v} {n : Type u → Type w}
+
+/-- Lift every operation of a handler into a new target monad. -/
+-- Keep this structural adapter transparent: dependent handler result types
+-- frequently need its pointwise reduction during elaboration.
+@[expose] def liftTarget (n : Type u → Type w) [MonadLiftT m n]
+    (handler : Handler m P) : Handler n P :=
+  fun operation => liftM (handler operation)
+
+@[simp]
+theorem liftTarget_apply (n : Type u → Type w) [MonadLiftT m n]
+    (handler : Handler m P) (operation : P.A) :
+    handler.liftTarget n operation = liftM (handler operation) :=
+  by rfl
+
+/-- Lifting a handler to its current target has no effect. -/
+@[simp]
+theorem liftTarget_self (handler : Handler m P) :
+    handler.liftTarget m = handler :=
+  by rfl
+
+/-- Run an effect before handling each operation.
+
+The inserted effect is sequenced before the underlying handler. Whether its
+effects remain observable if that handler subsequently fails depends on the
+target monad's transformer order; for example, `WriterT` over `Option` discards
+the log together with a failed result. The inserted effect's value is
+discarded. -/
+def preInsert [Monad n] [MonadLiftT m n] {α : Type u}
+    (handler : Handler m P) (before : P.A → n α) : Handler n P :=
+  fun operation => before operation *> liftM (handler operation)
+
+@[simp, grind =]
+theorem preInsert_apply [Monad n] [MonadLiftT m n] {α : Type u}
+    (handler : Handler m P) (before : P.A → n α) (operation : P.A) :
+    handler.preInsert before operation =
+      before operation *> liftM (handler operation) :=
+  by rfl
+
+/-- Run an effect after handling each operation.
+
+The inserted effect may depend on the response and is skipped if the
+underlying handler fails. Its result is discarded. -/
+def postInsert [Monad n] [MonadLiftT m n] {α : Type u}
+    (handler : Handler m P) (after : (operation : P.A) → P.B operation → n α) :
+    Handler n P :=
+  fun operation => do
+    let response ← liftM (handler operation)
+    let _ ← after operation response
+    return response
+
+@[simp, grind =]
+theorem postInsert_apply [Monad n] [MonadLiftT m n] {α : Type u}
+    (handler : Handler m P) (after : (operation : P.A) → P.B operation → n α)
+    (operation : P.A) :
+    handler.postInsert after operation = do
+      let response ← liftM (handler operation)
+      let _ ← after operation response
+      return response :=
+  by rfl
+
+/-! ## Writer traces -/
+
+variable [Monad m]
+
+/-- Record a response-independent trace before each handled operation. -/
+def withTraceBefore {ω : Type u} [Monoid ω]
+    (handler : Handler m P) (trace : P.A → ω) : Handler (WriterT ω m) P :=
+  handler.preInsert fun operation => tell (trace operation)
+
+@[simp, grind =]
+theorem withTraceBefore_apply {ω : Type u} [Monoid ω]
+    (handler : Handler m P) (trace : P.A → ω) (operation : P.A) :
+    handler.withTraceBefore trace operation = (do
+      tell (trace operation)
+      handler operation) :=
+  by rfl
+
+/-- Response-independent writer tracing is before-insertion of `tell`. -/
+theorem withTraceBefore_eq_preInsert {ω : Type u} [Monoid ω]
+    (handler : Handler m P) (trace : P.A → ω) :
+    handler.withTraceBefore trace =
+      handler.preInsert (fun operation => tell (trace operation)) := by
+  rfl
+
+/-- Record a response-dependent trace after each handled operation. -/
+def withTrace {ω : Type u} [Monoid ω]
+    (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω) :
+    Handler (WriterT ω m) P :=
+  handler.postInsert fun operation response => tell (trace operation response)
+
+@[simp, grind =]
+theorem withTrace_apply {ω : Type u} [Monoid ω]
+    (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω)
+    (operation : P.A) :
+    handler.withTrace trace operation = do
+      let response ← handler operation
+      tell (trace operation response)
+      return response :=
+  by rfl
+
+/-- Response-dependent writer tracing is after-insertion of `tell`. -/
+theorem withTrace_eq_postInsert {ω : Type u} [Monoid ω]
+    (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω) :
+    handler.withTrace trace =
+      handler.postInsert (fun operation response => tell (trace operation response)) := by
+  rfl
+
+/-- Append-flavoured response-independent tracing. -/
+def withTraceAppendBefore {ω : Type u} [EmptyCollection ω] [Append ω]
+    (handler : Handler m P) (trace : P.A → ω) : Handler (WriterT ω m) P :=
+  handler.preInsert fun operation => tell (trace operation)
+
+@[simp, grind =]
+theorem withTraceAppendBefore_apply {ω : Type u} [EmptyCollection ω] [Append ω]
+    (handler : Handler m P) (trace : P.A → ω) (operation : P.A) :
+    handler.withTraceAppendBefore trace operation = (do
+      tell (trace operation)
+      handler operation) :=
+  by rfl
+
+/-- Append-flavoured before-tracing is before-insertion of `tell`. -/
+theorem withTraceAppendBefore_eq_preInsert {ω : Type u}
+    [EmptyCollection ω] [Append ω]
+    (handler : Handler m P) (trace : P.A → ω) :
+    handler.withTraceAppendBefore trace =
+      handler.preInsert (fun operation => tell (trace operation)) := by
+  rfl
+
+/-- Append-flavoured response-dependent tracing. -/
+def withTraceAppend {ω : Type u} [EmptyCollection ω] [Append ω]
+    (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω) :
+    Handler (WriterT ω m) P :=
+  handler.postInsert fun operation response => tell (trace operation response)
+
+@[simp, grind =]
+theorem withTraceAppend_apply {ω : Type u} [EmptyCollection ω] [Append ω]
+    (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω)
+    (operation : P.A) :
+    handler.withTraceAppend trace operation = do
+      let response ← handler operation
+      tell (trace operation response)
+      return response :=
+  by rfl
+
+/-- Append-flavoured after-tracing is after-insertion of `tell`. -/
+theorem withTraceAppend_eq_postInsert {ω : Type u}
+    [EmptyCollection ω] [Append ω]
+    (handler : Handler m P) (trace : (operation : P.A) → P.B operation → ω) :
+    handler.withTraceAppend trace =
+      handler.postInsert (fun operation response => tell (trace operation response)) := by
+  rfl
+
+end Handler
+end PFunctor
diff --git a/PolyFunTest/PFunctor/Handler/Instrumentation.lean b/PolyFunTest/PFunctor/Handler/Instrumentation.lean
new file mode 100644
index 0000000..4637cd9
--- /dev/null
+++ b/PolyFunTest/PFunctor/Handler/Instrumentation.lean
@@ -0,0 +1,217 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+
+module
+
+public import Mathlib.Control.ULift
+public import PolyFun.PFunctor.Free.Basic
+public import PolyFun.PFunctor.Handler.Instrumentation
+
+/-!
+# Handler instrumentation regression tests
+
+Producer-level canaries for effect ordering, failure behavior,
+response-dependent writer events, noncommutative trace accumulation, target
+lifting across universes, and instrumentation of a multi-node `FreeM`
+program.
+-/
+
+@[expose] public section
+
+namespace PFunctor.Handler.Instrumentation.Tests
+
+/-- Two distinguishable operations, each answered by a natural number. -/
+@[reducible]
+def Q : PFunctor.{0, 0} := { A := Bool, B := fun _ => Nat }
+
+/-- Events distinguish when an operation starts, when its handler runs, and
+the response observed after it returns. -/
+inductive Event where
+  | before (operation : Bool)
+  | handled (operation : Bool) (response : Nat)
+  | after (operation : Bool) (response : Nat)
+  deriving DecidableEq, Repr
+
+/-- An order-sensitive event log with concatenation as multiplication. -/
+structure EventLog where
+  events : List Event
+  deriving DecidableEq, Repr
+
+instance : Monoid EventLog where
+  one := ⟨[]⟩
+  mul left right := ⟨left.events ++ right.events⟩
+  one_mul := fun ⟨_activities⟩ => rfl
+  mul_one := fun ⟨activities⟩ => congrArg EventLog.mk (List.append_nil activities)
+  mul_assoc := fun ⟨left⟩ ⟨middle⟩ ⟨right⟩ =>
+    congrArg EventLog.mk (List.append_assoc left middle right)
+
+/-- A writer-valued handler whose two branches have distinguishable answers. -/
+def writerHandler : Handler (Writer EventLog) Q
+  | true => do
+      tell ⟨[Event.handled true 2]⟩
+      return 2
+  | false => do
+      tell ⟨[Event.handled false 5]⟩
+      return 5
+
+def beforeWriter (operation : Bool) : Writer EventLog PUnit :=
+  tell ⟨[Event.before operation]⟩
+
+def afterWriter (operation : Bool) (response : Nat) :
+    Writer EventLog PUnit :=
+  tell ⟨[Event.after operation response]⟩
+
+/-- Pre-insertion occurs before the underlying handler. -/
+example :
+    Id.run (writerHandler.preInsert beforeWriter true).run =
+      (2, ⟨[Event.before true, Event.handled true 2]⟩) := by
+  rw [Handler.preInsert_apply]
+  change (2, (⟨[Event.before true, Event.handled true 2]⟩ : EventLog)) = _
+  rfl
+
+/-- Post-insertion observes the response and occurs after the handler. -/
+example :
+    Id.run (writerHandler.postInsert afterWriter false).run =
+      (5, ⟨[Event.handled false 5, Event.after false 5]⟩) := by
+  rw [Handler.postInsert_apply]
+  change (5, (⟨[Event.handled false 5, Event.after false 5]⟩ : EventLog)) = _
+  rfl
+
+/-- A failing base handler for transformer-order canaries. -/
+def failingHandler : Handler Option Q := fun _ => none
+
+/-- `WriterT` over `Option` discards a pre-inserted log when the handler
+fails, because the entire writer result is absent. -/
+example :
+    (failingHandler.withTraceBefore (fun operation =>
+      (⟨[Event.before operation]⟩ : EventLog)) true).run = none := by
+  simp [failingHandler]
+
+/-- A post-inserted event is skipped when the underlying handler fails. -/
+example :
+    (failingHandler.withTrace (fun operation response =>
+      (⟨[Event.after operation response]⟩ : EventLog)) false).run = none := by
+  simp [failingHandler]
+
+/-- With `OptionT` over `Writer`, the outer writer retains a pre-inserted event
+even when the inner optional result fails. -/
+def failingLoggedHandler : Handler (OptionT (Writer EventLog)) Q :=
+  fun _ => failure
+
+def beforeLoggedOption (operation : Bool) :
+    OptionT (Writer EventLog) PUnit :=
+  OptionT.lift (tell ⟨[Event.before operation]⟩)
+
+example :
+    Id.run ((failingLoggedHandler.preInsert beforeLoggedOption true).run).run =
+      ((none : Option Nat), ⟨[Event.before true]⟩) := by
+  rw [Handler.preInsert_apply]
+  change ((none : Option Nat), (⟨[Event.before true]⟩ : EventLog)) = _
+  rfl
+
+/-- A pure handler used to test writer instrumentation over a complete free
+program. -/
+def answerHandler : Handler Id Q
+  | true => 2
+  | false => 5
+
+/-- The first response selects a different second operation, so this is not a
+constant-branch or one-node canary. -/
+def twoNodeProgram : FreeM Q Nat :=
+  FreeM.liftBind true fun first =>
+    FreeM.liftBind (first == 5) fun second =>
+      pure (10 * first + second)
+
+def instrumentedHandler : Handler (Writer EventLog) Q :=
+  (answerHandler.withTraceBefore (fun operation =>
+    (⟨[Event.before operation]⟩ : EventLog))).postInsert afterWriter
+
+lemma instrumentedHandler_true : instrumentedHandler true =
+    WriterT.mk ((2, ⟨[Event.before true, Event.after true 2]⟩) :
+      Id (Nat × EventLog)) := by
+  unfold instrumentedHandler
+  rw [Handler.postInsert_apply, Handler.withTraceBefore_apply]
+  unfold answerHandler afterWriter
+  rfl
+
+lemma instrumentedHandler_false : instrumentedHandler false =
+    WriterT.mk ((5, ⟨[Event.before false, Event.after false 5]⟩) :
+      Id (Nat × EventLog)) := by
+  unfold instrumentedHandler
+  rw [Handler.postInsert_apply, Handler.withTraceBefore_apply]
+  unfold answerHandler afterWriter
+  rfl
+
+def expectedInstrumentedHandler : Handler (Writer EventLog) Q
+  | true => WriterT.mk ((2, ⟨[Event.before true, Event.after true 2]⟩) :
+      Id (Nat × EventLog))
+  | false => WriterT.mk ((5, ⟨[Event.before false, Event.after false 5]⟩) :
+      Id (Nat × EventLog))
+
+@[simp]
+lemma expectedInstrumentedHandler_true : expectedInstrumentedHandler true =
+    WriterT.mk ((2, ⟨[Event.before true, Event.after true 2]⟩) :
+      Id (Nat × EventLog)) := rfl
+
+@[simp]
+lemma expectedInstrumentedHandler_false : expectedInstrumentedHandler false =
+    WriterT.mk ((5, ⟨[Event.before false, Event.after false 5]⟩) :
+      Id (Nat × EventLog)) := rfl
+
+lemma instrumentedHandler_eq_expected :
+    instrumentedHandler = expectedInstrumentedHandler := by
+  funext operation
+  cases operation
+  · exact instrumentedHandler_false
+  · exact instrumentedHandler_true
+
+/-- Pre- and response-dependent post-events accumulate in execution order.
+The list-backed event monoid is noncommutative, so reversing node or pre/post
+order changes the expected result. -/
+example :
+    Id.run (twoNodeProgram.liftM instrumentedHandler).run =
+      (25, ⟨
+        [Event.before true, Event.after true 2,
+          Event.before false, Event.after false 5]⟩) := by
+  rw [instrumentedHandler_eq_expected]
+  unfold twoNodeProgram
+  change Id.run (FreeM.liftM expectedInstrumentedHandler
+    (FreeM.lift true >>= fun first =>
+      FreeM.lift (first == 5) >>= fun second =>
+        pure (10 * first + second))).run = _
+  rw [FreeM.liftM_lift_bind, expectedInstrumentedHandler_true]
+  simp only [WriterT.run_bind, WriterT.run_mk, Id.run_bind, Id.run_map]
+  simp only [Id.run]
+  have h : (2 == 5) = false := rfl
+  rw [h, FreeM.liftM_lift_bind, expectedInstrumentedHandler_false]
+  simp only [WriterT.run_bind, WriterT.run_mk]
+  simp_rw [FreeM.liftM_pure]
+  rfl
+
+/-! ## Target lifting and universes -/
+
+/-- An option computation lifted into a strictly higher result universe. -/
+abbrev HighOption (alpha : Type) : Type 1 := ULift.{1, 0} (Option alpha)
+
+instance : MonadLift Option HighOption where
+  monadLift computation := ULift.up computation
+
+/-- Positions may live above directions while the target monad is lifted into
+a higher result universe. -/
+@[reducible]
+def UniverseQ : PFunctor.{1, 0} := { A := Type 0, B := fun _ => Nat }
+
+def universeHandler : Handler Option UniverseQ := fun _ => some 7
+
+example : universeHandler.liftTarget Option = universeHandler := by
+  simp
+
+example : (universeHandler.liftTarget HighOption) Nat =
+    ULift.up (some 7) := by
+  change ULift.up (some 7) = ULift.up (some 7)
+  rfl
+
+end PFunctor.Handler.Instrumentation.Tests
diff --git a/docs/wiki/pfunctor.md b/docs/wiki/pfunctor.md
index de6c0d7..313f7e1 100644
--- a/docs/wiki/pfunctor.md
+++ b/docs/wiki/pfunctor.md
@@ -93,6 +93,7 @@ McBride 2010 / Dagand-McBride 2014 (displayed algebras / ornaments).
 | [`PolyFun/PFunctor/Dynamical/CofreeMate/FiniteProjection.lean`](../../PolyFun/PFunctor/Dynamical/CofreeMate/FiniteProjection.lean) | Proposition 8.49 for dynamical systems: composing `cofreeMate` with the depth-`n` cofree projection is exactly `DynSystem.nStep n`; the depth-two corollary agrees with `twoStep` after the inner right unitor. |
 | [`PolyFun/PFunctor/Dynamical/Behavior.lean`](../../PolyFun/PFunctor/Dynamical/Behavior.lean) | Closed-loop behaviour of a Moore machine: `feedbackStep`, `feedbackStream`, `next_iterate_feedback`. |
 | [`PolyFun/PFunctor/Handler.lean`](../../PolyFun/PFunctor/Handler.lean) | `Handler m p`: a monadic choice of direction at every position of `p`; the generic interface consumed by `FreeM.liftM`, with indexed coproduct combination. |
+| [`PolyFun/PFunctor/Handler/Instrumentation.lean`](../../PolyFun/PFunctor/Handler/Instrumentation.lean) | Target-monad lifting, pre- and post-handler effect insertion, and response-independent or response-dependent writer traces. |
 | [`PolyFun/PFunctor/Handler/Free.lean`](../../PolyFun/PFunctor/Handler/Free.lean) | Identity and categorical-order Kleisli composition for handlers valued in `FreeM`. |
 | [`PolyFun/PFunctor/Handler/Stateful.lean`](../../PolyFun/PFunctor/Handler/Stateful.lean) | `Handler.Stateful m S p`, the transparent `Handler (StateT S m) p` effectful Mealy interface; finite-program execution, stateless lifting, and contravariant reindexing by free handlers with identity, composition, and fusion laws. |
 | [`PolyFun/PFunctor/Resumption.lean`](../../PolyFun/PFunctor/Resumption.lean) | `Resumption p β := M (C β + p)`, the canonical possibly infinite tau-free return-or-query behavior; computational-view coinduction via `HeadMatch` / `bisim` / `corec_unique`; universe-polymorphic `map` / `bind` and lawful monad structure; and interface transport by `mapLens` with identity, composition, bind, and map laws. |
diff --git a/docs/wiki/repo-map.md b/docs/wiki/repo-map.md
index 0be98fe..bef981c 100644
--- a/docs/wiki/repo-map.md
+++ b/docs/wiki/repo-map.md
@@ -47,6 +47,7 @@ IPFunctor/Free/{Basic, Indexed} + IPFunctor/Notation/Common
 PFunctor/Display/Basic
   -> PFunctor/Display/{Chart, Coalgebra, Indexed, Free}
 IPFunctor/M + PFunctor/Display/Indexed -> PFunctor/Display/M
+PFunctor/Handler -> PFunctor/Handler/Instrumentation
 PFunctor/{Handler, Free/Basic} -> PFunctor/Handler/Free
   -> PFunctor/Handler/Stateful -> PFunctor/Handler/Normalization/Attr
   -> PFunctor/Handler/Normalization