diff --git a/changes/unreleased/occurrence-shared-defaults.performance.md b/changes/unreleased/occurrence-shared-defaults.performance.md
new file mode 100644
index 0000000000..fe1a56aec7
--- /dev/null
+++ b/changes/unreleased/occurrence-shared-defaults.performance.md
@@ -0,0 +1,16 @@
+- **Occurrences of one shape share their derived defaults and their verdicts.** A `=` default
+  that one pristine occurrence of a type derives from nothing but declared values under itself
+  is now recorded against the occurrence's shape — its type, classifiers and holding feature — in
+  a side table of the runtime context, and every other pristine occurrence of that shape reads
+  the recorded value instead of deriving it again and materializing the component tree the
+  derivation walked; an occurrence that states, writes, binds or classifies anything the
+  derivation read derives on its own, and a write under an occurrence invalidates what it took.
+  Within one `-satisfy` or `-validate=<object>` report, a check over occurrences of one shape is
+  evaluated once per distinct set of inputs and its verdict fanned out to each occurrence, which
+  still reports its own verdict, message and path in the same order. Values, verdicts and
+  diagnostics are unchanged, as `TestSparseValuesDifferential` asserts with sharing on and off
+  (`OPENSYSML_SHARED_DEFAULTS=0` turns it off; a context recording a trace shares nothing, so
+  the trace lists every evaluation). On the 12 800-satellite fleet constellation,
+  checking its 2 412 satisfaction assertions drops from 8.84 s and 23.4 GiB allocated to 4.59 s
+  and 7.2 GiB, and reading one summed attribute over every occurrence from 42.7 s and 141.3 GiB
+  to 3.85 s and 2.7 GiB.
diff --git a/docs/internals/performance.md b/docs/internals/performance.md
index bd59b9381d..b9fb7fb39d 100644
--- a/docs/internals/performance.md
+++ b/docs/internals/performance.md
@@ -188,13 +188,35 @@ costs:
 | one `part def` per satellite, 32 planes of 400 | 2 354 827 | 145 MB | 331 s | 49.8 GiB | 20.3 GB |
 | four blocks, `part sats : Block[400]` in 32 planes | 12 467 | 771 KB | 0.70 s | 289 MiB | 184 MB |
 
-The runtime then pays for the occurrences when something asks for them: the
-same network instantiates in 2.06 s and 801 MB, its 2 412 `satisfy`
-assertions check in 8.84 s and 23.4 GiB allocated, and reading one summed
-attribute over every occurrence costs 42.7 s and 141.3 GiB, because each
-occurrence is still an object with a value slot per feature whose component
-tree is materialized to evaluate it. Both forms, their element counts and
-what the runtime does with 12 800 occurrences are in the
+The runtime then pays for the occurrences when something asks for them. Each
+occurrence is an object with a value slot per effective feature, but a `=`
+default derived from nothing but declared values is derived once per shape
+— type, classifiers and holding feature — and taken from a `Context` side
+table by every other pristine occurrence of the shape, without materializing
+the subtree the derivation walked; within one report, a check over
+occurrences of one shape is evaluated once per distinct set of inputs and
+its verdict fanned out (`internal/exec/runtime/shared_default.go`,
+`shared_verdict.go`; `OPENSYSML_SHARED_DEFAULTS=0` turns it off, and a
+context recording a trace shares nothing, so the trace lists every
+evaluation). Measured on
+the same machine, before and after that sharing, one run each with
+`-memstats` and `/usr/bin/time`:
+
+| satellites | operation | before wall | allocated | peak RSS | after wall | allocated | peak RSS |
+| ---------- | --------- | ----------- | --------- | -------- | ---------- | --------- | -------- |
+| 1 600 | `-instantiate` the network | 0.44 s | 238.4 MiB | 195 MB | 0.45 s | 238.5 MiB | 195 MB |
+| 1 600 | `-satisfy`, 324 assertions | 0.71 s | 666.0 MiB | 306 MB | 0.60 s | 381.6 MiB | 272 MB |
+| 1 600 | read `dryMass` over every occurrence | 1.85 s | 2.9 GiB | 737 MB | 0.58 s | 306.3 MiB | 252 MB |
+| 12 800 | `-instantiate` the network | 2.06 s | 1.1 GiB | 801 MB | 1.97 s | 1.1 GiB | 763 MB |
+| 12 800 | `-satisfy`, 2 412 assertions | 8.84 s | 23.4 GiB | 1.49 GB | 4.59 s | 7.2 GiB | 1.32 GB |
+| 12 800 | read `dryMass` over every occurrence | 42.7 s | 141.3 GiB | 5.2 GB | 3.85 s | 2.7 GiB | 1.24 GB |
+
+The reports and values are identical before and after. What remains of the
+checking cost is per diverging unit — every assertion of this workload names
+one, which states its own as-built masses — whose subsystems are
+materialized and whose behaviors then run to the end of the report. Both
+forms, their element counts and what the runtime does with 12 800
+occurrences are in the
 [stress-test record](../project/satellite-network-stress-test.md) and the
 guide chapter on [modeling fleets](../guide/modeling-fleets.md).
 
diff --git a/docs/project/satellite-network-stress-test.md b/docs/project/satellite-network-stress-test.md
index 32dfc7b3f0..21a60d3608 100644
--- a/docs/project/satellite-network-stress-test.md
+++ b/docs/project/satellite-network-stress-test.md
@@ -269,8 +269,8 @@ declares **190 times fewer elements** at 12 800 satellites and validates in
 what the source declares, and the fleet source is the size of four
 spacecraft, twenty stations and the links between thirty-two planes.
 
-What the current runtime does with the 12 800 occurrences, on the same
-machine:
+What the runtime did with the 12 800 occurrences before it shared derived
+defaults and verdicts between them (the next section), on the same machine:
 
 | satellites | operation | wall | allocated | peak RSS |
 | ---------- | --------- | ---- | --------- | -------- |
@@ -321,30 +321,110 @@ Three limits of the current language and runtime shape the fleet form:
   a unit of it reports `multiplicity violation: lower bound too large or
   infinite`. The 12 800-satellite fleet is therefore 32 planes of 400.
 
+Before the runtime shared derived defaults, instantiating a fleet and
+reading a summed attribute over its occurrences cost, warm, **about 2 ms and
+1 MiB per satellite** — the per-satellite cost of a cold `-satisfy` over the
+single-definition form — because every occurrence's component tree was
+materialized to evaluate the sum.
+
+### Sharing derived defaults and verdicts between the occurrences
+
+The runtime now holds, in side tables of the `Context`, what the occurrences
+of one shape have in common beyond their feature list
+([scaling to very large models](large-model-scaling-design.md), one
+definition, many occurrences):
+
+- **Shared derived defaults.** The first pristine occurrence of a shape — an
+  object of a type, with its classifiers, held by a feature — to derive a
+  `=` default whose evaluation read only declared values under itself records
+  the value, and the paths it read, against the shape. Every other pristine
+  occurrence of the shape takes the recorded value when it is read, without
+  materializing the subtree the derivation walked; the features that
+  subtree would have materialized are owed, and settled if anything later
+  asks for them. A write, a binding, a behavior run, a classifier or a
+  redefinition anywhere the derivation read makes the occurrence derive on
+  its own, as does a random draw, a clock read or a lifetime read in the
+  derivation — all three are the run's, not the shape's — and a write under
+  an occurrence invalidates what it took. An occurrence with a destroyed
+  object along a read path takes nothing either: its read reports the
+  object destroyed, as it does without sharing. Only scalars held by value —
+  numbers, strings, quantities, complex numbers, enumeration literals, null —
+  are shared; a value naming an object or a
+  sequence is derived per occurrence. Every occurrence still has a feature
+  value per effective feature: what is shared is the derivation, and the
+  value it produced, not the slot.
+- **Verification over distinct shapes.** Within one `satisfy` report the
+  checks whose subjects are occurrences of one shape are evaluated once per
+  distinct set of inputs: a check that read only declared values evaluates
+  once for the shape, one that read a value an occurrence states of its own
+  once per distinct value read, and the verdict is fanned out to every
+  occurrence with its own subject path. The verdicts, their messages and
+  their order are those of evaluating every check.
+
+`OPENSYSML_SHARED_DEFAULTS=0` turns both off, which is how
+`TestSparseValuesDifferential` in `internal/exec/runtime` compares every
+readable value and every verdict, sharing on and off, over the fixtures, the
+execution-conformance models and generated fleets.
+
+Measured one run each on the machine named at the top, with `-memstats`
+and `/usr/bin/time`; the "before" binary is the runtime of the table above,
+built beside the "after" and run the same hour (the earlier table's figures
+differ from it by run-to-run variance):
+
+| satellites | operation | before wall | allocated | peak RSS | after wall | allocated | peak RSS |
+| ---------- | --------- | ----------- | --------- | -------- | ---------- | --------- | -------- |
+| 1 600 | `-validate` | 0.22 s | 102.2 MiB | 108 MB | 0.23 s | 102.1 MiB | 104 MB |
+| 1 600 | `-instantiate` the network | 0.44 s | 238.4 MiB | 195 MB | 0.45 s | 238.5 MiB | 195 MB |
+| 1 600 | `-satisfy`, 324 assertions | 0.71 s | 666.0 MiB | 306 MB | 0.60 s | 381.6 MiB | 272 MB |
+| 1 600 | `%eval` of `plane<i>.sats.dryMass`, all 8 planes | 1.85 s | 2.9 GiB | 737 MB | 0.58 s | 306.3 MiB | 252 MB |
+| 12 800 | `-validate` | 0.70 s | 289.4 MiB | 184 MB | 0.73 s | 289.0 MiB | 175 MB |
+| 12 800 | `-instantiate` the network | 2.06 s | 1.1 GiB | 801 MB | 1.97 s | 1.1 GiB | 763 MB |
+| 12 800 | `-satisfy`, 2 412 assertions | 8.84 s | 23.4 GiB | 1.49 GB | 4.59 s | 7.2 GiB | 1.32 GB |
+| 12 800 | `%eval` of `plane<i>.sats.dryMass`, all 32 planes | 42.7 s | 141.3 GiB | 5.2 GB | 3.85 s | 2.7 GiB | 1.24 GB |
+
+The reports are identical line for line: the same 2 412 verdicts in the same
+order, and the same 12 800 masses. Validation does not move — nothing in
+loading changed — and neither does instantiation, which derives nothing.
+Checking halves, and the whole of that comes from the shared defaults:
+every assertion of this workload names a diverging unit, which states its
+own as-built masses, so no verdict here stands for another and each is
+evaluated — but what each evaluation costs is lower because the
+components' `mass` and `powerDraw` defaults are taken from the shape rather
+than materialized and started. What remains is the per-unit work the
+assertions on the diverging units do: materializing the unit's subsystems,
+whose behaviors then run to the end of the report. Verdict fan-out shows
+where units state nothing of their own: a requirement satisfied by such
+units is decided once for all of them, and once more per unit stating a
+value (`satisfy_distinct_shapes_mixed` under
+`internal/exec/runtime/testdata/conformance/`). Reading one summed
+attribute over every occurrence is where the sharing pays most — the first occurrence of each block derives `dryMass`
+over its component tree, the other 12 796 take it — and is now **11 times
+faster with 52 times less allocation**.
+
 `BenchmarkFleetInstantiate` and `BenchmarkFleetSatisfy` in
 `tests/stressmodel` measure, warm, instantiating the fleet network and
-reading `sats.dryMass` over four planes, and re-checking every assertion:
+reading `sats.dryMass` over four planes, and re-checking every assertion in
+a session that has already checked them once:
 
 ```bash
 go test ./tests/stressmodel -run '^$' -bench Fleet -benchmem -benchtime 3x
 ```
 
-| satellites | elements | instantiate + read four planes | per satellite | allocated | assertions | warm re-check | allocated |
-| ---------- | -------- | ------------------------------ | ------------- | --------- | ---------- | ------------- | --------- |
-| 32 | 1 179 | 29 ms | 0.9 ms | 18.4 MiB | 24 | 0.9 ms | 0.5 MiB |
-| 128 | 1 715 | 87 ms | 0.7 ms | 93.1 MiB | 36 | 1.2 ms | 1.0 MiB |
-| 512 | 3 947 | 460 ms | 0.9 ms | 882 MiB | 108 | 8.5 ms | 7.3 MiB |
-
-Warm, instantiating a fleet and reading a summed attribute over its
-occurrences costs **about 1 ms and 1.7 MiB per satellite** — of the order
-of the per-satellite cost of a cold `-satisfy` over the single-definition
-form — because every
-occurrence's component tree is still materialized to evaluate the sum. What
-would change that is sparse per-occurrence values and verification over
-distinct shapes ([scaling to very large models](large-model-scaling-design.md),
-one definition, many occurrences): an occurrence whose feature holds its
-block's default storing nothing for it, and a check over N occurrences that
-read only block-level values evaluating once.
+| satellites | elements | instantiate + read four planes, before | after | per satellite, after | allocated, before | after | assertions | warm re-check, before | after | allocated, before | after |
+| ---------- | -------- | -------------------------------------- | ----- | -------------------- | ----------------- | ----- | ---------- | --------------------- | ----- | ----------------- | ----- |
+| 32 | 1 179 | 29 ms | 16 ms | 0.49 ms | 18.4 MiB | 7.7 MiB | 24 | 0.9 ms | 2.5 ms | 0.5 MiB | 1.0 MiB |
+| 128 | 1 715 | 87 ms | 28 ms | 0.22 ms | 93.1 MiB | 15.0 MiB | 36 | 1.2 ms | 2.4 ms | 1.0 MiB | 2.0 MiB |
+| 512 | 3 947 | 460 ms | 73 ms | 0.14 ms | 882 MiB | 44.6 MiB | 108 | 8.5 ms | 12.2 ms | 7.3 MiB | 10.7 MiB |
+
+Instantiating and reading over the occurrences is now sub-linear per
+satellite — the per-satellite cost falls as the fleet grows, since the
+derivation is paid per block and the rest is one object and one shared read
+per occurrence. The warm re-check is **slower** by one to four
+milliseconds per report: in a session where every value is already
+materialized there is no derivation left to share, and the report still
+traces what each check reads to decide which verdicts it may fan out. That
+is the cost of sharing when it finds nothing to share; the cold `-satisfy`
+above, where it does, is the case the fleet form is for.
 
 ## Editing: what an editor pays per keystroke
 
diff --git a/internal/exec/runtime/adopt.go b/internal/exec/runtime/adopt.go
index bfffd18e76..219599ddfb 100644
--- a/internal/exec/runtime/adopt.go
+++ b/internal/exec/runtime/adopt.go
@@ -866,6 +866,8 @@ func (a *adoption) commit() {
 		prevTypes := plan.obj.types()
 		plan.obj.Type = plan.typeSym
 		plan.obj.classifiers = plan.classifiers
+		// Every value taken from a shape is derived again here, so nothing is owed for one.
+		plan.obj.owed = nil
 		// Names of one redefined feature share a feature value, which is rebound once, to
 		// the feature of the name the shared feature value was created under.
 		done := make(map[*FeatureValue]bool, len(plan.obj.FeatureValues))
@@ -883,11 +885,11 @@ func (a *adoption) commit() {
 			// A value an expression states is derived again here, so it cannot go
 			// stale against what that expression now reads.
 			if a.ctx.derivedFeatureValue(fv) {
-				fv.Value, fv.Values, fv.Materialized = Value{}, Value{}, false
+				fv.Value, fv.Values, fv.Materialized, fv.intrinsic = Value{}, Value{}, false, false
 				continue
 			}
 			if a.ctx.collectedFeatureValue(fv) {
-				fv.Value, fv.Values, fv.Materialized = Value{}, Value{}, false
+				fv.Value, fv.Values, fv.Materialized, fv.intrinsic = Value{}, Value{}, false, false
 				continue
 			}
 			// A connector reads the features the `connect` clause names, which are
@@ -897,7 +899,7 @@ func (a *adoption) commit() {
 				if id, held := fv.Value.Object(); held {
 					plan.obj.keepConnector(fv, id)
 				}
-				fv.Value, fv.Values, fv.Materialized = Value{}, Value{}, false
+				fv.Value, fv.Values, fv.Materialized, fv.intrinsic = Value{}, Value{}, false, false
 				continue
 			}
 			fv.Value = a.rewrite(fv.Value)
diff --git a/internal/exec/runtime/binding.go b/internal/exec/runtime/binding.go
index 814a811b48..3092ae130c 100644
--- a/internal/exec/runtime/binding.go
+++ b/internal/exec/runtime/binding.go
@@ -196,7 +196,7 @@ func (ctx *Context) resolveBindingValue(inst *Instance, name string) (Value, boo
 	ctx.noteProbeWrite(target)
 	target.Value = Value{}
 	target.Values = Value{}
-	target.Materialized = false
+	target.Materialized, target.intrinsic = false, false
 	target.BindingDerived, target.Assumed = false, false
 	val, found, err := ctx.resolveBindings(inst, target, name, key)
 	ctx.afterWrite(target, before)
@@ -491,7 +491,7 @@ func (ctx *Context) ownEndpointValue(loc bindingLocation) (Value, bool, error) {
 			return Value{}, false, err
 		}
 	}
-	ctx.noteRead(fv)
+	ctx.noteRead(loc.instance, fv)
 	val := fv.HeldValue()
 	return val, val.Kind != ValInvalid, nil
 }
@@ -819,7 +819,7 @@ func (ctx *Context) bindingLocationValue(loc bindingLocation, materialize bool)
 	if fv.BindingDerived {
 		if ctx.CompositeTypeOf(fv.Feature) != nil {
 			if val := fv.HeldValue(); val.Kind != ValInvalid {
-				ctx.noteRead(fv)
+				ctx.noteRead(loc.instance, fv)
 				return val, true, nil
 			}
 		}
@@ -840,7 +840,7 @@ func (ctx *Context) bindingLocationValue(loc bindingLocation, materialize bool)
 			return Value{}, false, err
 		}
 	}
-	ctx.noteRead(fv)
+	ctx.noteRead(loc.instance, fv)
 	if val := fv.HeldValue(); val.Kind != ValInvalid {
 		return val, true, nil
 	}
@@ -911,7 +911,7 @@ func (ctx *Context) assignBindingValue(inst *Instance, fv *FeatureValue, name st
 		fv.Value = Value{}
 		fv.Values = val
 	}
-	fv.Materialized = true
+	fv.Materialized, fv.intrinsic = true, false
 	fv.BindingDerived, fv.Assumed = true, false
 	return nil
 }
diff --git a/internal/exec/runtime/classifier_behavior.go b/internal/exec/runtime/classifier_behavior.go
index b17df48a97..bb582d24ef 100644
--- a/internal/exec/runtime/classifier_behavior.go
+++ b/internal/exec/runtime/classifier_behavior.go
@@ -371,7 +371,7 @@ func (ctx *Context) forgetValuesNaming(abandoned map[int64]bool) {
 				continue
 			}
 			fv.Value, fv.Values = Value{}, Value{}
-			fv.Materialized, fv.Written = false, false
+			fv.Materialized, fv.Written, fv.intrinsic = false, false, false
 			ctx.invalidateDependents(fv)
 		}
 	}
@@ -660,6 +660,7 @@ func (ctx *Context) startBehaviorsOf(inst *Instance) error {
 			}
 			behavior.binding = i
 			inst.behaviors = append(inst.behaviors, behavior)
+			ctx.behaviorsAttached++
 			ctx.pendingBehaviors = append(ctx.pendingBehaviors, behavior)
 			ctx.objectBehaviors = append(ctx.objectBehaviors, behavior)
 			ctx.workChanged()
diff --git a/internal/exec/runtime/classify.go b/internal/exec/runtime/classify.go
index 2a100052b3..17f4341380 100644
--- a/internal/exec/runtime/classify.go
+++ b/internal/exec/runtime/classify.go
@@ -244,7 +244,16 @@ func (ctx *Context) classify(inst *Instance, typ *symbols.Symbol) error {
 		return nil
 	}
 	inherited := ctx.instanceConforms(inst, typ)
+	ctx.observeClassify(inst, typ)
 	commit, rollback := ctx.beginJournal()
+	// A classifier may redefine what a value taken from the shape read: what the take
+	// left unmaterialized is materialized first, so the redefinition reaches the value.
+	if !inherited && ctx.classifierRedeclares(inst, typ) {
+		if err := ctx.settleOwed(inst); err != nil {
+			rollback()
+			return err
+		}
+	}
 	classifiers, values, running := inst.classifiers, maps.Clone(inst.FeatureValues), len(inst.behaviors)
 	ctx.noteProbeUndo(func() {
 		if len(inst.behaviors) > running {
@@ -286,6 +295,18 @@ func (ctx *Context) classify(inst *Instance, typ *symbols.Symbol) error {
 	return nil
 }
 
+// classifierRedeclares reports whether typ declares a feature inst does not hold, or one
+// it holds under another declaration: classifying by it may change what inst's values read.
+func (ctx *Context) classifierRedeclares(inst *Instance, typ *symbols.Symbol) bool {
+	features := ctx.FeaturesOf(typ)
+	for i := range features {
+		if fv, ok := inst.FeatureValues[features[i].Name]; !ok || fv.Feature.Symbol != features[i].Symbol {
+			return true
+		}
+	}
+	return false
+}
+
 // refineFeatureValue makes a carried feature value read the classifier's declaration when it redefines the
 // one read (KerML 1.0 §7.3.4.5), or the classifier specializes the type declaring it and so masks it (§7.3.2.1).
 func (ctx *Context) refineFeatureValue(inst *Instance, fv *FeatureValue, feat *EffectiveFeature, typ *symbols.Symbol) error {
@@ -331,17 +352,31 @@ func declaredBy[T any](ctx *Context, types []*symbols.Symbol, of func(*symbols.S
 	if len(types) == 1 {
 		return of(types[0])
 	}
-	covered := map[*symbols.Scope]bool{}
+	// The scopes the earlier types cover are gathered only once a later type declares
+	// something, since most features have nothing declared for them.
+	var covered map[*symbols.Scope]bool
+	cover := func(typ *symbols.Symbol) {
+		covered[DeclScope(typ)] = true
+		for _, sup := range ctx.model.semantics.AllSupertypes(typ) {
+			covered[DeclScope(sup)] = true
+		}
+	}
 	var out []T
-	for _, typ := range types {
-		for _, rel := range of(typ) {
+	for i, typ := range types {
+		rels := of(typ)
+		if len(rels) != 0 && covered == nil {
+			covered = map[*symbols.Scope]bool{}
+			for _, earlier := range types[:i] {
+				cover(earlier)
+			}
+		}
+		for _, rel := range rels {
 			if scope := scopeOf(rel); scope == nil || !covered[scope] {
 				out = append(out, rel)
 			}
 		}
-		covered[DeclScope(typ)] = true
-		for _, sup := range ctx.model.semantics.AllSupertypes(typ) {
-			covered[DeclScope(sup)] = true
+		if covered != nil {
+			cover(typ)
 		}
 	}
 	return out
diff --git a/internal/exec/runtime/clock_read.go b/internal/exec/runtime/clock_read.go
index 488b0f1584..b5725886a5 100644
--- a/internal/exec/runtime/clock_read.go
+++ b/internal/exec/runtime/clock_read.go
@@ -46,10 +46,12 @@ func (ctx *Context) universalClockObject(fqn string) (Value, error) {
 // executor of the context advances: a Time::Clock reads the instant on its own
 // scale, seconds since the run began as `accept at` waits for it; any other
 // Clock the Kernel's bare number of seconds. Other members are not answered.
+// The instant is the run's, not the shape's: nothing derived over it is shared.
 func (ctx *Context) clockMember(inst *Instance, name string) (Value, bool, error) {
 	if !ctx.isClockTime(inst, name) {
 		return Value{}, false, nil
 	}
+	ctx.unshareTraces()
 	if ctx.conformsToLibrary(ctx.objectType(inst), timeClockFQN) {
 		return ctx.ClockValue(), true, nil
 	}
diff --git a/internal/exec/runtime/context.go b/internal/exec/runtime/context.go
index 88690bf519..2d21902e19 100644
--- a/internal/exec/runtime/context.go
+++ b/internal/exec/runtime/context.go
@@ -196,6 +196,21 @@ type Context struct {
 	// deriving are the `=` values being derived, innermost last; every feature
 	// value read while one is records it as a dependent (see dependents.go).
 	deriving []derivation
+	// tracing observes the derivations under way, innermost last, for the reads
+	// that decide whether each is one every occurrence of its shape shares.
+	tracing []derivationTrace
+	// shareDefaults turns on the sharing of derived defaults between occurrences of
+	// one shape; sharedDefaults holds them, shapes interns the shapes they are
+	// keyed by, and sharedTaken counts the values taken from it (shared_default.go).
+	shareDefaults  bool
+	sharedDefaults map[sharedKey]*sharedDefault
+	shapes         map[shapeNode]*shapeNode
+	sharedTaken    int64
+	// verdicts is the span sharing verdicts between objects of one shape; nil outside one.
+	verdicts *verdictMemo
+	// behaviorsAttached counts the object behaviors attached so far, so a
+	// derivation knows whether one was attached under it.
+	behaviorsAttached int64
 	// runBoundaries mark, innermost last, where in objectBehaviors and in
 	// pendingBehaviors the behaviors a change still to be kept or undone attached
 	// begin: the only ones a drain under it may run (see nextRunnableBehavior).
@@ -333,6 +348,10 @@ func NewContext(model *Model, maxSteps int64) *Context {
 		bindingOwners:           make(map[featureValueRef]*ast.Usage),
 		collectingSubsets:       make(map[featureValueRef]bool),
 		readingSubsetted:        make(map[featureValueRef]bool),
+
+		shareDefaults:  SharedDefaultsFromEnv(),
+		sharedDefaults: make(map[sharedKey]*sharedDefault),
+		shapes:         make(map[shapeNode]*shapeNode),
 	}
 	ctx.took = &idMark{high: 1}
 	ctx.ids = newIDSequence(ctx.took)
@@ -1123,11 +1142,13 @@ func (ctx *Context) CheckConstraintOn(sym *symbols.Symbol, scope *symbols.Scope,
 	if err := RequireConstraint(sym); err != nil {
 		return CheckResult{Subject: self}, err
 	}
-	subject, err := ctx.checkSubject("constraint", sym.Name, sym, self)
-	if err != nil {
-		return CheckResult{}, err
-	}
+	return ctx.checkOn(sym, "constraint", sym.Name, sym, self, func(subject carrier) (CheckResult, error) {
+		return ctx.checkConstraintOn(sym, scope, subject)
+	})
+}
 
+// checkConstraintOn is CheckConstraintOn evaluated on the object it resolved to.
+func (ctx *Context) checkConstraintOn(sym *symbols.Symbol, scope *symbols.Scope, subject carrier) (CheckResult, error) {
 	// Evaluate every condition the constraint states, inherited ones included.
 	conds := ctx.conditionsOf(sym, ctx.chainMembers(sym, scope))
 	holds, err := ctx.evaluateConditions(conditionCheck{
@@ -1427,11 +1448,13 @@ func (ctx *Context) CheckRequirementOn(sym *symbols.Symbol, scope *symbols.Scope
 	if err := RequireRequirement(sym); err != nil {
 		return CheckResult{Subject: self}, err
 	}
-	subject, err := ctx.checkSubject("requirement", sym.Name, sym, self)
-	if err != nil {
-		return CheckResult{}, err
-	}
+	return ctx.checkOn(sym, "requirement", sym.Name, sym, self, func(subject carrier) (CheckResult, error) {
+		return ctx.checkRequirementOn(sym, scope, subject)
+	})
+}
 
+// checkRequirementOn is CheckRequirementOn evaluated on the object it resolved to.
+func (ctx *Context) checkRequirementOn(sym *symbols.Symbol, scope *symbols.Scope, subject carrier) (CheckResult, error) {
 	// Requirement-local bindings are shared by every member, whichever scope it
 	// was declared in.
 	members := ctx.chainMembers(sym, scope)
diff --git a/internal/exec/runtime/dependents.go b/internal/exec/runtime/dependents.go
index 7a560175f7..8718cfd6ba 100644
--- a/internal/exec/runtime/dependents.go
+++ b/internal/exec/runtime/dependents.go
@@ -18,15 +18,21 @@ type derivation struct {
 
 // deriveFeatureValue evaluates fv's `=` expression, recording what it reads, over
 // again while a read wrote under it; the step limit bounds a run that never settles.
-func (ctx *Context) deriveFeatureValue(inst *Instance, fv *FeatureValue, name string) (Value, error) {
+// It reports whether the derivation read declared values within inst alone, and those reads.
+func (ctx *Context) deriveFeatureValue(inst *Instance, fv *FeatureValue, name string) (Value, bool, []sharedRead, error) {
 	if !ctx.derivable(fv) {
-		return ctx.evalFeatureValueDefault(inst, fv, name)
+		top := ctx.beginTrace(inst, fv)
+		val, err := ctx.evalFeatureValueDefault(inst, fv, name)
+		clean, reads := ctx.endTrace(top)
+		return val, clean, reads, err
 	}
 	for {
 		ctx.forgetReads(fv)
+		top := ctx.beginTrace(inst, fv)
 		val, stale, err := ctx.deriveOnce(inst, fv, name)
+		clean, reads := ctx.endTrace(top)
 		if err != nil || !stale {
-			return val, err
+			return val, clean, reads, err
 		}
 	}
 }
@@ -105,8 +111,11 @@ func (ctx *Context) deriveOnce(inst *Instance, fv *FeatureValue, name string) (v
 }
 
 // noteRead lists the value being derived, if any, as a dependent of the fv just read,
-// and fv among what it reads.
-func (ctx *Context) noteRead(fv *FeatureValue) {
+// held by inst, and fv among what it reads; a derivation being observed sees the read.
+func (ctx *Context) noteRead(inst *Instance, fv *FeatureValue) {
+	if len(ctx.tracing) != 0 {
+		ctx.observeRead(inst, fv)
+	}
 	if len(ctx.deriving) == 0 {
 		return
 	}
@@ -114,15 +123,20 @@ func (ctx *Context) noteRead(fv *FeatureValue) {
 	if dep == fv {
 		return
 	}
-	for _, listed := range fv.dependents {
+	ctx.listRead(fv, dep)
+}
+
+// listRead lists dep as a dependent of src and src among what dep reads, once.
+func (ctx *Context) listRead(src, dep *FeatureValue) {
+	for _, listed := range src.dependents {
 		if listed == dep {
 			return
 		}
 	}
-	ctx.noteProbeWrite(fv)
+	ctx.noteProbeWrite(src)
 	ctx.noteProbeWrite(dep)
-	fv.dependents = append(fv.dependents, dep)
-	dep.reads = append(dep.reads, fv)
+	src.dependents = append(src.dependents, dep)
+	dep.reads = append(dep.reads, src)
 }
 
 // held is what a feature value held before a write, with what depended on it then.
@@ -292,7 +306,7 @@ func (ctx *Context) invalidate(dependents []*FeatureValue) (deriving []*FeatureV
 			ctx.invalidateDependents(dep)
 		default:
 			ctx.noteProbeWrite(dep)
-			dep.Value, dep.Values, dep.Materialized = Value{}, Value{}, false
+			dep.Value, dep.Values, dep.Materialized, dep.intrinsic = Value{}, Value{}, false, false
 			ctx.invalidateDependents(dep)
 		}
 	}
diff --git a/internal/exec/runtime/extent.go b/internal/exec/runtime/extent.go
index c355fe7a98..bf171b2773 100644
--- a/internal/exec/runtime/extent.go
+++ b/internal/exec/runtime/extent.go
@@ -27,9 +27,12 @@ func (ec *EvalContext) evalExtent(n *ast.OperatorExpr) (Value, error) {
 		return Value{}, fmt.Errorf("%w: 'all' requires a type, %s is a %s",
 			ErrTypeMismatch, qualifiedNameToString(qn), target.Notation())
 	}
-	switch {
-	case target.Kind == symbols.SymbolEnumerationDef:
+	if target.Kind == symbols.SymbolEnumerationDef {
 		return ec.literalValues(sem.LiteralsOf(target))
+	}
+	// The extent is the run's, not the shape's: nothing derived over it is shared.
+	ec.ctx.unshareTraces()
+	switch {
 	case sem.IsVariationFeature(target):
 		return ec.variantValues(target, sem.VariantsOf(target))
 	case sem.IsDataType(target):
diff --git a/internal/exec/runtime/held_image.go b/internal/exec/runtime/held_image.go
index 86b617ba01..df53558bd8 100644
--- a/internal/exec/runtime/held_image.go
+++ b/internal/exec/runtime/held_image.go
@@ -90,6 +90,8 @@ type imagedObject struct {
 }
 
 // imagedFeature is one feature value by value, with every name the object reads it under.
+// shared lists what the shape's derivation of a declared value read, when on record,
+// and owed marks one taken from the shape before materializing all of that.
 type imagedFeature struct {
 	names          []string
 	feature        EffectiveFeature
@@ -97,6 +99,10 @@ type imagedFeature struct {
 	materialized   bool
 	written        bool
 	bindingDerived bool
+	assumed        bool
+	intrinsic      bool
+	shared         [][]string
+	owed           bool
 	dependents     []imagedFeatureRef
 	reads          []imagedFeatureRef
 	readsLives     bool // derived from the lives: which objects there are, and when each began and ended
@@ -337,6 +343,10 @@ func (t *imaging) object(inst *Instance) error {
 	for _, id := range obj.anonymous {
 		t.reach(id)
 	}
+	owed := make(map[*FeatureValue]*sharedDefault, len(inst.owed))
+	for _, o := range inst.owed {
+		owed[o.fv] = o.shared
+	}
 	index := make(map[*FeatureValue]int)
 	for _, name := range slices.Sorted(maps.Keys(inst.FeatureValues)) {
 		fv := inst.FeatureValues[name]
@@ -357,10 +367,18 @@ func (t *imaging) object(inst *Instance) error {
 		f := imagedFeature{
 			names: []string{name}, value: fv.Value, values: fv.Values,
 			materialized: fv.Materialized, written: fv.Written, bindingDerived: fv.BindingDerived,
+			assumed: fv.Assumed, intrinsic: fv.intrinsic,
 		}
 		if fv.Feature != nil {
 			f.feature = *fv.Feature
 		}
+		if o, ok := owed[fv]; ok && fv.declared() {
+			f.shared, f.owed = o.paths, true
+		} else if fv.declared() && len(fv.reads) != 0 {
+			if shared, ok := ctx.sharedRecordOf(inst, fv); ok {
+				f.shared = shared.paths
+			}
+		}
 		obj.features = append(obj.features, f)
 	}
 	for fv, id := range inst.keptConnectors {
@@ -558,6 +576,7 @@ func (img *HeldImage) Materialize(dst *Context) error {
 	mark := dst.materializeMark()
 	if err := m.run(); err != nil {
 		mark.rollBack(dst)
+		m.unrecord()
 		return err
 	}
 	return nil
@@ -656,10 +675,11 @@ func (mark materializeMark) rollBack(ctx *Context) {
 
 // materializing builds one context's objects for an image.
 type materializing struct {
-	dst  *Context
-	img  *HeldImage
-	made map[int64]*Instance
-	runs []*runState
+	dst      *Context
+	img      *HeldImage
+	made     map[int64]*Instance
+	runs     []*runState
+	recorded []sharedKey
 }
 
 // bring answers the object made here for an imaged identity.
@@ -716,6 +736,7 @@ func (m *materializing) run() error {
 	}
 	for _, obj := range img.objects {
 		m.edges(obj)
+		m.records(obj)
 	}
 	// The objects made are lives of dst: what derived from the lives, imaged or dst's own, derives again.
 	dst.livesChanged()
@@ -772,6 +793,7 @@ func (m *materializing) object(obj imagedObject) error {
 		fv := &FeatureValue{
 			Feature:      m.feature(inst, f.feature),
 			Materialized: f.materialized, Written: f.written, BindingDerived: f.bindingDerived,
+			Assumed: f.assumed, intrinsic: f.intrinsic,
 		}
 		var err error
 		if fv.Value, err = m.value(f.value); err != nil {
@@ -837,6 +859,39 @@ func (m *materializing) edges(obj imagedObject) {
 	}
 }
 
+// records puts on dst's shared table what the imaged values' derivations read, so the
+// object's shape shares them on, and owes again what a value taken from it left unmaterialized.
+func (m *materializing) records(obj imagedObject) {
+	inst := m.made[obj.id]
+	shape := m.dst.shapeOf(inst)
+	for _, f := range obj.features {
+		if f.shared == nil {
+			continue
+		}
+		fv := inst.FeatureValues[f.names[0]]
+		shared := &sharedDefault{value: fv.Value, paths: f.shared}
+		if shape != nil {
+			key := sharedKey{shape: shape, feature: fv.Feature}
+			if prior, ok := m.dst.sharedDefaults[key]; ok {
+				shared = prior
+			} else {
+				m.dst.sharedDefaults[key] = shared
+				m.recorded = append(m.recorded, key)
+			}
+		}
+		if f.owed {
+			inst.owed = append(inst.owed, owedDefault{fv: fv, shared: shared})
+		}
+	}
+}
+
+// unrecord takes off dst's shared table the records a failed materialization put there.
+func (m *materializing) unrecord() {
+	for _, key := range m.recorded {
+		delete(m.dst.sharedDefaults, key)
+	}
+}
+
 // featureAt is the feature value made for an imaged reference.
 func (m *materializing) featureAt(ref imagedFeatureRef) *FeatureValue {
 	at := slices.IndexFunc(m.img.objects, func(o imagedObject) bool { return o.id == ref.object })
diff --git a/internal/exec/runtime/held_image_behavior.go b/internal/exec/runtime/held_image_behavior.go
index b67ff035e6..21d0d2bad8 100644
--- a/internal/exec/runtime/held_image_behavior.go
+++ b/internal/exec/runtime/held_image_behavior.go
@@ -483,6 +483,7 @@ func (m *materializing) behavior(b imagedBehavior) error {
 		behavior.Action = exec
 	}
 	inst.behaviors = append(inst.behaviors, behavior)
+	dst.behaviorsAttached++
 	dst.objectBehaviors = append(dst.objectBehaviors, behavior)
 	dst.workChanged()
 	return nil
diff --git a/internal/exec/runtime/held_image_test.go b/internal/exec/runtime/held_image_test.go
index 9c3d127c58..6b3a420a7c 100644
--- a/internal/exec/runtime/held_image_test.go
+++ b/internal/exec/runtime/held_image_test.go
@@ -1098,7 +1098,7 @@ func TestHeldImageRefusesAUsageDenotingAnotherObjectOfTheDestination(t *testing.
 // destinationState is every part of a context a materialization writes, as one value to compare.
 type destinationState struct {
 	instances, created, lives, behaviors, messages, occurrences, metadata, variants, selected int
-	onClock                                                                                   int
+	onClock, shared                                                                           int
 	nextID, tookHigh, activations, runs                                                       int64
 	clock                                                                                     float64
 	clockRun                                                                                  *runState
@@ -1109,8 +1109,8 @@ func destinationStateOf(ctx *Context) destinationState {
 		instances: len(ctx.instances), created: len(ctx.created), lives: len(ctx.lives), behaviors: len(ctx.objectBehaviors),
 		messages: len(ctx.messages), occurrences: len(ctx.occurrences), metadata: len(ctx.metadataObjects),
 		variants: len(ctx.variantObjects), selected: len(ctx.selectedVariants),
-		onClock: len(ctx.clock.waiters),
-		nextID:  ctx.ids.next, tookHigh: ctx.took.high, activations: ctx.activations, runs: ctx.runs,
+		onClock: len(ctx.clock.waiters), shared: len(ctx.sharedDefaults),
+		nextID: ctx.ids.next, tookHigh: ctx.took.high, activations: ctx.activations, runs: ctx.runs,
 		clock: ctx.clock.now, clockRun: ctx.clockRun.state,
 	}
 }
diff --git a/internal/exec/runtime/instance.go b/internal/exec/runtime/instance.go
index d6618ce09f..f7fd978ada 100644
--- a/internal/exec/runtime/instance.go
+++ b/internal/exec/runtime/instance.go
@@ -58,6 +58,10 @@ type Instance struct {
 	// explicit marks an object a caller asked for by name, which stands on its
 	// own even where its usage is a feature of a type.
 	explicit bool
+
+	// owed are the derived values this object took from its shape before
+	// materializing all their derivations read (see shared_default.go).
+	owed []owedDefault
 }
 
 // Owner answers the object holding this one and the feature of it that does, or
@@ -95,6 +99,9 @@ type FeatureValue struct {
 	// changing is set while a write to this value is under way, so a write nested
 	// in it counts as part of it (see beforeWrite).
 	changing bool
+	// intrinsic marks a value the feature's declarations alone materialized, which
+	// every occurrence of the shape holds alike (see shared_default.go).
+	intrinsic bool
 }
 
 // HeldValue is the value the feature value reads as: its collection when the feature is
@@ -266,7 +273,7 @@ func (ctx *Context) initFeatureValue(inst *Instance, fv *FeatureValue, feat *Eff
 			val := Value{Kind: ValConst, Const: semVal}
 			if ctx.checkDefault(inst, fv, feat.Name, &val, admitDeclared) == nil {
 				fv.Value = val
-				fv.Materialized = true
+				fv.Materialized, fv.intrinsic = true, true
 			}
 		}
 	}
@@ -299,7 +306,7 @@ func (ctx *Context) unfoldSubsettedDefaults(inst *Instance, typ *symbols.Symbol,
 				continue
 			}
 			ctx.noteProbeWrite(fv)
-			fv.Value, fv.Values, fv.Materialized = Value{}, Value{}, false
+			fv.Value, fv.Values, fv.Materialized, fv.intrinsic = Value{}, Value{}, false, false
 			ctx.invalidateDependents(fv)
 		}
 	}
@@ -732,7 +739,8 @@ func (inst *Instance) SetFeatureValue(ctx *Context, name string, value Value) er
 			fv.Value = Value{}
 		}
 		fv.Materialized, fv.Written = true, true
-		fv.BindingDerived, fv.Assumed = false, false
+		fv.BindingDerived, fv.Assumed, fv.intrinsic = false, false, false
+		ctx.unshareTraces()
 		ctx.afterWrite(fv, before)
 		return nil
 	})
@@ -751,7 +759,7 @@ func (inst *Instance) materializeFeatureValue(ctx *Context, name string, open *o
 	if err != nil {
 		return nil, err
 	}
-	ctx.noteRead(fv)
+	ctx.noteRead(inst, fv)
 	return fv, nil
 }
 
@@ -880,14 +888,17 @@ func (inst *Instance) materializeVariation(ctx *Context, fv *FeatureValue, name
 		return nil, fmt.Errorf("feature value %s.%s: %w", inst.Type.Name, name, err)
 	}
 	fv.Value = bound
-	fv.Materialized = true
+	fv.Materialized, fv.intrinsic = true, false
 	return fv, nil
 }
 
 // materializeDerived evaluates a default against this instance and holds what
 // it states once that conforms to the feature's multiplicity and type.
 func (inst *Instance) materializeDerived(ctx *Context, fv *FeatureValue, name string) (*FeatureValue, error) {
-	val, err := ctx.deriveFeatureValue(inst, fv, name)
+	if ctx.takeShared(inst, fv) {
+		return fv, nil
+	}
+	val, clean, reads, err := ctx.deriveFeatureValue(inst, fv, name)
 	if err != nil {
 		return nil, err
 	}
@@ -903,7 +914,8 @@ func (inst *Instance) materializeDerived(ctx *Context, fv *FeatureValue, name st
 	} else {
 		fv.Values = val
 	}
-	fv.Materialized = true
+	fv.Materialized, fv.intrinsic = true, clean
+	ctx.shareDerived(inst, fv, val, clean, reads)
 	return fv, nil
 }
 
@@ -941,7 +953,7 @@ func (inst *Instance) materializeComposite(ctx *Context, fv *FeatureValue, name
 			return nil, err
 		}
 		fv.Value = Value{Kind: ValInstance, Instance: childInst.ID}
-		fv.Materialized = true
+		fv.Materialized, fv.intrinsic = true, true
 		if err := ctx.startClassifierBehaviors(childInst, mark); err != nil {
 			return nil, err
 		}
@@ -979,7 +991,7 @@ func (inst *Instance) materializeCompositeCollection(ctx *Context, fv *FeatureVa
 	mark := len(ctx.created)
 	children, unfill, err := ctx.fillOptionalSubsetters(inst, name, count)
 	fail := func(err error) error {
-		fv.Values, fv.Materialized = Value{}, false
+		fv.Values, fv.Materialized, fv.intrinsic = Value{}, false, false
 		ctx.abandonInstancesSince(mark)
 		unfill()
 		release()
@@ -1003,6 +1015,7 @@ func (inst *Instance) materializeCompositeCollection(ctx *Context, fv *FeatureVa
 	fv.Values = ctx.collectionOf(fv.Feature, seq.Elements())
 	fv.Materialized = true
 	fv.Assumed = mult.AdmitsMore(int64(seq.Size()))
+	fv.intrinsic = ctx.subsettersDeclared(inst, name)
 	if err := ctx.startClassifierBehaviorsOf(children, mark); err != nil {
 		return fail(err)
 	}
@@ -1078,7 +1091,7 @@ func (inst *Instance) holdContributed(ctx *Context, fv *FeatureValue, name strin
 	} else {
 		fv.Values = val
 	}
-	fv.Materialized = true
+	fv.Materialized, fv.intrinsic = true, ctx.subsettersDeclared(inst, name)
 	fv.Assumed = !symbols.IsAbstract(fv.Feature.Symbol) && fv.Feature.Multiplicity.AdmitsMore(int64(len(contributed)))
 	return fv, nil
 }
diff --git a/internal/exec/runtime/lifetimes.go b/internal/exec/runtime/lifetimes.go
index f87cc03614..4eb7c1d072 100644
--- a/internal/exec/runtime/lifetimes.go
+++ b/internal/exec/runtime/lifetimes.go
@@ -33,8 +33,12 @@ type life struct {
 func (l life) alive() bool { return l.began > 0 && l.ended == 0 }
 
 // readsLives lists the `=` value being derived, if any, as reading the lives: which
-// objects there are, and when each began and ended.
-func (ctx *Context) readsLives() { ctx.noteRead(&ctx.lifetimes) }
+// objects there are, and when each began and ended. The lives are the run's, not the
+// shape's, so nothing derived over them is shared.
+func (ctx *Context) readsLives() {
+	ctx.unshareTraces()
+	ctx.noteRead(nil, &ctx.lifetimes)
+}
 
 // livesChanged unmaterializes what derived from the lives, save what is deriving now:
 // a change a `=` value makes while deriving is its own, and what it derives reflects it.
@@ -186,6 +190,7 @@ func (ctx *Context) createDuring(op string, inst *Instance, mark int64) error {
 // outlives its whole or ends twice, and ends the behaviors they perform; a behavior
 // under way ends where its call catches the unwinding, which destroy returns.
 func (ctx *Context) destroy(inst *Instance) error {
+	ctx.unshareTraces()
 	if err := ctx.checkLiving(inst); err != nil {
 		return err
 	}
diff --git a/internal/exec/runtime/modeled.go b/internal/exec/runtime/modeled.go
index a5b8baaa5e..1e72a4f903 100644
--- a/internal/exec/runtime/modeled.go
+++ b/internal/exec/runtime/modeled.go
@@ -188,7 +188,9 @@ type distribution struct {
 // draw makes the draw the call what asks for — the witness's under replay, the
 // distribution's fixed point under a fixed policy, else one from the run's modeled
 // stream — noting it for the trace and the witness; a probe's draw is undone with the probe.
+// A draw is the run's, not the shape's: what it feeds is never shared between occurrences.
 func (ctx *Context) draw(what string, dist distribution) (semantics.Value, error) {
+	ctx.unshareTraces()
 	val, err := ctx.scheduling().draw(what, dist)
 	if err != nil {
 		return semantics.Value{}, err
diff --git a/internal/exec/runtime/robustness_test.go b/internal/exec/runtime/robustness_test.go
index bb9d1332dc..770389d47a 100644
--- a/internal/exec/runtime/robustness_test.go
+++ b/internal/exec/runtime/robustness_test.go
@@ -504,6 +504,99 @@ func TestRuntimeRobustness(t *testing.T) {
 	t.Run("random_bounds_reversed", testRandomBoundsReversed)
 	t.Run("random_duration_without_a_seed", testRandomDurationWithoutASeed)
 	t.Run("monte_carlo_plan_without_runs", testMonteCarloPlanWithoutRuns)
+	t.Run("shared_default_over_a_cyclic_derivation", testSharedDefaultOverACyclicDerivation)
+	t.Run("shared_default_taken_over_a_write_that_then_fails", testSharedDefaultTakenOverAWriteThatThenFails)
+}
+
+// A `=` value defined in terms of itself fails on every occurrence of the shape
+// with the same typed error, and the failure is never shared as a value.
+func testSharedDefaultOverACyclicDerivation(t *testing.T) {
+	idx, _, ctx := buildRuntime(t, "<shared-cycle>", parseAndBuild(t, `package P {
+		part def Sat {
+			attribute a = b + 1;
+			attribute b = a + 1;
+		}
+		part def Fleet { part sats : Sat[3]; }
+	}`))
+	ctx.SetSharedDefaults(true)
+	fleet, err := ctx.Instantiate(oneSymbol(t, idx, "P::Fleet"))
+	if err != nil {
+		t.Fatalf("instantiate: %v", err)
+	}
+	sats, err := fleet.GetFeatureValue(ctx, "sats")
+	if err != nil {
+		t.Fatalf("sats: %v", err)
+	}
+	var first string
+	for i, held := range elementsOf(sats.HeldValue()) {
+		id, _ := held.Object()
+		sat, _ := ctx.Instance(id)
+		_, err := sat.GetFeatureValue(ctx, "a")
+		if !errors.Is(err, ErrCyclicFeatureValue) {
+			t.Fatalf("sats#(%d).a: got %v, want %v", i+1, err, ErrCyclicFeatureValue)
+		}
+		if i == 0 {
+			first = err.Error()
+		} else if err.Error() != first {
+			t.Errorf("sats#(%d).a fails as %q, the first as %q", i+1, err, first)
+		}
+	}
+	if taken := ctx.SharedDefaultsTaken(); taken != 0 {
+		t.Errorf("%d shared defaults taken from a derivation that never produced a value", taken)
+	}
+}
+
+// A write under an occurrence that took a shared value re-derives it on that
+// occurrence alone: a write the derivation cannot then use fails as a typed error
+// there, while the other occurrences keep the shape's value.
+func testSharedDefaultTakenOverAWriteThatThenFails(t *testing.T) {
+	idx, _, ctx := buildRuntime(t, "<shared-then-fails>", parseAndBuild(t, `package P {
+		part def Sat {
+			attribute d = 2;
+			attribute q = 10 / d;
+		}
+		part def Fleet { part sats : Sat[2]; }
+	}`))
+	ctx.SetSharedDefaults(true)
+	fleet, err := ctx.Instantiate(oneSymbol(t, idx, "P::Fleet"))
+	if err != nil {
+		t.Fatalf("instantiate: %v", err)
+	}
+	sats, err := fleet.GetFeatureValue(ctx, "sats")
+	if err != nil {
+		t.Fatalf("sats: %v", err)
+	}
+	held := elementsOf(sats.HeldValue())
+	sat := func(i int) *Instance {
+		id, _ := held[i].Object()
+		inst, _ := ctx.Instance(id)
+		return inst
+	}
+	for i := range held {
+		fv, err := sat(i).GetFeatureValue(ctx, "q")
+		if err != nil {
+			t.Fatalf("sats#(%d).q: %v", i+1, err)
+		}
+		if got := FormatValue(fv.Value); got != "5.0" {
+			t.Fatalf("sats#(%d).q = %s, want 5.0", i+1, got)
+		}
+	}
+	if taken := ctx.SharedDefaultsTaken(); taken != 1 {
+		t.Fatalf("shared defaults taken = %d, want 1", taken)
+	}
+	if err := sat(1).SetFeatureValue(ctx, "d", integerValue(0)); err != nil {
+		t.Fatalf("sats#(2).d = 0: %v", err)
+	}
+	if _, err := sat(1).GetFeatureValue(ctx, "q"); err == nil || !strings.Contains(err.Error(), "division by zero") {
+		t.Fatalf("sats#(2).q after d = 0: got %v, want a division by zero", err)
+	}
+	fv, err := sat(0).GetFeatureValue(ctx, "q")
+	if err != nil {
+		t.Fatalf("sats#(1).q after the write to sats#(2): %v", err)
+	}
+	if got := FormatValue(fv.Value); got != "5.0" {
+		t.Errorf("sats#(1).q = %s after the write to sats#(2), want 5.0", got)
+	}
 }
 
 func testBindingConflict(t *testing.T) {
diff --git a/internal/exec/runtime/satisfy.go b/internal/exec/runtime/satisfy.go
index b5abce3d85..d7f5484f18 100644
--- a/internal/exec/runtime/satisfy.go
+++ b/internal/exec/runtime/satisfy.go
@@ -268,7 +268,6 @@ func (ctx *Context) CheckSatisfactionOn(a *SatisfyAssertion, subject *Instance)
 		}
 		subject = inst
 	}
-
 	// The requirement being satisfied chooses the object its conditions read the
 	// same way `%requirement` does, so an object holding the carrier nested
 	// answers about that nested object rather than about the declaration.
@@ -278,12 +277,15 @@ func (ctx *Context) CheckSatisfactionOn(a *SatisfyAssertion, subject *Instance)
 	if carrying == nil {
 		carrying = target
 	}
-	resolved, err := ctx.checkSubject("satisfaction", a.Text(), carrying, subject)
-	if err != nil {
-		return CheckResult{}, err
-	}
-	reached := resolved // the object resolved to, named by where it was reached from
-	subject = resolved.instance
+	return ctx.checkOn(sharedElement(a), "satisfaction", a.Text(), carrying, subject, func(reached carrier) (CheckResult, error) {
+		return ctx.checkSatisfactionOn(a, target, reached)
+	})
+}
+
+// checkSatisfactionOn is CheckSatisfactionOn evaluated on the object it resolved
+// to, named by where it was reached from.
+func (ctx *Context) checkSatisfactionOn(a *SatisfyAssertion, target *symbols.Symbol, reached carrier) (CheckResult, error) {
+	subject := reached.instance
 
 	scope := target.OwnerScope
 	members := ctx.chainMembers(target, scope)
diff --git a/internal/exec/runtime/shared_default.go b/internal/exec/runtime/shared_default.go
new file mode 100644
index 0000000000..fee127adf7
--- /dev/null
+++ b/internal/exec/runtime/shared_default.go
@@ -0,0 +1,552 @@
+package runtime
+
+import (
+	"strconv"
+	"strings"
+
+	"github.com/Open-MBEE/OpenSysML/internal/semantic/symbols"
+	"github.com/Open-MBEE/OpenSysML/internal/workspace/envvar"
+)
+
+// A `=` value derived on an occurrence from nothing but what its declarations
+// materialize is a property of the occurrence's shape, not of the occurrence: the
+// context keeps it in a side table keyed by shape and feature, and every other
+// occurrence of the shape whose reads are still as declared takes it from there
+// instead of materializing what it would read. The feature value slot stays, so a
+// value taken this way reads exactly as one derived in place, and is invalidated
+// as one: what the derivation read is listed as read on the taking occurrence.
+
+// SharedDefaultsEnvVar switches the sharing of derived defaults between
+// occurrences of one shape off when set to 0 (or false/off/no).
+const SharedDefaultsEnvVar = "OPENSYSML_SHARED_DEFAULTS"
+
+// SharedDefaultsFromEnv reports whether the environment leaves derived-default
+// sharing on, which it does unless SharedDefaultsEnvVar switches it off.
+func SharedDefaultsFromEnv() bool {
+	switch strings.ToLower(strings.TrimSpace(envvar.Lookup(SharedDefaultsEnvVar))) {
+	case "0", "false", "off", "no":
+		return false
+	}
+	return true
+}
+
+// SetSharedDefaults turns derived-default sharing between occurrences on or off.
+func (ctx *Context) SetSharedDefaults(on bool) { ctx.shareDefaults = on }
+
+// SharedDefaults reports whether this context shares derived defaults between occurrences.
+func (ctx *Context) SharedDefaults() bool { return ctx.shareDefaults }
+
+// sharing reports whether evaluations are shared now: a traced context shares none,
+// since a trace records every evaluation and a value taken from the shape has none.
+func (ctx *Context) sharing() bool { return ctx.shareDefaults && ctx.trace == nil }
+
+// SharedDefaultsTaken counts the derived values occurrences took from the shared
+// table rather than deriving; a measure of what the sharing saved.
+func (ctx *Context) SharedDefaultsTaken() int64 { return ctx.sharedTaken }
+
+// shapeNode is one interned occurrence shape: the type of an object and, for one
+// held by another, the declaration of the feature holding it; a classifier the
+// object has since been given is a node of its own over the shape it classifies.
+// What the holder is otherwise does not reach the object's declared values: a read
+// outside the object leaves a derivation unshared, and a binding declared over it
+// is looked for on every occurrence taking a value.
+type shapeNode struct {
+	outer      *shapeNode
+	feature    *symbols.Symbol
+	typ        *symbols.Symbol
+	classifier bool
+}
+
+// sharedKey names a derived default of a shape.
+type sharedKey struct {
+	shape   *shapeNode
+	feature *EffectiveFeature
+}
+
+// sharedDefault is a value derived from declared reads alone, with the paths of
+// those reads from the occurrence it was derived on, in the order they were read.
+type sharedDefault struct {
+	value Value
+	paths [][]string
+}
+
+// sharedRead is one feature value a derivation read, as a path from the object it was
+// read on: the feature's name, or what a shared value of that object read in turn. A
+// check may read a value not as declared; then the read carries the value as an input.
+type sharedRead struct {
+	inst   *Instance
+	path   []string
+	value  Value
+	valued bool
+}
+
+// sharedInput is a value a check read that is not as declared, as a path from the
+// object checked: another object of the shape takes the verdict when it reads the same.
+type sharedInput struct {
+	path  []string
+	value Value
+}
+
+// derivationTrace observes one derivation of a `=` value on inst, or one check on
+// inst: clean while every read so far was of a declared value within inst and nothing
+// else happened, save a check classifying inst by a type it already conforms to.
+type derivationTrace struct {
+	inst       *Instance
+	fv         *FeatureValue
+	attached   int64
+	clean      bool
+	reads      []sharedRead
+	classified []*symbols.Symbol
+}
+
+// owedDefault is a value an occurrence took from the shared table before
+// materializing all the derivation read: what it still owes materializing.
+type owedDefault struct {
+	fv     *FeatureValue
+	shared *sharedDefault
+}
+
+// shapeOf interns the shape of inst, nil for an object materialized from no type or
+// held by a feature declared by none: its declarations follow from its type, its
+// classifiers and the declaration of the feature holding it.
+func (ctx *Context) shapeOf(inst *Instance) *shapeNode {
+	if inst.Type == nil {
+		return nil
+	}
+	var feature *symbols.Symbol
+	if owner, name := inst.Owner(); owner != nil {
+		held, ok := owner.FeatureValues[name]
+		if !ok || held.Feature.Symbol == nil {
+			return nil
+		}
+		feature = held.Feature.Symbol
+	}
+	shape := ctx.internShape(shapeNode{feature: feature, typ: inst.Type})
+	for _, classifier := range inst.classifiers {
+		shape = ctx.internShape(shapeNode{outer: shape, typ: classifier, classifier: true})
+	}
+	return shape
+}
+
+// internShape returns the one node standing for node.
+func (ctx *Context) internShape(node shapeNode) *shapeNode {
+	if interned, ok := ctx.shapes[node]; ok {
+		return interned
+	}
+	interned := &node
+	ctx.shapes[node] = interned
+	return interned
+}
+
+// declared reports whether the feature value holds what its declarations alone
+// materialize: neither written, bound, assumed nor otherwise made up.
+func (s *FeatureValue) declared() bool {
+	return s.Materialized && s.intrinsic && !s.Written && !s.BindingDerived && !s.Assumed
+}
+
+// subsettersDeclared reports whether every feature of inst subsetting the named one
+// holds a declared value, so what they contribute to it follows from declarations alone.
+func (ctx *Context) subsettersDeclared(inst *Instance, name string) bool {
+	for _, feat := range ctx.subsettingFeaturesOf(inst, name) {
+		if fv, ok := inst.FeatureValues[feat.Name]; !ok || !fv.declared() {
+			return false
+		}
+	}
+	return true
+}
+
+// shareable reports whether a derived value may be held by every occurrence of the
+// shape: a scalar whose payload no occurrence can change, and that names no object.
+func shareable(val Value) bool {
+	switch val.Kind {
+	case ValConst, ValNull, ValString, ValQuantity, ValEnumLiteral, ValComplex:
+		return true
+	}
+	return false
+}
+
+// sharesDefault reports whether fv's derived default on inst is one its shape may
+// hold: sharing is on, the feature holds one value its subsetters do not populate,
+// no binding or write determines it, and no behavior run makes the reads its own.
+func (ctx *Context) sharesDefault(inst *Instance, fv *FeatureValue) bool {
+	return ctx.sharing() && fv.Feature.Scalar() && !fv.Written && !fv.BindingDerived &&
+		ctx.behaviorRunDepth == 0 && !ctx.defaultYieldsToSubsetters(inst, fv.Feature) &&
+		ctx.shapeOf(inst) != nil
+}
+
+// beginTrace opens the observation of fv's derivation on inst.
+func (ctx *Context) beginTrace(inst *Instance, fv *FeatureValue) int {
+	return ctx.beginTraceOn(inst, fv, ctx.sharesDefault(inst, fv))
+}
+
+// beginTraceOn opens the observation of an evaluation on inst — fv's derivation, or
+// a check with no feature value of its own — clean only when it may be shared at all.
+func (ctx *Context) beginTraceOn(inst *Instance, fv *FeatureValue, clean bool) int {
+	ctx.tracing = append(ctx.tracing, derivationTrace{
+		inst: inst, fv: fv, clean: clean, attached: ctx.behaviorsAttached,
+	})
+	return len(ctx.tracing) - 1
+}
+
+// endTrace closes the observation opened at top, reporting the derivation clean when
+// every read was declared and no behavior was attached under it.
+func (ctx *Context) endTrace(top int) (clean bool, reads []sharedRead) {
+	clean, reads, _ = ctx.endTraceClassified(top)
+	return clean, reads
+}
+
+// endTraceClassified is endTrace also reporting the classifiers the evaluation gave
+// the object it was on.
+func (ctx *Context) endTraceClassified(top int) (clean bool, reads []sharedRead, classified []*symbols.Symbol) {
+	t := ctx.tracing[top]
+	ctx.tracing = ctx.tracing[:top]
+	if !t.clean || ctx.behaviorsAttached != t.attached {
+		return false, nil, nil
+	}
+	return true, t.reads, t.classified
+}
+
+// observeClassify notes, for every evaluation being observed, that inst is being
+// classified by typ: a check classifying its own object is on record to classify
+// every object it stands for alike; any other classification makes the evaluation
+// the occurrence's own.
+func (ctx *Context) observeClassify(inst *Instance, typ *symbols.Symbol) {
+	for i := range ctx.tracing {
+		t := &ctx.tracing[i]
+		if !t.clean {
+			continue
+		}
+		if t.fv != nil || t.inst != inst {
+			t.clean = false
+			continue
+		}
+		t.classified = append(t.classified, typ)
+	}
+}
+
+// unshareTraces makes every derivation being observed its occurrence's own: what
+// changed under it is not what every occurrence of the shape has.
+func (ctx *Context) unshareTraces() {
+	for i := range ctx.tracing {
+		ctx.tracing[i].clean = false
+	}
+}
+
+// observeRead notes, for every derivation being observed, the read of fv held by
+// inst: a read outside the derivation's occurrence, or of a value not as declared,
+// makes the derivation the occurrence's own — save that a check reading a scalar
+// not as declared takes it as an input. A derived value read stands for what it read
+// in turn, which its shape's record lists; one with no record is not shared.
+func (ctx *Context) observeRead(inst *Instance, fv *FeatureValue) {
+	for i := range ctx.tracing {
+		t := &ctx.tracing[i]
+		if !t.clean || t.fv == fv {
+			continue
+		}
+		if !ctx.declaredWithin(inst, t.inst) {
+			t.clean = false
+			continue
+		}
+		if !fv.declared() {
+			if t.fv != nil || !fv.Materialized || !shareable(fv.Value) || !ctx.singlyWithin(inst, t.inst) {
+				t.clean = false
+				continue
+			}
+			t.reads = append(t.reads, sharedRead{inst: inst, path: []string{fv.Feature.Name}, value: fv.Value, valued: true})
+			continue
+		}
+		t.reads = append(t.reads, sharedRead{inst: inst, path: []string{fv.Feature.Name}})
+		if len(fv.reads) == 0 {
+			continue
+		}
+		shared, ok := ctx.sharedRecordOf(inst, fv)
+		if !ok {
+			t.clean = false
+			continue
+		}
+		for _, path := range shared.paths {
+			t.reads = append(t.reads, sharedRead{inst: inst, path: path})
+		}
+	}
+}
+
+// sharedRecordOf finds what the derivation of fv, held declared by inst, read: the
+// record of inst's shape, or of the shape inst had before a classifier that left the
+// value standing, which is what it would still derive.
+func (ctx *Context) sharedRecordOf(inst *Instance, fv *FeatureValue) (*sharedDefault, bool) {
+	for shape := ctx.shapeOf(inst); shape != nil; shape = shape.outer {
+		if shared, ok := ctx.sharedDefaults[sharedKey{shape: shape, feature: fv.Feature}]; ok {
+			return shared, true
+		}
+		if !shape.classifier {
+			break
+		}
+	}
+	return nil, false
+}
+
+// declaredWithin reports whether inst is root itself or an object root's declarations
+// materialize under it: held, at every step, by a declared composite value of an
+// unclassified object.
+func (ctx *Context) declaredWithin(inst, root *Instance) bool {
+	for inst != root {
+		if len(inst.classifiers) != 0 {
+			return false
+		}
+		owner, feature := inst.Owner()
+		if owner == nil {
+			return false
+		}
+		if held, ok := owner.FeatureValues[feature]; !ok || !held.declared() {
+			return false
+		}
+		inst = owner
+	}
+	return true
+}
+
+// singlyWithin reports whether inst is root itself or held under it by single-valued
+// features at every step, so a path of feature names from root names inst alone.
+func (ctx *Context) singlyWithin(inst, root *Instance) bool {
+	for inst != root {
+		owner, feature := inst.Owner()
+		if owner == nil {
+			return false
+		}
+		if held, ok := owner.FeatureValues[feature]; !ok || !held.Feature.Scalar() {
+			return false
+		}
+		inst = owner
+	}
+	return true
+}
+
+// sharedPaths turns the reads of a clean derivation on root into paths from root, in
+// the order they were read — those of declared values, and those taken as inputs
+// with the value read; nil when a binding anywhere on the chain to a read could
+// determine it differently on another occurrence.
+func (ctx *Context) sharedPaths(root *Instance, reads []sharedRead) (paths [][]string, inputs []sharedInput) {
+	seen := make(map[string]bool, len(reads))
+	paths = make([][]string, 0, len(reads))
+	for _, read := range reads {
+		var above []string
+		for inst := read.inst; inst != root; {
+			owner, feature := inst.Owner()
+			above = append(above, feature)
+			inst = owner
+		}
+		path := make([]string, 0, len(above)+len(read.path))
+		for i := len(above) - 1; i >= 0; i-- {
+			path = append(path, above[i])
+		}
+		path = append(path, read.path...)
+		key := pathKey(path)
+		if seen[key] {
+			continue
+		}
+		seen[key] = true
+		if ctx.bindingDeclaredFor(read.inst, strings.Join(read.path, ".")) {
+			return nil, nil
+		}
+		if read.valued {
+			inputs = append(inputs, sharedInput{path: path, value: read.value})
+		} else {
+			paths = append(paths, path)
+		}
+	}
+	return paths, inputs
+}
+
+// pathKey encodes a path so that no two segment sequences share a key: a quoted
+// feature name may itself contain the dot that separates segments.
+func pathKey(path []string) string {
+	var key strings.Builder
+	for _, segment := range path {
+		key.WriteString(strconv.Itoa(len(segment)))
+		key.WriteByte(':')
+		key.WriteString(segment)
+	}
+	return key.String()
+}
+
+// bindingDeclaredFor reports whether any type on the chain holding inst declares a
+// binding for the named feature, as resolveBindings would find one.
+func (ctx *Context) bindingDeclaredFor(inst *Instance, name string) bool {
+	path := name
+	for current := inst; current != nil; {
+		if len(ctx.bindingsForFeature(current.Type, path)) != 0 {
+			return true
+		}
+		for _, classifier := range current.classifiers {
+			if len(ctx.bindingsForFeature(classifier, path)) != 0 {
+				return true
+			}
+		}
+		owner, ownerFeature := current.Owner()
+		if owner == nil || ownerFeature == "" {
+			return false
+		}
+		path = ownerFeature + "." + path
+		current = owner
+	}
+	return false
+}
+
+// shareDerived records val as the derived default of fv's feature for inst's shape,
+// when the derivation was clean and the value can be held by every occurrence.
+func (ctx *Context) shareDerived(inst *Instance, fv *FeatureValue, val Value, clean bool, reads []sharedRead) {
+	if !clean || !shareable(val) || !ctx.sharesDefault(inst, fv) {
+		return
+	}
+	paths, inputs := ctx.sharedPaths(inst, reads)
+	if paths == nil || len(inputs) != 0 {
+		return
+	}
+	key := sharedKey{shape: ctx.shapeOf(inst), feature: fv.Feature}
+	if prior, ok := ctx.sharedDefaults[key]; ok {
+		ctx.noteProbeUndo(func() { ctx.sharedDefaults[key] = prior })
+	} else {
+		ctx.noteProbeUndo(func() { delete(ctx.sharedDefaults, key) })
+	}
+	ctx.sharedDefaults[key] = &sharedDefault{value: val, paths: paths}
+}
+
+// takeShared holds on fv, unmaterialized on inst, the value its shape derived for the
+// feature, if one is on record and every value that derivation read is, on inst, still
+// as declared or not yet materialized. What it would have read is listed as read, and
+// what it did not materialize on the way is owed (see settleOwed).
+func (ctx *Context) takeShared(inst *Instance, fv *FeatureValue) bool {
+	if !ctx.sharesDefault(inst, fv) {
+		return false
+	}
+	shared, ok := ctx.sharedDefaults[sharedKey{shape: ctx.shapeOf(inst), feature: fv.Feature}]
+	if !ok {
+		return false
+	}
+	var sources []*FeatureValue
+	owes := false
+	for _, path := range shared.paths {
+		if ctx.bindingDeclaredFor(inst, strings.Join(path, ".")) {
+			return false
+		}
+		var eligible bool
+		before := len(sources)
+		if sources, eligible = ctx.declaredAlong(inst, path, sources); !eligible {
+			return false
+		}
+		for _, src := range sources[before:] {
+			owes = owes || !src.Materialized
+		}
+	}
+	ctx.noteProbeWrite(fv)
+	if ctx.derivable(fv) {
+		ctx.forgetReads(fv)
+		for _, src := range sources {
+			if src != fv {
+				ctx.listRead(src, fv)
+			}
+		}
+	}
+	fv.Value = shared.value
+	fv.Materialized, fv.intrinsic = true, true
+	if owes {
+		inst.owe(ctx, fv, shared)
+	}
+	taken := ctx.sharedTaken
+	ctx.noteProbeUndo(func() { ctx.sharedTaken = taken })
+	ctx.sharedTaken++
+	return true
+}
+
+// declaredAlong follows path from inst, appending to sources every feature value on
+// the way; eligible while each is as declared, stopping at one not yet materialized.
+// A destroyed object on the way holds nothing to read, so nothing along it is eligible.
+func (ctx *Context) declaredAlong(inst *Instance, path []string, sources []*FeatureValue) ([]*FeatureValue, bool) {
+	if _, destroyed := ctx.Destroyed(inst); destroyed {
+		return sources, false
+	}
+	fv, ok := inst.FeatureValues[path[0]]
+	if !ok {
+		return sources, false
+	}
+	sources = append(sources, fv)
+	if !fv.Materialized {
+		return sources, true
+	}
+	if !fv.declared() {
+		return sources, false
+	}
+	if len(path) == 1 {
+		return sources, true
+	}
+	for _, held := range elementsOf(fv.HeldValue()) {
+		child, ok := ctx.instances[held.Instance]
+		if held.Kind != ValInstance || !ok || len(child.classifiers) != 0 {
+			return sources, false
+		}
+		if sources, ok = ctx.declaredAlong(child, path[1:], sources); !ok {
+			return sources, false
+		}
+	}
+	return sources, true
+}
+
+// owe records that fv took shared before materializing all its derivation read;
+// the journal under way forgets it with the take.
+func (inst *Instance) owe(ctx *Context, fv *FeatureValue, shared *sharedDefault) {
+	for i := range inst.owed {
+		if inst.owed[i].fv == fv {
+			prior := inst.owed[i].shared
+			ctx.noteProbeUndo(func() { inst.owed[i].shared = prior })
+			inst.owed[i].shared = shared
+			return
+		}
+	}
+	n := len(inst.owed)
+	ctx.noteProbeUndo(func() { inst.owed = inst.owed[:n] })
+	inst.owed = append(inst.owed, owedDefault{fv: fv, shared: shared})
+}
+
+// settleOwed materializes, on inst and each object holding it, what the values they
+// took shared would have materialized to be derived in place: an object about to
+// be classified reads as one whose values were all derived on it.
+func (ctx *Context) settleOwed(inst *Instance) error {
+	for ; inst != nil; inst, _ = inst.Owner() {
+		owed, at := inst.owed, inst
+		if len(owed) == 0 {
+			continue
+		}
+		ctx.noteProbeUndo(func() { at.owed = owed })
+		at.owed = nil
+		for _, o := range owed {
+			if !o.fv.declared() {
+				continue
+			}
+			for _, path := range o.shared.paths {
+				if err := ctx.materializeAlong(at, path); err != nil {
+					return err
+				}
+			}
+		}
+	}
+	return nil
+}
+
+// materializeAlong reads every feature value on path from inst.
+func (ctx *Context) materializeAlong(inst *Instance, path []string) error {
+	fv, err := inst.GetFeatureValue(ctx, path[0])
+	if err != nil {
+		return err
+	}
+	if len(path) == 1 {
+		return nil
+	}
+	for _, held := range elementsOf(fv.HeldValue()) {
+		if child, ok := ctx.instances[held.Instance]; held.Kind == ValInstance && ok {
+			if err := ctx.materializeAlong(child, path[1:]); err != nil {
+				return err
+			}
+		}
+	}
+	return nil
+}
diff --git a/internal/exec/runtime/shared_default_test.go b/internal/exec/runtime/shared_default_test.go
new file mode 100644
index 0000000000..b73b9ae126
--- /dev/null
+++ b/internal/exec/runtime/shared_default_test.go
@@ -0,0 +1,820 @@
+package runtime
+
+import (
+	"errors"
+	"slices"
+	"strconv"
+	"strings"
+	"testing"
+
+	"github.com/Open-MBEE/OpenSysML/internal/semantic/symbols"
+)
+
+// sharedFixture indexes src with derived-default sharing on and instantiates the
+// named part, returning it with the context and index.
+func sharedFixture(t *testing.T, src, part string) (*Context, *Instance, *symbols.Index) {
+	t.Helper()
+	ctx, idx := contextForSource(t, src)
+	ctx.SetSharedDefaults(true)
+	inst, err := ctx.Instantiate(lookupOne(t, idx, part))
+	if err != nil {
+		t.Fatalf("instantiate %s: %v", part, err)
+	}
+	return ctx, inst, idx
+}
+
+// at follows a dotted path of features from inst, indexing a collection element
+// one-based as `sats.2`, and returns the object reached.
+func at(t *testing.T, ctx *Context, inst *Instance, path string) *Instance {
+	t.Helper()
+	for _, step := range strings.Split(path, ".") {
+		if step == "" {
+			continue
+		}
+		name, index := step, 0
+		if i := strings.IndexByte(step, '['); i >= 0 {
+			name = step[:i]
+			for _, c := range step[i+1 : len(step)-1] {
+				index = index*10 + int(c-'0')
+			}
+		}
+		fv, err := inst.GetFeatureValue(ctx, name)
+		if err != nil {
+			t.Fatalf("%s: %v", path, err)
+		}
+		held := elementsOf(fv.HeldValue())
+		if index > 0 {
+			held = held[index-1 : index]
+		}
+		if len(held) != 1 {
+			t.Fatalf("%s: %s holds %d objects, want one", path, name, len(held))
+		}
+		id, ok := held[0].Object()
+		if !ok {
+			t.Fatalf("%s: %s holds no object", path, name)
+		}
+		inst, _ = ctx.Instance(id)
+	}
+	return inst
+}
+
+// read reads the named feature of the object at path and formats it.
+func read(t *testing.T, ctx *Context, inst *Instance, path, name string) string {
+	t.Helper()
+	fv, err := at(t, ctx, inst, path).GetFeatureValue(ctx, name)
+	if err != nil {
+		t.Fatalf("%s.%s: %v", path, name, err)
+	}
+	val, err := fv.ReadValue(name)
+	if err != nil {
+		t.Fatalf("%s.%s: %v", path, name, err)
+	}
+	return FormatValue(val)
+}
+
+// write sets the named feature of the object at path to an integer.
+func write(t *testing.T, ctx *Context, inst *Instance, path, name string, n int64) {
+	t.Helper()
+	if err := at(t, ctx, inst, path).SetFeatureValue(ctx, name, integerValue(n)); err != nil {
+		t.Fatalf("%s.%s = %d: %v", path, name, n, err)
+	}
+}
+
+// expect fails unless the named feature at path reads as want.
+func expect(t *testing.T, ctx *Context, inst *Instance, path, name, want string) {
+	t.Helper()
+	if got := read(t, ctx, inst, path, name); got != want {
+		t.Errorf("%s.%s = %s, want %s", path, name, got, want)
+	}
+}
+
+// expectTaken fails unless the context took the given number of shared defaults so far.
+func expectTaken(t *testing.T, ctx *Context, want int64) {
+	t.Helper()
+	if got := ctx.SharedDefaultsTaken(); got != want {
+		t.Errorf("shared defaults taken = %d, want %d", got, want)
+	}
+}
+
+const fleetSrc = `package test {
+	part def Sat {
+		attribute a : ScalarValues::Integer = 2;
+		attribute b : ScalarValues::Integer = a * 3;
+	}
+	part def Fleet {
+		part sats : Sat[3];
+	}
+	part fleet : Fleet;
+}`
+
+// A derived default read on one occurrence is taken by the others of the shape
+// without deriving again, and reads the same.
+func TestSharedDefaultTakenByOccurrencesOfShape(t *testing.T) {
+	ctx, fleet, _ := sharedFixture(t, fleetSrc, "test::fleet")
+	for i := 1; i <= 3; i++ {
+		expect(t, ctx, fleet, "sats["+string(rune('0'+i))+"]", "b", "6")
+	}
+	expectTaken(t, ctx, 2)
+}
+
+// Every scalar kind held by value — number, string, quantity, complex, enum
+// literal — is shared; a value naming an object or a sequence is derived on each.
+func TestSharedDefaultKinds(t *testing.T) {
+	idx, _, ctx := buildRuntimeWithLibraries(t, "<test>", parseAndBuild(t, `package test {
+	private import SI::*;
+	enum def Band { L; S; }
+	part def Radio { attribute gain : ScalarValues::Real = 3.0; }
+	part def Sat {
+		attribute n : ScalarValues::Integer = 2;
+		attribute s : ScalarValues::String = "sat-" + "x";
+		attribute q = n * 5 [kg];
+		attribute z = ComplexFunctions::rect(1.0, n);
+		attribute band : Band = Band::S;
+		attribute chosen : Band = band;
+		part radio : Radio;
+		attribute r = radio;
+		attribute seq : ScalarValues::Integer[2] = (n, n + 1);
+	}
+	part def Fleet { part sats : Sat[3]; }
+	part fleet : Fleet;
+}`))
+	ctx.SetSharedDefaults(true)
+	fleet, err := ctx.Instantiate(lookupOne(t, idx, "test::fleet"))
+	if err != nil {
+		t.Fatalf("instantiate: %v", err)
+	}
+	shared := map[string]string{"s": `"sat-x"`, "q": "10 [kg]", "z": "1.0 + 2.0i", "chosen": "Band::S"}
+	own := map[string]string{"r": "", "seq": "[2, 3]"}
+	for name, want := range shared {
+		for i := 1; i <= 3; i++ {
+			expect(t, ctx, fleet, "sats["+string(rune('0'+i))+"]", name, want)
+		}
+	}
+	expectTaken(t, ctx, int64(2*len(shared)))
+	for name, want := range own {
+		for i := 1; i <= 3; i++ {
+			got := read(t, ctx, fleet, "sats["+string(rune('0'+i))+"]", name)
+			if want != "" && got != want {
+				t.Errorf("sats[%d].%s = %s, want %s", i, name, got, want)
+			}
+		}
+	}
+	expectTaken(t, ctx, int64(2*len(shared)))
+	radios := map[string]bool{}
+	for i := 1; i <= 3; i++ {
+		radios[read(t, ctx, fleet, "sats["+string(rune('0'+i))+"]", "r")] = true
+	}
+	if len(radios) != 3 {
+		t.Errorf("r names %d distinct objects over three occurrences, want 3", len(radios))
+	}
+}
+
+// An occurrence whose input diverged before the read derives its own value; one
+// diverging after taking a shared value is invalidated like a value derived in place.
+func TestSharedDefaultFollowsDivergence(t *testing.T) {
+	ctx, fleet, _ := sharedFixture(t, fleetSrc, "test::fleet")
+	write(t, ctx, fleet, "sats[2]", "a", 5)
+	expect(t, ctx, fleet, "sats[1]", "b", "6")
+	expect(t, ctx, fleet, "sats[2]", "b", "15")
+	expect(t, ctx, fleet, "sats[3]", "b", "6")
+	expectTaken(t, ctx, 1)
+	write(t, ctx, fleet, "sats[3]", "a", 7)
+	expect(t, ctx, fleet, "sats[3]", "b", "21")
+	expect(t, ctx, fleet, "sats[1]", "b", "6")
+	expectTaken(t, ctx, 1)
+}
+
+// A value derived on a diverged occurrence is that occurrence's own: the shape
+// does not take it.
+func TestDivergedOccurrenceDoesNotShareItsDefault(t *testing.T) {
+	ctx, fleet, _ := sharedFixture(t, fleetSrc, "test::fleet")
+	write(t, ctx, fleet, "sats[1]", "a", 5)
+	expect(t, ctx, fleet, "sats[1]", "b", "15")
+	expect(t, ctx, fleet, "sats[2]", "b", "6")
+	expect(t, ctx, fleet, "sats[3]", "b", "6")
+	expectTaken(t, ctx, 1)
+}
+
+const subtreeSrc = `package test {
+	part def Comp {
+		attribute m : ScalarValues::Integer = 3;
+	}
+	part def Sat {
+		part c1 : Comp;
+		part c2 : Comp {
+			attribute :>> m = 4;
+		}
+		attribute total : ScalarValues::Integer = c1.m + c2.m;
+	}
+	part def Fleet {
+		part sats : Sat[3];
+	}
+	part fleet : Fleet;
+}`
+
+// A default read through the occurrence's own subtree is taken without
+// materializing that subtree, and a later write under it still invalidates the value.
+func TestSharedDefaultOverSubtreeInvalidatedByLaterWrite(t *testing.T) {
+	ctx, fleet, _ := sharedFixture(t, subtreeSrc, "test::fleet")
+	expect(t, ctx, fleet, "sats[1]", "total", "7")
+	expect(t, ctx, fleet, "sats[2]", "total", "7")
+	expectTaken(t, ctx, 1)
+	if fv := at(t, ctx, fleet, "sats[2]").FeatureValues["c1"]; fv.Materialized {
+		t.Error("sats[2].c1 was materialized to take a shared total")
+	}
+	write(t, ctx, fleet, "sats[2].c1", "m", 10)
+	expect(t, ctx, fleet, "sats[2]", "total", "14")
+	expect(t, ctx, fleet, "sats[1]", "total", "7")
+	write(t, ctx, fleet, "sats[3].c2", "m", 1)
+	expect(t, ctx, fleet, "sats[3]", "total", "4")
+	expectTaken(t, ctx, 1)
+}
+
+// Turning sharing off leaves every occurrence deriving for itself.
+func TestSharedDefaultsOffDerivesEverywhere(t *testing.T) {
+	ctx, idx := contextForSource(t, fleetSrc)
+	ctx.SetSharedDefaults(false)
+	fleet, err := ctx.Instantiate(lookupOne(t, idx, "test::fleet"))
+	if err != nil {
+		t.Fatal(err)
+	}
+	for i := 1; i <= 3; i++ {
+		expect(t, ctx, fleet, "sats["+string(rune('0'+i))+"]", "b", "6")
+	}
+	expectTaken(t, ctx, 0)
+}
+
+const classifiedFleetSrc = `package test {
+	part def Sat {
+		attribute a : ScalarValues::Integer = 2;
+		attribute b : ScalarValues::Integer = a * 3;
+	}
+	part def Heavy :> Sat {
+		attribute :>> a = 10;
+	}
+	part def Fleet {
+		part sats : Sat[3];
+	}
+	part fleet : Fleet;
+}`
+
+// A classifier redefining what a taken value read gives the occurrence its own
+// value, whether it is classified before or after the take; undoing the
+// classification with its change restores the shape's value.
+func TestSharedDefaultUnderClassification(t *testing.T) {
+	ctx, fleet, idx := sharedFixture(t, classifiedFleetSrc, "test::fleet")
+	heavy := lookupOne(t, idx, "test::Heavy")
+	expect(t, ctx, fleet, "sats[1]", "b", "6")
+	expect(t, ctx, fleet, "sats[2]", "b", "6")
+	expectTaken(t, ctx, 1)
+	if err := ctx.classify(at(t, ctx, fleet, "sats[2]"), heavy); err != nil {
+		t.Fatalf("classify sats[2]: %v", err)
+	}
+	expect(t, ctx, fleet, "sats[2]", "b", "30")
+	expect(t, ctx, fleet, "sats[1]", "b", "6")
+	if err := ctx.classify(at(t, ctx, fleet, "sats[3]"), heavy); err != nil {
+		t.Fatalf("classify sats[3]: %v", err)
+	}
+	expect(t, ctx, fleet, "sats[3]", "b", "30")
+	expectTaken(t, ctx, 2)
+
+	end := ctx.beginProbe()
+	if err := ctx.classify(at(t, ctx, fleet, "sats[1]"), heavy); err != nil {
+		t.Fatalf("classify sats[1]: %v", err)
+	}
+	expect(t, ctx, fleet, "sats[1]", "b", "30")
+	end()
+	expect(t, ctx, fleet, "sats[1]", "b", "6")
+}
+
+const failingDefaultSrc = `package test {
+	part def Sat {
+		attribute a : ScalarValues::Integer = 2;
+		attribute b : ScalarValues::Integer = a / 0;
+	}
+	part def Fleet {
+		part sats : Sat[2];
+	}
+	part fleet : Fleet;
+}`
+
+// A default that fails to derive is never shared: every occurrence reports the
+// failure for itself, the same way it would deriving in place.
+func TestSharedDefaultFailureIsNotShared(t *testing.T) {
+	ctx, fleet, _ := sharedFixture(t, failingDefaultSrc, "test::fleet")
+	var errs []string
+	for _, path := range []string{"sats[1]", "sats[2]"} {
+		_, err := at(t, ctx, fleet, path).GetFeatureValue(ctx, "b")
+		if err == nil {
+			t.Fatalf("%s.b derived from a division by zero", path)
+		}
+		errs = append(errs, err.Error())
+	}
+	if errs[0] != errs[1] {
+		t.Errorf("the occurrences fail differently:\n%s\n%s", errs[0], errs[1])
+	}
+	expectTaken(t, ctx, 0)
+}
+
+const imagedFleetSrc = `package test {
+	part def Comp {
+		attribute m : ScalarValues::Integer = 3;
+	}
+	part def Sat {
+		part c1 : Comp;
+		attribute total : ScalarValues::Integer = c1.m + 1;
+		attribute twice : ScalarValues::Integer = total * 2;
+	}
+	part def Heavy :> Sat {
+		part :>> c1 { attribute :>> m = 9; }
+	}
+	part def Fleet {
+		part sats : Sat[2];
+	}
+	part fleet : Fleet;
+}`
+
+// An image of an occurrence that took a value shared over its unmaterialized
+// subtree materializes as one that derived it in place, still owing that subtree
+// and still sharing what its restored values derive: classifying and writing under
+// the restored object reach the value.
+func TestSharedDefaultSurvivesHeldImage(t *testing.T) {
+	ctx, fleet, idx := sharedFixture(t, imagedFleetSrc, "test::fleet")
+	expect(t, ctx, fleet, "sats[1]", "total", "4")
+	expect(t, ctx, fleet, "sats[2]", "total", "4")
+	expectTaken(t, ctx, 1)
+	if at(t, ctx, fleet, "sats[2]").FeatureValues["c1"].Materialized {
+		t.Fatal("sats[2].c1 was materialized to take a shared total")
+	}
+	dst := imageInto(t, ctx, fleet)
+	restored, ok := dst.Instance(fleet.ID)
+	if !ok {
+		t.Fatalf("object #%d not materialized from the image", fleet.ID)
+	}
+	if owed := at(t, dst, restored, "sats[2]").owed; len(owed) != 1 || owed[0].fv != at(t, dst, restored, "sats[2]").FeatureValues["total"] {
+		t.Errorf("restored sats[2] owes %d values, want its total", len(owed))
+	}
+	expect(t, dst, restored, "sats[1]", "twice", "8")
+	expect(t, dst, restored, "sats[2]", "twice", "8")
+	expectTaken(t, dst, 1)
+	if err := dst.classify(at(t, dst, restored, "sats[2]"), lookupOne(t, idx, "test::Heavy")); err != nil {
+		t.Fatalf("classify sats[2]: %v", err)
+	}
+	expect(t, dst, restored, "sats[2]", "total", "10")
+	write(t, dst, restored, "sats[1].c1", "m", 10)
+	expect(t, dst, restored, "sats[1]", "total", "11")
+	expect(t, ctx, fleet, "sats[1]", "total", "4")
+	expect(t, ctx, fleet, "sats[2]", "total", "4")
+}
+
+func TestPathKeyDistinguishesDottedNames(t *testing.T) {
+	quoted, nested := pathKey([]string{"a.b"}), pathKey([]string{"a", "b"})
+	if quoted == nested {
+		t.Fatalf("pathKey conflates a quoted 'a.b' with the nested path a.b: %q", quoted)
+	}
+	if pathKey([]string{"a", "b"}) != nested {
+		t.Fatal("pathKey is not stable over equal paths")
+	}
+}
+
+const collectionFleetSrc = `package test {
+	part def Comp {
+		attribute k : ScalarValues::Integer = 2;
+		attribute m : ScalarValues::Integer = k + 1;
+	}
+	part def HeavyComp :> Comp {
+		attribute :>> m = 9;
+	}
+	part def Sat {
+		part comps : Comp[2];
+		attribute total : ScalarValues::Integer = comps#(1).m + comps#(2).m;
+	}
+	part def Tagged :> Sat {
+		attribute tag : ScalarValues::Integer = 0;
+	}
+	part def Fleet {
+		part sats : Sat[2];
+	}
+	part fleet : Fleet;
+}`
+
+// A value taken over a collection some of whose elements were read already is owed
+// for the elements that were not: a classifier redeclaring the occurrence settles
+// them, and one redefining what a lazy element derives reaches the value.
+func TestSharedDefaultOwesEveryLazyElement(t *testing.T) {
+	ctx, fleet, idx := sharedFixture(t, collectionFleetSrc, "test::fleet")
+	expect(t, ctx, fleet, "sats[1]", "total", "6")
+	expect(t, ctx, fleet, "sats[2].comps[2]", "m", "3")
+	lazy := at(t, ctx, fleet, "sats[2].comps[1]").FeatureValues["m"]
+	if lazy.Materialized {
+		t.Fatal("sats[2].comps[1].m was materialized by reading comps[2].m")
+	}
+	expect(t, ctx, fleet, "sats[2]", "total", "6")
+	sat := at(t, ctx, fleet, "sats[2]")
+	if len(sat.owed) != 1 || sat.owed[0].fv != sat.FeatureValues["total"] {
+		t.Fatalf("sats[2] owes %d values, want its total", len(sat.owed))
+	}
+	if err := ctx.classify(sat, lookupOne(t, idx, "test::Tagged")); err != nil {
+		t.Fatalf("classify sats[2]: %v", err)
+	}
+	if !lazy.Materialized || len(sat.owed) != 0 {
+		t.Fatalf("classifying sats[2] left comps[1].m materialized=%v, owing %d", lazy.Materialized, len(sat.owed))
+	}
+	if err := ctx.classify(at(t, ctx, fleet, "sats[2].comps[1]"), lookupOne(t, idx, "test::HeavyComp")); err != nil {
+		t.Fatalf("classify sats[2].comps[1]: %v", err)
+	}
+	expect(t, ctx, fleet, "sats[2]", "total", "12")
+	expect(t, ctx, fleet, "sats[1]", "total", "6")
+}
+
+const extentFleetSrc = `package test {
+	private import SequenceFunctions::*;
+	part def Wheel;
+	part def Sat {
+		attribute wheelCount : ScalarValues::Natural = size(all Wheel);
+		assert constraint enough { size(all Wheel) >= 2 }
+	}
+}`
+
+// A value or verdict decided over the run's extent is the occurrence's own: another
+// occurrence of the shape sees the objects made since, not what the first one counted.
+func TestExtentIsNotSharedBetweenOccurrences(t *testing.T) {
+	ctx, idx := libraryShapeContext(t, extentFleetSrc)
+	ctx.SetSharedDefaults(true)
+	defer ctx.ShareVerdicts()()
+	root := idx.DocumentRoot("<test>")
+	make := func(name string) *Instance {
+		inst, err := ctx.Instantiate(lookupOne(t, idx, name))
+		if err != nil {
+			t.Fatalf("instantiate %s: %v", name, err)
+		}
+		return inst
+	}
+	verdict := func(sat *Instance) string {
+		report, err := ctx.ValidateObject(sat, []*symbols.Scope{root})
+		if err != nil {
+			t.Fatalf("validate #%d: %v", sat.ID, err)
+		}
+		if len(report.Verdicts) != 1 {
+			t.Fatalf("#%d has %d verdicts, want its one constraint", sat.ID, len(report.Verdicts))
+		}
+		return report.Verdicts[0].Status.String()
+	}
+	make("test::Wheel")
+	first := make("test::Sat")
+	expect(t, ctx, first, "", "wheelCount", "1")
+	if got := verdict(first); got != "violated" {
+		t.Errorf("enough on the first sat = %s, want violated", got)
+	}
+	make("test::Wheel")
+	second := make("test::Sat")
+	expect(t, ctx, second, "", "wheelCount", "2")
+	if got := verdict(second); got != "holds" {
+		t.Errorf("enough on the second sat = %s, want holds", got)
+	}
+	expectTaken(t, ctx, 0)
+	if taken := ctx.SharedVerdictsTaken(); taken != 0 {
+		t.Errorf("shared verdicts taken = %d, want none over the extent", taken)
+	}
+}
+
+// A materialization that fails after installing the image's shared records takes them
+// off again: the destination's shared table is as the failed image found it.
+func TestSharedDefaultRecordsUndoneWithFailedImage(t *testing.T) {
+	ctx, fleet, _ := sharedFixture(t, imagedFleetSrc, "test::fleet")
+	expect(t, ctx, fleet, "sats[1]", "total", "4")
+	expect(t, ctx, fleet, "sats[2]", "total", "4")
+	img, err := ctx.Image(fleet)
+	if err != nil {
+		t.Fatalf("Image: %v", err)
+	}
+	sound := img.messages
+	inBody := Value{Kind: ValFunction, ref: &functionValue{
+		shape:     &calcShape{Sym: &symbols.Symbol{Name: "inBody"}, Name: "inBody"},
+		enclosing: []frame{{vars: map[string]Value{"k": integerValue(1)}, run: 1}},
+	}}
+	img.messages = append(slices.Clone(sound), Message{Object: fleet.ID, SignalType: "go", Payload: map[string]Value{"k": inBody}})
+	dst := NewContext(ctx.Model(), 10000)
+	var notPortable *NotPortableError
+	if err := img.Materialize(dst); !errors.As(err, &notPortable) {
+		t.Fatalf("Materialize with a message it cannot carry = %v, want a NotPortableError", err)
+	}
+	if n := len(dst.sharedDefaults); n != 0 {
+		t.Errorf("the failed materialization left %d shared records on the destination", n)
+	}
+	img.messages = sound
+	if err := img.Materialize(dst); err != nil {
+		t.Fatalf("Materialize after the failure: %v", err)
+	}
+	restored, ok := dst.Instance(fleet.ID)
+	if !ok {
+		t.Fatalf("object #%d not materialized from the image", fleet.ID)
+	}
+	expect(t, dst, restored, "sats[1]", "twice", "8")
+	expect(t, dst, restored, "sats[2]", "twice", "8")
+	expectTaken(t, dst, 1)
+}
+
+// Restoring a snapshot rewinds what occurrences took from the shared table along
+// with the values they took: the count reads as it did at the snapshot, and the
+// takes since are made again on the way back.
+func TestSharedDefaultsTakenRestoredWithSnapshot(t *testing.T) {
+	ctx, fleet, _ := sharedFixture(t, fleetSrc, "test::fleet")
+	expect(t, ctx, fleet, "sats[1]", "b", "6")
+	snapshot, err := ctx.Snapshot()
+	if err != nil {
+		t.Fatalf("Snapshot: %v", err)
+	}
+	defer snapshot.Release()
+	expect(t, ctx, fleet, "sats[2]", "b", "6")
+	expect(t, ctx, fleet, "sats[3]", "b", "6")
+	expectTaken(t, ctx, 2)
+	snapshot.Restore()
+	expectTaken(t, ctx, 0)
+	if at(t, ctx, fleet, "sats[2]").FeatureValues["b"].Materialized {
+		t.Fatal("sats[2].b still materialized after the restore")
+	}
+	expect(t, ctx, fleet, "sats[2]", "b", "6")
+	expectTaken(t, ctx, 1)
+}
+
+// A probe's takes from the shared table are undone with the values it took: the
+// count reads as it did before the probe.
+func TestSharedDefaultsTakenUndoneWithProbe(t *testing.T) {
+	ctx, fleet, _ := sharedFixture(t, fleetSrc, "test::fleet")
+	expect(t, ctx, fleet, "sats[1]", "b", "6")
+	end := ctx.beginProbe()
+	expect(t, ctx, fleet, "sats[2]", "b", "6")
+	expectTaken(t, ctx, 1)
+	end()
+	expectTaken(t, ctx, 0)
+	if at(t, ctx, fleet, "sats[2]").FeatureValues["b"].Materialized {
+		t.Fatal("sats[2].b still materialized after the probe")
+	}
+	expect(t, ctx, fleet, "sats[2]", "b", "6")
+	expectTaken(t, ctx, 1)
+}
+
+const assumedFleetSrc = `package test {
+	part def Comp {
+		attribute k : ScalarValues::Integer = 2;
+	}
+	part def Sat {
+		part comps : Comp[2..*];
+		attribute n : ScalarValues::Integer = comps#(1).k + 1;
+	}
+	part def Fleet {
+		part sats : Sat[2];
+	}
+	part fleet : Fleet;
+}`
+
+// A population assumed to meet its multiplicity is imaged as assumed: restored, a
+// value derived over it stays the occurrence's own, as on the source.
+func TestAssumedPopulationSurvivesHeldImage(t *testing.T) {
+	ctx, fleet, _ := sharedFixture(t, assumedFleetSrc, "test::fleet")
+	expect(t, ctx, fleet, "sats[1]", "n", "3")
+	expect(t, ctx, fleet, "sats[2]", "n", "3")
+	expectTaken(t, ctx, 0)
+	if !at(t, ctx, fleet, "sats[1]").FeatureValues["comps"].Assumed {
+		t.Fatal("sats[1].comps is not assumed on the source")
+	}
+	dst := imageInto(t, ctx, fleet)
+	restored, ok := dst.Instance(fleet.ID)
+	if !ok {
+		t.Fatalf("object #%d not materialized from the image", fleet.ID)
+	}
+	for _, sat := range []string{"sats[1]", "sats[2]"} {
+		if !at(t, dst, restored, sat).FeatureValues["comps"].Assumed {
+			t.Errorf("restored %s.comps is no longer assumed", sat)
+		}
+	}
+	expect(t, dst, restored, "sats[1]", "n", "3")
+	expect(t, dst, restored, "sats[2]", "n", "3")
+	expectTaken(t, dst, 0)
+}
+
+// Adoption derives a taken value again, so it owes nothing: carried over and imaged
+// before it is read, the occurrence derives it on the destination as declared.
+func TestAdoptedOccurrenceOwesNothingForAValueDerivedAgain(t *testing.T) {
+	prev := contextOver(t, imagedFleetSrc)
+	prev.SetSharedDefaults(true)
+	fleet, err := prev.Instantiate(lookupOne(t, prev.Resolver().Index(), "test::fleet"))
+	if err != nil {
+		t.Fatalf("Instantiate: %v", err)
+	}
+	expect(t, prev, fleet, "sats[1]", "total", "4")
+	expect(t, prev, fleet, "sats[2]", "total", "4")
+	if owed := at(t, prev, fleet, "sats[2]").owed; len(owed) != 1 {
+		t.Fatalf("sats[2] owes %d values before the carry-over, want its total", len(owed))
+	}
+	shapes := prev.ShapesOf(fleet)
+	ctx := contextOver(t, imagedFleetSrc)
+	ctx.SetSharedDefaults(true)
+	if _, err := ctx.Adopt(prev, shapes, fleet); err != nil {
+		t.Fatalf("Adopt: %v", err)
+	}
+	if owed := at(t, ctx, fleet, "sats[2]").owed; len(owed) != 0 {
+		t.Errorf("adopted sats[2] owes %d values for a total derived again", len(owed))
+	}
+	dst := imageInto(t, ctx, fleet)
+	restored, ok := dst.Instance(fleet.ID)
+	if !ok {
+		t.Fatalf("object #%d not materialized from the image", fleet.ID)
+	}
+	if owed := at(t, dst, restored, "sats[2]").owed; len(owed) != 0 {
+		t.Errorf("restored sats[2] owes %d values, want none", len(owed))
+	}
+	expect(t, dst, restored, "sats[2]", "total", "4")
+	expect(t, dst, restored, "sats[1]", "total", "4")
+	expect(t, ctx, fleet, "sats[2]", "total", "4")
+}
+
+// A taken value invalidated by a write under its occurrence is imaged as what it is,
+// a value not yet derived: the destination derives it over the written value.
+func TestInvalidatedTakenValueIsImagedAsUnderived(t *testing.T) {
+	ctx, fleet, _ := sharedFixture(t, imagedFleetSrc, "test::fleet")
+	expect(t, ctx, fleet, "sats[1]", "total", "4")
+	expect(t, ctx, fleet, "sats[2]", "total", "4")
+	write(t, ctx, fleet, "sats[2].c1", "m", 10)
+	if at(t, ctx, fleet, "sats[2]").FeatureValues["total"].Materialized {
+		t.Fatal("sats[2].total still materialized over a written c1.m")
+	}
+	dst := imageInto(t, ctx, fleet)
+	restored, ok := dst.Instance(fleet.ID)
+	if !ok {
+		t.Fatalf("object #%d not materialized from the image", fleet.ID)
+	}
+	if owed := at(t, dst, restored, "sats[2]").owed; len(owed) != 0 {
+		t.Errorf("restored sats[2] owes %d values, want none", len(owed))
+	}
+	expect(t, dst, restored, "sats[2]", "total", "11")
+	expect(t, dst, restored, "sats[1]", "total", "4")
+	expect(t, ctx, fleet, "sats[2]", "total", "11")
+}
+
+const lifetimeFleetSrc = `package test {
+	private import OccurrenceFunctions::*;
+	requirement def Running {
+		subject s : Sat;
+		require constraint { isDuring(s.c1) }
+	}
+	part def Comp;
+	part def Sat {
+		part c1 : Comp;
+		attribute running : ScalarValues::Boolean = isDuring(c1);
+	}
+	part def Fleet {
+		part sats : Sat[2];
+	}
+	part fleet : Fleet {
+		satisfy Running by sats;
+	}
+}`
+
+// A lifetime is the run's, not the shape's: a default derived over one is the
+// occurrence's own, and an occurrence whose part has ended derives its own.
+func TestLifetimeReadsAreNotShared(t *testing.T) {
+	idx, _, ctx := buildRuntimeWithLibraries(t, "<test>", parseAndBuild(t, lifetimeFleetSrc))
+	ctx.SetSharedDefaults(true)
+	fleet, err := ctx.Instantiate(lookupOne(t, idx, "test::fleet"))
+	if err != nil {
+		t.Fatalf("instantiate: %v", err)
+	}
+	if err := ctx.destroy(at(t, ctx, fleet, "sats[2].c1")); err != nil {
+		t.Fatalf("destroy sats[2].c1: %v", err)
+	}
+	expect(t, ctx, fleet, "sats[1]", "running", "true")
+	expect(t, ctx, fleet, "sats[2]", "running", "false")
+	expectTaken(t, ctx, 0)
+}
+
+const drawingFleetSrc = `package test {
+	private import RandomFunctions::*;
+	requirement def Bounded {
+		subject s : Sat;
+		require constraint { uniform(0.0, 1.0) < 2.0 }
+	}
+	part def Sat {
+		attribute jitter : ScalarValues::Real = uniform(0.0, 1.0);
+	}
+	part def Fleet {
+		part sats : Sat[3];
+	}
+	part fleet : Fleet {
+		satisfy Bounded by sats;
+	}
+}`
+
+// A random draw is the run's, not the shape's: a default or a check that draws is
+// evaluated on every occurrence, so the stream is drawn from once per occurrence.
+func TestRandomDrawsAreNotShared(t *testing.T) {
+	idx, _, ctx := buildRuntimeWithLibraries(t, "<test>", parseAndBuild(t, drawingFleetSrc))
+	ctx.SetSharedDefaults(true)
+	ctx.SetModelSeed(7)
+	fleet, err := ctx.Instantiate(lookupOne(t, idx, "test::fleet"))
+	if err != nil {
+		t.Fatalf("instantiate: %v", err)
+	}
+	for i := 1; i <= 3; i++ {
+		read(t, ctx, fleet, "sats["+strconv.Itoa(i)+"]", "jitter")
+	}
+	if draws := ctx.DrawsTaken(); len(draws) != 3 {
+		t.Errorf("draws taken = %d after reading three defaults, want 3", len(draws))
+	}
+	expectTaken(t, ctx, 0)
+	done := ctx.ShareVerdicts()
+	report, err := ctx.ValidateObject(fleet, []*symbols.Scope{idx.DocumentRoot("<test>")})
+	done()
+	if err != nil {
+		t.Fatalf("validate: %v", err)
+	}
+	if !report.Valid() {
+		t.Errorf("report not valid: %+v", report.Verdicts)
+	}
+	if draws := ctx.DrawsTaken(); len(draws) != 6 {
+		t.Errorf("draws taken = %d after checking three occurrences, want 6", len(draws))
+	}
+	if taken := ctx.SharedVerdictsTaken(); taken != 0 {
+		t.Errorf("shared verdicts taken = %d over a check that draws, want 0", taken)
+	}
+}
+
+const clockFleetSrc = `package test {
+	requirement def Early {
+		subject s : Sat;
+		require constraint { s.localClock.currentTime < 5.0 }
+	}
+	part def Sat {
+		attribute stamp : ScalarValues::Real = localClock.currentTime + 1.0;
+	}
+	part def Fleet {
+		part sats : Sat[3];
+	}
+	part fleet : Fleet {
+		satisfy Early by sats;
+	}
+}`
+
+// The clock is the run's, not the shape's: a default or a check reading a Clock's
+// currentTime is evaluated on every occurrence, at the instant it is read.
+func TestClockReadsAreNotShared(t *testing.T) {
+	idx, _, ctx := buildRuntimeWithLibraries(t, "<test>", parseAndBuild(t, clockFleetSrc))
+	ctx.SetSharedDefaults(true)
+	fleet, err := ctx.Instantiate(lookupOne(t, idx, "test::fleet"))
+	if err != nil {
+		t.Fatalf("instantiate: %v", err)
+	}
+	for i := 1; i <= 2; i++ {
+		if got := read(t, ctx, fleet, "sats["+strconv.Itoa(i)+"]", "stamp"); got != "1.0" {
+			t.Errorf("sats[%d].stamp at t=0 = %s, want 1.0", i, got)
+		}
+	}
+	if _, err := ctx.Advance(10); err != nil {
+		t.Fatalf("advance: %v", err)
+	}
+	if got := read(t, ctx, fleet, "sats[3]", "stamp"); got != "11.0" {
+		t.Errorf("sats[3].stamp at t=10 = %s, want 11.0", got)
+	}
+	expectTaken(t, ctx, 0)
+	done := ctx.ShareVerdicts()
+	report, err := ctx.ValidateObject(fleet, []*symbols.Scope{idx.DocumentRoot("<test>")})
+	done()
+	if err != nil {
+		t.Fatalf("validate: %v", err)
+	}
+	if report.Valid() {
+		t.Errorf("report valid at t=10, want every check failed: %+v", report.Verdicts)
+	}
+	if taken := ctx.SharedVerdictsTaken(); taken != 0 {
+		t.Errorf("shared verdicts taken = %d over a check that reads the clock, want 0", taken)
+	}
+}
+
+// A part destroyed before its holder first reads through it is refused by the
+// eligibility walk, so the holder derives for itself and finds the part destroyed.
+func TestDestroyedPartIsNotReadThroughSharedDefault(t *testing.T) {
+	for _, on := range []bool{true, false} {
+		ctx, idx := contextForSource(t, subtreeSrc)
+		ctx.SetSharedDefaults(on)
+		fleet, err := ctx.Instantiate(lookupOne(t, idx, "test::fleet"))
+		if err != nil {
+			t.Fatalf("instantiate: %v", err)
+		}
+		expect(t, ctx, fleet, "sats[1]", "total", "7")
+		if err := ctx.destroy(at(t, ctx, fleet, "sats[2].c1")); err != nil {
+			t.Fatalf("destroy sats[2].c1: %v", err)
+		}
+		_, err = at(t, ctx, fleet, "sats[2]").GetFeatureValue(ctx, "total")
+		if !errors.Is(err, ErrOccurrenceDestroyed) {
+			t.Errorf("sharing=%v: sats[2].total over a destroyed c1: %v, want ErrOccurrenceDestroyed", on, err)
+		}
+		expect(t, ctx, fleet, "sats[3]", "total", "7")
+		if err := ctx.destroy(at(t, ctx, fleet, "sats[3]")); err != nil {
+			t.Fatalf("destroy sats[3]: %v", err)
+		}
+		if _, err := at(t, ctx, fleet, "sats[3]").GetFeatureValue(ctx, "total"); !errors.Is(err, ErrOccurrenceDestroyed) {
+			t.Errorf("sharing=%v: destroyed sats[3].total: %v, want ErrOccurrenceDestroyed", on, err)
+		}
+	}
+}
diff --git a/internal/exec/runtime/shared_verdict.go b/internal/exec/runtime/shared_verdict.go
new file mode 100644
index 0000000000..90967d9f8e
--- /dev/null
+++ b/internal/exec/runtime/shared_verdict.go
@@ -0,0 +1,234 @@
+package runtime
+
+import (
+	"strings"
+
+	"github.com/Open-MBEE/OpenSysML/internal/semantic/symbols"
+)
+
+// A check on an object whose conditions read only declared values decides the
+// same for every object of its shape those values are still as declared on; one
+// reading values not as declared decides the same for every object reading the same.
+// While verdicts are shared, the first check on each distinct input is on record and
+// the others take it.
+
+// ShareVerdicts opens a span over which checks on objects of one shape share their
+// verdicts; the function returned closes it. A span opened within another
+// continues it.
+func (ctx *Context) ShareVerdicts() (done func()) {
+	if ctx.verdicts != nil {
+		return func() {}
+	}
+	ctx.verdicts = &verdictMemo{verdicts: make(map[verdictKey][]*sharedVerdict)}
+	return func() { ctx.verdicts = nil }
+}
+
+// SharedVerdictsTaken counts the verdicts taken from the open span rather than
+// decided by evaluating; zero outside a span.
+func (ctx *Context) SharedVerdictsTaken() int {
+	if ctx.verdicts == nil {
+		return 0
+	}
+	return ctx.verdicts.taken
+}
+
+// verdictKey names one element checked one way on one shape: a requirement checked
+// directly and a satisfaction of it, which binds its subject, are two checks.
+type verdictKey struct {
+	element *symbols.Symbol
+	kind    string
+	shape   *shapeNode
+}
+
+// sharedVerdict is what a check decided about the first object of a shape reading
+// its inputs, with the paths of the declared values it read from that object, the
+// inputs it read not as declared, and the classifiers it gave it.
+type sharedVerdict struct {
+	inst       *Instance
+	result     CheckResult
+	err        error
+	paths      [][]string
+	inputs     []sharedInput
+	classified []*symbols.Symbol
+}
+
+// verdictMemo holds the verdicts shared over one span, one per distinct input of
+// each element checked on each shape.
+type verdictMemo struct {
+	verdicts map[verdictKey][]*sharedVerdict
+	taken    int
+}
+
+// checkOn resolves the object a check of carrying is about, then answers check on
+// it: shared across self's shape when self itself is that object, since finding it
+// walks structure no verdict depends on, else evaluated on the object resolved to.
+func (ctx *Context) checkOn(element *symbols.Symbol, kind, name string, carrying *symbols.Symbol, self *Instance, check func(carrier) (CheckResult, error)) (CheckResult, error) {
+	resolved, err := ctx.checkSubject(kind, name, carrying, self)
+	if err != nil {
+		return CheckResult{}, err
+	}
+	if resolved.instance != self {
+		return check(resolved)
+	}
+	return ctx.checkShared(element, kind, name, self, func() (CheckResult, error) { return check(resolved) })
+}
+
+// checkShared answers check on self: from the open span when a verdict of element on
+// self's shape is on record whose declared reads are as declared on self and whose
+// inputs self reads the same, else by evaluating it, which records the verdict when
+// it may stand for the shape. kind is how element is checked; name is how it is named
+// in self's messages.
+func (ctx *Context) checkShared(element *symbols.Symbol, kind, name string, self *Instance, check func() (CheckResult, error)) (CheckResult, error) {
+	memo := ctx.verdicts
+	if memo == nil || !ctx.sharing() || element == nil || self == nil {
+		return check()
+	}
+	shape := ctx.shapeOf(self)
+	if shape == nil {
+		return check()
+	}
+	key := verdictKey{element: element, kind: kind, shape: shape}
+	for _, shared := range memo.verdicts[key] {
+		if ctx.declaredAlongAll(self, shared.paths) && ctx.readsInputs(self, shared.inputs) && ctx.classifyAs(self, shared.classified) {
+			memo.taken++
+			return shared.on(self, name)
+		}
+	}
+	top := ctx.beginTraceOn(self, nil, ctx.behaviorRunDepth == 0)
+	result, err := check()
+	clean, reads, classified := ctx.endTraceClassified(top)
+	if !clean || !fansOut(result, err, self) {
+		return result, err
+	}
+	if paths, inputs := ctx.sharedPaths(self, reads); paths != nil {
+		memo.verdicts[key] = append(memo.verdicts[key], &sharedVerdict{
+			inst: self, result: result, err: err, paths: paths, inputs: inputs, classified: classified,
+		})
+	}
+	return result, err
+}
+
+// readsInputs reports whether inst reads, at the path of each input, the value the
+// shared check read: the same kind of value, equal, expressed the same way.
+func (ctx *Context) readsInputs(inst *Instance, inputs []sharedInput) bool {
+	for _, input := range inputs {
+		if ctx.bindingDeclaredFor(inst, strings.Join(input.path, ".")) {
+			return false
+		}
+		val, ok := ctx.readAlong(inst, input.path)
+		if !ok || !sameInput(val, input.value) {
+			return false
+		}
+	}
+	return true
+}
+
+// readAlong reads the value at path from inst, through single objects held on the way;
+// false when the path leads through a collection, an object with classifiers, or fails.
+func (ctx *Context) readAlong(inst *Instance, path []string) (Value, bool) {
+	for len(path) > 1 {
+		fv, err := inst.GetFeatureValue(ctx, path[0])
+		if err != nil || !fv.Feature.Scalar() {
+			return Value{}, false
+		}
+		held := fv.HeldValue()
+		child, ok := ctx.instances[held.Instance]
+		if held.Kind != ValInstance || !ok || len(child.classifiers) != 0 {
+			return Value{}, false
+		}
+		inst, path = child, path[1:]
+	}
+	fv, err := inst.GetFeatureValue(ctx, path[0])
+	if err != nil {
+		return Value{}, false
+	}
+	return fv.Value, true
+}
+
+// sameInput reports whether two values a check read are indistinguishable to it:
+// one kind, equal, and for a number or quantity carried and expressed the same way.
+func sameInput(a, b Value) bool {
+	if a.Kind != b.Kind || !valueEqual(a, b) {
+		return false
+	}
+	switch a.Kind {
+	case ValConst:
+		return a.Const.Kind == b.Const.Kind
+	case ValQuantity:
+		return a.Quantity().Unit.Text == b.Quantity().Unit.Text
+	}
+	return true
+}
+
+// classifyAs gives inst the classifiers a shared check gave the object it was decided
+// on, as one transaction; false, with inst as it was, when one is refused.
+func (ctx *Context) classifyAs(inst *Instance, classified []*symbols.Symbol) bool {
+	if len(classified) == 0 {
+		return true
+	}
+	commit, rollback := ctx.beginJournal()
+	for _, typ := range classified {
+		if err := ctx.classify(inst, typ); err != nil {
+			rollback()
+			return false
+		}
+	}
+	commit()
+	return true
+}
+
+// on restates the verdict about inst, named name in its message.
+func (v *sharedVerdict) on(inst *Instance, name string) (CheckResult, error) {
+	result := v.result
+	if result.Subject == v.inst {
+		result.Subject = inst
+	}
+	if result.SubjectRoot == v.inst {
+		result.SubjectRoot = inst
+	}
+	err := v.err
+	if violation, ok := err.(*ViolationError); ok {
+		restated := *violation
+		restated.Element = name
+		err = &restated
+	}
+	return result, err
+}
+
+// fansOut reports whether a verdict about inst is one every object of its shape may
+// take: it resolved to inst itself or to no object, and its error, if any, states
+// only the condition violated.
+func fansOut(result CheckResult, err error, inst *Instance) bool {
+	if result.Subject != nil && result.Subject != inst {
+		return false
+	}
+	if err == nil {
+		return true
+	}
+	_, violation := err.(*ViolationError)
+	return violation
+}
+
+// declaredAlongAll reports whether every path from inst leads through values as
+// declared, or not yet materialized, with no binding declared over any of them.
+func (ctx *Context) declaredAlongAll(inst *Instance, paths [][]string) bool {
+	for _, path := range paths {
+		if ctx.bindingDeclaredFor(inst, strings.Join(path, ".")) {
+			return false
+		}
+		if _, eligible := ctx.declaredAlong(inst, path, nil); !eligible {
+			return false
+		}
+	}
+	return true
+}
+
+// sharedElement is the element a satisfaction assertion's verdict is shared under:
+// the requirement it references when the assertion states nothing of its own, so
+// two assertions of it about objects of one shape share; else the assertion.
+func sharedElement(a *SatisfyAssertion) *symbols.Symbol {
+	if a.Requirement != nil && !a.Negated && len(unwrappedDeclMembers(a.Symbol.Decl)) == 0 {
+		return a.Requirement
+	}
+	return a.Symbol
+}
diff --git a/internal/exec/runtime/shared_verdict_test.go b/internal/exec/runtime/shared_verdict_test.go
new file mode 100644
index 0000000000..14c8717426
--- /dev/null
+++ b/internal/exec/runtime/shared_verdict_test.go
@@ -0,0 +1,444 @@
+package runtime
+
+import (
+	"fmt"
+	"strings"
+	"testing"
+
+	"github.com/Open-MBEE/OpenSysML/internal/semantic/symbols"
+)
+
+// sparseSides instantiates and validates the named part with sharing on and off,
+// returning both readings and how much the sharing side shared.
+func sparseSides(t *testing.T, src, part string) (sharing, materializing string, shared int) {
+	t.Helper()
+	ctx, idx := contextForSource(t, src)
+	ctx.SetSharedDefaults(true)
+	sym := lookupOne(t, idx, part)
+	root := idx.DocumentRoot("<test>")
+	sharing, shared = sparseReading(ctx, sym, root)
+	off, _ := contextForSource(t, src)
+	off.SetSharedDefaults(false)
+	materializing, _ = sparseReading(off, sym, root)
+	if sharing != materializing {
+		t.Errorf("sharing reads differently from materializing\n--- sharing\n%s\n--- materializing\n%s", sharing, materializing)
+	}
+	return sharing, materializing, shared
+}
+
+// verdictLines are the verdict lines of a reading, in report order.
+func verdictLines(reading string) []string {
+	var out []string
+	for _, line := range strings.Split(reading, "\n") {
+		if strings.HasPrefix(line, "constraint ") || strings.HasPrefix(line, "requirement ") || strings.HasPrefix(line, "satisfaction ") {
+			out = append(out, line)
+		}
+	}
+	return out
+}
+
+const mixedVerdictSrc = `package test {
+	part def Sat {
+		attribute a : ScalarValues::Integer = 2;
+		attribute b : ScalarValues::Integer = a * 3;
+		assert constraint light { b <= 10 }
+		requirement fits { require constraint { b < 20 } }
+	}
+	part def Fleet {
+		part sats : Sat[5];
+		part heavy :> sats {
+			attribute :>> a = 5;
+		}
+		part huge :> sats {
+			attribute :>> a = 9;
+		}
+	}
+	part fleet : Fleet;
+}`
+
+// Verdicts over occurrences of one shape are decided once and fanned out; an
+// occurrence with its own value is decided on its own, in the same report order.
+func TestSharedVerdictsOverMixedShapes(t *testing.T) {
+	reading, _, shared := sparseSides(t, mixedVerdictSrc, "test::fleet")
+	lines := verdictLines(reading)
+	want := []string{
+		`constraint "assert constraint light" on "sats[1]": violated (constraint light: assertion evaluated to false: b <= 10)`,
+		`requirement "requirement fits" on "sats[1]": holds`,
+		`constraint "assert constraint light" on "sats[2]": violated (constraint light: assertion evaluated to false: b <= 10)`,
+		`requirement "requirement fits" on "sats[2]": violated (requirement fits: require condition evaluated to false: b < 20)`,
+		`constraint "assert constraint light" on "sats[3]": holds`,
+		`requirement "requirement fits" on "sats[3]": holds`,
+		`constraint "assert constraint light" on "sats[4]": holds`,
+		`requirement "requirement fits" on "sats[4]": holds`,
+		`constraint "assert constraint light" on "sats[5]": holds`,
+		`requirement "requirement fits" on "sats[5]": holds`,
+	}
+	if strings.Join(lines, "\n") != strings.Join(want, "\n") {
+		t.Errorf("verdicts:\n%s\nwant:\n%s", strings.Join(lines, "\n"), strings.Join(want, "\n"))
+	}
+	if shared == 0 {
+		t.Error("no default or verdict shared over five occurrences")
+	}
+}
+
+// A satisfaction assertion about occurrences named by subsetting members shares
+// its verdict between those reading only declared values.
+func TestSharedSatisfactionVerdicts(t *testing.T) {
+	const src = `package test {
+	requirement def MassLimit {
+		subject s : Sat;
+		attribute limit : ScalarValues::Integer = 10;
+		require constraint { s.b <= limit }
+	}
+	part def Sat {
+		attribute a : ScalarValues::Integer = 2;
+		attribute b : ScalarValues::Integer = a * 3;
+	}
+	part def Fleet {
+		part sats : Sat[4];
+		part unit1 :> sats;
+		part unit2 :> sats;
+		part unit3 :> sats {
+			attribute :>> a = 5;
+		}
+	}
+	part fleet : Fleet {
+		satisfy MassLimit by unit1;
+		satisfy MassLimit by unit2;
+		satisfy MassLimit by unit3;
+	}
+}`
+	reading, _, _ := sparseSides(t, src, "test::fleet")
+	lines := verdictLines(reading)
+	want := []string{
+		`satisfaction "satisfy MassLimit by unit1" on "sats[1]": holds`,
+		`satisfaction "satisfy MassLimit by unit2" on "sats[2]": holds`,
+		`satisfaction "satisfy MassLimit by unit3" on "sats[3]": violated (satisfaction satisfy MassLimit by unit3: require condition evaluated to false: s.b <= limit)`,
+	}
+	if strings.Join(lines, "\n") != strings.Join(want, "\n") {
+		t.Errorf("verdicts:\n%s\nwant:\n%s", strings.Join(lines, "\n"), strings.Join(want, "\n"))
+	}
+}
+
+// A condition deciding on the identity of its bound subject or actor compares it
+// with an object it reads outside the occurrence, which makes the check the
+// occurrence's own: nothing is shared, and each occurrence gets its own verdict.
+func TestSubjectIdentityIsNotShared(t *testing.T) {
+	const src = `package test {
+	requirement def IsLead {
+		subject s : Sat;
+		require constraint { s == fleet.lead }
+	}
+	requirement def IsLeadActor {
+		subject s : Sat;
+		actor chief : Sat = fleet.lead;
+		require constraint { s == chief }
+	}
+	requirement def IsOwnTwin {
+		subject s : Sat;
+		require constraint { s == s.twin }
+	}
+	part def Sat {
+		attribute a : ScalarValues::Integer = 2;
+		ref part twin : Sat = fleet.lead;
+	}
+	part def Fleet {
+		part sats : Sat[3];
+		ref part lead : Sat = sats#(2);
+	}
+	part fleet : Fleet {
+		satisfy IsLead by sats;
+		satisfy IsLeadActor by sats;
+		satisfy IsOwnTwin by sats;
+	}
+}`
+	reading, _, shared := sparseSides(t, src, "test::fleet")
+	if shared != 0 {
+		t.Errorf("shared %d values or verdicts deciding on an object's identity", shared)
+	}
+	lines := verdictLines(reading)
+	want := []string{
+		`satisfaction "satisfy IsLead by sats" on "sats[1]": violated (satisfaction satisfy IsLead by sats: require condition evaluated to false: s == fleet.lead)`,
+		`satisfaction "satisfy IsLeadActor by sats" on "sats[1]": violated (satisfaction satisfy IsLeadActor by sats: require condition evaluated to false: s == chief)`,
+		`satisfaction "satisfy IsOwnTwin by sats" on "sats[1]": violated (satisfaction satisfy IsOwnTwin by sats: require condition evaluated to false: s == s.twin)`,
+		`satisfaction "satisfy IsLead by sats" on "sats[1].twin": holds`,
+		`satisfaction "satisfy IsLeadActor by sats" on "sats[1].twin": holds`,
+		`satisfaction "satisfy IsOwnTwin by sats" on "sats[1].twin": holds`,
+		`satisfaction "satisfy IsLead by sats" on "sats[3]": violated (satisfaction satisfy IsLead by sats: require condition evaluated to false: s == fleet.lead)`,
+		`satisfaction "satisfy IsLeadActor by sats" on "sats[3]": violated (satisfaction satisfy IsLeadActor by sats: require condition evaluated to false: s == chief)`,
+		`satisfaction "satisfy IsOwnTwin by sats" on "sats[3]": violated (satisfaction satisfy IsOwnTwin by sats: require condition evaluated to false: s == s.twin)`,
+	}
+	if strings.Join(lines, "\n") != strings.Join(want, "\n") {
+		t.Errorf("verdicts:\n%s\nwant:\n%s", strings.Join(lines, "\n"), strings.Join(want, "\n"))
+	}
+}
+
+// A requirement checked directly on the objects carrying it and a satisfaction of it
+// by those objects are two checks: the satisfaction binds the subject to the object
+// and reports under its own kind, so neither takes the other's verdict, while the
+// satisfactions of one shape still share theirs.
+func TestRequirementAndSatisfactionVerdictsAreNotShared(t *testing.T) {
+	const src = `package test {
+	part def Sat {
+		attribute mass : ScalarValues::Integer = 50;
+		requirement light {
+			require constraint { mass < 10 }
+		}
+		requirement bounded {
+			subject s : Sat;
+			require constraint { s.mass < 100 }
+		}
+	}
+	part def Fleet {
+		part sats : Sat[3];
+	}
+	part fleet : Fleet {
+		satisfy sats.light by sats;
+		satisfy sats.bounded by sats;
+	}
+}`
+	reading, _, shared := sparseSides(t, src, "test::fleet")
+	if shared == 0 {
+		t.Errorf("satisfactions of one shape shared nothing")
+	}
+	lines := verdictLines(reading)
+	want := []string{
+		`requirement "requirement light" on "sats[1]": violated (requirement light: require condition evaluated to false: mass < 10)`,
+		`requirement "requirement bounded" on "sats[1]": undecided (requirement bounded: require condition evaluation failed: no value for feature s)`,
+		`satisfaction "satisfy sats::light by sats" on "sats[1]": violated (satisfaction satisfy sats::light by sats: require condition evaluated to false: mass < 10)`,
+		`satisfaction "satisfy sats::bounded by sats" on "sats[1]": holds`,
+		`requirement "requirement light" on "sats[2]": violated (requirement light: require condition evaluated to false: mass < 10)`,
+		`requirement "requirement bounded" on "sats[2]": undecided (requirement bounded: require condition evaluation failed: no value for feature s)`,
+		`satisfaction "satisfy sats::light by sats" on "sats[2]": violated (satisfaction satisfy sats::light by sats: require condition evaluated to false: mass < 10)`,
+		`satisfaction "satisfy sats::bounded by sats" on "sats[2]": holds`,
+		`requirement "requirement light" on "sats[3]": violated (requirement light: require condition evaluated to false: mass < 10)`,
+		`requirement "requirement bounded" on "sats[3]": undecided (requirement bounded: require condition evaluation failed: no value for feature s)`,
+		`satisfaction "satisfy sats::light by sats" on "sats[3]": violated (satisfaction satisfy sats::light by sats: require condition evaluated to false: mass < 10)`,
+		`satisfaction "satisfy sats::bounded by sats" on "sats[3]": holds`,
+	}
+	if strings.Join(lines, "\n") != strings.Join(want, "\n") {
+		t.Errorf("verdicts:\n%s\nwant:\n%s", strings.Join(lines, "\n"), strings.Join(want, "\n"))
+	}
+}
+
+// Within a span a check is decided once per distinct input: occurrences as declared
+// take one verdict, occurrences written the same value another; none outside the span.
+func TestSharedVerdictsOncePerDistinctInput(t *testing.T) {
+	ctx, fleet, idx := sharedFixture(t, mixedVerdictSrc, "test::fleet")
+	light := lookupOne(t, idx, "test::Sat::light")
+	scope := lookupOne(t, idx, "test::Sat").Scope
+	done := ctx.ShareVerdicts()
+	defer done()
+	check := func(occurrence string, holds bool) {
+		t.Helper()
+		result, err := ctx.CheckConstraintOn(light, scope, at(t, ctx, fleet, occurrence))
+		if result.Holds != holds || (err == nil) != holds {
+			t.Fatalf("%s light = %v, %v; want holds %v", occurrence, result.Holds, err, holds)
+		}
+	}
+	expectTaken := func(want int) {
+		t.Helper()
+		if got := ctx.SharedVerdictsTaken(); got != want {
+			t.Errorf("verdicts taken = %d, want %d", got, want)
+		}
+	}
+	// Declared occurrences: decided once, taken by the second.
+	check("sats[3]", true)
+	check("sats[4]", true)
+	expectTaken(1)
+	// An occurrence with its own value is decided on its own inputs …
+	write(t, ctx, fleet, "sats[5]", "a", 4)
+	check("sats[5]", false)
+	expectTaken(1)
+	// … and another reading the same value takes that verdict; a third input is decided again.
+	write(t, ctx, fleet, "sats[4]", "a", 4)
+	check("sats[4]", false)
+	expectTaken(2)
+	write(t, ctx, fleet, "sats[3]", "a", 3)
+	check("sats[3]", true)
+	expectTaken(2)
+	write(t, ctx, fleet, "sats[5]", "a", 3)
+	check("sats[5]", true)
+	expectTaken(3)
+	done()
+	expectTaken(0)
+}
+
+// A traced context shares nothing: the trace records every check and derivation as
+// the materializing path makes them, and sharing resumes once the trace is detached.
+func TestTracedContextSharesNothing(t *testing.T) {
+	traced := func(share bool) (*TraceRecorder, string, int) {
+		ctx, idx := contextForSource(t, mixedVerdictSrc)
+		ctx.SetSharedDefaults(share)
+		tr := NewTraceRecorder()
+		ctx.SetTrace(tr)
+		reading, shared := sparseReading(ctx, lookupOne(t, idx, "test::fleet"), idx.DocumentRoot("<test>"))
+		return tr, reading, shared
+	}
+	sharingTrace, sharingReading, shared := traced(true)
+	materializingTrace, materializingReading, _ := traced(false)
+	if shared != 0 {
+		t.Errorf("a traced context shared %d evaluations", shared)
+	}
+	if len(sharingTrace.Entries()) == 0 {
+		t.Fatal("validating recorded no trace")
+	}
+	if sharingTrace.String() != materializingTrace.String() || sharingReading != materializingReading {
+		t.Errorf("traced sharing context differs from the materializing one\n--- sharing\n%s%s\n--- materializing\n%s%s",
+			sharingTrace, sharingReading, materializingTrace, materializingReading)
+	}
+
+	ctx, idx := contextForSource(t, mixedVerdictSrc)
+	ctx.SetSharedDefaults(true)
+	ctx.SetTrace(NewTraceRecorder())
+	ctx.SetTrace(nil)
+	if _, shared := sparseReading(ctx, lookupOne(t, idx, "test::fleet"), idx.DocumentRoot("<test>")); shared == 0 {
+		t.Error("nothing shared once the trace was detached")
+	}
+}
+
+// A condition deciding on a lifetime decides on the run's state of one occurrence:
+// nothing is shared, and an occurrence whose part has ended gets its own verdict.
+func TestLifetimeVerdictsAreNotShared(t *testing.T) {
+	idx, _, ctx := buildRuntimeWithLibraries(t, "<test>", parseAndBuild(t, lifetimeFleetSrc))
+	ctx.SetSharedDefaults(true)
+	fleet, err := ctx.Instantiate(lookupOne(t, idx, "test::fleet"))
+	if err != nil {
+		t.Fatalf("instantiate: %v", err)
+	}
+	if err := ctx.destroy(at(t, ctx, fleet, "sats[2].c1")); err != nil {
+		t.Fatalf("destroy sats[2].c1: %v", err)
+	}
+	done := ctx.ShareVerdicts()
+	defer done()
+	report, err := ctx.ValidateObject(fleet, []*symbols.Scope{idx.DocumentRoot("<test>")})
+	if err != nil {
+		t.Fatalf("validate: %v", err)
+	}
+	var lines []string
+	for _, v := range report.Verdicts {
+		if v.Kind == "satisfaction" {
+			lines = append(lines, fmt.Sprintf("%s on %q: %s", v.Kind, strings.Join(v.Path, "."), v.Status))
+		}
+	}
+	want := []string{
+		`satisfaction on "sats[1]": holds`,
+		`satisfaction on "sats[2]": violated`,
+	}
+	if strings.Join(lines, "\n") != strings.Join(want, "\n") {
+		t.Errorf("verdicts:\n%s\nwant:\n%s", strings.Join(lines, "\n"), strings.Join(want, "\n"))
+	}
+	if shared := int(ctx.SharedDefaultsTaken()) + ctx.SharedVerdictsTaken(); shared != 0 {
+		t.Errorf("shared %d values or verdicts deciding on a lifetime", shared)
+	}
+}
+
+// libraryVerdicts validates the fleet of a library-backed model, sharing or not,
+// and answers its verdict lines with what the sharing saved.
+func libraryVerdicts(t *testing.T, src string, on bool) ([]string, int) {
+	t.Helper()
+	idx, _, ctx := buildRuntimeWithLibraries(t, "<test>", parseAndBuild(t, src))
+	ctx.SetSharedDefaults(on)
+	fleet, err := ctx.Instantiate(lookupOne(t, idx, "test::fleet"))
+	if err != nil {
+		t.Fatalf("instantiate: %v", err)
+	}
+	done := ctx.ShareVerdicts()
+	defer done()
+	report, err := ctx.ValidateObject(fleet, []*symbols.Scope{idx.DocumentRoot("<test>")})
+	if err != nil {
+		t.Fatalf("validate: %v", err)
+	}
+	var lines []string
+	for _, v := range report.Verdicts {
+		lines = append(lines, fmt.Sprintf("%s on %q: %s", v.Kind, strings.Join(v.Path, "."), v.Status))
+	}
+	return lines, int(ctx.SharedDefaultsTaken()) + ctx.SharedVerdictsTaken()
+}
+
+// An extent reads through every object it may reach, so one enumerated after a
+// verdict was taken counts the parts the taken check never materialized.
+func TestExtentAfterSharedVerdictsCountsEveryOccurrence(t *testing.T) {
+	const src = `package test {
+		private import SequenceFunctions::size;
+		part def Comp { attribute mass : ScalarValues::Integer = 3; }
+		part def Sat {
+			part comp : Comp;
+			requirement light { require constraint { comp.mass < 10 } }
+		}
+		part def Tail {
+			requirement complete { require constraint { size(all Comp) == 3 } }
+		}
+		part def Fleet {
+			part sats : Sat[3];
+			part tail : Tail;
+		}
+		part fleet : Fleet;
+	}`
+	sharing, shared := libraryVerdicts(t, src, true)
+	materializing, _ := libraryVerdicts(t, src, false)
+	want := []string{
+		`requirement on "sats[1]": holds`,
+		`requirement on "sats[2]": holds`,
+		`requirement on "sats[3]": holds`,
+		`requirement on "tail": holds`,
+	}
+	if strings.Join(sharing, "\n") != strings.Join(want, "\n") {
+		t.Errorf("verdicts:\n%s\nwant:\n%s", strings.Join(sharing, "\n"), strings.Join(want, "\n"))
+	}
+	if strings.Join(sharing, "\n") != strings.Join(materializing, "\n") {
+		t.Errorf("sharing decides differently from materializing:\n%s\nvs\n%s", strings.Join(sharing, "\n"), strings.Join(materializing, "\n"))
+	}
+	if shared != 2 {
+		t.Errorf("shared %d verdicts over three occurrences, want 2", shared)
+	}
+}
+
+// A verdict on record for a shape is not taken by an object whose part along a read
+// path was destroyed: that object's check reads the part and reports it destroyed.
+func TestDestroyedPartIsNotCheckedThroughSharedVerdict(t *testing.T) {
+	const src = `package test {
+		requirement def Light {
+			subject s : Sat;
+			require constraint { s.comp.mass < 10 }
+		}
+		part def Comp { attribute mass : ScalarValues::Integer = 3; }
+		part def Sat { part comp : Comp; }
+		part def Fleet { part sats : Sat[3]; }
+		part fleet : Fleet { satisfy Light by sats; }
+	}`
+	var got [2][]string
+	for i, on := range []bool{true, false} {
+		ctx, idx := contextForSource(t, src)
+		ctx.SetSharedDefaults(on)
+		fleet, err := ctx.Instantiate(lookupOne(t, idx, "test::fleet"))
+		if err != nil {
+			t.Fatalf("instantiate: %v", err)
+		}
+		done := ctx.ShareVerdicts()
+		defer done()
+		scopes := []*symbols.Scope{idx.DocumentRoot("<test>")}
+		if _, err := ctx.ValidateObject(fleet, scopes); err != nil {
+			t.Fatalf("validate: %v", err)
+		}
+		if err := ctx.destroy(at(t, ctx, fleet, "sats[2].comp")); err != nil {
+			t.Fatalf("destroy sats[2].comp: %v", err)
+		}
+		report, err := ctx.ValidateObject(fleet, scopes)
+		if err != nil {
+			t.Fatalf("validate: %v", err)
+		}
+		for _, v := range report.Verdicts {
+			if v.Kind == "satisfaction" {
+				line := fmt.Sprintf("%s on %q: %s %v", v.Kind, strings.Join(v.Path, "."), v.Status, v.Err)
+				got[i] = append(got[i], line[:strings.LastIndex(line, " at ")+1])
+			}
+		}
+	}
+	if strings.Join(got[0], "\n") != strings.Join(got[1], "\n") {
+		t.Errorf("verdicts with sharing:\n%s\nwithout:\n%s", strings.Join(got[0], "\n"), strings.Join(got[1], "\n"))
+	}
+	if len(got[1]) != 3 || !strings.Contains(got[1][1], "undecided") || !strings.Contains(got[1][1], "was destroyed") {
+		t.Errorf("verdicts over a destroyed part:\n%s", strings.Join(got[1], "\n"))
+	}
+}
diff --git a/internal/exec/runtime/sparse_differential_test.go b/internal/exec/runtime/sparse_differential_test.go
new file mode 100644
index 0000000000..c533756a47
--- /dev/null
+++ b/internal/exec/runtime/sparse_differential_test.go
@@ -0,0 +1,242 @@
+package runtime
+
+import (
+	"fmt"
+	"os"
+	"sort"
+	"strings"
+	"sync/atomic"
+	"testing"
+
+	"github.com/Open-MBEE/OpenSysML/internal/semantic/resolve"
+	"github.com/Open-MBEE/OpenSysML/internal/semantic/semantics"
+	"github.com/Open-MBEE/OpenSysML/internal/semantic/symbols"
+	"github.com/Open-MBEE/OpenSysML/internal/syntax/parser"
+	"github.com/Open-MBEE/OpenSysML/internal/syntax/source"
+	"github.com/Open-MBEE/OpenSysML/internal/workspace/libs"
+	"github.com/Open-MBEE/OpenSysML/tests/stressmodel"
+)
+
+// sparseDifferentialMaxSteps bounds one instantiation on either side, so a
+// model that never settles stops at the budget on both.
+const sparseDifferentialMaxSteps int64 = 20000
+
+// TestSparseValuesDifferential instantiates every part declared at the top of
+// every model under the differential roots with shared defaults on and off,
+// requiring the same readable values, materialization errors and verdicts.
+// Each file is a parallel subtest: every one builds its own model and contexts.
+func TestSparseValuesDifferential(t *testing.T) {
+	var files []string
+	for _, root := range differentialRoots {
+		files = append(files, sysmlFilesUnder(t, root)...)
+	}
+	sort.Strings(files)
+	if len(files) == 0 {
+		t.Fatal("no .sysml files under the differential roots")
+	}
+	var parts, shared atomic.Int64
+	t.Run("files", func(t *testing.T) {
+		for _, path := range files {
+			t.Run(path, func(t *testing.T) {
+				t.Parallel()
+				src, err := os.ReadFile(path)
+				if err != nil {
+					t.Fatal(err)
+				}
+				n, taken := sparseDifferentialSource(t, path, src, partSymbolsUnder)
+				parts.Add(int64(n))
+				shared.Add(int64(taken))
+			})
+		}
+	})
+	if parts.Load() == 0 {
+		t.Fatal("no part instantiated in any file")
+	}
+	t.Logf("%d files: %d parts compared, %d defaults and verdicts shared", len(files), parts.Load(), shared.Load())
+}
+
+// TestSparseValuesDifferentialFleet compares both sides over the fleet form of
+// the stress-test constellation: two planes of twenty, each a block whose
+// occurrences share its defaults except the two units per plane stating
+// as-built values of their own. The constellation is read through the parts
+// the model declares, so each definition is read once, as the type of its usage.
+func TestSparseValuesDifferentialFleet(t *testing.T) {
+	network := stressmodel.SatelliteNetwork{Planes: 2, Satellites: 20, GroundStations: 2, Fleet: true}
+	src, stats := network.Source()
+	name := fmt.Sprintf("fleet-%d.sysml", stats.Satellites)
+	parts, shared := sparseDifferentialSource(t, name, []byte(src), partUsagesUnder)
+	if shared == 0 {
+		t.Errorf("%s: no default or verdict shared between the occurrences", name)
+	}
+	t.Logf("%s: %d parts compared, %d defaults and verdicts shared", name, parts, shared)
+}
+
+// sparseDifferentialSource builds the model src, named path, once and
+// instantiates each of the parts roots picks from it on a sharing and a
+// materializing context, returning the number compared and how many values the
+// sharing side took from its type rather than deriving.
+func sparseDifferentialSource(t *testing.T, path string, src []byte, roots func(*symbols.Scope) []*symbols.Symbol) (parts, shared int) {
+	t.Helper()
+	idx := libs.NewModelIndex()
+	idx.AddDocument(path, parser.New(source.New(path, src)).ParseFile())
+	idx.ExpandWildcardImports()
+	resolver := resolve.New(idx)
+	model := semantics.NewModel(resolver)
+	root := idx.DocumentRoot(path)
+	for _, sym := range roots(root) {
+		sharing := NewContext(NewModel(model, resolver), sparseDifferentialMaxSteps)
+		sharing.SetSharedDefaults(true)
+		materializing := NewContext(NewModel(model, resolver), sparseDifferentialMaxSteps)
+		materializing.SetSharedDefaults(false)
+		name := path + ": " + sym.Name
+		got, taken := sparseReading(sharing, sym, root)
+		want, _ := sparseReading(materializing, sym, root)
+		if got != want {
+			t.Errorf("%s: sharing defaults reads differently from materializing them\n--- sharing\n%s\n--- materializing\n%s", name, got, want)
+		}
+		parts++
+		shared += taken
+	}
+	return parts, shared
+}
+
+// sparseReading instantiates sym on ctx and reports everything the object shows:
+// every readable value, the errors reading raised, and every verdict validating
+// it decides — and how many defaults and verdicts the context shared.
+func sparseReading(ctx *Context, sym *symbols.Symbol, root *symbols.Scope) (string, int) {
+	done := ctx.ShareVerdicts()
+	defer done()
+	inst, err := ctx.Instantiate(sym)
+	if err != nil {
+		return "instantiate: " + err.Error(), 0
+	}
+	var b strings.Builder
+	w := &readableWalk{ctx: ctx, out: &b, visited: map[int64]bool{inst.ID: true}}
+	w.walk(inst, sym.Name, 0)
+	report, err := ctx.ValidateObject(inst, []*symbols.Scope{root})
+	if err != nil {
+		fmt.Fprintf(&b, "validate: %v\n", err)
+	}
+	for _, v := range report.Verdicts {
+		fmt.Fprintf(&b, "%s %q on %q: %s", v.Kind, v.Text, strings.Join(v.Path, "."), v.Status)
+		if v.Err != nil {
+			fmt.Fprintf(&b, " (%v)", v.Err)
+		}
+		b.WriteString("\n")
+	}
+	fmt.Fprintf(&b, "valid %v bounded %v unread %d\n", report.Valid(), report.Bounded, len(report.Unread))
+	return b.String(), int(ctx.SharedDefaultsTaken()) + ctx.SharedVerdictsTaken()
+}
+
+// readableWalk reads every value an object graph shows, down to the depth a
+// listing descends, naming held objects by path rather than by identity.
+type readableWalk struct {
+	ctx     *Context
+	out     *strings.Builder
+	visited map[int64]bool
+}
+
+func (w *readableWalk) walk(inst *Instance, path string, depth int) {
+	if depth > maxMaterializeDepth {
+		fmt.Fprintf(w.out, "%s: (not expanded)\n", path)
+		return
+	}
+	for _, of := range w.ctx.FeaturesOfObject(inst) {
+		if holdsVerdict(of.Feature) || isBehaviorKind(of.Feature) {
+			continue
+		}
+		name := path + "." + of.Name
+		fv, err := inst.GetFeatureValue(w.ctx, of.Name)
+		if err != nil {
+			fmt.Fprintf(w.out, "%s: <error: %v>\n", name, err)
+			continue
+		}
+		val, err := fv.ReadValue(of.Name)
+		if err != nil {
+			fmt.Fprintf(w.out, "%s: <read error: %v>\n", name, err)
+			continue
+		}
+		fmt.Fprintf(w.out, "%s = %s\n", name, w.format(val))
+		for i, held := range heldInstances(w.ctx, fv) {
+			if w.visited[held.ID] {
+				continue
+			}
+			w.visited[held.ID] = true
+			w.walk(held, fmt.Sprintf("%s[%d]", name, i+1), depth+1)
+		}
+	}
+}
+
+// format renders a value with objects named by type, since the two sides
+// number objects differently when one derives without materializing.
+func (w *readableWalk) format(val Value) string {
+	switch val.Kind {
+	case ValInstance, ValVariant:
+		if id, ok := val.Object(); ok {
+			if inst, ok := w.ctx.Instance(id); ok && inst.Type != nil {
+				return "object " + inst.Type.Name
+			}
+			return "object"
+		}
+	case ValSequence:
+		if seq := val.Sequence(); seq != nil {
+			return "[" + strings.Join(w.formatAll(seq.Elements()), ", ") + "]"
+		}
+	case ValSet:
+		if set := val.Set(); set != nil {
+			return "Set{" + strings.Join(w.formatAll(set.Elements()), ", ") + "}"
+		}
+	}
+	return FormatValue(val)
+}
+
+func (w *readableWalk) formatAll(elements []Value) []string {
+	parts := make([]string, len(elements))
+	for i, element := range elements {
+		parts[i] = w.format(element)
+	}
+	return parts
+}
+
+// isBehaviorKind reports whether a feature is a behavior an object performs
+// rather than a value it holds; an abstract one is a collection held.
+func isBehaviorKind(feat *EffectiveFeature) bool {
+	if feat.Symbol == nil || symbols.IsAbstract(feat.Symbol) {
+		return false
+	}
+	switch feat.Symbol.Kind {
+	case symbols.SymbolStateUsage, symbols.SymbolActionUsage:
+		return true
+	}
+	return false
+}
+
+// partUsagesUnder lists the part usages declared directly in scope's packages:
+// the objects the model declares, through which their definitions are read.
+func partUsagesUnder(scope *symbols.Scope) []*symbols.Symbol {
+	var out []*symbols.Symbol
+	for _, sym := range partSymbolsUnder(scope) {
+		if sym.Kind == symbols.SymbolPartUsage {
+			out = append(out, sym)
+		}
+	}
+	return out
+}
+
+// partSymbolsUnder lists the part definitions and usages declared directly in
+// scope's packages, the objects a listing instantiates by name.
+func partSymbolsUnder(scope *symbols.Scope) []*symbols.Symbol {
+	if scope == nil {
+		return nil
+	}
+	var out []*symbols.Symbol
+	for _, sym := range scope.Members() {
+		switch sym.Kind {
+		case symbols.SymbolPartDef, symbols.SymbolPartUsage:
+			out = append(out, sym)
+		case symbols.SymbolPackage:
+			out = append(out, partSymbolsUnder(sym.Scope)...)
+		}
+	}
+	return out
+}
diff --git a/internal/exec/runtime/subsetting.go b/internal/exec/runtime/subsetting.go
index dc960fe588..8f5022b735 100644
--- a/internal/exec/runtime/subsetting.go
+++ b/internal/exec/runtime/subsetting.go
@@ -549,7 +549,7 @@ func (ctx *Context) fillOptionalSubsetters(inst *Instance, name string, n int) (
 		} else {
 			fill.fv.Values = ctx.collectionOf(fill.fv.Feature, fill.held)
 		}
-		fill.fv.Materialized = true
+		fill.fv.Materialized, fill.fv.intrinsic = true, false
 		ctx.invalidateDependents(fill.fv)
 	}
 	return made, undo, nil
diff --git a/internal/exec/runtime/subsetting_test.go b/internal/exec/runtime/subsetting_test.go
index 69f0cd521b..f5e2467cd2 100644
--- a/internal/exec/runtime/subsetting_test.go
+++ b/internal/exec/runtime/subsetting_test.go
@@ -3,7 +3,10 @@ package runtime
 import (
 	"errors"
 	"slices"
+	"strings"
 	"testing"
+
+	"github.com/Open-MBEE/OpenSysML/internal/semantic/symbols"
 )
 
 const redefinedCollectionModel = `
@@ -379,3 +382,64 @@ func TestSubsetterContributionIsTypedByTheSubsettedFeature(t *testing.T) {
 		}
 	}
 }
+
+// TestSubsettersAreFoundThroughEachClassifier: a classifier's subsetter of a feature the
+// object carries from another type is found under the queried name, its redefinition
+// alias and, for a classifier that also redefines the target, its own name; a name the
+// type neither declares nor subsets has none.
+func TestSubsettersAreFoundThroughEachClassifier(t *testing.T) {
+	idx, _, ctx := buildRuntimeWithLibraries(t, "<test>", parseAndBuild(t, `
+		package test {
+			private import ScalarValues::Real;
+			part def Item { attribute mass : Real; }
+			part def Bay { part items : Item[*]; }
+			part def Loaded :> Bay { part crate : Item :> items { attribute :>> mass = 2.0; } }
+			part def Renamed :> Bay {
+				part cargo : Item[*] :>> items;
+				part pallet : Item :> cargo { attribute :>> mass = 3.0; }
+			}
+			part bay : Bay;
+		}
+	`))
+	loaded, renamed := lookupOne(t, idx, "test::Loaded"), lookupOne(t, idx, "test::Renamed")
+	wants := map[string]struct {
+		typ  *symbols.Symbol
+		name string
+		want string
+	}{
+		"inherited target":           {loaded, "items", "crate"},
+		"redefined target":           {renamed, "items", "pallet"},
+		"redefining name":            {renamed, "cargo", "pallet"},
+		"name the type lacks":        {loaded, "cargo", ""},
+		"the target is no subsetter": {renamed, "pallet", ""},
+	}
+	for label, tc := range wants {
+		var got []string
+		for _, feat := range ctx.SubsettingFeatures(nil, tc.typ, tc.name) {
+			got = append(got, feat.Name)
+		}
+		if strings.Join(got, ",") != tc.want {
+			t.Errorf("%s: SubsettingFeatures(%s, %s) = %v, want %q", label, tc.typ.Name, tc.name, got, tc.want)
+		}
+	}
+	bay := instantiateNamed(t, ctx, idx, "test::bay")
+	for _, classifier := range []*symbols.Symbol{loaded, renamed} {
+		if err := ctx.classify(bay, classifier); err != nil {
+			t.Fatalf("classify(%s): %v", classifier.Name, err)
+		}
+	}
+	var got []string
+	for _, feat := range ctx.subsettingFeaturesOf(bay, "items") {
+		got = append(got, feat.Name)
+	}
+	if strings.Join(got, ",") != "crate,pallet" {
+		t.Errorf("subsetters of items through Bay, Loaded and Renamed = %v, want crate then pallet", got)
+	}
+	fv, err := bay.GetFeatureValue(ctx, "items")
+	if err != nil {
+		t.Fatalf("GetFeatureValue(items): %v", err)
+	}
+	if n := len(elementsOf(fv.HeldValue())); n != 2 {
+		t.Errorf("items holds %d elements after classifying, want the two subsetters'", n)
+	}
+}
diff --git a/internal/exec/runtime/testdata/conformance/occurrence_default_over_diverged_sibling.expected.json b/internal/exec/runtime/testdata/conformance/occurrence_default_over_diverged_sibling.expected.json
new file mode 100644
index 0000000000..d399b21a7c
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/occurrence_default_over_diverged_sibling.expected.json
@@ -0,0 +1,15 @@
+{
+  "type": "instance",
+  "libraries": true,
+  "instantiate": "test::fleet",
+  "materialization": {},
+  "validation": {
+    "verdicts": [
+      {"kind": "constraint", "assertion": "assert constraint fits", "object": "sats[1]", "status": "violated", "error": "evaluated to false"},
+      {"kind": "constraint", "assertion": "assert constraint fits", "object": "sats[2]", "status": "holds"},
+      {"kind": "constraint", "assertion": "assert constraint fits", "object": "sats[3]", "status": "holds"},
+      {"kind": "constraint", "assertion": "assert constraint fits", "object": "sats[4]", "status": "holds"}
+    ],
+    "valid": false
+  }
+}
diff --git a/internal/exec/runtime/testdata/conformance/occurrence_default_over_diverged_sibling.sysml b/internal/exec/runtime/testdata/conformance/occurrence_default_over_diverged_sibling.sysml
new file mode 100644
index 0000000000..29db1af731
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/occurrence_default_over_diverged_sibling.sysml
@@ -0,0 +1,27 @@
+// A default that is an expression over a sibling feature follows the sibling
+// on each occurrence: a unit restating its bus mass derives its own dry mass,
+// and the constraint asserted about it fails for that unit alone, while the
+// units keeping the definition's default all read the definition's value.
+package test {
+    private import ScalarValues::Real;
+
+    part def Bus { attribute mass : Real default = 120.0; }
+    part def Payload { attribute mass : Real default = 45.0; }
+
+    part def Spacecraft {
+        part bus : Bus;
+        part payload : Payload;
+        attribute margin : Real default = 1.1;
+        attribute dryMass : Real = (bus.mass + payload.mass) * margin;
+        assert constraint fits { dryMass < 200.0 }
+    }
+
+    part def Fleet {
+        part sats : Spacecraft[4];
+        part heavy :> sats {
+            part :>> bus { attribute :>> mass = 160.0; }
+        }
+    }
+
+    part fleet : Fleet;
+}
diff --git a/internal/exec/runtime/testdata/conformance/occurrence_default_shared.expected.json b/internal/exec/runtime/testdata/conformance/occurrence_default_shared.expected.json
new file mode 100644
index 0000000000..ddda4bfc91
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/occurrence_default_shared.expected.json
@@ -0,0 +1,15 @@
+{
+  "type": "instance",
+  "libraries": true,
+  "instantiate": "test::fleet",
+  "materialization": {},
+  "validation": {
+    "verdicts": [
+      {"kind": "constraint", "assertion": "assert constraint fits", "object": "sats[1]", "status": "holds"},
+      {"kind": "constraint", "assertion": "assert constraint fits", "object": "sats[2]", "status": "holds"},
+      {"kind": "constraint", "assertion": "assert constraint fits", "object": "sats[3]", "status": "holds"},
+      {"kind": "constraint", "assertion": "assert constraint fits", "object": "sats[4]", "status": "holds"}
+    ],
+    "valid": true
+  }
+}
diff --git a/internal/exec/runtime/testdata/conformance/occurrence_default_shared.sysml b/internal/exec/runtime/testdata/conformance/occurrence_default_shared.sysml
new file mode 100644
index 0000000000..17f4f9d559
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/occurrence_default_shared.sysml
@@ -0,0 +1,23 @@
+// Every occurrence of a definition holds the definition's defaults: a fleet of
+// spacecraft declared with one multiplicity reads the same derived mass from
+// each, and the constraint asserted about it is decided for all of them.
+package test {
+    private import ScalarValues::Real;
+
+    part def Bus { attribute mass : Real default = 120.0; }
+    part def Payload { attribute mass : Real default = 45.0; }
+
+    part def Spacecraft {
+        part bus : Bus;
+        part payload : Payload;
+        attribute margin : Real default = 1.1;
+        attribute dryMass : Real = (bus.mass + payload.mass) * margin;
+        assert constraint fits { dryMass < 200.0 }
+    }
+
+    part def Fleet {
+        part sats : Spacecraft[4];
+    }
+
+    part fleet : Fleet;
+}
diff --git a/internal/exec/runtime/testdata/conformance/occurrence_table_diverging_units.expected.json b/internal/exec/runtime/testdata/conformance/occurrence_table_diverging_units.expected.json
new file mode 100644
index 0000000000..6f54ddf6eb
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/occurrence_table_diverging_units.expected.json
@@ -0,0 +1,17 @@
+{
+  "type": "instance",
+  "libraries": true,
+  "instantiate": "test::fleet",
+  "materialization": {},
+  "validation": {
+    "verdicts": [
+      {"kind": "requirement", "assertion": "requirement massGrowth", "object": "sats[1]", "status": "holds"},
+      {"kind": "requirement", "assertion": "requirement massGrowth", "object": "sats[2]", "status": "violated", "error": "evaluated to false"},
+      {"kind": "requirement", "assertion": "requirement massGrowth", "object": "sats[3]", "status": "holds"},
+      {"kind": "requirement", "assertion": "requirement massGrowth", "object": "sats[4]", "status": "holds"},
+      {"kind": "requirement", "assertion": "requirement massGrowth", "object": "sats[5]", "status": "holds"},
+      {"kind": "requirement", "assertion": "requirement massGrowth", "object": "sats[6]", "status": "holds"}
+    ],
+    "valid": false
+  }
+}
diff --git a/internal/exec/runtime/testdata/conformance/occurrence_table_diverging_units.sysml b/internal/exec/runtime/testdata/conformance/occurrence_table_diverging_units.sysml
new file mode 100644
index 0000000000..eb749cbb14
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/occurrence_table_diverging_units.sysml
@@ -0,0 +1,37 @@
+// A fleet's per-unit values are a table of subsetting members, each restating
+// what its unit measured; the other occurrences keep the definition's catalog
+// values. The requirement each unit carries reads the unit's own row where one
+// is stated and the catalog value where none is, so its verdict differs only
+// where the as-built mass does.
+package test {
+    private import ScalarValues::Real;
+    private import ScalarValues::String;
+
+    part def Spacecraft {
+        attribute serial : String default = "catalog";
+        attribute catalogMass : Real default = 180.0;
+        attribute asBuiltMass : Real default = catalogMass;
+        attribute growth : Real = asBuiltMass - catalogMass;
+        requirement massGrowth {
+            attribute g : Real = growth;
+            require constraint { g <= 5.0 }
+        }
+    }
+
+    part def Fleet {
+        part sats : Spacecraft[6];
+        part unit1 :> sats {
+            attribute :>> serial = "SN-001";
+            attribute :>> asBuiltMass = 183.5;
+        }
+        part unit2 :> sats {
+            attribute :>> serial = "SN-002";
+            attribute :>> asBuiltMass = 191.0;
+        }
+        part unit3 :> sats {
+            attribute :>> serial = "SN-003";
+        }
+    }
+
+    part fleet : Fleet;
+}
diff --git a/internal/exec/runtime/testdata/conformance/satisfy_distinct_shapes_mixed.expected.json b/internal/exec/runtime/testdata/conformance/satisfy_distinct_shapes_mixed.expected.json
new file mode 100644
index 0000000000..f1b74f4cb6
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/satisfy_distinct_shapes_mixed.expected.json
@@ -0,0 +1,11 @@
+{
+  "type": "satisfy",
+  "libraries": true,
+  "evaluate": "test::fleet",
+  "assertions": {
+    "satisfy launchLimit by unit1": true,
+    "satisfy launchLimit by unit2": false,
+    "satisfy launchLimit by unit3": true,
+    "satisfy launchLimit by unit4": true
+  }
+}
diff --git a/internal/exec/runtime/testdata/conformance/satisfy_distinct_shapes_mixed.sysml b/internal/exec/runtime/testdata/conformance/satisfy_distinct_shapes_mixed.sysml
new file mode 100644
index 0000000000..338f44efba
--- /dev/null
+++ b/internal/exec/runtime/testdata/conformance/satisfy_distinct_shapes_mixed.sysml
@@ -0,0 +1,36 @@
+// A requirement satisfied by several occurrences of one definition is decided
+// once for the occurrences reading only the definition's defaults and once more
+// for each occurrence stating a value of its own; every satisfaction still
+// reports its own verdict, in the order the assertions are declared.
+package test {
+    private import ScalarValues::Real;
+
+    part def Spacecraft {
+        attribute catalogMass : Real default = 180.0;
+        attribute asBuiltMass : Real default = catalogMass;
+        attribute margin : Real default = 1.1;
+        attribute launchMass : Real = asBuiltMass * margin;
+    }
+
+    requirement def LaunchMassLimit {
+        subject s : Spacecraft;
+        attribute limit : Real = 205.0;
+        require constraint { s.launchMass <= limit }
+    }
+    requirement launchLimit : LaunchMassLimit;
+
+    part def Fleet {
+        part sats : Spacecraft[5];
+        part unit1 :> sats;
+        part unit2 :> sats { attribute :>> asBuiltMass = 190.0; }
+        part unit3 :> sats;
+        part unit4 :> sats { attribute :>> asBuiltMass = 184.0; }
+    }
+
+    part fleet : Fleet {
+        assert satisfy launchLimit by unit1;
+        assert satisfy launchLimit by unit2;
+        assert satisfy launchLimit by unit3;
+        assert satisfy launchLimit by unit4;
+    }
+}
diff --git a/internal/exec/runtime/validate.go b/internal/exec/runtime/validate.go
index 74c32ebcce..803d6bc650 100644
--- a/internal/exec/runtime/validate.go
+++ b/internal/exec/runtime/validate.go
@@ -175,6 +175,8 @@ func (ctx *Context) validateObjectWithin(root *Instance, scopes []*symbols.Scope
 	}
 	w := ctx.walkHeldObjects(root, budget)
 	report := ValidationReport{Root: root, Bounded: w.bounded, Unread: w.unread}
+	// Objects of one shape reading only declared values share one verdict.
+	defer ctx.ShareVerdicts()()
 	// Every object's carried assertions are read first, since a satisfaction one
 	// states may be about any object of the tree; verdicts then go out object by object.
 	carried := make([][]ObjectVerdict, len(w.objects))
diff --git a/internal/frontend/repl/query.go b/internal/frontend/repl/query.go
index 95364f0c12..ff49fc785c 100644
--- a/internal/frontend/repl/query.go
+++ b/internal/frontend/repl/query.go
@@ -298,6 +298,9 @@ func (s *Session) checkSatisfy(name string) []Verdict {
 		// Nothing was checked, so nothing is claimed about the model.
 		return []Verdict{unresolvedVerdict(name, fmt.Sprintf("no satisfaction assertion in %s", where))}
 	}
+	// The assertions are checked as one report, so those about objects of one
+	// shape reading only its declared values are decided once.
+	defer ctx.ShareVerdicts()()
 	verdicts := make([]Verdict, 0, len(assertions))
 	for _, a := range assertions {
 		verdicts = append(verdicts, s.satisfyVerdict(ctx, a))