diff --git a/compiler/cfg.go b/compiler/cfg.go
index 8e8178d7..3191d7e8 100644
--- a/compiler/cfg.go
+++ b/compiler/cfg.go
@@ -376,6 +376,15 @@ func (cfg *CFG) typedStatementEvents(stmt ast.Statement, reads []VarEvent, effec
 		}
 		events = append(events, VarEvent{Name: target.Value, Kind: Read, Token: target.Tok()})
 	}
+	// A callee that reads its seed observes an existing destination. A fresh
+	// destination supplies a zero seed, so there is nothing to read.
+	for _, targetIndex := range effect.CalleeReadsSeed {
+		target := let.Name[targetIndex]
+		if !cfg.isDefined(target.Value) {
+			continue
+		}
+		events = append(events, VarEvent{Name: target.Value, Kind: Read, Token: target.Tok()})
+	}
 	for _, write := range effect.Writes {
 		target := let.Name[write.TargetIndex]
 		var kind EventType
diff --git a/compiler/cfg_test.go b/compiler/cfg_test.go
index bafab129..94027ffb 100644
--- a/compiler/cfg_test.go
+++ b/compiler/cfg_test.go
@@ -142,6 +142,48 @@ func getValidTestCases() []cfgTestCase {
 			name:  "Failable Value Protects Only Its Own Destination",
 			input: "x = 7\na = 10\na, b = x < 5, 30\na, b",
 		},
+		{
+			// The callee always writes, but its value depends on the incoming
+			// seed, so the prior value is read rather than overwritten.
+			name: "Seed Dependent Call Reads Prior Value",
+			code: `res = maybeIncrement(x)
+    res = x > 0 x
+    res = res + 1`,
+			input: "x = 20\nx = maybeIncrement(-1)\nx",
+		},
+		{
+			// The dependency composes through a wrapper whose only statement
+			// forwards the output to a seed-reading callee.
+			name: "Nested Seed Dependent Call Reads Prior Value",
+			code: `res = maybeIncrement(x)
+    res = x > 0 x
+    res = res + 1
+
+res = outer(x)
+    res = maybeIncrement(x)`,
+			input: "x = 20\nx = outer(-1)\nx",
+		},
+		{
+			// Inside a body, the inner call reads the reset value, which keeps
+			// that unconditional write live.
+			name: "Reset Before Seed Dependent Call Inside Body",
+			code: `res = maybeIncrement(x)
+    res = x > 0 x
+    res = res + 1
+
+res = resetThenIncrement(x)
+    res = 0
+    res = maybeIncrement(x)`,
+			input: "x = resetThenIncrement(-1)\nx",
+		},
+		{
+			// An indirect output reads its destination-seeded staging slot.
+			name: "Indirect Seed Dependent Call Reads Prior Value",
+			code: `s = maybeTag(n, t)
+    s = n > 0 t
+    s = s ⊕ "!"`,
+			input: "w = \"hi\"\nw = maybeTag(-1, \"x\")\nw",
+		},
 	}
 }
 
@@ -210,6 +252,51 @@ func getErrorTestCases() []cfgTestCase {
 			input:         "x = 7\nx = alwaysWrite(0:2)\nx",
 			errorContains: `unconditional assignment to "x" overwrites a previous value that was never used`,
 		},
+		{
+			// A definite overwrite before the read removes the seed dependency,
+			// so the prior value really is unused.
+			name: "Overwrite Before Seed Read Still Overwrites Prior Value",
+			code: `res = overwrite(x)
+    res = x
+    res = res + 1`,
+			input:         "x = 7\nx = overwrite(3)\nx",
+			errorContains: `unconditional assignment to "x" overwrites a previous value that was never used`,
+		},
+		{
+			// The nested read observes the reset, never the caller's value.
+			name: "Reset Before Nested Seed Read Overwrites Prior Value",
+			code: `res = maybeIncrement(x)
+    res = x > 0 x
+    res = res + 1
+
+res = resetThenIncrement(x)
+    res = 0
+    res = maybeIncrement(x)`,
+			input:         "x = 7\nx = resetThenIncrement(-1)\nx",
+			errorContains: `unconditional assignment to "x" overwrites a previous value that was never used`,
+		},
+		{
+			// A heap destination cannot seed a static-string output: the
+			// callee's staging slot gets an ABI-typed zero seed, so the
+			// destination's value is never observed and the overwrite is real.
+			name: "Incompatible Storage Seed Does Not Reach Callee",
+			code: `s = readStatic(n)
+    s = n > 0 "x"
+    "seen <-s>"
+    s = "done"`,
+			input:         "value = \"never\" ⊕ \"read\"\nvalue = readStatic(0)\nvalue",
+			errorContains: `unconditional assignment to "value" overwrites a previous value that was never used`,
+		},
+		{
+			// A fresh destination supplies a zero seed; the callee's read does
+			// not make the result used.
+			name: "Fresh Seed Dependent Result Is Unused",
+			code: `res = maybeIncrement(x)
+    res = x > 0 x
+    res = res + 1`,
+			input:         "x = maybeIncrement(-1)",
+			errorContains: `value assigned to "x" is never used`,
+		},
 		{
 			// A || yields whenever its final fallback does, so the resolver
 			// boundary holds and this write is unconditional.
diff --git a/compiler/effects.go b/compiler/effects.go
index fad03c9f..6b0cdc77 100644
--- a/compiler/effects.go
+++ b/compiler/effects.go
@@ -60,6 +60,35 @@ func (effect YieldEffect) String() string {
 	}
 }
 
+// SeedEffect describes whether a scalar body can observe one output's
+// incoming value before that output is definitely replaced. It is independent
+// of WriteEffect: an unconditional computed update reads its seed, while a
+// conditional write may leave preservation entirely to the caller. Uncomputed
+// and Invalid are publication states, not lattice members.
+type SeedEffect uint8
+
+const (
+	SeedUncomputed SeedEffect = iota
+	SeedInvalid
+	NoSeedRead
+	MaySeedRead
+)
+
+func (effect SeedEffect) String() string {
+	switch effect {
+	case SeedUncomputed:
+		return "Uncomputed"
+	case SeedInvalid:
+		return "Invalid"
+	case NoSeedRead:
+		return "NoSeedRead"
+	case MaySeedRead:
+		return "MaySeedRead"
+	default:
+		return fmt.Sprintf("SeedEffect(%d)", effect)
+	}
+}
+
 // TargetWriteEffect is one entry in a sparse, position-preserving target
 // vector. Discard targets have no entry; TargetIndex keeps later entries tied
 // to their original LHS slots.
@@ -69,11 +98,23 @@ type TargetWriteEffect struct {
 }
 
 // StatementEffect contains the target facts derived for one assignment.
-// ReadsSeed holds LHS indices whose existing value is consumed by a direct
-// MayWrite callee output at the assignment boundary.
+// ReadsSeed holds LHS indices whose existing value resolves a direct MayWrite
+// callee output at the assignment boundary; such a write preserves a value
+// rather than producing one. CalleeReadsSeed holds LHS indices whose value the
+// callee body itself may read before definitely replacing it, whatever the
+// write effect: the callee may read its seed and the destination's storage
+// lets that seed reach it. A fresh destination still supplies a zero seed, so
+// consumers decide whether an existing value is involved.
 type StatementEffect struct {
-	Writes    []TargetWriteEffect
-	ReadsSeed []int
+	Writes          []TargetWriteEffect
+	ReadsSeed       []int
+	CalleeReadsSeed []int
+}
+
+// replacesTarget reports whether the statement definitely stores a value the
+// body produced: a MustWrite not manufactured by reading the destination seed.
+func (effect StatementEffect) replacesTarget(write TargetWriteEffect) bool {
+	return write.Effect == MustWrite && !slices.Contains(effect.ReadsSeed, write.TargetIndex)
 }
 
 func validPublishedEffects(effects []WriteEffect, count int) bool {
@@ -90,6 +131,20 @@ func validPublishedEffects(effects []WriteEffect, count int) bool {
 	return true
 }
 
+func validPublishedSeedEffects(effects []SeedEffect, count int) bool {
+	if len(effects) != count {
+		return false
+	}
+
+	for _, effect := range effects {
+		if effect != NoSeedRead && effect != MaySeedRead {
+			return false
+		}
+	}
+
+	return true
+}
+
 func joinYield(left, right YieldEffect) YieldEffect {
 	if left == YieldInvalid || right == YieldInvalid {
 		return YieldInvalid
@@ -117,14 +172,22 @@ func classifyWriteEffect(yield YieldEffect, maySkip bool) WriteEffect {
 	return MustWrite
 }
 
+// bodyEffects pairs the write and seed facts of one specialization's outputs:
+// the published summary of a settled callee, or the provisional working
+// values of a component still being settled.
+type bodyEffects struct {
+	writes []WriteEffect
+	seeds  []SeedEffect
+}
+
 type effectAnalyzer struct {
 	compiler        *Compiler
 	funcNameMangled string
 	graph           *specializationCallGraph
-	working         [][]WriteEffect
+	working         []bodyEffects
 }
 
-func newEffectAnalyzer(compiler *Compiler, mangled string, graph *specializationCallGraph, working [][]WriteEffect) *effectAnalyzer {
+func newEffectAnalyzer(compiler *Compiler, mangled string, graph *specializationCallGraph, working []bodyEffects) *effectAnalyzer {
 	return &effectAnalyzer{
 		compiler:        compiler,
 		funcNameMangled: mangled,
@@ -263,7 +326,7 @@ func (analyzer *effectAnalyzer) deriveCall(expr *ast.CallExpression) []YieldEffe
 		invocation = joinYield(invocation, MayYield)
 	}
 
-	callee := analyzer.callBodyOutputEffects(expr)
+	callee := analyzer.callBodyEffects(expr).writes
 	if len(callee) != len(info.OutTypes) {
 		panic(fmt.Sprintf("internal: call %s has %d output effects for %d typed outputs", expr.Function.Value, len(callee), len(info.OutTypes)))
 	}
@@ -284,12 +347,12 @@ func (analyzer *effectAnalyzer) deriveCall(expr *ast.CallExpression) []YieldEffe
 	return info.YieldEffects
 }
 
-func (analyzer *effectAnalyzer) callBodyOutputEffects(expr *ast.CallExpression) []WriteEffect {
+func (analyzer *effectAnalyzer) callBodyEffects(expr *ast.CallExpression) bodyEffects {
 	info := analyzer.exprInfo(expr)
 	mangled := Mangle(analyzer.compiler.MangledPath, expr.Function.Value, info.CallParamTypes)
 	f := analyzer.compiler.FuncCache[mangled]
 	if f.Settled {
-		return f.BodyOutputEffects
+		return bodyEffects{writes: f.BodyOutputEffects, seeds: f.BodySeedEffects}
 	}
 
 	if analyzer.graph == nil {
@@ -373,7 +436,7 @@ func (analyzer *effectAnalyzer) seedResolvedYield(expr ast.Expression, slot int,
 		return YieldUncomputed, false
 	}
 
-	callee := analyzer.callBodyOutputEffects(call)
+	callee := analyzer.callBodyEffects(call).writes
 	needsSeed := callee[slot] == MayWrite || analyzer.callOwnsPossiblyEmptyDomain(call, conditionRanges)
 	if !needsSeed {
 		return YieldUncomputed, false
@@ -400,6 +463,47 @@ func (analyzer *effectAnalyzer) callOwnsPossiblyEmptyDomain(call *ast.CallExpres
 	return false
 }
 
+// calleeReadsSeed reports whether a resolved call's callee may read the
+// destination of one output slot. Only a call reads a destination, and an
+// unpublished seed fact is an ICE: unknown analysis must not mean no seed
+// reads. The read composes only when the seed reaches the callee. Lowering
+// seeds an indirect output's staging slot from the destination only when the
+// two storage types are identical (makeCallOutputAdapters); a mismatched
+// flavor gets an ABI-typed zero seed, so the callee never observes the
+// destination's value. A direct scalar return always matches its destination.
+func (analyzer *effectAnalyzer) calleeReadsSeed(expr ast.Expression, slot int, target string) bool {
+	call, ok := expr.(*ast.CallExpression)
+	if !ok {
+		return false
+	}
+
+	info := analyzer.exprInfo(call)
+	if !typesResolved(info.OutTypes) {
+		return false
+	}
+
+	seeds := analyzer.callBodyEffects(call).seeds
+	if !validPublishedSeedEffects(seeds, len(info.OutTypes)) {
+		panic(fmt.Sprintf("internal: call %s has unpublished seed effects %v", call.Function.Value, seeds))
+	}
+	if seeds[slot] != MaySeedRead {
+		return false
+	}
+
+	return TypeEqual(analyzer.bindingSlotType(target), info.OutTypes[slot])
+}
+
+// bindingSlotType returns the solver's slot type for a named target, the
+// same authority lowering's destSlotType consults for an assignment.
+func (analyzer *effectAnalyzer) bindingSlotType(name string) Type {
+	slotType, recorded := analyzer.compiler.FuncCache[analyzer.funcNameMangled].Vars[name]
+	if !recorded {
+		panic(fmt.Sprintf("internal: target %s of %s has no recorded slot type", name, analyzer.funcNameMangled))
+	}
+
+	return slotType
+}
+
 func (analyzer *effectAnalyzer) deriveStatements(statements []ast.Statement, initiallyDefined map[string]struct{}) map[*ast.LetStatement]StatementEffect {
 	defined := make(map[string]struct{}, len(initiallyDefined))
 
@@ -455,6 +559,9 @@ func (analyzer *effectAnalyzer) deriveLet(stmt *ast.LetStatement, defined map[st
 				result.ReadsSeed = append(result.ReadsSeed, index)
 				yield = seededYield
 			}
+			if analyzer.calleeReadsSeed(expr, slot, target.Value) {
+				result.CalleeReadsSeed = append(result.CalleeReadsSeed, index)
+			}
 			result.Writes = append(result.Writes, TargetWriteEffect{
 				TargetIndex: index,
 				Effect:      classifyWriteEffect(yield, maySkip),
@@ -486,8 +593,13 @@ func validStatementEffect(stmt *ast.LetStatement, effect StatementEffect) bool {
 		return false
 	}
 
+	return validSeedTargets(stmt, effect.ReadsSeed) && validSeedTargets(stmt, effect.CalleeReadsSeed)
+}
+
+// validSeedTargets requires ascending, unique, named LHS indices.
+func validSeedTargets(stmt *ast.LetStatement, targets []int) bool {
 	lastTarget := -1
-	for _, targetIndex := range effect.ReadsSeed {
+	for _, targetIndex := range targets {
 		if targetIndex <= lastTarget || targetIndex >= len(stmt.Name) {
 			return false
 		}
@@ -501,19 +613,20 @@ func validStatementEffect(stmt *ast.LetStatement, effect StatementEffect) bool {
 	return true
 }
 
-func deriveBodyOutputEffects(template *ast.FuncStatement, statements map[*ast.LetStatement]StatementEffect) []WriteEffect {
-	effects := make([]WriteEffect, len(template.Outputs))
-
-	for i := range effects {
-		effects[i] = MayWrite
-	}
-
+func outputIndices(template *ast.FuncStatement) map[string]int {
 	outputIndex := make(map[string]int, len(template.Outputs))
 
 	for i, output := range template.Outputs {
 		outputIndex[output.Value] = i
 	}
 
+	return outputIndex
+}
+
+func deriveBodyOutputEffects(template *ast.FuncStatement, statements map[*ast.LetStatement]StatementEffect) []WriteEffect {
+	effects := slices.Repeat([]WriteEffect{MayWrite}, len(template.Outputs))
+	outputIndex := outputIndices(template)
+
 	for _, statement := range template.Body.Statements {
 		stmt, ok := statement.(*ast.LetStatement)
 		if !ok {
@@ -526,7 +639,7 @@ func deriveBodyOutputEffects(template *ast.FuncStatement, statements map[*ast.Le
 		}
 
 		for _, write := range statementEffect.Writes {
-			if write.Effect != MustWrite || slices.Contains(statementEffect.ReadsSeed, write.TargetIndex) {
+			if !statementEffect.replacesTarget(write) {
 				continue
 			}
 			index, isOutput := outputIndex[stmt.Name[write.TargetIndex].Value]
@@ -539,6 +652,142 @@ func deriveBodyOutputEffects(template *ast.FuncStatement, statements map[*ast.Le
 	return effects
 }
 
+// seedFold walks one body in statement order and records which outputs are
+// read while they may still hold their incoming value. Reads precede writes
+// within a statement, and a recorded read is permanent: a seed copied to a
+// local before the output is replaced still reaches the body's results.
+type seedFold struct {
+	outputIndex map[string]int
+	replaced    []bool
+	effects     []SeedEffect
+	defined     map[string]struct{}
+	isGlobal    func(string) bool
+}
+
+func newSeedFold(template *ast.FuncStatement, isGlobal func(string) bool) *seedFold {
+	fold := &seedFold{
+		outputIndex: outputIndices(template),
+		replaced:    make([]bool, len(template.Outputs)),
+		effects:     slices.Repeat([]SeedEffect{NoSeedRead}, len(template.Outputs)),
+		defined:     functionInitialBindings(template),
+		isGlobal:    isGlobal,
+	}
+
+	// Outputs are bound to their seeds before the body runs, so a marker
+	// naming one resolves like the solver and lowering resolve it.
+	for _, output := range template.Outputs {
+		fold.defined[output.Value] = struct{}{}
+	}
+
+	return fold
+}
+
+func (fold *seedFold) isDefined(name string) bool {
+	if _, exists := fold.defined[name]; exists {
+		return true
+	}
+
+	return fold.isGlobal(name)
+}
+
+func (fold *seedFold) read(name string) {
+	index, isOutput := fold.outputIndex[name]
+	if isOutput && !fold.replaced[index] {
+		fold.effects[index] = MaySeedRead
+	}
+}
+
+func (fold *seedFold) replace(name string) {
+	if index, isOutput := fold.outputIndex[name]; isOutput {
+		fold.replaced[index] = true
+	}
+}
+
+func (fold *seedFold) foldStatement(stmt *ast.LetStatement, effect StatementEffect) {
+	for _, targetIndex := range effect.CalleeReadsSeed {
+		fold.read(stmt.Name[targetIndex].Value)
+	}
+
+	for _, write := range effect.Writes {
+		if effect.replacesTarget(write) {
+			fold.replace(stmt.Name[write.TargetIndex].Value)
+		}
+	}
+
+	for _, target := range stmt.Name {
+		if !isDiscard(target) {
+			fold.defined[target.Value] = struct{}{}
+		}
+	}
+}
+
+// deriveBodySeedEffects summarizes, per output, whether the scalar body may
+// read that output's incoming value. Explicit reads come from conditions,
+// values, print arguments, and resolved formatting markers; implicit reads
+// come from callees that read their own seed. A boundary-resolved write only
+// preserves the seed, so it does not replace the output.
+func deriveBodySeedEffects(template *ast.FuncStatement, statements map[*ast.LetStatement]StatementEffect, isGlobal func(string) bool) []SeedEffect {
+	fold := newSeedFold(template, isGlobal)
+
+	for _, statement := range template.Body.Statements {
+		for _, name := range statementReadNames(statement, fold.isDefined) {
+			fold.read(name)
+		}
+
+		stmt, ok := statement.(*ast.LetStatement)
+		if !ok {
+			continue
+		}
+
+		effect, exists := statements[stmt]
+		if !exists || !validStatementEffect(stmt, effect) {
+			return slices.Repeat([]SeedEffect{SeedInvalid}, len(template.Outputs))
+		}
+		fold.foldStatement(stmt, effect)
+	}
+
+	return fold.effects
+}
+
+// statementReadNames returns every identifier a statement reads in source
+// order, including resolved formatting markers and their dynamic width and
+// precision operands.
+func statementReadNames(statement ast.Statement, isDefined func(string) bool) []string {
+	var names []string
+
+	switch stmt := statement.(type) {
+	case *ast.LetStatement:
+		for _, condition := range stmt.Condition {
+			names = appendExprReadNames(names, condition, isDefined)
+		}
+		for _, value := range stmt.Value {
+			names = appendExprReadNames(names, value, isDefined)
+		}
+	case *ast.PrintStatement:
+		for _, argument := range stmt.Expression.Arguments {
+			names = appendExprReadNames(names, argument, isDefined)
+		}
+	}
+
+	return names
+}
+
+func appendExprReadNames(names []string, expr ast.Expression, isDefined func(string) bool) []string {
+	switch e := expr.(type) {
+	case *ast.Identifier:
+		return append(names, e.Value)
+	case *ast.StringLiteral:
+		mains, specs := formatMarkerIdentifiers(e.Token.Literal, isDefined)
+		return append(append(names, mains...), specs...)
+	}
+
+	for _, child := range ast.ExprChildren(expr) {
+		names = appendExprReadNames(names, child, isDefined)
+	}
+
+	return names
+}
+
 type specializationNodeID int
 
 type specializationNode struct {
@@ -755,23 +1004,31 @@ func (state *tarjanState) visit(id specializationNodeID) {
 }
 
 // deriveEffectNode refreshes one specialization and reports whether any output
-// weakened from MustWrite to MayWrite.
-func (ts *TypeSolver) deriveEffectNode(graph *specializationCallGraph, working [][]WriteEffect, id specializationNodeID) bool {
+// weakened from MustWrite to MayWrite or grew from NoSeedRead to MaySeedRead.
+// Both directions are conservative, and either one must requeue callers.
+func (ts *TypeSolver) deriveEffectNode(graph *specializationCallGraph, working []bodyEffects, id specializationNodeID) bool {
 	node := &graph.nodes[id]
 	walked := ts.walkedFuncs[node.mangled]
 	initial := functionInitialBindings(walked.template)
-	analyzer := newEffectAnalyzer(ts.ScriptCompiler.Compiler, node.mangled, graph, working)
+	compiler := ts.ScriptCompiler.Compiler
+	analyzer := newEffectAnalyzer(compiler, node.mangled, graph, working)
 	statements := analyzer.deriveStatements(walked.template.Body.Statements, initial)
-	derived := deriveBodyOutputEffects(walked.template, statements)
+	writes := deriveBodyOutputEffects(walked.template, statements)
+	seeds := deriveBodySeedEffects(walked.template, statements, compiler.CodeCompiler.isGlobalBinding)
 
-	if !validPublishedEffects(derived, len(walked.info.Sig.OutTypes)) {
+	outputs := len(walked.info.Sig.OutTypes)
+	if !validPublishedEffects(writes, outputs) || !validPublishedSeedEffects(seeds, outputs) {
 		panic(fmt.Sprintf("internal: invalid effects for specialization %s", node.mangled))
 	}
 
 	changed := false
-	for outputIndex, effect := range derived {
-		if working[id][outputIndex] == MustWrite && effect == MayWrite {
-			working[id][outputIndex] = MayWrite
+	for outputIndex := range outputs {
+		if working[id].writes[outputIndex] == MustWrite && writes[outputIndex] == MayWrite {
+			working[id].writes[outputIndex] = MayWrite
+			changed = true
+		}
+		if working[id].seeds[outputIndex] == NoSeedRead && seeds[outputIndex] == MaySeedRead {
+			working[id].seeds[outputIndex] = MaySeedRead
 			changed = true
 		}
 	}
@@ -795,9 +1052,10 @@ func enqueueRecursiveEffectCallers(graph *specializationCallGraph, id specializa
 	return pending
 }
 
-// settleEffectComponent weakens one SCC to a fixed point and publishes all
-// members only after their shared worklist drains.
-func (ts *TypeSolver) settleEffectComponent(graph *specializationCallGraph, working [][]WriteEffect, component []specializationNodeID, queued []bool) {
+// settleEffectComponent drives one SCC to a fixed point and publishes all
+// members' write and seed facts together, only after their shared worklist
+// drains.
+func (ts *TypeSolver) settleEffectComponent(graph *specializationCallGraph, working []bodyEffects, component []specializationNodeID, queued []bool) {
 	pending := slices.Clone(component)
 
 	for _, id := range pending {
@@ -813,17 +1071,21 @@ func (ts *TypeSolver) settleEffectComponent(graph *specializationCallGraph, work
 	}
 
 	for _, id := range component {
-		node := &graph.nodes[id]
-		ts.walkedFuncs[node.mangled].info.BodyOutputEffects = slices.Clone(working[id])
+		info := ts.walkedFuncs[graph.nodes[id].mangled].info
+		info.BodyOutputEffects = slices.Clone(working[id].writes)
+		info.BodySeedEffects = slices.Clone(working[id].seeds)
 	}
 }
 
 func (ts *TypeSolver) settleEffects(graph *specializationCallGraph) {
-	working := make([][]WriteEffect, len(graph.nodes))
+	working := make([]bodyEffects, len(graph.nodes))
 
 	for id := range graph.nodes {
-		walked := ts.walkedFuncs[graph.nodes[id].mangled]
-		working[id] = slices.Repeat([]WriteEffect{MustWrite}, len(walked.info.Sig.OutTypes))
+		outputs := len(ts.walkedFuncs[graph.nodes[id].mangled].info.Sig.OutTypes)
+		working[id] = bodyEffects{
+			writes: slices.Repeat([]WriteEffect{MustWrite}, outputs),
+			seeds:  slices.Repeat([]SeedEffect{NoSeedRead}, outputs),
+		}
 	}
 
 	components := graph.calleeFirstComponents()
diff --git a/compiler/effects_test.go b/compiler/effects_test.go
index ef0b8862..c8ce62c8 100644
--- a/compiler/effects_test.go
+++ b/compiler/effects_test.go
@@ -28,24 +28,30 @@ func TestValidStatementEffectShape(t *testing.T) {
 		{TargetIndex: 2, Effect: MayWrite},
 	}
 	tests := []struct {
-		name      string
-		writes    []TargetWriteEffect
-		readsSeed []int
-		valid     bool
+		name            string
+		writes          []TargetWriteEffect
+		readsSeed       []int
+		calleeReadsSeed []int
+		valid           bool
 	}{
 		{name: "valid direct writes", writes: directWrites, valid: true},
 		{name: "valid mixed write effects", writes: mixedWrites, valid: true},
 		{name: "valid seed targets", writes: directWrites, readsSeed: []int{0, 2}, valid: true},
+		{name: "valid callee seed targets", writes: mixedWrites, calleeReadsSeed: []int{0, 2}, valid: true},
+		{name: "valid overlapping seed facts", writes: directWrites, readsSeed: []int{0}, calleeReadsSeed: []int{0}, valid: true},
 		{name: "missing named target", writes: directWrites[:1]},
 		{name: "write targets discard", writes: []TargetWriteEffect{{TargetIndex: 0, Effect: MustWrite}, {TargetIndex: 1, Effect: MustWrite}}},
 		{name: "invalid write state", writes: []TargetWriteEffect{{TargetIndex: 0, Effect: MustWrite}, {TargetIndex: 2, Effect: WriteInvalid}}},
 		{name: "duplicate seed target", writes: directWrites, readsSeed: []int{0, 0}},
 		{name: "seed targets discard", writes: directWrites, readsSeed: []int{1}},
+		{name: "descending callee seed targets", writes: directWrites, calleeReadsSeed: []int{2, 0}},
+		{name: "callee seed targets discard", writes: directWrites, calleeReadsSeed: []int{1}},
+		{name: "callee seed target out of range", writes: directWrites, calleeReadsSeed: []int{3}},
 	}
 
 	for _, test := range tests {
 		t.Run(test.name, func(t *testing.T) {
-			effect := StatementEffect{Writes: test.writes, ReadsSeed: test.readsSeed}
+			effect := StatementEffect{Writes: test.writes, ReadsSeed: test.readsSeed, CalleeReadsSeed: test.calleeReadsSeed}
 
 			require.Equal(t, test.valid, validStatementEffect(stmt, effect))
 		})
@@ -194,6 +200,7 @@ seeded, always, failed, gated`)
 	seededEffect := ts.ScriptCompiler.Script.Root.StatementEffects[seeded]
 	requireTargetEffects(t, seededEffect, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
 	require.Equal(t, []int{0}, seededEffect.ReadsSeed)
+	require.Empty(t, seededEffect.CalleeReadsSeed)
 	require.Equal(t, []YieldEffect{MayYield}, ts.ExprCache[key(ts.FuncNameMangled, seeded.Value[0])].YieldEffects)
 
 	freshEffect := ts.ScriptCompiler.Script.Root.StatementEffects[fresh]
@@ -217,6 +224,10 @@ seeded, always, failed, gated`)
 
 	require.Equal(t, []WriteEffect{MayWrite}, maybeFunc.BodyOutputEffects)
 	require.Equal(t, []WriteEffect{MustWrite}, alwaysFunc.BodyOutputEffects)
+	// Skipping a write leaves preservation to the caller; neither body reads
+	// its incoming value.
+	require.Equal(t, []SeedEffect{NoSeedRead}, maybeFunc.BodySeedEffects)
+	require.Equal(t, []SeedEffect{NoSeedRead}, alwaysFunc.BodySeedEffects)
 	require.True(t, maybeFunc.Settled)
 	require.True(t, alwaysFunc.Settled)
 }
@@ -242,6 +253,9 @@ fresh, existing`)
 
 	require.NotNil(t, wrap)
 	require.Equal(t, []WriteEffect{MayWrite}, wrap.BodyOutputEffects)
+	// The inner boundary resolution only passes the seed through; nothing in
+	// the body consumes it.
+	require.Equal(t, []SeedEffect{NoSeedRead}, wrap.BodySeedEffects)
 
 	template, ok := cc.lookupFuncTemplate("Wrap", 1)
 	require.True(t, ok)
@@ -249,11 +263,13 @@ fresh, existing`)
 	firstBodyEffect := wrap.StatementEffects[firstBodyStmt]
 	requireTargetEffects(t, firstBodyEffect, TargetWriteEffect{TargetIndex: 0, Effect: MayWrite})
 	require.Empty(t, firstBodyEffect.ReadsSeed)
+	require.Empty(t, firstBodyEffect.CalleeReadsSeed)
 
 	secondBodyStmt := template.Body.Statements[1].(*ast.LetStatement)
 	secondBodyEffect := wrap.StatementEffects[secondBodyStmt]
 	requireTargetEffects(t, secondBodyEffect, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
 	require.Equal(t, []int{0}, secondBodyEffect.ReadsSeed)
+	require.Empty(t, secondBodyEffect.CalleeReadsSeed)
 
 	fresh := ts.ScriptCompiler.Program.Statements[0].(*ast.LetStatement)
 	freshEffect := ts.ScriptCompiler.Script.Root.StatementEffects[fresh]
@@ -517,3 +533,324 @@ value`)
 
 	require.Equal(t, []YieldEffect{YieldInvalid}, analyzer.deriveExpr(call))
 }
+
+// requireBodyEffects checks the published write and seed facts of every
+// settled specialization named name; a ranged call also settles the scalar
+// companion, and both summarize the same body.
+func requireBodyEffects(t *testing.T, cc *CodeCompiler, name string, writes []WriteEffect, seeds []SeedEffect) {
+	t.Helper()
+
+	found := 0
+	for mangled, f := range cc.Compiler.FuncCache {
+		if f.Sig.Name != name {
+			continue
+		}
+		found++
+		require.True(t, f.Settled, mangled)
+		require.Equal(t, writes, f.BodyOutputEffects, mangled)
+		require.Equal(t, seeds, f.BodySeedEffects, mangled)
+	}
+	require.NotZero(t, found, "missing specialization of %s", name)
+}
+
+func scriptStatementEffect(t *testing.T, ts *TypeSolver, index int) StatementEffect {
+	t.Helper()
+
+	stmt := ts.ScriptCompiler.Program.Statements[index].(*ast.LetStatement)
+	effect, exists := ts.ScriptCompiler.Script.Root.StatementEffects[stmt]
+	require.True(t, exists)
+	return effect
+}
+
+func bodyStatementEffect(t *testing.T, cc *CodeCompiler, name string, index int) StatementEffect {
+	t.Helper()
+
+	template, ok := cc.lookupFuncTemplate(name, 1)
+	require.True(t, ok)
+	stmt := template.Body.Statements[index].(*ast.LetStatement)
+
+	for _, f := range cc.Compiler.FuncCache {
+		if f.Sig.Name != name {
+			continue
+		}
+		effect, exists := f.StatementEffects[stmt]
+		require.True(t, exists)
+		return effect
+	}
+
+	require.Fail(t, "missing specialization", name)
+	return StatementEffect{}
+}
+
+func TestSeedDependentMustWriteReadsDestination(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, "seedDependentEffects", "", mustParseCode(t, `y = MaybeIncrement(x)
+    y = x > 0 x
+    y = y + 1
+
+y = Overwrite(x)
+    y = x
+    y = y + 1`))
+	require.Empty(t, cc.Compile())
+
+	ts := solveScriptTypes(t, ctx, cc, t.Name(), `seeded = 20
+seeded = MaybeIncrement(-1)
+fresh = MaybeIncrement(-1)
+replaced = 7
+replaced = Overwrite(3)
+seeded, fresh, replaced`)
+
+	// The write effect is the same; only the seed dependency differs.
+	requireBodyEffects(t, cc, "MaybeIncrement", []WriteEffect{MustWrite}, []SeedEffect{MaySeedRead})
+	requireBodyEffects(t, cc, "Overwrite", []WriteEffect{MustWrite}, []SeedEffect{NoSeedRead})
+
+	seeded := scriptStatementEffect(t, ts, 1)
+	requireTargetEffects(t, seeded, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, seeded.ReadsSeed)
+	require.Equal(t, []int{0}, seeded.CalleeReadsSeed)
+
+	// The fact describes the callee; a fresh destination has no value for the
+	// CFG to read.
+	fresh := scriptStatementEffect(t, ts, 2)
+	requireTargetEffects(t, fresh, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, fresh.ReadsSeed)
+	require.Equal(t, []int{0}, fresh.CalleeReadsSeed)
+
+	replaced := scriptStatementEffect(t, ts, 4)
+	requireTargetEffects(t, replaced, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, replaced.ReadsSeed)
+	require.Empty(t, replaced.CalleeReadsSeed)
+}
+
+func TestSeedReadSurvivesCopyConditionAndPrint(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, "stickySeedEffects", "", mustParseCode(t, `y = CopyThenReplace(x)
+    y = x > 0 x
+    saved = y
+    y = x
+    y = y + saved
+
+y = GatedRead(x)
+    y = x > 0 x
+    y = y > 0 x
+    y = x
+
+y = PrintedRead(x)
+    y = x > 0 x
+    y
+    y = x
+
+y = MarkerRead(x)
+    y = x > 0 x
+    "seed -y"
+    y = x
+
+y = WidthRead(x)
+    y = x > 0 x
+    "-x%(-y)d"
+    y = x`))
+	require.Empty(t, cc.Compile())
+
+	solveScriptTypes(t, ctx, cc, t.Name(), `a = CopyThenReplace(1)
+b = GatedRead(1)
+c = PrintedRead(1)
+d = MarkerRead(1)
+e = WidthRead(1)
+a, b, c, d, e`)
+
+	for _, name := range []string{"CopyThenReplace", "GatedRead", "PrintedRead", "MarkerRead", "WidthRead"} {
+		requireBodyEffects(t, cc, name, []WriteEffect{MustWrite}, []SeedEffect{MaySeedRead})
+	}
+}
+
+func TestNestedSeedReadsCompose(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, "nestedSeedEffects", "", mustParseCode(t, `y = MaybeIncrement(x)
+    y = x > 0 x
+    y = y + 1
+
+y = Outer(x)
+    y = MaybeIncrement(x)
+
+y = ResetThenIncrement(x)
+    y = 0
+    y = MaybeIncrement(x)`))
+	require.Empty(t, cc.Compile())
+
+	solveScriptTypes(t, ctx, cc, t.Name(), `a = Outer(1)
+b = ResetThenIncrement(1)
+a, b`)
+
+	requireBodyEffects(t, cc, "Outer", []WriteEffect{MustWrite}, []SeedEffect{MaySeedRead})
+	requireBodyEffects(t, cc, "ResetThenIncrement", []WriteEffect{MustWrite}, []SeedEffect{NoSeedRead})
+
+	// The output is unpublished at its first statement, so the callee's read
+	// is recorded without a boundary resolution.
+	outerCall := bodyStatementEffect(t, cc, "Outer", 0)
+	requireTargetEffects(t, outerCall, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, outerCall.ReadsSeed)
+	require.Equal(t, []int{0}, outerCall.CalleeReadsSeed)
+
+	// The inner call reads the reset value, which keeps that write live.
+	resetCall := bodyStatementEffect(t, cc, "ResetThenIncrement", 1)
+	requireTargetEffects(t, resetCall, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, resetCall.ReadsSeed)
+	require.Equal(t, []int{0}, resetCall.CalleeReadsSeed)
+}
+
+func TestCrossOutputSeedReads(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, "crossOutputSeedEffects", "", mustParseCode(t, `a, b = Cross(x)
+    a = x > 0 x
+    b = a + 1
+    a = x`))
+	require.Empty(t, cc.Compile())
+
+	ts := solveScriptTypes(t, ctx, cc, t.Name(), `p = 20
+p, q = Cross(-1)
+p, q`)
+
+	requireBodyEffects(t, cc, "Cross", []WriteEffect{MustWrite, MustWrite}, []SeedEffect{MaySeedRead, NoSeedRead})
+
+	call := scriptStatementEffect(t, ts, 1)
+	requireTargetEffects(t, call,
+		TargetWriteEffect{TargetIndex: 0, Effect: MustWrite},
+		TargetWriteEffect{TargetIndex: 1, Effect: MustWrite},
+	)
+	require.Empty(t, call.ReadsSeed)
+	require.Equal(t, []int{0}, call.CalleeReadsSeed)
+}
+
+func TestRecursiveSeedReadsConvergeAcrossSCC(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	// A reads its seed only through B, so the fact must grow across the
+	// component after B's own read is discovered.
+	cc := NewCodeCompiler(ctx, "recursiveSeedEffects", "", mustParseCode(t, `y = A(n)
+    y = B(n)
+
+y = B(n)
+    y = n == 0 1
+    y = n > 0 A(n - 1)
+    y = y + 1`))
+	require.Empty(t, cc.Compile())
+
+	solveScriptTypes(t, ctx, cc, t.Name(), `result = A(2)
+result`)
+
+	requireBodyEffects(t, cc, "A", []WriteEffect{MustWrite}, []SeedEffect{MaySeedRead})
+	requireBodyEffects(t, cc, "B", []WriteEffect{MustWrite}, []SeedEffect{MaySeedRead})
+}
+
+func TestIndirectCalleeSeedReadsCompose(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, "indirectSeedEffects", "", mustParseCode(t, `s = MaybeTag(n, t)
+    s = n > 0 t
+    s = s ⊕ "!"
+
+s = GatedTag(n, t)
+    s = n > 0 t
+    s = n > 1 s ⊕ "!"`))
+	require.Empty(t, cc.Compile())
+
+	ts := solveScriptTypes(t, ctx, cc, t.Name(), `w = "hi"
+w = MaybeTag(-1, "x")
+v = "hi"
+v = GatedTag(-1, "x")
+w, v`)
+
+	requireBodyEffects(t, cc, "MaybeTag", []WriteEffect{MustWrite}, []SeedEffect{MaySeedRead})
+	requireBodyEffects(t, cc, "GatedTag", []WriteEffect{MayWrite}, []SeedEffect{MaySeedRead})
+
+	// Indirect outputs never resolve at the boundary, but the dependency on
+	// the destination-seeded staging slot composes all the same.
+	mustWrite := scriptStatementEffect(t, ts, 1)
+	requireTargetEffects(t, mustWrite, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, mustWrite.ReadsSeed)
+	require.Equal(t, []int{0}, mustWrite.CalleeReadsSeed)
+
+	mayWrite := scriptStatementEffect(t, ts, 3)
+	requireTargetEffects(t, mayWrite, TargetWriteEffect{TargetIndex: 0, Effect: MayWrite})
+	require.Empty(t, mayWrite.ReadsSeed)
+	require.Equal(t, []int{0}, mayWrite.CalleeReadsSeed)
+}
+
+func TestFunctionDomainSeedReadsKeepBoundaryFacts(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, "domainSeedEffects", "", mustParseCode(t, `y = AccRange(r)
+    y = r > 5 r
+    y = y + r`))
+	require.Empty(t, cc.Compile())
+
+	ts := solveScriptTypes(t, ctx, cc, t.Name(), `existing = 20
+existing = AccRange(0:3)
+empty = 20
+empty = AccRange(0:0)
+fresh = AccRange(0:3)
+existing, empty, fresh`)
+
+	requireBodyEffects(t, cc, "AccRange", []WriteEffect{MustWrite}, []SeedEffect{MaySeedRead})
+
+	existing := scriptStatementEffect(t, ts, 1)
+	requireTargetEffects(t, existing, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, existing.ReadsSeed)
+	require.Equal(t, []int{0}, existing.CalleeReadsSeed)
+
+	// A possibly empty call-owned domain still resolves at the boundary; the
+	// two facts coexist on one target.
+	empty := scriptStatementEffect(t, ts, 3)
+	requireTargetEffects(t, empty, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Equal(t, []int{0}, empty.ReadsSeed)
+	require.Equal(t, []int{0}, empty.CalleeReadsSeed)
+
+	fresh := scriptStatementEffect(t, ts, 4)
+	requireTargetEffects(t, fresh, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, fresh.ReadsSeed)
+	require.Equal(t, []int{0}, fresh.CalleeReadsSeed)
+}
+
+func TestCalleeSeedReadRequiresCompatibleStorage(t *testing.T) {
+	ctx := llvm.NewContext()
+	defer ctx.Dispose()
+
+	cc := NewCodeCompiler(ctx, "storageSeedEffects", "", mustParseCode(t, `s = ReadStatic(n)
+    s = n > 0 "x"
+    "seen <-s>"
+    s = "done"`))
+	require.Empty(t, cc.Compile())
+
+	ts := solveScriptTypes(t, ctx, cc, t.Name(), `static = "hi"
+static = ReadStatic(0)
+heap = "never" ⊕ "read"
+heap = ReadStatic(0)
+static, heap`)
+
+	requireBodyEffects(t, cc, "ReadStatic", []WriteEffect{MustWrite}, []SeedEffect{MaySeedRead})
+
+	// A static destination shares the callee's storage, so its value seeds
+	// the callee's staging slot and is read there.
+	static := scriptStatementEffect(t, ts, 1)
+	requireTargetEffects(t, static, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, static.ReadsSeed)
+	require.Equal(t, []int{0}, static.CalleeReadsSeed)
+
+	// A heap destination gets an ABI-typed zero seed instead, so nothing of
+	// the destination reaches the callee and no read is recorded.
+	heap := scriptStatementEffect(t, ts, 3)
+	requireTargetEffects(t, heap, TargetWriteEffect{TargetIndex: 0, Effect: MustWrite})
+	require.Empty(t, heap.ReadsSeed)
+	require.Empty(t, heap.CalleeReadsSeed)
+}
diff --git a/compiler/solver.go b/compiler/solver.go
index 10176250..2dffb34b 100644
--- a/compiler/solver.go
+++ b/compiler/solver.go
@@ -2468,6 +2468,7 @@ func newFunc(name string, bodyArgs []Type, template *ast.FuncStatement) *FuncInf
 		Vars:              make(map[string]Type),
 		StatementEffects:  make(map[*ast.LetStatement]StatementEffect),
 		BodyOutputEffects: slices.Repeat([]WriteEffect{WriteUncomputed}, len(template.Outputs)),
+		BodySeedEffects:   slices.Repeat([]SeedEffect{SeedUncomputed}, len(template.Outputs)),
 	}
 	for i := range f.Sig.OutTypes {
 		f.Sig.OutTypes[i] = Unresolved{}
diff --git a/compiler/solver_test.go b/compiler/solver_test.go
index aea3b290..ab90ed86 100644
--- a/compiler/solver_test.go
+++ b/compiler/solver_test.go
@@ -77,6 +77,7 @@ x, y`
 	isEvenFunc := newFunc(call.Function.Value, args, template)
 	cc.Compiler.FuncCache[isEvenMangled] = isEvenFunc
 	require.Equal(t, []WriteEffect{WriteUncomputed, WriteUncomputed}, isEvenFunc.BodyOutputEffects)
+	require.Equal(t, []SeedEffect{SeedUncomputed, SeedUncomputed}, isEvenFunc.BodySeedEffects)
 	isOddMangled := Mangle(cc.Compiler.MangledPath, "isOdd", args)
 
 	ts.Converging = false
@@ -112,6 +113,8 @@ x, y`
 	require.True(t, isOddFunc.Settled)
 	require.Equal(t, []WriteEffect{MayWrite, MayWrite}, isEvenFunc.BodyOutputEffects)
 	require.Equal(t, []WriteEffect{MayWrite, MayWrite}, isOddFunc.BodyOutputEffects)
+	require.Equal(t, []SeedEffect{NoSeedRead, NoSeedRead}, isEvenFunc.BodySeedEffects)
+	require.Equal(t, []SeedEffect{NoSeedRead, NoSeedRead}, isOddFunc.BodySeedEffects)
 
 	ts.Solve()
 	require.Empty(t, ts.Errors)
diff --git a/compiler/types.go b/compiler/types.go
index b187de81..07057eb0 100644
--- a/compiler/types.go
+++ b/compiler/types.go
@@ -284,8 +284,12 @@ type FuncInfo struct {
 	// BodyOutputEffects summarizes the typed scalar body before a call-owned
 	// Range or ArrayRange domain determines whether that body executes.
 	BodyOutputEffects []WriteEffect
-	CFGResult         *SpecializationCFGResult
-	Settled           bool
+	// BodySeedEffects records, per output, whether that body may read the
+	// output's incoming value before definitely replacing it. It is published
+	// together with BodyOutputEffects; the two facts are independent.
+	BodySeedEffects []SeedEffect
+	CFGResult       *SpecializationCFGResult
+	Settled         bool
 }
 
 func (f *FuncInfo) AllTypesInferred() bool {
diff --git a/docs/Pluto Effects and Follow-up Plan.md b/docs/Pluto Effects and Follow-up Plan.md
index c4a7070b..5ae9ec51 100644
--- a/docs/Pluto Effects and Follow-up Plan.md	
+++ b/docs/Pluto Effects and Follow-up Plan.md	
@@ -19,6 +19,11 @@ type, and stored type separately, as the corrected code comment already does.
 
 ## 1. Next compiler PR: seed dependency analysis
 
+Resolved by [PR #102](https://github.com/thiremani/pluto/pull/102), which
+publishes a per-output `SeedEffect` beside `BodyOutputEffects`, records
+`StatementEffect.CalleeReadsSeed` at call sites, and consumes both in the CFG;
+[PIR plan, section 15](./Pluto%20IR%20Plan.md) is the canonical description.
+
 Preserve the existing seeded-output semantics and public ABI. Correct the
 analysis before deciding whether a later language version should change those
 semantics.
@@ -92,27 +97,29 @@ discipline. Unknown analysis must not silently mean no seed reads.
 
 ### Acceptance criteria
 
-- [ ] The reproducer compiles without a redundant print and produces 21; the
+- [x] The reproducer compiles without a redundant print and produces 21; the
   fresh-target variant produces 1.
-- [ ] Unconditional seed-dependent writes remain `MustWrite`, with the old
+- [x] Unconditional seed-dependent writes remain `MustWrite`, with the old
   destination live where needed.
-- [ ] A definite overwrite before any read removes the incoming-seed dependency;
+- [x] A definite overwrite before any read removes the incoming-seed dependency;
   a conditional overwrite does not. Copying the seed to a local first preserves
   the dependency even if the output is subsequently overwritten.
-- [ ] A seed read only in a condition or printed string still counts when the
+- [x] A seed read only in a condition or printed string still counts when the
   output is later unconditionally overwritten. Seed reads are not limited to
   dependencies of the returned value.
-- [ ] Nested calls, recursive summaries, multiple outputs, cross-output seed
+- [x] Nested calls, recursive summaries, multiple outputs, cross-output seed
   reads, and zero/one/many-iteration cases are covered.
-- [ ] Fresh targets, discards, incompatible-storage zero seeds, caller argument
+- [x] Fresh targets, discards, incompatible-storage zero seeds, caller argument
   failure, and caller-side retention keep their existing distinct behavior.
 - [ ] CFG and PIR consume settled solver facts rather than independently
   rediscovering dependencies. Existing unused-write diagnostics still work.
-- [ ] Direct and indirect calls preserve staging and alias-input regressions.
+  PR #102 covers the CFG; PIR does not route calls yet, so its consumption of
+  `BodySeedEffects`/`CalleeReadsSeed` is owed by Step 4 call routing.
+- [x] Direct and indirect calls preserve staging and alias-input regressions.
   Public symbols and prototypes do not change with body effects; every public
   direct scalar return retains its existing hidden seed parameter.
-- [ ] Cold and warm caches agree on summaries, diagnostics, and output.
-- [ ] Effect tests, CFG regression tests, ABI/IR checks, race tests, and relevant
+- [x] Cold and warm caches agree on summaries, diagnostics, and output.
+- [x] Effect tests, CFG regression tests, ABI/IR checks, race tests, and relevant
   leak checks pass. Run the full leak suite before submitting the compiler PR.
 
 ## 2. Formatting: model `%n` as an explicit write operand
@@ -198,7 +205,7 @@ and [ABI stability plan](./Pluto%20ABI%20Optimization%20Plan.md).
 
 | Work | Completion criterion / existing reference |
 | --- | --- |
-| Seed/effect correctness | Section 1; next compiler PR before broadening call routing |
+| Seed/effect correctness | Section 1; resolved by [PR #102](https://github.com/thiremani/pluto/pull/102) |
 | `%n` effect contract | Section 2; separate bounded change with formatting semantics updated |
 | Output path protection | [Issue #80](https://github.com/thiremani/pluto/issues/80): compilation cannot overwrite source/configuration through name collisions or unsafe path resolution |
 | Numeric edge behavior | Define and guard integer divide/remainder faults and invalid shift counts; audit range/count/allocation arithmetic |
diff --git a/docs/Pluto IR Plan.md b/docs/Pluto IR Plan.md
index c5f35aff..95480c8f 100644
--- a/docs/Pluto IR Plan.md	
+++ b/docs/Pluto IR Plan.md	
@@ -849,11 +849,14 @@ consume the raw, validity-carrying result and see the skip.
 Boundary resolution implies an **implicit read of the destination seed**, and
 only where the dependency is real: after a successful invocation, at an
 *existing* target whose direct callee output is `MayWrite`, resolved at `=`.
-A fresh destination, a discard, a nested or targetless call, or an
-all-`MustWrite` callee reads nothing. Step 2A records this as a `ReadsSeed`
-fact on the call site — the CFG is untouched in 2A — and Step 2B converts the
-fact into an ordinary CFG read event, so a `MustWrite` classification cannot
-let backward liveness kill the prior value.
+A fresh destination, a discard, or a nested or targetless call resolves
+nothing at the boundary. An all-`MustWrite` callee needs no boundary
+resolution either, but its body may still read the seed; that is the separate
+`SeedEffect` fact below, and the two must not be conflated. Step 2A records
+boundary resolution as a `ReadsSeed` fact on the call site — the CFG is
+untouched in 2A — and Step 2B converts the fact into an ordinary CFG read
+event, so a `MustWrite` classification cannot let backward liveness kill the
+prior value.
 
 The validity-carrying result comes from a **private direct-call variant**
 behind the stable seeded entry point (§1). The clone **keeps the seed
@@ -874,6 +877,52 @@ The variant lands in Step 4; letting print treat a resolved seed as always
 yielded was rejected, since an unwritten output would then print stale data
 instead of suppressing the invocation.
 
+### SeedEffect
+
+`SeedEffect` records, per declared output, whether the scalar body can read
+that output's **incoming value** before definitely replacing it: `NoSeedRead`
+or `MaySeedRead`, with `Uncomputed` and `Invalid` as publication states
+outside the lattice. It is independent of `WriteEffect`. `y = x > 0 x` then
+`y = y + 1` is `MustWrite` and `MaySeedRead`: the last statement always
+writes, but its value depends on the seed, so `a = 20` followed by that call
+must print 21 and compile without an intervening read. `y = x` then
+`y = y + 1` is `MustWrite` and `NoSeedRead`: the definite overwrite comes
+first. A conditionally writing body may inspect its seed or leave preservation
+entirely to the caller; `MayWrite` alone says nothing about which.
+
+Three facts stay separate, each with its own consumer:
+
+| Fact | Question | Where |
+| --- | --- | --- |
+| Body write effect | Does this output receive a body-produced value whenever the scalar body runs? | `BodyOutputEffects`; yield propagation and call routing |
+| Seed-read dependency | Can the body read this output's incoming value before it is definitely replaced? | `BodySeedEffects`; caller liveness and future scheduling |
+| Boundary resolution | Does this assignment use its existing destination to resolve a non-writing direct result? | `StatementEffect.ReadsSeed`; keep-old at `=` |
+
+The body fold is order-sensitive. Explicit reads — conditions, values, print
+arguments, and resolved formatting markers with their dynamic width and
+precision operands — and implicit reads through a callee whose output is
+`MaySeedRead` happen before the statement's writes. An output stops being
+observable once a raw `MustWrite` replaces it; a boundary-resolved write only
+preserves the seed and replaces nothing. The fact is sticky: copying the seed
+to a local before the overwrite keeps the dependency, as does a read only in a
+condition or a printed string. Reads feeding another output count, so
+`a, b = F(x)` with `b = a + 1` before `a = x` reads `a`'s seed. A
+function-owned `Range` domain needs no special case: the first iteration is
+the body, and a zero-iteration call is already resolved at the boundary.
+
+At a call site the callee's fact composes into `StatementEffect.CalleeReadsSeed`
+whatever the ABI, but only when the seed reaches the callee: an indirect
+output reads its destination-seeded staging slot exactly as a direct return
+reads its hidden seed parameter, and lowering seeds that slot from the
+destination only when the two storage types are identical
+(`makeCallOutputAdapters`). A mismatched flavor — a `StrH` destination for a
+`StrG` output, say — gets an ABI-typed zero seed, so the callee never observes
+the destination's value and no read is recorded; the prior value stays an
+overwrite candidate. Only boundary resolution is direct-ABI specific. A fresh
+destination supplies a zero seed, so the CFG emits a read only for a defined
+binding, while the enclosing body's fold treats a call at a not-yet-replaced
+output as a read of that output.
+
 ### Convergence and publication
 
 **Folding a body into an output summary.** A declared output's body summary is
@@ -886,8 +935,10 @@ destination seed (`ReadsSeed`) also leaves the summary unchanged: preserving
 an earlier value does not prove that the body wrote one. The published
 `BodyOutputEffects` deliberately stop before a call-owned domain: a `Range` or
 `ArrayRange` parameter controls whether
-the scalar body executes, not what the body does when it executes. Each call
-combines that reusable body summary with its solved domain. A provably
+the scalar body executes, not what the body does when it executes. The seed
+fold runs beside the write fold over the same statement effects, and the two
+summaries publish together as `BodyOutputEffects` and `BodySeedEffects`. Each
+call combines that reusable body summary with its solved domain. A provably
 non-empty literal can therefore preserve `MustWrite`, while an empty or unknown
 domain weakens the call to `MayWrite`. A range created *inside* the body still
 weakens only the outputs its statements drive — a possibly empty local range
@@ -934,17 +985,20 @@ them **callee-first** in reverse topological order — this is what lets a
 component assume every callee outside it has already published. Within one
 component:
 
-1. Seed every member's outputs with a provisional `MustWrite` working vector. A
-   recursive call reads that provisional value — which is why `Uncomputed`
-   cannot be a lattice element, as there would be nothing to read.
+1. Seed every member's outputs with provisional `MustWrite` and `NoSeedRead`
+   working vectors. A recursive call reads those provisional values — which is
+   why `Uncomputed` cannot be a lattice element, as there would be nothing to
+   read.
 2. Iterate the component, recomputing outputs from rebuilt statement effects
    and callees' current values. Callees outside the component contribute their
    published summaries.
-3. Weaken monotonically, `MustWrite → MayWrite` only. The working vector
-   **persists across body walks** within the component; it is not cleared with
+3. Move monotonically toward the conservative side only: `MustWrite →
+   MayWrite` and `NoSeedRead → MaySeedRead`. Either change requeues the
+   member's callers within the component. The working vectors **persist across
+   body walks** within the component; they are not cleared with
    `FuncInfo.Vars`.
-4. Stop when nothing changes — at most one weakening per slot.
-5. Publish one coherent snapshot for the whole component at once.
+4. Stop when nothing changes — at most one change per slot and fact.
+5. Publish one coherent snapshot of both facts for the whole component at once.
 
 An `Invalid` output blocks publication for its entire component; provisional
 values are never read outside it.
@@ -980,8 +1034,9 @@ width/precision variables on a resolved marker remain structural errors.
 After a stable specialization batch reaches its effect SCC fixed point, each
 node runs effect-sensitive CFG dataflow exactly once and caches its diagnostics.
 For a let, event order is condition reads, RHS reads, `ReadsSeed` destination
-reads, then sparse `StatementEffect.Writes` mapped by `TargetIndex`; all reads
-therefore observe the simultaneous assignment's pre-commit snapshot. Print
+reads, `CalleeReadsSeed` destination reads for defined bindings, then sparse
+`StatementEffect.Writes` mapped by `TargetIndex`; all reads therefore observe
+the simultaneous assignment's pre-commit snapshot. Print
 arguments contribute ordinary reads even though prints have no statement
 effect entry. An unreachable template gets structural and parser checks only:
 effects cannot be derived without types. Consequently, a library-only package
@@ -998,8 +1053,9 @@ The two diagnostics consume effects differently:
   value requires **both** writes to be `MustWrite`. This cures the former
   conditional-write false positive that forced tests to interleave reads merely
   to silence it. A prior seed overwritten by a proven-`MustWrite` call output
-  without being read is instead a true positive: remove the seed or read it
-  explicitly when its value is semantically required.
+  that neither the caller nor the callee body reads is instead a true
+  positive: remove the seed or read it explicitly when its value is
+  semantically required.
 
 After a script solve succeeds, CFG first treats the script as a zero-input,
 zero-output template for structural validation, then runs effect-sensitive
diff --git a/tests/seed/seed_read.exp b/tests/seed/seed_read.exp
new file mode 100644
index 00000000..127c316c
--- /dev/null
+++ b/tests/seed/seed_read.exp
@@ -0,0 +1,19 @@
+Seeded: 21
+Fresh: 1
+Written: 6
+Nested: 21
+Reset: 1
+Cross: -1 21
+inside 20
+Printed: -1
+Zero: 20
+One: 20
+Many: 23
+ManyFresh: 3
+Tag: hi!
+TagWritten: x!
+seen <hi>
+Static: done
+neverread
+seen <>
+Heap: done
diff --git a/tests/seed/seed_read.pt b/tests/seed/seed_read.pt
new file mode 100644
index 00000000..f4530ae1
--- /dev/null
+++ b/tests/seed/seed_read.pt
@@ -0,0 +1,36 @@
+# A body whose last statement always writes can still depend on the incoming
+# output seed. Each caller below assigns such a call over an existing value
+# without reading it first; the analysis keeps that value live.
+y = MaybeIncrement(x)
+    y = x > 0 x
+    y = y + 1
+
+y = Outer(x)
+    y = MaybeIncrement(x)
+
+y = ResetThenIncrement(x)
+    y = 0
+    y = MaybeIncrement(x)
+
+a, b = Cross(x)
+    a = x > 0 x
+    b = a + 1
+    a = x
+
+y = Printed(x)
+    y = x > 0 x
+    "inside -y"
+    y = x
+
+y = AccRange(r)
+    y = r > 5 r
+    y = y + r
+
+s = MaybeTag(n, t)
+    s = n > 0 t
+    s = s ⊕ "!"
+
+s = ReadStatic(n)
+    s = n > 0 "x"
+    "seen <-s>"
+    s = "done"
diff --git a/tests/seed/seed_read.spt b/tests/seed/seed_read.spt
new file mode 100644
index 00000000..ef10e1ef
--- /dev/null
+++ b/tests/seed/seed_read.spt
@@ -0,0 +1,43 @@
+seeded = 20
+seeded = MaybeIncrement(-1)
+"Seeded: -seeded"
+fresh = MaybeIncrement(-1)
+"Fresh: -fresh"
+written = 20
+written = MaybeIncrement(5)
+"Written: -written"
+nested = 20
+nested = Outer(-1)
+"Nested: -nested"
+reset = ResetThenIncrement(-1)
+"Reset: -reset"
+crossA = 20
+crossA, crossB = Cross(-1)
+"Cross: -crossA -crossB"
+printed = 20
+printed = Printed(-1)
+"Printed: -printed"
+zero = 20
+zero = AccRange(0:0)
+"Zero: -zero"
+one = 20
+one = AccRange(0:1)
+"One: -one"
+many = 20
+many = AccRange(0:3)
+"Many: -many"
+manyFresh = AccRange(0:3)
+"ManyFresh: -manyFresh"
+tag = "hi"
+tag = MaybeTag(-1, "x")
+"Tag: -tag"
+tagWritten = "hi"
+tagWritten = MaybeTag(1, "x")
+"TagWritten: -tagWritten"
+static = "hi"
+static = ReadStatic(0)
+"Static: -static"
+heap = "never" ⊕ "read"
+heap
+heap = ReadStatic(0)
+"Heap: -heap"
diff --git a/tests/seed/seed_read_warm.exp b/tests/seed/seed_read_warm.exp
new file mode 100644
index 00000000..173af044
--- /dev/null
+++ b/tests/seed/seed_read_warm.exp
@@ -0,0 +1,4 @@
+WarmSeeded: 21
+WarmNested: 21
+WarmMany: 23
+WarmTag: hi!
diff --git a/tests/seed/seed_read_warm.spt b/tests/seed/seed_read_warm.spt
new file mode 100644
index 00000000..34625981
--- /dev/null
+++ b/tests/seed/seed_read_warm.spt
@@ -0,0 +1,14 @@
+# Compiled after seed_read.spt in the same run, so every callee is already
+# settled and its seed facts are replayed from the shared cache.
+seeded = 20
+seeded = MaybeIncrement(-1)
+"WarmSeeded: -seeded"
+nested = 20
+nested = Outer(-1)
+"WarmNested: -nested"
+many = 20
+many = AccRange(0:3)
+"WarmMany: -many"
+tag = "hi"
+tag = MaybeTag(-1, "x")
+"WarmTag: -tag"