diff --git a/Makefile b/Makefile
index ba141e31d..00449f427 100644
--- a/Makefile
+++ b/Makefile
@@ -298,7 +298,7 @@ stage-oidc-fixtures:
 
 ## test-property: Run property tests (FullChaos 100 iterations, others 50)
 test-property:
-	go test -C tests/blackbox -tags=property -run 'TestProperty_Sequential|TestProperty_Concurrent' -v -count=1 -rapid.checks=50 -timeout=60m
+	go test -C tests/blackbox -tags=property -run 'TestProperty_Sequential|TestProperty_Concurrent|TestProperty_RenameViaApply|TestRenameViaApply_Deterministic' -v -count=1 -rapid.checks=50 -timeout=60m
 	go test -C tests/blackbox -tags=property -run TestProperty_FullChaos -v -count=1 -rapid.checks=100 -timeout=60m
 
 ## mutation-test: Run mutation testing across all unit-tested packages and generate report
diff --git a/tests/blackbox/executor.go b/tests/blackbox/executor.go
index e5a299d98..c6d78743d 100644
--- a/tests/blackbox/executor.go
+++ b/tests/blackbox/executor.go
@@ -403,7 +403,7 @@ func (h *TestHarness) reconcileCompletedAcceptedCommands(t *testing.T, model *St
 	for i := len(completed) - 1; i >= 0; i-- {
 		cc := completed[i]
 		t.Logf("reconcileCompletedAcceptedCommands: command %s completed early (state=%s)", cc.ac.CommandID, cc.cmd.State)
-		correctModelFromCommandOutcome(t, &cc.cmd, model, model.Pool, cc.ac.Snapshots, corrected, cc.ac.IsReconcile, cc.ac.SupersededSlots)
+		correctModelFromCommandOutcome(t, &cc.cmd, model, model.Pool, cc.ac.Snapshots, corrected, cc.ac.IsReconcile, cc.ac.SupersededSlots, cc.ac.Rename)
 	}
 
 	model.AcceptedCommands = remaining
@@ -446,7 +446,7 @@ func (h *TestHarness) AssertAllInvariants(t *testing.T, model ...*StateModel) {
 	// ResetAgentState, creating cloud resources that haven't been persisted
 	// to inventory yet. When orphans are found, we clean them up and
 	// re-check. If the orphan persists across retries, it's a real bug.
-	resourceViolations := h.checkResourceInvariantsWithRetry(t, ignoreNativeIDs)
+	resourceViolations := h.checkResourceInvariantsWithRetry(t, ignoreNativeIDs, model...)
 	violations = append(violations, resourceViolations...)
 	if opLog, err := h.TryGetOperationLog(); err == nil {
 		violations = append(violations, CheckOperationLogInvariants(opLog)...)
@@ -477,6 +477,13 @@ func (h *TestHarness) AssertAllInvariants(t *testing.T, model ...*StateModel) {
 		violations = append(violations, modelViolations...)
 	}
 
+	// Violations detected while correcting the model from command outcomes
+	// (identity changes, dropped renames) surface here.
+	if len(model) > 0 && model[0] != nil {
+		violations = append(violations, model[0].PendingViolations...)
+		model[0].PendingViolations = nil
+	}
+
 	for _, v := range violations {
 		t.Logf("invariant violation: %s", v.Message)
 	}
@@ -488,7 +495,7 @@ func (h *TestHarness) AssertAllInvariants(t *testing.T, model ...*StateModel) {
 // prior rapid iterations can create cloud resources after ResetAgentState;
 // these resolve themselves once the stale operations complete and the cloud
 // entries are cleaned. Genuine invariant bugs persist across retries.
-func (h *TestHarness) checkResourceInvariantsWithRetry(t *testing.T, ignoreNativeIDs map[string]bool) []Violation {
+func (h *TestHarness) checkResourceInvariantsWithRetry(t *testing.T, ignoreNativeIDs map[string]bool, model ...*StateModel) []Violation {
 	t.Helper()
 
 	const maxRetries = 3
@@ -512,6 +519,12 @@ func (h *TestHarness) checkResourceInvariantsWithRetry(t *testing.T, ignoreNativ
 			continue
 		}
 		resourceViolations := CheckInvariants(inventory, cloudState, ignoreNativeIDs)
+		// RFC-0041: also assert rename invariants whenever the model has
+		// recorded a rename. The check is a no-op when no PreviousLabel is
+		// set anywhere; cheap to run unconditionally.
+		if len(model) > 0 && model[0] != nil {
+			resourceViolations = append(resourceViolations, CheckRenameInvariants(model[0], inventory)...)
+		}
 
 		if len(resourceViolations) == 0 {
 			return nil
@@ -811,15 +824,14 @@ func resolveResourceUpdateSlot(model *StateModel, pool *ResourcePool, ru apimode
 		return -1, -1
 	}
 
+	// Use LabelForResource so a slot renamed via OpRename matches against the
+	// resource update's current label rather than the slot's index-derived
+	// default. Without this a post-rename outcome (destroy of renamed-X,
+	// update on renamed-X, etc.) never finds its slot and the model fails to
+	// transition.
 	slotIdx := -1
 	for idx := range model.Stack(stackIdx).Resources {
-		var label string
-		if pool != nil {
-			label = pool.LabelForStack(model.Stack(stackIdx).Label, idx)
-		} else {
-			label = resourceLabelForStack(model.Stack(stackIdx).Label, idx)
-		}
-		if label == ru.ResourceLabel {
+		if model.LabelForResource(stackIdx, idx) == ru.ResourceLabel {
 			slotIdx = idx
 			break
 		}
@@ -925,7 +937,7 @@ func applyReconcileGuarantee(model *StateModel, stackIdx int, reconcileIDs []int
 // first) by DrainPendingCommands. The corrected map tracks which resources
 // have already been corrected by a later command — earlier commands skip
 // those resources so the latest outcome wins.
-func correctModelFromCommandOutcome(t *testing.T, cmd *apimodel.Command, model *StateModel, pool *ResourcePool, snapshots []ResourceSnapshot, corrected map[struct{ stackIdx, slotIdx int }]bool, isReconcile bool, superseded map[ResourceSlotRef]bool) {
+func correctModelFromCommandOutcome(t *testing.T, cmd *apimodel.Command, model *StateModel, pool *ResourcePool, snapshots []ResourceSnapshot, corrected map[struct{ stackIdx, slotIdx int }]bool, isReconcile bool, superseded map[ResourceSlotRef]bool, rename *PendingRename) {
 	t.Helper()
 
 	if cmd == nil {
@@ -934,6 +946,31 @@ func correctModelFromCommandOutcome(t *testing.T, cmd *apimodel.Command, model *
 
 	type slotKey = struct{ stackIdx, slotIdx int }
 
+	// RFC-0041: a successful command that carried a rename overlay must have
+	// performed it as an in-place UPDATE of the existing resource at its new
+	// label. A destroy+recreate shows up as a create RU at the new label
+	// instead, and a dropped alias makes the engine treat the new label as a
+	// brand-new resource (also a create). Identity stability of the update
+	// itself (NativeID/KSUID unchanged) is checked in the update case below.
+	if rename != nil && cmd.State == "Success" {
+		found := false
+		for _, ru := range cmd.ResourceUpdates {
+			if ru.State == "Success" && ru.Operation == "update" && ru.ResourceLabel == rename.NewLabel {
+				found = true
+				break
+			}
+		}
+		if !found {
+			model.AddPendingViolation(Violation{
+				Kind: ViolationRenameRecreatedResource,
+				Message: fmt.Sprintf(
+					"command %s succeeded but contains no update RU at the renamed label %q (was %q, stack %s) — the rename was dropped or executed as destroy+recreate",
+					cmd.CommandID, rename.NewLabel, rename.OldLabel, model.Stack(rename.StackIndex).Label,
+				),
+			})
+		}
+	}
+
 	// Log all resource updates for debugging.
 	t.Logf("correctModelFromCommandOutcome: cmd=%s state=%s has %d snapshots, %d resource updates",
 		cmd.CommandID, cmd.State, len(snapshots), len(cmd.ResourceUpdates))
@@ -984,16 +1021,40 @@ func correctModelFromCommandOutcome(t *testing.T, cmd *apimodel.Command, model *
 				}
 				model.ApplyCreated(stackIdx, []int{slotIdx}, props)
 				model.SetNativeID(stackIdx, slotIdx, ru.NativeID)
+				model.SetKsuid(stackIdx, slotIdx, ru.ResourceID)
 			case "delete":
 				model.ApplyDestroyed(stackIdx, []int{slotIdx})
 				model.MarkAuthoritativeSlot(stackIdx, slotIdx)
 				model.ClearNativeID(stackIdx, slotIdx)
+				model.ClearKsuid(stackIdx, slotIdx)
 			case "update":
 				// Don't let updates override authoritative slots (e.g. TTL destroy).
 				// Only creates can clear authoritative status.
 				if model.IsAuthoritativeSlot(stackIdx, slotIdx) {
 					goto markDone
 				}
+				// RFC-0041: an update never changes a resource's identity —
+				// that would be replace semantics. Check before adopting the
+				// RU's NativeID/KSUID so a rename that swapped the identity is
+				// caught rather than absorbed.
+				if tracked := model.GetNativeID(stackIdx, slotIdx); tracked != "" && ru.NativeID != "" && tracked != ru.NativeID {
+					model.AddPendingViolation(Violation{
+						Kind: ViolationRenameIdentityChanged,
+						Message: fmt.Sprintf(
+							"update RU for stack=%s label=%s changed NativeID %s → %s (cmd=%s)",
+							ru.StackName, ru.ResourceLabel, tracked, ru.NativeID, cmd.CommandID,
+						),
+					})
+				}
+				if tracked := model.GetKsuid(stackIdx, slotIdx); tracked != "" && ru.ResourceID != "" && tracked != ru.ResourceID {
+					model.AddPendingViolation(Violation{
+						Kind: ViolationRenameIdentityChanged,
+						Message: fmt.Sprintf(
+							"update RU for stack=%s label=%s changed KSUID %s → %s (cmd=%s)",
+							ru.StackName, ru.ResourceLabel, tracked, ru.ResourceID, cmd.CommandID,
+						),
+					})
+				}
 				if ru.Properties != nil {
 					props := model.NormalizePropertiesForResource(stackIdx, slotIdx, string(ru.Properties))
 					// Update properties without touching existence state or
@@ -1004,6 +1065,7 @@ func correctModelFromCommandOutcome(t *testing.T, cmd *apimodel.Command, model *
 					}
 				}
 				model.SetNativeID(stackIdx, slotIdx, ru.NativeID)
+				model.SetKsuid(stackIdx, slotIdx, ru.ResourceID)
 			}
 		} else {
 			// Failed/Canceled — revert to pre-command snapshot state.
@@ -1029,11 +1091,13 @@ func correctModelFromCommandOutcome(t *testing.T, cmd *apimodel.Command, model *
 				}
 			} else if snap, ok := snapBySlot[key]; ok {
 				res := model.Resource(stackIdx, slotIdx)
-				if res != nil && (res.State != snap.State || res.Properties != snap.Properties) {
+				if res != nil && (res.State != snap.State || res.Properties != snap.Properties || res.CurrentLabel != snap.CurrentLabel || res.PreviousLabel != snap.PreviousLabel) {
 					t.Logf("correctModelFromCommandOutcome: reverting stack=%s slot=%d from %v to %v (ru.State=%s, op=%s)",
 						model.Stack(stackIdx).Label, slotIdx, res.State, snap.State, ru.State, ru.Operation)
 					res.State = snap.State
 					res.Properties = snap.Properties
+					res.CurrentLabel = snap.CurrentLabel
+					res.PreviousLabel = snap.PreviousLabel
 				}
 			} else {
 				// No snapshot — derive from operation semantics.
@@ -1083,7 +1147,20 @@ func correctModelFromCommandOutcome(t *testing.T, cmd *apimodel.Command, model *
 				continue
 			}
 			res := model.Resource(key.stackIdx, key.slotIdx)
-			if res == nil || (res.State == snap.State && res.Properties == snap.Properties) {
+			if res == nil {
+				continue
+			}
+			// A rename recorded optimistically for this command never reached
+			// the engine if the slot produced no RU — restore the snapshot's
+			// labels regardless of whether State changed, or the model keeps
+			// a label the engine never persisted.
+			if res.CurrentLabel != snap.CurrentLabel || res.PreviousLabel != snap.PreviousLabel {
+				t.Logf("correctModelFromCommandOutcome: reverting unmentioned slot labels stack=%s slot=%d %q → %q (command state=%s)",
+					model.Stack(key.stackIdx).Label, key.slotIdx, res.CurrentLabel, snap.CurrentLabel, cmd.State)
+				res.CurrentLabel = snap.CurrentLabel
+				res.PreviousLabel = snap.PreviousLabel
+			}
+			if res.State == snap.State && res.Properties == snap.Properties {
 				continue
 			}
 			t.Logf("correctModelFromCommandOutcome: reverting unmentioned slot stack=%s slot=%d from %v to %v (command state=%s)",
@@ -1144,17 +1221,62 @@ func (h *TestHarness) executeApply(t *testing.T, op *Operation, model *StateMode
 	}
 
 	stackLabel := model.Stack(op.StackIndex).Label
+
+	// RFC-0041: optional rename overlay. The generator sets RenameSlotIndex
+	// when this apply should also rename one slot. Honoured only if the
+	// slot is currently StateExists — for a not-yet-existing slot a rename
+	// is meaningless (the apply will create it, no alias needed). When
+	// honoured, the rename is folded into the label overrides BEFORE the
+	// forma is built, so child `$res` references to the renamed slot carry
+	// the new label (the engine resolves intra-forma references against
+	// declared labels — a reference to the old label would not resolve).
+	// The renamed resource then gets Alias set to its previous label, and
+	// everything downstream (RecordRename on acceptance, snapshot revert
+	// on failure) flows through the standard apply path so an Update can
+	// model label-only, property-only, or both depending on whether the
+	// Properties template also changed.
+	performRename := false
+	var renameOldLabel string
+	if op.RenameSlotIndex >= 0 && op.RenameNewLabel != "" {
+		if res := model.Resource(op.StackIndex, op.RenameSlotIndex); res != nil && res.State == StateExists {
+			renameOldLabel = model.LabelForResource(op.StackIndex, op.RenameSlotIndex)
+			performRename = renameOldLabel != "" && renameOldLabel != op.RenameNewLabel
+		}
+	}
+
+	overrides := model.LabelOverrides(op.StackIndex)
+	if performRename {
+		if overrides == nil {
+			overrides = make(map[int]string)
+		}
+		overrides[op.RenameSlotIndex] = op.RenameNewLabel
+	}
+
 	var forma *pkgmodel.Forma
 	if model.Pool != nil {
-		forma = FormaFromPoolResources(model.Pool, stackLabel, model.ProviderStackLabel, op.ResourceIDs, op.Properties, op.ChildProperties)
+		forma = FormaFromPoolResources(model.Pool, stackLabel, model.ProviderStackLabel, op.ResourceIDs, op.Properties, op.ChildProperties, overrides, model.LabelOverrides(0))
 	} else {
-		forma = FormaFromStackResources(stackLabel, op.ResourceIDs, op.Properties)
+		forma = FormaFromStackResources(stackLabel, op.ResourceIDs, overrides, op.Properties)
+	}
+
+	if performRename {
+		found := false
+		for i := range forma.Resources {
+			if forma.Resources[i].Stack == stackLabel && forma.Resources[i].Label == op.RenameNewLabel {
+				forma.Resources[i].Alias = renameOldLabel
+				found = true
+				break
+			}
+		}
+		// A cross-stack slot on the provider stack is skipped by the forma
+		// builder; if the renamed slot produced no resource, drop the rename.
+		performRename = found
 	}
+
 	// Program response sequences before submitting the command.
 	var programmedSeqs []testcontrol.PluginOpSequence
 	if op.DrawnOutcomes != nil {
-		nativeIDs := model.NativeIDsByLabel()
-		programmedSeqs = buildPluginOpSequences(op.DrawnOutcomes, op.StackIndex, stackLabel, op.ResourceIDs, model, nativeIDs, false, model.Pool)
+		programmedSeqs = buildPluginOpSequences(op.DrawnOutcomes, op.StackIndex, stackLabel, op.ResourceIDs, model, false, model.Pool)
 		if len(programmedSeqs) > 0 {
 			h.ProgramResponses(t, programmedSeqs)
 		}
@@ -1212,6 +1334,14 @@ func (h *TestHarness) executeApply(t *testing.T, op *Operation, model *StateMode
 	}
 	snapshots := model.SnapshotResources(op.StackIndex, snapshotIDs)
 
+	// Record the rename BEFORE computing property predictions: the template's
+	// NAME resolves through LabelForResource, and the engine persists the
+	// renamed slot's Name as the new label. The snapshots above captured the
+	// pre-rename overlay, so a failed/canceled command reverts cleanly.
+	if performRename {
+		model.RecordRename(op.StackIndex, op.RenameSlotIndex, op.RenameNewLabel)
+	}
+
 	// Immediate model update: predict outcomes at submission time.
 	successIDs := successfulResourceIDs(op, op.StackIndex, op.ResourceIDs, model.Pool, false, model)
 	if len(successIDs) > 0 {
@@ -1236,7 +1366,19 @@ func (h *TestHarness) executeApply(t *testing.T, op *Operation, model *StateMode
 		model.SaveLastReconcile(op.StackIndex, op.ResourceIDs, resolvedProps)
 	}
 	model.TrackAcceptedCommand(commandID, snapshots, requestedSlotRefs(op.StackIndex, op.ResourceIDs), h.currentOperationLogSize(t), mode == pkgmodel.FormaApplyModeReconcile)
-	t.Logf("[op %d] Apply (%s) stack=%s resources %v → accepted, model updated (success=%v)", op.SequenceNum, op.ApplyMode, stackLabel, op.ResourceIDs, successIDs)
+	if performRename {
+		h.RenamesAccepted++
+		model.AcceptedCommands[len(model.AcceptedCommands)-1].Rename = &PendingRename{
+			StackIndex: op.StackIndex,
+			SlotIndex:  op.RenameSlotIndex,
+			OldLabel:   renameOldLabel,
+			NewLabel:   op.RenameNewLabel,
+		}
+		t.Logf("[op %d] Apply (%s) stack=%s resources %v → accepted, model updated (success=%v) + rename slot=%d %q → %q",
+			op.SequenceNum, op.ApplyMode, stackLabel, op.ResourceIDs, successIDs, op.RenameSlotIndex, renameOldLabel, op.RenameNewLabel)
+	} else {
+		t.Logf("[op %d] Apply (%s) stack=%s resources %v → accepted, model updated (success=%v)", op.SequenceNum, op.ApplyMode, stackLabel, op.ResourceIDs, successIDs)
+	}
 }
 
 func (h *TestHarness) executeDestroy(t *testing.T, op *Operation, model *StateModel) {
@@ -1272,13 +1414,12 @@ func (h *TestHarness) executeDestroy(t *testing.T, op *Operation, model *StateMo
 func (h *TestHarness) executeDestroyDefault(t *testing.T, op *Operation, model *StateModel, stackLabel string, existingIDs []int) {
 	t.Helper()
 
-	forma := FormaFromStackResources(stackLabel, existingIDs)
+	forma := FormaFromStackResources(stackLabel, existingIDs, model.LabelOverrides(op.StackIndex))
 
 	// Program response sequences before submitting the command.
 	var programmedSeqs []testcontrol.PluginOpSequence
 	if op.DrawnOutcomes != nil {
-		nativeIDs := model.NativeIDsByLabel()
-		programmedSeqs = buildPluginOpSequences(op.DrawnOutcomes, op.StackIndex, stackLabel, existingIDs, model, nativeIDs, true, model.Pool)
+		programmedSeqs = buildPluginOpSequences(op.DrawnOutcomes, op.StackIndex, stackLabel, existingIDs, model, true, model.Pool)
 		if len(programmedSeqs) > 0 {
 			h.ProgramResponses(t, programmedSeqs)
 		}
@@ -1332,7 +1473,7 @@ func (h *TestHarness) executeDestroyAbort(t *testing.T, op *Operation, model *St
 		}
 	}
 
-	forma := FormaFromPoolResources(model.Pool, stackLabel, model.ProviderStackLabel, existingIDs, defaultDestroyParentProps, defaultDestroyChildProps)
+	forma := FormaFromPoolResources(model.Pool, stackLabel, model.ProviderStackLabel, existingIDs, defaultDestroyParentProps, defaultDestroyChildProps, model.LabelOverrides(op.StackIndex), model.LabelOverrides(0))
 
 	if hasDependents {
 		// Simulate to check whether the agent would create cascade deletes.
@@ -1358,8 +1499,7 @@ func (h *TestHarness) executeDestroyAbort(t *testing.T, op *Operation, model *St
 	// Program response sequences before submitting the command.
 	var programmedSeqs []testcontrol.PluginOpSequence
 	if op.DrawnOutcomes != nil {
-		nativeIDs := model.NativeIDsByLabel()
-		programmedSeqs = buildPluginOpSequences(op.DrawnOutcomes, op.StackIndex, stackLabel, existingIDs, model, nativeIDs, true, model.Pool)
+		programmedSeqs = buildPluginOpSequences(op.DrawnOutcomes, op.StackIndex, stackLabel, existingIDs, model, true, model.Pool)
 		if len(programmedSeqs) > 0 {
 			h.ProgramResponses(t, programmedSeqs)
 		}
@@ -1405,13 +1545,12 @@ func (h *TestHarness) executeDestroyAbort(t *testing.T, op *Operation, model *St
 func (h *TestHarness) executeDestroyCascade(t *testing.T, op *Operation, model *StateModel, stackLabel string, existingIDs []int) {
 	t.Helper()
 
-	forma := FormaFromPoolResources(model.Pool, stackLabel, model.ProviderStackLabel, existingIDs, defaultDestroyParentProps, defaultDestroyChildProps)
+	forma := FormaFromPoolResources(model.Pool, stackLabel, model.ProviderStackLabel, existingIDs, defaultDestroyParentProps, defaultDestroyChildProps, model.LabelOverrides(op.StackIndex), model.LabelOverrides(0))
 
 	// Program response sequences before submitting the command.
 	var programmedSeqs []testcontrol.PluginOpSequence
 	if op.DrawnOutcomes != nil {
-		nativeIDs := model.NativeIDsByLabel()
-		programmedSeqs = buildPluginOpSequences(op.DrawnOutcomes, op.StackIndex, stackLabel, existingIDs, model, nativeIDs, true, model.Pool)
+		programmedSeqs = buildPluginOpSequences(op.DrawnOutcomes, op.StackIndex, stackLabel, existingIDs, model, true, model.Pool)
 		if len(programmedSeqs) > 0 {
 			h.ProgramResponses(t, programmedSeqs)
 		}
@@ -1591,9 +1730,11 @@ func (h *TestHarness) executeCancel(t *testing.T, op *Operation, model *StateMod
 				}
 				model.ApplyCreated(stackIdx, []int{slotIdx}, props)
 				model.SetNativeID(stackIdx, slotIdx, ru.NativeID)
+				model.SetKsuid(stackIdx, slotIdx, ru.ResourceID)
 			case "delete":
 				model.ApplyDestroyed(stackIdx, []int{slotIdx})
 				model.ClearNativeID(stackIdx, slotIdx)
+				model.ClearKsuid(stackIdx, slotIdx)
 			}
 		}
 	}
@@ -1613,14 +1754,12 @@ func (h *TestHarness) executeCancel(t *testing.T, op *Operation, model *StateMod
 func buildLabelToSnapshotMap(snapshots []ResourceSnapshot, model *StateModel) map[string]ResourceSnapshot {
 	m := make(map[string]ResourceSnapshot, len(snapshots))
 	for _, snap := range snapshots {
-		stackLabel := model.Stack(snap.StackIndex).Label
-		var label string
-		if model.Pool != nil {
-			label = model.Pool.LabelForStack(stackLabel, snap.SlotIndex)
-		} else {
-			label = resourceLabelForStack(stackLabel, snap.SlotIndex)
-		}
-		m[label] = snap
+		// Key by the label the agent currently knows the slot by. The model
+		// carries the optimistic rename overlay, so a slot renamed by the
+		// canceled command itself resolves to the new label the RU reports;
+		// the snapshot's own labels are the pre-command state to revert TO,
+		// not the lookup key.
+		m[model.LabelForResource(snap.StackIndex, snap.SlotIndex)] = snap
 	}
 	return m
 }
@@ -2208,7 +2347,7 @@ func (h *TestHarness) DrainPendingCommands(t *testing.T, model *StateModel, time
 	for i := len(drained) - 1; i >= 0; i-- {
 		dc := drained[i]
 		if dc.cmd != nil {
-			correctModelFromCommandOutcome(t, dc.cmd, model, model.Pool, dc.ac.Snapshots, corrected, dc.ac.IsReconcile, dc.ac.SupersededSlots)
+			correctModelFromCommandOutcome(t, dc.cmd, model, model.Pool, dc.ac.Snapshots, corrected, dc.ac.IsReconcile, dc.ac.SupersededSlots, dc.ac.Rename)
 		}
 	}
 	h.reconcileAmbiguousFailedCommands(t, model, drained)
@@ -2264,7 +2403,7 @@ func (h *TestHarness) SetupStacks(t *testing.T, model *StateModel, config Proper
 		stackLabel := model.Stack(stackIdx).Label
 		ids := []int{0} // just the first resource
 
-		forma := FormaFromStackResources(stackLabel, ids)
+		forma := FormaFromStackResources(stackLabel, ids, nil)
 		resp, err := h.client.ApplyForma(forma, pkgmodel.FormaApplyModeReconcile, false, clientID, false)
 		if err != nil {
 			t.Logf("SetupStacks: stack %s apply rejected: %v", stackLabel, err)
@@ -2560,13 +2699,19 @@ func (h *TestHarness) dumpRawResourceRows(t *testing.T, resources []pkgmodel.Res
 // FormaFromResourceIDs builds a forma containing the resources at the given
 // pool indices on the default stack. Used by smoke tests and ResetAgentState.
 func FormaFromResourceIDs(ids []int) *pkgmodel.Forma {
-	return FormaFromStackResources("default", ids)
+	return FormaFromStackResources("default", ids, nil)
 }
 
 // FormaFromStackResources builds a forma containing the resources at the given
 // pool indices on the specified stack, using the given properties template.
 // The "NAME" placeholder in propsTemplate is replaced with each resource's label.
-func FormaFromStackResources(stackLabel string, ids []int, propsTemplate ...string) *pkgmodel.Forma {
+// FormaFromStackResources builds a forma containing the resources at the given
+// slot indices. labelOverrides, if non-nil, maps slot index -> custom label;
+// for slots present in the map, the override is used instead of the default
+// index-derived label. Used to support OpRename: after a rename, the slot's
+// label override flows into subsequent applies so the renamed resource is
+// addressed by its new label.
+func FormaFromStackResources(stackLabel string, ids []int, labelOverrides map[int]string, propsTemplate ...string) *pkgmodel.Forma {
 	template := `{"Name":"NAME","Value":"v1","SetTags":[],"EntityTags":[],"OrderedItems":[]}`
 	if len(propsTemplate) > 0 && propsTemplate[0] != "" {
 		template = propsTemplate[0]
@@ -2575,6 +2720,9 @@ func FormaFromStackResources(stackLabel string, ids []int, propsTemplate ...stri
 	resources := make([]pkgmodel.Resource, len(ids))
 	for i, id := range ids {
 		name := resourceLabelForStack(stackLabel, id)
+		if override, ok := labelOverrides[id]; ok && override != "" {
+			name = override
+		}
 		props := strings.Replace(template, `"NAME"`, `"`+name+`"`, 1)
 		resources[i] = pkgmodel.Resource{
 			Label:      name,
@@ -2606,14 +2754,23 @@ func FormaFromStackResources(stackLabel string, ids []int, propsTemplate ...stri
 // types, schemas, and resolvable ParentId references for child/grandchild slots.
 // parentProps is the properties template for Test::Generic::Resource (with "NAME" placeholder).
 // childProps is the properties template for child/grandchild types (with "NAME" and "PARENT_ID" placeholders).
+// labelOverrides, if non-nil, maps slot index -> custom label for slots on
+// this stack and takes priority over the pool's default LabelForStack
+// derivation. It applies both to a resource's own label and to the parent
+// labels in child `$res` references, so a renamed parent stays referenced
+// by its current label. providerLabelOverrides is the same map for the
+// provider stack (stack 0), consulted for cross-stack parent references.
 func FormaFromPoolResources(pool *ResourcePool, stackLabel string, providerStackLabel string, ids []int,
-	parentProps string, childProps string) *pkgmodel.Forma {
+	parentProps string, childProps string, labelOverrides map[int]string, providerLabelOverrides map[int]string) *pkgmodel.Forma {
 
 	resources := make([]pkgmodel.Resource, 0, len(ids))
 
 	for _, idx := range ids {
 		slot := pool.Slots[idx]
 		label := pool.LabelForStack(stackLabel, idx)
+		if override, ok := labelOverrides[idx]; ok && override != "" {
+			label = override
+		}
 
 		switch {
 		case pool.IsParent(idx):
@@ -2637,6 +2794,9 @@ func FormaFromPoolResources(pool *ResourcePool, stackLabel string, providerStack
 			}
 			props := strings.Replace(childProps, `"NAME"`, `"`+label+`"`, 1)
 			parentLabel := pool.CrossStackParentLabelForStack(providerStackLabel, idx)
+			if override, ok := providerLabelOverrides[pool.Slots[idx].CrossStackParentSlot]; ok && override != "" {
+				parentLabel = override
+			}
 			parentType := pool.CrossStackParentType(idx)
 			resObj, _ := json.Marshal(map[string]any{
 				"$res":      true,
@@ -2664,6 +2824,9 @@ func FormaFromPoolResources(pool *ResourcePool, stackLabel string, providerStack
 			// The metastructure expects {"$res":true, "$label":"...", "$type":"...",
 			// "$stack":"...", "$property":"..."} — NOT raw {"$ref":"formae://..."}.
 			parentLabel := pool.ParentLabelForStack(stackLabel, idx)
+			if override, ok := labelOverrides[pool.Slots[idx].ParentIndex]; ok && override != "" {
+				parentLabel = override
+			}
 			parentType := pool.ParentType(idx)
 			resObj, _ := json.Marshal(map[string]any{
 				"$res":      true,
@@ -2743,7 +2906,6 @@ func buildPluginOpSequences(
 	stackLabel string,
 	resourceIDs []int,
 	model *StateModel,
-	nativeIDs map[string]string,
 	isDestroy bool,
 	pool *ResourcePool,
 ) []testcontrol.PluginOpSequence {
@@ -2825,20 +2987,16 @@ func buildPluginOpSequences(
 			continue // no drawn outcome for this slot — will succeed by default
 		}
 
-		// Determine the resource label
-		var label string
-		if pool != nil {
-			label = pool.LabelForStack(stackLabel, slotIdx)
-		} else {
-			label = resourceLabelForStack(stackLabel, slotIdx)
-		}
+		// The label the forma carries for this slot — rename-overlay aware,
+		// so failure injection keeps working after a slot has been renamed.
+		label := model.LabelForResource(stackIndex, slotIdx)
 
 		res := model.Stack(stackIndex).Resources[slotIdx]
 		exists := res != nil && res.State == StateExists
 
 		if exists {
 			// Resource exists -> will be Read+Update or Read+Delete
-			nativeID := nativeIDs[stackLabel+":"+label]
+			nativeID := model.GetNativeID(stackIndex, slotIdx)
 			if nativeID == "" {
 				continue // can't program without NativeID
 			}
@@ -2868,7 +3026,7 @@ func buildPluginOpSequences(
 			// Resource doesn't exist -> will be a Create
 			// If the resource has resolvables, program the ResolveCache read of the
 			// referenced resource first. Only program Create if that read succeeds.
-			if resolveTarget, ok := resolveReadMatchKey(pool, model, stackIndex, stackLabel, slotIdx, nativeIDs); ok && len(outcome.ReadSteps) > 0 {
+			if resolveTarget, ok := resolveReadMatchKey(pool, model, stackIndex, slotIdx); ok && len(outcome.ReadSteps) > 0 {
 				sequences = append(sequences, testcontrol.PluginOpSequence{
 					MatchKey:  resolveTarget,
 					Operation: "Read",
@@ -2898,21 +3056,20 @@ func hasResolveReadPhase(pool *ResourcePool, slotIdx int) bool {
 	return pool.Slots[slotIdx].ParentIndex >= 0 || pool.IsCrossStack(slotIdx)
 }
 
-func resolveReadMatchKey(pool *ResourcePool, model *StateModel, stackIdx int, stackLabel string, slotIdx int, nativeIDs map[string]string) (string, bool) {
+func resolveReadMatchKey(pool *ResourcePool, model *StateModel, stackIdx int, slotIdx int) (string, bool) {
 	if pool == nil {
 		return "", false
 	}
 	if pool.IsCrossStack(slotIdx) {
-		parentLabel := pool.CrossStackParentLabelForStack(model.ProviderStackLabel, slotIdx)
-		nativeID := nativeIDs[model.ProviderStackLabel+":"+parentLabel]
+		// Cross-stack parents live on the provider stack (stack 0).
+		nativeID := model.GetNativeID(0, pool.Slots[slotIdx].CrossStackParentSlot)
 		return nativeID, nativeID != ""
 	}
 	parentIdx := pool.Slots[slotIdx].ParentIndex
 	if parentIdx < 0 {
 		return "", false
 	}
-	parentLabel := pool.ParentLabelForStack(stackLabel, slotIdx)
-	nativeID := nativeIDs[stackLabel+":"+parentLabel]
+	nativeID := model.GetNativeID(stackIdx, parentIdx)
 	return nativeID, nativeID != ""
 }
 
@@ -2961,11 +3118,12 @@ func (h *TestHarness) executeSetTTLPolicy(t *testing.T, op *Operation, model *St
 	policy := json.RawMessage(fmt.Sprintf(`{"Type":"ttl","TTLSeconds":%d,"OnDependents":"cascade"}`, ttlSeconds))
 
 	var forma *pkgmodel.Forma
+	overrides := model.LabelOverrides(model.StackIndexByLabel(stackLabel))
 	if model.Pool != nil {
 		forma = FormaFromPoolResources(model.Pool, stackLabel, model.ProviderStackLabel, existingIDs,
-			resourceProperties(stackLabel, existingIDs), defaultDestroyChildProps)
+			resourceProperties(stackLabel, existingIDs), defaultDestroyChildProps, overrides, model.LabelOverrides(0))
 	} else {
-		forma = FormaFromStackResources(stackLabel, existingIDs, resourceProperties(stackLabel, existingIDs))
+		forma = FormaFromStackResources(stackLabel, existingIDs, overrides, resourceProperties(stackLabel, existingIDs))
 	}
 	for i := range forma.Stacks {
 		if forma.Stacks[i].Label == stackLabel {
diff --git a/tests/blackbox/generators.go b/tests/blackbox/generators.go
index bf41c8e0f..c36fd7bc2 100644
--- a/tests/blackbox/generators.go
+++ b/tests/blackbox/generators.go
@@ -40,7 +40,7 @@ func OperationSequenceGen(config PropertyTestConfig) *rapid.Generator[[]Operatio
 		count := rapid.IntRange(config.OperationCount.Min, config.OperationCount.Max).Draw(t, "count")
 		ops := make([]Operation, count)
 		for i := range ops {
-			ops[i] = SingleOperationGen(config).Draw(t, fmt.Sprintf("op-%d", i))
+			ops[i] = SingleOperationGen(config, i).Draw(t, fmt.Sprintf("op-%d", i))
 		}
 
 		// Enforce OpCrashAgent constraints: at most once, not first or last.
@@ -60,15 +60,17 @@ func OperationSequenceGen(config PropertyTestConfig) *rapid.Generator[[]Operatio
 }
 
 // SingleOperationGen returns a rapid generator that produces a single operation
-// whose kind and parameters respect the given config.
-func SingleOperationGen(config PropertyTestConfig) *rapid.Generator[Operation] {
+// whose kind and parameters respect the given config. seq is the operation's
+// position in the sequence; it parameterizes draws that must be unique per
+// operation (rename labels).
+func SingleOperationGen(config PropertyTestConfig, seq int) *rapid.Generator[Operation] {
 	return rapid.Custom(func(t *rapid.T) Operation {
 		kinds := allowedKinds(config)
 		kindIdx := rapid.IntRange(0, len(kinds)-1).Draw(t, "kind")
 		kind := kinds[kindIdx]
 
 		op := Operation{Kind: kind}
-		fillOperationFields(t, &op, config)
+		fillOperationFields(t, &op, config, seq)
 		return op
 	})
 }
@@ -163,7 +165,7 @@ func drawnOutcomeGen(t *rapid.T, label string) DrawnOutcome {
 }
 
 // fillOperationFields populates the kind-specific fields on the operation.
-func fillOperationFields(t *rapid.T, op *Operation, config PropertyTestConfig) {
+func fillOperationFields(t *rapid.T, op *Operation, config PropertyTestConfig, seq int) {
 	pool := resourcePoolForConfig(config)
 	slotCount := slotCountForConfig(config, pool)
 
@@ -188,6 +190,23 @@ func fillOperationFields(t *rapid.T, op *Operation, config PropertyTestConfig) {
 			op.ResourceIDs = resourceIDsGen(t, config.ResourceCount, 1)
 		}
 		op.Properties = resourcePropsGen(t)
+		// RFC-0041: with rename enabled, OpApply optionally carries a rename
+		// overlay for one slot from ResourceIDs. The executor only honours
+		// the overlay if that slot is StateExists at execution time
+		// (otherwise rename is a no-op). Combined with the property template
+		// above this lets a single apply model an update as label-only,
+		// property-only, or both. The label embeds the operation's sequence
+		// position, so no two renames in a sequence can produce the same
+		// label — label reuse would make slot resolution ambiguous.
+		op.RenameSlotIndex = -1
+		if config.EnableRename && len(op.ResourceIDs) > 0 {
+			if rapid.IntRange(0, 2).Draw(t, "applyRenameRoll") == 0 {
+				op.RenameSlotIndex = renameSlotIndexFromIDs(t, op.ResourceIDs)
+				if op.RenameSlotIndex >= 0 {
+					op.RenameNewLabel = fmt.Sprintf("renamed-%d", seq)
+				}
+			}
+		}
 		if config.EnableFailures {
 			op.DrawnOutcomes = make(map[string]DrawnOutcome)
 			for i := 0; i < slotCount; i++ {
@@ -523,3 +542,15 @@ func subsequenceGen(t *rapid.T, values []string, label string) []string {
 	}
 	return result
 }
+
+// renameSlotIndexFromIDs picks one slot from `ids` to rename as part of an
+// OpApply. Any slot is eligible: the forma builders thread label overrides
+// through parent references, so renaming a slot that others reference keeps
+// their `$res` blocks pointing at the current label. Returns -1 when `ids`
+// is empty — the caller treats that as "no rename on this apply".
+func renameSlotIndexFromIDs(t *rapid.T, ids []int) int {
+	if len(ids) == 0 {
+		return -1
+	}
+	return rapid.SampledFrom(ids).Draw(t, "applyRenameSlot")
+}
diff --git a/tests/blackbox/generators_test.go b/tests/blackbox/generators_test.go
index 85b387738..2a1f34504 100644
--- a/tests/blackbox/generators_test.go
+++ b/tests/blackbox/generators_test.go
@@ -326,7 +326,7 @@ func TestResponseSequenceGen(t *testing.T) {
 				StackCount:     2,
 			}
 			op := Operation{Kind: OpApply}
-			fillOperationFields(rt, &op, config)
+			fillOperationFields(rt, &op, config, 0)
 
 			require.NotNil(t, op.DrawnOutcomes, "DrawnOutcomes should be non-nil when EnableFailures=true")
 			// Should have entries for all resource slots in the target stack.
@@ -347,7 +347,7 @@ func TestResponseSequenceGen(t *testing.T) {
 				StackCount:     2,
 			}
 			op := Operation{Kind: OpApply}
-			fillOperationFields(rt, &op, config)
+			fillOperationFields(rt, &op, config, 0)
 
 			assert.Nil(t, op.DrawnOutcomes, "DrawnOutcomes should be nil when EnableFailures=false")
 		})
@@ -368,7 +368,7 @@ func TestResponseSequenceGen(t *testing.T) {
 
 			// We need a pool for onDependents to be set.
 			op := Operation{Kind: OpDestroy}
-			fillOperationFields(rt, &op, config)
+			fillOperationFields(rt, &op, config, 0)
 
 			require.NotNil(t, op.DrawnOutcomes, "DrawnOutcomes should be non-nil for OpDestroy with EnableFailures")
 
diff --git a/tests/blackbox/harness.go b/tests/blackbox/harness.go
index abc11f72c..a23f4269e 100644
--- a/tests/blackbox/harness.go
+++ b/tests/blackbox/harness.go
@@ -54,6 +54,12 @@ type TestHarness struct {
 	cancel     context.CancelFunc
 	pluginsDir string
 
+	// RenamesAccepted counts renames the agent accepted across all rapid
+	// iterations. Tests that enable rename assert it is non-zero after
+	// rapid.Check so a broken rename path cannot pass vacuously (a rejected
+	// or no-op rename executes no rename at all).
+	RenamesAccepted int
+
 	// Agent subprocess
 	agentCmd     *exec.Cmd
 	agentLogFile *os.File
diff --git a/tests/blackbox/invariants.go b/tests/blackbox/invariants.go
index 402bb6d56..2f32bf386 100644
--- a/tests/blackbox/invariants.go
+++ b/tests/blackbox/invariants.go
@@ -18,13 +18,17 @@ import (
 type ViolationKind int
 
 const (
-	ViolationPhantomResource        ViolationKind = iota // in inventory but not in cloud
-	ViolationOrphanedResource                            // in cloud but not in inventory
-	ViolationPropertyMismatch                            // inventory and cloud properties differ
-	ViolationCommandNotTerminal                          // command not in terminal state
-	ViolationResolvableNotResolved                       // resolvable $ref not properly resolved
-	ViolationModelInventoryMismatch                      // model expected state doesn't match inventory
-	ViolationDuplicateNativeID                           // two or more inventory rows share a NativeID (RFC-0041)
+	ViolationPhantomResource              ViolationKind = iota // in inventory but not in cloud
+	ViolationOrphanedResource                                  // in cloud but not in inventory
+	ViolationPropertyMismatch                                  // inventory and cloud properties differ
+	ViolationCommandNotTerminal                                // command not in terminal state
+	ViolationResolvableNotResolved                             // resolvable $ref not properly resolved
+	ViolationModelInventoryMismatch                            // model expected state doesn't match inventory
+	ViolationDuplicateNativeID                                 // two or more inventory rows share a NativeID (RFC-0041)
+	ViolationRenameOldLabelStillPresent                        // after rename, inventory still has a row at the old label (RFC-0041)
+	ViolationRenameLabelDriftFromNativeID                      // inventory row's label diverges from the slot's CurrentLabel for the same NativeID (RFC-0041)
+	ViolationRenameIdentityChanged                             // a successful update RU changed the resource's NativeID or KSUID (RFC-0041)
+	ViolationRenameRecreatedResource                           // a renamed slot was fulfilled by a create — rename must be an in-place update (RFC-0041)
 )
 
 // Violation describes a single invariant violation.
@@ -726,3 +730,111 @@ func CheckOperationLogInvariants(opLog []testcontrol.OperationLogEntry) []Violat
 
 	return violations
 }
+
+// CheckRenameInvariants verifies RFC-0041 invariants after one or more
+// renames. For every slot whose PreviousLabel is non-empty (a rename
+// landed on it), the inventory must NOT carry a row at the old
+// (Stack, Type, PreviousLabel) tuple with that slot's identity — that
+// would mean the rename left the old row behind instead of renaming the
+// existing one. The identity guard (NativeID/KSUID match) keeps a
+// different slot legitimately renamed onto the freed label from being
+// flagged.
+//
+// Also: for every managed inventory row whose NativeID the model tracks
+// (via SetNativeID), the row's Label must equal the slot's current label,
+// and its KSUID must match the tracked KSUID. This is the positive
+// identity-preservation check: rename keeps the (NativeID, KSUID) pair
+// stable, and the slot's CurrentLabel overlay must match what's in cloud.
+func CheckRenameInvariants(model *StateModel, inventory []pkgmodel.Resource) []Violation {
+	var violations []Violation
+	if model == nil {
+		return violations
+	}
+
+	// Index inventory rows by (stack, type, label) for O(1) lookup.
+	type key struct{ stack, typ, label string }
+	rows := make(map[key]pkgmodel.Resource, len(inventory))
+	for _, r := range inventory {
+		rows[key{stack: r.Stack, typ: r.Type, label: r.Label}] = r
+	}
+
+	for _, stack := range model.Stacks {
+		for slotIdx, res := range stack.Resources {
+			if res == nil || res.PreviousLabel == "" {
+				continue
+			}
+			// Determine the resource type by consulting the pool when one is
+			// present; otherwise default to Test::Generic::Resource.
+			resType := "Test::Generic::Resource"
+			if model.Pool != nil && slotIdx < len(model.Pool.Slots) {
+				resType = model.Pool.Slots[slotIdx].Type
+			}
+			oldKey := key{stack: stack.Label, typ: resType, label: res.PreviousLabel}
+			hit, present := rows[oldKey]
+			if !present || !hit.Managed {
+				continue
+			}
+			// Identity guard: only flag the row if it belongs to this slot's
+			// lineage. A different slot renamed onto the freed label is legal.
+			stackIdx := model.StackIndexByLabel(stack.Label)
+			trackedNativeID := model.GetNativeID(stackIdx, slotIdx)
+			trackedKsuid := model.GetKsuid(stackIdx, slotIdx)
+			sameLineage := (trackedNativeID != "" && hit.NativeID == trackedNativeID) ||
+				(trackedKsuid != "" && hit.Ksuid == trackedKsuid)
+			if !sameLineage {
+				continue
+			}
+			violations = append(violations, Violation{
+				Kind: ViolationRenameOldLabelStillPresent,
+				Message: fmt.Sprintf(
+					"slot %d (stack %s, type %s) was renamed away from %q but a managed inventory row still carries that label (ksuid=%s, nativeID=%s)",
+					slotIdx, stack.Label, resType, res.PreviousLabel, hit.Ksuid, hit.NativeID,
+				),
+			})
+		}
+	}
+
+	// Identity-preservation check via NativeID. For each inventory row whose
+	// NativeID the model has tracked, compare its label to the slot's
+	// CurrentLabel-aware label. Mismatch means a rename either didn't reach
+	// inventory or got reverted without the model's overlay rolling back.
+	nativeIDToSlot := make(map[string][2]int, len(model.NativeIDs))
+	for k, nid := range model.NativeIDs {
+		var stackIdx, slotIdx int
+		fmt.Sscanf(k, "%d:%d", &stackIdx, &slotIdx)
+		nativeIDToSlot[nid] = [2]int{stackIdx, slotIdx}
+	}
+	for _, r := range inventory {
+		if !r.Managed || r.NativeID == "" {
+			continue
+		}
+		slot, tracked := nativeIDToSlot[r.NativeID]
+		if !tracked {
+			continue
+		}
+		expectedLabel := model.LabelForResource(slot[0], slot[1])
+		if r.Label != expectedLabel {
+			violations = append(violations, Violation{
+				Kind: ViolationRenameLabelDriftFromNativeID,
+				Message: fmt.Sprintf(
+					"inventory row NativeID=%s carries label=%q but the model expects label=%q for slot (stack %d, slot %d)",
+					r.NativeID, r.Label, expectedLabel, slot[0], slot[1],
+				),
+			})
+		}
+		// KSUID stability: the row for a tracked NativeID must carry the
+		// KSUID the model recorded for that slot. A fresh KSUID under the
+		// same NativeID means a rename minted a new resource identity.
+		if trackedKsuid := model.GetKsuid(slot[0], slot[1]); trackedKsuid != "" && r.Ksuid != "" && r.Ksuid != trackedKsuid {
+			violations = append(violations, Violation{
+				Kind: ViolationRenameIdentityChanged,
+				Message: fmt.Sprintf(
+					"inventory row NativeID=%s label=%q carries ksuid=%s but the model tracked ksuid=%s for slot (stack %d, slot %d)",
+					r.NativeID, r.Label, r.Ksuid, trackedKsuid, slot[0], slot[1],
+				),
+			})
+		}
+	}
+
+	return violations
+}
diff --git a/tests/blackbox/invariants_rename_test.go b/tests/blackbox/invariants_rename_test.go
index 61137aca3..e5b2beb36 100644
--- a/tests/blackbox/invariants_rename_test.go
+++ b/tests/blackbox/invariants_rename_test.go
@@ -9,6 +9,8 @@ package blackbox
 import (
 	"testing"
 
+	"github.com/stretchr/testify/require"
+
 	pkgmodel "github.com/platform-engineering-labs/formae/pkg/model"
 	"github.com/platform-engineering-labs/formae/tests/testcontrol"
 )
@@ -61,3 +63,58 @@ func TestCheckInvariants_SingleRowPerNativeID_OK(t *testing.T) {
 		}
 	}
 }
+
+// After a rename, a managed inventory row at the slot's previous label is a
+// violation only when it belongs to that slot's lineage (same NativeID or
+// KSUID). A different slot legitimately renamed onto the freed label must
+// not be flagged.
+func TestCheckRenameInvariants_OldLabelIdentityGuard(t *testing.T) {
+	model := NewStateModel(1, 3)
+	model.ApplyCreated(0, []int{1}, "")
+	model.SetNativeID(0, 1, "test-42")
+	model.SetKsuid(0, 1, "K_B")
+	model.RecordRename(0, 1, "renamed-0")
+	model.RecordRename(0, 1, "renamed-1") // PreviousLabel is now "renamed-0"
+
+	// Another lineage's row occupies the freed label: legal, not flagged.
+	reused := []pkgmodel.Resource{
+		{Stack: "stack-0", Type: "Test::Generic::Resource", Label: "renamed-0", NativeID: "test-77", Ksuid: "K_OTHER", Managed: true},
+		{Stack: "stack-0", Type: "Test::Generic::Resource", Label: "renamed-1", NativeID: "test-42", Ksuid: "K_B", Managed: true},
+	}
+	require.Empty(t, CheckRenameInvariants(model, reused),
+		"a different lineage on the freed label must not be flagged")
+
+	// The slot's own lineage still on the old label: the rename leaked it.
+	// Fires the old-label check and, because the tracked NativeID carries
+	// the wrong label, the positive label-drift check as well.
+	leaked := []pkgmodel.Resource{
+		{Stack: "stack-0", Type: "Test::Generic::Resource", Label: "renamed-0", NativeID: "test-42", Ksuid: "K_B", Managed: true},
+	}
+	violations := CheckRenameInvariants(model, leaked)
+	kinds := make(map[ViolationKind]bool, len(violations))
+	for _, v := range violations {
+		kinds[v.Kind] = true
+	}
+	require.True(t, kinds[ViolationRenameOldLabelStillPresent], "leaked old-label row must be flagged: %v", violations)
+}
+
+// For a tracked NativeID the inventory row must carry both the current
+// label and the tracked KSUID — a fresh KSUID under the same NativeID means
+// the rename minted a new resource identity.
+func TestCheckRenameInvariants_KsuidStability(t *testing.T) {
+	model := NewStateModel(1, 3)
+	model.ApplyCreated(0, []int{1}, "")
+	model.SetNativeID(0, 1, "test-42")
+	model.SetKsuid(0, 1, "K_B")
+	model.RecordRename(0, 1, "renamed-0")
+
+	inventory := []pkgmodel.Resource{
+		{Stack: "stack-0", Type: "Test::Generic::Resource", Label: "renamed-0", NativeID: "test-42", Ksuid: "K_FRESH", Managed: true},
+	}
+	violations := CheckRenameInvariants(model, inventory)
+	require.Len(t, violations, 1)
+	require.Equal(t, ViolationRenameIdentityChanged, violations[0].Kind)
+
+	inventory[0].Ksuid = "K_B"
+	require.Empty(t, CheckRenameInvariants(model, inventory))
+}
diff --git a/tests/blackbox/operations.go b/tests/blackbox/operations.go
index b88efd613..33c0cd7e4 100644
--- a/tests/blackbox/operations.go
+++ b/tests/blackbox/operations.go
@@ -95,6 +95,19 @@ type Operation struct {
 	// nil map means no failure injection (all succeed).
 	DrawnOutcomes map[string]DrawnOutcome
 
+	// For OpApply: optional rename overlay. When RenameSlotIndex >= 0 and
+	// the slot is currently StateExists, the apply additionally renames the
+	// slot — the constructed forma carries Label=RenameNewLabel and
+	// Alias=<slot's current label> for that one resource. Combined with the
+	// usual property-template path this lets a single apply model:
+	//   - property change only (RenameSlotIndex = -1)
+	//   - label change only (RenameSlotIndex set, Properties left at the
+	//     same template that produced the current state)
+	//   - both (RenameSlotIndex set, Properties template changed)
+	// (RFC-0041.)
+	RenameSlotIndex int
+	RenameNewLabel  string
+
 	// Set during execution to track ordering.
 	SequenceNum int
 }
@@ -133,6 +146,23 @@ type ResourceSnapshot struct {
 	SlotIndex  int
 	State      ResourceState
 	Properties string
+	// CurrentLabel/PreviousLabel capture the rename overlay at snapshot time
+	// so a failed/canceled OpRename can be unwound. Without these a rename
+	// that was accepted then rejected during execution would leave the
+	// model's CurrentLabel pointing at a label the engine never persisted.
+	CurrentLabel  string
+	PreviousLabel string
+}
+
+// PendingRename records that a command carried a rename overlay: the forma
+// declared the slot under NewLabel with Alias set to OldLabel. On a
+// successful command the engine must have performed it as an in-place update
+// (an update RU carrying OldLabel); the drain asserts that.
+type PendingRename struct {
+	StackIndex int
+	SlotIndex  int
+	OldLabel   string
+	NewLabel   string
 }
 
 // AcceptedCommand tracks a command that was accepted by the agent during the chaos phase.
@@ -141,7 +171,8 @@ type AcceptedCommand struct {
 	Snapshots      []ResourceSnapshot // pre-command state for revert on cancel
 	OpLogSize      int                // operation log length immediately after acceptance
 	RequestedSlots []ResourceSlotRef
-	IsReconcile    bool // true if the command was reconcile mode (properties = full desired state)
+	IsReconcile    bool           // true if the command was reconcile mode (properties = full desired state)
+	Rename         *PendingRename // set when the command carried a rename overlay
 	// Resolved is true when the cancel handler has already processed this
 	// command. The command remains in AcceptedCommands so that
 	// DrainPendingCommands can include its outcome when resolving conflicts
@@ -194,6 +225,10 @@ type PropertyTestConfig struct {
 	// EnableCrashInjection allows OpCrashAgent operations (kill -9 + restart).
 	EnableCrashInjection bool
 
+	// EnableRename allows OpRename operations (RFC-0041). When set the
+	// generator may draw a rename for any slot currently in StateExists.
+	EnableRename bool
+
 	// StackCount is the number of independent stacks (1 for sequential tests, 2-3 for concurrent).
 	StackCount int
 }
diff --git a/tests/blackbox/property_test.go b/tests/blackbox/property_test.go
index 1fac028f8..e29e7ba91 100644
--- a/tests/blackbox/property_test.go
+++ b/tests/blackbox/property_test.go
@@ -151,6 +151,7 @@ func TestProperty_FullChaos(t *testing.T) {
 				EnableForceReconcile: true,
 				EnableTTL:            true,
 				EnableCrashInjection: true,
+				EnableRename:         true,
 			}
 
 			h.ResetAgentState(t)
@@ -177,3 +178,55 @@ func TestProperty_FullChaos(t *testing.T) {
 		})
 	})
 }
+
+// TestProperty_RenameViaApply exercises the rename-folded-into-OpApply
+// path in isolation. Single stack, applies only (reconcile + patch),
+// EnableRename on, no chaos ops. The generator may decide on each apply
+// whether to also rename one slot from ResourceIDs; combined with the
+// usual property template the apply models an update as label-only,
+// property-only, or both.
+//
+// This is the focused regression for RFC-0041: any rename-shaped failure
+// (duplicate NativeID, old label still in inventory, slot label drift
+// from the overlay) fires from CheckInvariants + CheckRenameInvariants
+// inside AssertAllInvariants.
+func TestProperty_RenameViaApply(t *testing.T) {
+	testutil.RunTestFromProjectRoot(t, func(t *testing.T) {
+		h := NewTestHarness(t, 10*time.Second)
+		defer h.Cleanup()
+
+		rapid.Check(t, func(rt *rapid.T) {
+			config := PropertyTestConfig{
+				ResourceCount:  10,
+				OperationCount: Range{Min: 3, Max: 10},
+				StackCount:     1,
+				EnableRename:   true,
+			}
+
+			h.ResetAgentState(t)
+			model := NewStateModel(config.StackCount, config.ResourceCount)
+			h.SetupStacks(t, model, config)
+
+			ops := OperationSequenceGen(config).Draw(rt, "ops")
+			for i, op := range ops {
+				op.SequenceNum = i
+				h.ExecuteOperation(t, &op, model)
+				// Drain after every operation: with a single stack, a second
+				// apply submitted while the first is in flight is rejected by
+				// the agent's stack-overlap admission check. Rename needs the
+				// slot to already exist, i.e. exactly those later applies —
+				// serializing keeps them (and their renames) landing.
+				h.DrainPendingCommands(t, model, 30*time.Second)
+			}
+
+			h.TriggerSyncAndWait(t, model)
+			h.AssertAllInvariants(t, model)
+		})
+
+		// Whether any generated sequence exercises a rename depends on the
+		// draws (the slot must already exist when the rename-carrying apply
+		// executes), so the count is informational here. Guaranteed rename
+		// coverage lives in TestRenameViaApply_Deterministic.
+		t.Logf("TestProperty_RenameViaApply: %d renames accepted across the run", h.RenamesAccepted)
+	})
+}
diff --git a/tests/blackbox/rename_test.go b/tests/blackbox/rename_test.go
new file mode 100644
index 000000000..dc874b1c9
--- /dev/null
+++ b/tests/blackbox/rename_test.go
@@ -0,0 +1,71 @@
+// © 2026 Platform Engineering Labs Inc.
+//
+// SPDX-License-Identifier: FSL-1.1-ALv2
+
+//go:build integration || property
+
+package blackbox
+
+import (
+	"testing"
+	"time"
+
+	"github.com/platform-engineering-labs/formae/internal/metastructure/testutil"
+	"github.com/stretchr/testify/require"
+)
+
+// Deterministic rename coverage: create resources, rename one via the apply
+// overlay, and assert the rename invariants against real inventory. The
+// rapid-driven TestProperty_RenameViaApply explores rename under generated
+// sequences, but whether any sequence exercises a rename depends on the
+// draws; this test guarantees the rename path executes on every run.
+func TestRenameViaApply_Deterministic(t *testing.T) {
+	testutil.RunTestFromProjectRoot(t, func(t *testing.T) {
+		h := NewTestHarness(t, 10*time.Second)
+		defer h.Cleanup()
+		h.ResetAgentState(t)
+		config := PropertyTestConfig{ResourceCount: 10, StackCount: 1, EnableRename: true}
+		model := NewStateModel(config.StackCount, config.ResourceCount)
+		h.SetupStacks(t, model, config)
+
+		create := Operation{Kind: OpApply, ApplyMode: "reconcile", StackIndex: 0,
+			ResourceIDs: []int{0, 1, 2}, Properties: defaultDestroyParentProps,
+			ChildProperties: defaultDestroyChildProps, RenameSlotIndex: -1}
+		h.ExecuteOperation(t, &create, model)
+		h.DrainPendingCommands(t, model, 30*time.Second)
+		require.Equal(t, StateExists, model.Resource(0, 0).State, "create must land before the rename")
+
+		// Rename the parent (slot 0) while its child (slot 1) references it:
+		// the overlay rewrites the child's $res reference to the new label.
+		rename := Operation{Kind: OpApply, ApplyMode: "reconcile", StackIndex: 0,
+			ResourceIDs: []int{0, 1, 2}, Properties: defaultDestroyParentProps,
+			ChildProperties: defaultDestroyChildProps, RenameSlotIndex: 0, RenameNewLabel: "renamed-0"}
+		h.ExecuteOperation(t, &rename, model)
+		h.DrainPendingCommands(t, model, 30*time.Second)
+
+		require.NotZero(t, h.RenamesAccepted, "the rename apply must be accepted")
+		require.Equal(t, "renamed-0", model.Resource(0, 0).CurrentLabel)
+
+		// A second rename of the same slot exercises the PreviousLabel chain.
+		rename2 := Operation{Kind: OpApply, ApplyMode: "reconcile", StackIndex: 0,
+			ResourceIDs: []int{0, 1, 2}, Properties: defaultDestroyParentProps,
+			ChildProperties: defaultDestroyChildProps, RenameSlotIndex: 0, RenameNewLabel: "renamed-1"}
+		h.ExecuteOperation(t, &rename2, model)
+		h.DrainPendingCommands(t, model, 30*time.Second)
+
+		h.TriggerSyncAndWait(t, model)
+		h.AssertAllInvariants(t, model)
+
+		managed, _, err := h.extractManagedAndUnmanagedInventory()
+		require.NoError(t, err)
+		var labels []string
+		for _, r := range managed {
+			if r.Stack == "stack-0" {
+				labels = append(labels, r.Label)
+			}
+		}
+		require.Contains(t, labels, "renamed-1", "inventory must carry the renamed label")
+		require.NotContains(t, labels, "renamed-0", "the intermediate label must be gone")
+		require.NotContains(t, labels, "res-stack-0-a", "the original label must be gone")
+	})
+}
diff --git a/tests/blackbox/state_model.go b/tests/blackbox/state_model.go
index 15496ea63..0aa16bbfd 100644
--- a/tests/blackbox/state_model.go
+++ b/tests/blackbox/state_model.go
@@ -28,6 +28,16 @@ type ExpectedResource struct {
 	Index      int
 	Properties string
 	State      ResourceState
+	// CurrentLabel overrides the default index-derived label for this slot.
+	// Set when an OpRename has renamed the slot's resource. Empty means the
+	// slot uses the default label produced by resourceLabelForStack().
+	// (RFC-0041 follow-up: enables OpRename in the rapid generators.)
+	CurrentLabel string
+	// PreviousLabel is the label this slot carried before the most recent
+	// rename. Used by OpRename invariants and by executeRename to build the
+	// `alias` field on the next forma. Cleared once a subsequent rename
+	// records its own previous label.
+	PreviousLabel string
 }
 
 // ExpectedUnmanagedResource tracks the expected state of a discovered
@@ -74,6 +84,14 @@ type StateModel struct {
 	// Populated from command response ResourceUpdate.NativeID on successful
 	// creates/updates. Cleared on successful deletes.
 	NativeIDs map[string]string
+	// Ksuids maps "stackIdx:slotIdx" → the resource's KSUID, populated from
+	// command response ResourceUpdate.ResourceID the same way as NativeIDs.
+	// A rename must keep both stable; the correction path checks that.
+	Ksuids map[string]string
+	// PendingViolations collects violations detected while correcting the
+	// model from command outcomes (e.g. an update RU that changed a
+	// resource's identity). Drained and asserted by AssertAllInvariants.
+	PendingViolations []Violation
 	// DriftExcludedStacks marks stacks whose resources are no longer valid
 	// drift targets this iteration: a canceled changeset can leave its
 	// resources registered as in-progress with the synchronizer for an
@@ -135,6 +153,7 @@ func NewStateModel(stackCount, resourcesPerStack int) *StateModel {
 		UnmanagedResources:  make(map[string]*ExpectedUnmanagedResource),
 		AuthoritativeSlots:  make(map[string]bool),
 		NativeIDs:           make(map[string]string),
+		Ksuids:              make(map[string]string),
 		DriftExcludedStacks: make(map[int]bool),
 	}
 }
@@ -186,6 +205,27 @@ func (m *StateModel) SupersedeSlots(refs []ResourceSlotRef) {
 	}
 }
 
+func (m *StateModel) SetKsuid(stackIdx, slotIdx int, ksuid string) {
+	if ksuid != "" {
+		m.Ksuids[nativeIDKey(stackIdx, slotIdx)] = ksuid
+	}
+}
+
+func (m *StateModel) GetKsuid(stackIdx, slotIdx int) string {
+	return m.Ksuids[nativeIDKey(stackIdx, slotIdx)]
+}
+
+func (m *StateModel) ClearKsuid(stackIdx, slotIdx int) {
+	delete(m.Ksuids, nativeIDKey(stackIdx, slotIdx))
+}
+
+// AddPendingViolation records a violation detected outside the invariant
+// checks (e.g. during command-outcome correction). Asserted and cleared by
+// AssertAllInvariants.
+func (m *StateModel) AddPendingViolation(v Violation) {
+	m.PendingViolations = append(m.PendingViolations, v)
+}
+
 // FindDriftEligibleResource finds a managed resource that exists in the model,
 // has a tracked NativeID, and is untouched by in-flight commands. Used for
 // selecting OOB drift targets: drift is absorbed synchronously via a forced
@@ -236,12 +276,7 @@ func (m *StateModel) FindDriftEligibleResource(sequenceNum int) (stackIdx, slotI
 			if m.Pool != nil && m.Pool.IsCrossStack(idx) && busyStacks[0] {
 				continue
 			}
-			var label string
-			if m.Pool != nil {
-				label = m.Pool.LabelForStack(stack.Label, idx)
-			} else {
-				label = resourceLabelForStack(stack.Label, idx)
-			}
+			label := m.LabelForResource(si, idx)
 			var rType string
 			if m.Pool != nil {
 				rType = m.Pool.Slots[idx].Type
@@ -258,26 +293,6 @@ func (m *StateModel) FindDriftEligibleResource(sequenceNum int) (stackIdx, slotI
 	return c.stackIdx, c.slotIdx, c.stackLabel, c.label, c.rType, c.nativeID, true
 }
 
-// NativeIDsByLabel returns a map of "stackLabel:resourceLabel" → NativeID for
-// all tracked native IDs. This matches the format expected by
-// buildPluginOpSequences and resolveReadMatchKey.
-func (m *StateModel) NativeIDsByLabel() map[string]string {
-	result := make(map[string]string, len(m.NativeIDs))
-	for key, nativeID := range m.NativeIDs {
-		var stackIdx, slotIdx int
-		fmt.Sscanf(key, "%d:%d", &stackIdx, &slotIdx)
-		stackLabel := m.Stacks[stackIdx].Label
-		var label string
-		if m.Pool != nil {
-			label = m.Pool.LabelForStack(stackLabel, slotIdx)
-		} else {
-			label = resourceLabelForStack(stackLabel, slotIdx)
-		}
-		result[stackLabel+":"+label] = nativeID
-	}
-	return result
-}
-
 func (m *StateModel) MarkAuthoritativeSlot(stackIdx, slotIdx int) {
 	m.AuthoritativeSlots[slotKeyString(stackIdx, slotIdx)] = true
 }
@@ -422,8 +437,16 @@ func (m *StateModel) Resource(stackIndex, idx int) *ExpectedResource {
 	return m.Stacks[stackIndex].Resources[idx]
 }
 
-// LabelForResource returns the expected label for the resource slot on the stack.
+// LabelForResource returns the expected label for the resource slot on the
+// stack. RFC-0041: after a RecordRename, the slot's CurrentLabel overrides
+// the index-derived default; invariant checks and findResourceSlot rely on
+// this to match a renamed slot against its inventory row by the new label.
 func (m *StateModel) LabelForResource(stackIndex, idx int) string {
+	if stackIndex >= 0 && stackIndex < len(m.Stacks) {
+		if res, ok := m.Stacks[stackIndex].Resources[idx]; ok && res != nil && res.CurrentLabel != "" {
+			return res.CurrentLabel
+		}
+	}
 	stackLabel := m.Stacks[stackIndex].Label
 	if m.Pool != nil {
 		return m.Pool.LabelForStack(stackLabel, idx)
@@ -431,6 +454,60 @@ func (m *StateModel) LabelForResource(stackIndex, idx int) string {
 	return resourceLabelForStack(stackLabel, idx)
 }
 
+// DefaultLabelForResource returns the index-derived label for the slot,
+// ignoring any rename overlay. This is the label a slot gets on (re)create.
+func (m *StateModel) DefaultLabelForResource(stackIndex, idx int) string {
+	stackLabel := m.Stacks[stackIndex].Label
+	if m.Pool != nil {
+		return m.Pool.LabelForStack(stackLabel, idx)
+	}
+	return resourceLabelForStack(stackLabel, idx)
+}
+
+// RecordRename updates the model after a rename was accepted. After this
+// call, LabelForResource returns newLabel and the slot remembers the label
+// it carried immediately before.
+func (m *StateModel) RecordRename(stackIdx, slotIdx int, newLabel string) {
+	res, ok := m.Stack(stackIdx).Resources[slotIdx]
+	if !ok || res == nil {
+		return
+	}
+	res.PreviousLabel = m.LabelForResource(stackIdx, slotIdx)
+	res.CurrentLabel = newLabel
+}
+
+// StackIndexByLabel returns the stack index for the given stack label, or -1
+// if no stack with that label exists.
+func (m *StateModel) StackIndexByLabel(label string) int {
+	for i := range m.Stacks {
+		if m.Stacks[i].Label == label {
+			return i
+		}
+	}
+	return -1
+}
+
+// LabelOverrides returns a map of slot index -> current label for slots that
+// have been renamed. Callers that build a forma for a stack pass this map to
+// FormaFromPoolResources / FormaFromStackResources so the constructed forma
+// carries and references resources by their post-rename labels. A nil map
+// means every slot uses its default index-derived label.
+func (m *StateModel) LabelOverrides(stackIdx int) map[int]string {
+	if stackIdx < 0 || stackIdx >= len(m.Stacks) {
+		return nil
+	}
+	var overrides map[int]string
+	for idx, res := range m.Stack(stackIdx).Resources {
+		if res != nil && res.CurrentLabel != "" {
+			if overrides == nil {
+				overrides = make(map[int]string)
+			}
+			overrides[idx] = res.CurrentLabel
+		}
+	}
+	return overrides
+}
+
 // TypeForResource returns the expected type for the resource slot.
 func (m *StateModel) TypeForResource(idx int) string {
 	if m.Pool != nil {
@@ -468,6 +545,11 @@ func (m *StateModel) ApplyCreatedResolved(stackIndex int, propertiesByID map[int
 }
 
 // ApplyDestroyed marks the given resources on the given stack as not existing.
+// The rename overlay is deliberately kept: a destroyed slot's label stays at
+// its renamed value, so a later recreate targets the same label the engine
+// last knew the slot by. Clearing it would make a recreate after a FAILED
+// destroy (real resource still alive under the renamed label) declare a
+// second resource under the default label.
 func (m *StateModel) ApplyDestroyed(stackIndex int, resourceIDs []int) {
 	stack := &m.Stacks[stackIndex]
 	for _, id := range resourceIDs {
@@ -547,10 +629,12 @@ func (m *StateModel) SnapshotResources(stackIndex int, resourceIDs []int) []Reso
 		res := m.Resource(stackIndex, id)
 		if res != nil {
 			snapshots = append(snapshots, ResourceSnapshot{
-				StackIndex: stackIndex,
-				SlotIndex:  id,
-				State:      res.State,
-				Properties: res.Properties,
+				StackIndex:    stackIndex,
+				SlotIndex:     id,
+				State:         res.State,
+				Properties:    res.Properties,
+				CurrentLabel:  res.CurrentLabel,
+				PreviousLabel: res.PreviousLabel,
 			})
 		}
 	}
@@ -564,6 +648,8 @@ func (m *StateModel) RevertResources(snapshots []ResourceSnapshot) {
 		if res != nil {
 			res.State = snap.State
 			res.Properties = snap.Properties
+			res.CurrentLabel = snap.CurrentLabel
+			res.PreviousLabel = snap.PreviousLabel
 		}
 	}
 }
diff --git a/tests/blackbox/state_model_test.go b/tests/blackbox/state_model_test.go
index 667715ea9..fa26f0e7a 100644
--- a/tests/blackbox/state_model_test.go
+++ b/tests/blackbox/state_model_test.go
@@ -42,7 +42,7 @@ func TestCorrectModelFromCommandOutcome_FailedCreateForcesNotExist(t *testing.T)
 	}
 
 	corrected := map[struct{ stackIdx, slotIdx int }]bool{}
-	correctModelFromCommandOutcome(t, cmd, model, nil, snapshots, corrected, true, nil)
+	correctModelFromCommandOutcome(t, cmd, model, nil, snapshots, corrected, true, nil, nil)
 
 	require.Equal(t, StateNotExist, model.Resource(0, 1).State,
 		"a failed create must leave the slot NotExist, not revert to a stale Exists snapshot")
@@ -68,7 +68,7 @@ func TestCorrectModelFromCommandOutcome_FailedDeleteRevertsToSnapshot(t *testing
 	}
 
 	corrected := map[struct{ stackIdx, slotIdx int }]bool{}
-	correctModelFromCommandOutcome(t, cmd, model, nil, snapshots, corrected, true, nil)
+	correctModelFromCommandOutcome(t, cmd, model, nil, snapshots, corrected, true, nil, nil)
 
 	require.Equal(t, StateExists, model.Resource(0, 1).State,
 		"a failed delete leaves the resource in place, reverting to its Exists snapshot")
@@ -95,8 +95,8 @@ func TestCorrectModelFromCommandOutcome_ReverseOrderFailedCreatesStayNotExist(t
 	corrected := map[struct{ stackIdx, slotIdx int }]bool{}
 	newerSnap := []ResourceSnapshot{{StackIndex: 0, SlotIndex: 1, State: StateNotExist}}
 	olderSnap := []ResourceSnapshot{{StackIndex: 0, SlotIndex: 1, State: StateExists}} // stale
-	correctModelFromCommandOutcome(t, newerCmd, model, nil, newerSnap, corrected, true, nil)
-	correctModelFromCommandOutcome(t, olderCmd, model, nil, olderSnap, corrected, true, nil)
+	correctModelFromCommandOutcome(t, newerCmd, model, nil, newerSnap, corrected, true, nil, nil)
+	correctModelFromCommandOutcome(t, olderCmd, model, nil, olderSnap, corrected, true, nil, nil)
 
 	require.Equal(t, StateNotExist, model.Resource(0, 1).State,
 		"an older failed-create command must not resurrect a slot from its stale Exists snapshot")
@@ -579,7 +579,7 @@ func TestCorrectModelFromCommandOutcome_UnmentionedCrossStackSlotReverts(t *test
 		ResourceUpdates: nil, // the command died before reaching this slot
 	}
 	corrected := map[struct{ stackIdx, slotIdx int }]bool{}
-	correctModelFromCommandOutcome(t, cmd, model, model.Pool, snapshots, corrected, false, nil)
+	correctModelFromCommandOutcome(t, cmd, model, model.Pool, snapshots, corrected, false, nil, nil)
 
 	require.Equal(t, StateNotExist, model.Resource(1, crossIdx).State,
 		"an unmentioned cross-stack slot in a failed command reverts to its snapshot")
@@ -713,7 +713,7 @@ func TestCorrectModelFromCommandOutcome_TTLSupersededSlotStaysDestroyed(t *testi
 	}
 	corrected := map[struct{ stackIdx, slotIdx int }]bool{}
 	ac := model.AcceptedCommands[0]
-	correctModelFromCommandOutcome(t, cmd, model, model.Pool, ac.Snapshots, corrected, true, ac.SupersededSlots)
+	correctModelFromCommandOutcome(t, cmd, model, model.Pool, ac.Snapshots, corrected, true, ac.SupersededSlots, nil)
 
 	require.Equal(t, StateNotExist, model.Resource(2, xslot).State,
 		"a TTL-destroyed slot must not be resurrected by a stale command's create RU")
@@ -745,9 +745,116 @@ func TestCorrectModelFromCommandOutcome_UnmentionedSlotRevertsProperties(t *test
 		}},
 	}
 	corrected := map[struct{ stackIdx, slotIdx int }]bool{}
-	correctModelFromCommandOutcome(t, cmd, model, nil, snapshots, corrected, false, nil)
+	correctModelFromCommandOutcome(t, cmd, model, nil, snapshots, corrected, false, nil, nil)
 
 	require.Equal(t, StateExists, model.Resource(0, 1).State)
 	require.Equal(t, `{"Value":"v1"}`, model.Resource(0, 1).Properties,
 		"optimistic properties must revert to the snapshot when the failed command never touched the slot")
 }
+
+// A failed command whose renamed slot produced no resource update must have
+// the optimistic rename rolled back, even though the slot's State never
+// changed — the engine never persisted the new label, so keeping it would
+// let the model track a label that does not exist in inventory.
+func TestCorrectModelFromCommandOutcome_UnmentionedSlotRevertsLabels(t *testing.T) {
+	model := NewStateModel(1, 3)
+	model.ApplyCreated(0, []int{1}, "")
+	model.RecordRename(0, 1, "renamed-0") // optimistic: rename accepted
+
+	snapshots := []ResourceSnapshot{{StackIndex: 0, SlotIndex: 1, State: StateExists}} // pre-rename: no overlay
+	cmd := &apimodel.Command{
+		CommandID:       "cmd-failed-rename",
+		State:           "FinishedWithErrors",
+		ResourceUpdates: nil, // the renamed slot never got a resource update
+	}
+
+	corrected := map[struct{ stackIdx, slotIdx int }]bool{}
+	correctModelFromCommandOutcome(t, cmd, model, nil, snapshots, corrected, true, nil, nil)
+
+	require.Empty(t, model.Resource(0, 1).CurrentLabel,
+		"the optimistic rename must be rolled back when the slot is unmentioned in a failed command")
+	require.Empty(t, model.Resource(0, 1).PreviousLabel)
+	require.Equal(t, StateExists, model.Resource(0, 1).State)
+}
+
+// A successful command that carried a rename must contain a success update
+// RU at the renamed label — a destroy+recreate (or a dropped alias that made
+// the engine treat the new label as a fresh resource) produces a create RU
+// there instead.
+func TestCorrectModelFromCommandOutcome_RenameFulfilledByCreateIsViolation(t *testing.T) {
+	model := NewStateModel(1, 3)
+	model.ApplyCreated(0, []int{1}, "")
+	model.SetNativeID(0, 1, "test-42")
+	model.RecordRename(0, 1, "renamed-0")
+
+	cmd := &apimodel.Command{
+		CommandID: "cmd-recreated-rename",
+		State:     "Success",
+		ResourceUpdates: []apimodel.ResourceUpdate{{
+			StackName:     "stack-0",
+			ResourceLabel: "renamed-0",
+			Operation:     "create", // rename executed as destroy+recreate
+			State:         "Success",
+			NativeID:      "test-99",
+		}},
+	}
+
+	corrected := map[struct{ stackIdx, slotIdx int }]bool{}
+	rename := &PendingRename{StackIndex: 0, SlotIndex: 1, OldLabel: "res-stack-0-b", NewLabel: "renamed-0"}
+	correctModelFromCommandOutcome(t, cmd, model, nil, nil, corrected, false, nil, rename)
+
+	require.NotEmpty(t, model.PendingViolations)
+	require.Equal(t, ViolationRenameRecreatedResource, model.PendingViolations[0].Kind)
+
+	// The same command with an in-place update RU produces no violation.
+	model2 := NewStateModel(1, 3)
+	model2.ApplyCreated(0, []int{1}, "")
+	model2.SetNativeID(0, 1, "test-42")
+	model2.RecordRename(0, 1, "renamed-0")
+	cmd2 := &apimodel.Command{
+		CommandID: "cmd-genuine-rename",
+		State:     "Success",
+		ResourceUpdates: []apimodel.ResourceUpdate{{
+			StackName:     "stack-0",
+			ResourceLabel: "renamed-0",
+			Operation:     "update",
+			State:         "Success",
+			NativeID:      "test-42",
+		}},
+	}
+	correctModelFromCommandOutcome(t, cmd2, model2, nil, nil, map[struct{ stackIdx, slotIdx int }]bool{}, false, nil, rename)
+	require.Empty(t, model2.PendingViolations)
+}
+
+// An update RU never changes a resource's identity — a different NativeID or
+// KSUID in the response means the engine replaced the resource instead of
+// updating it in place. The check must fire BEFORE the model adopts the new
+// identity, or the final invariants compare against the adopted value and
+// pass vacuously.
+func TestCorrectModelFromCommandOutcome_UpdateChangingIdentityIsViolation(t *testing.T) {
+	model := NewStateModel(1, 3)
+	model.ApplyCreated(0, []int{1}, "")
+	model.SetNativeID(0, 1, "test-42")
+	model.SetKsuid(0, 1, "K_OLD")
+
+	cmd := &apimodel.Command{
+		CommandID: "cmd-identity-swap",
+		State:     "Success",
+		ResourceUpdates: []apimodel.ResourceUpdate{{
+			StackName:     "stack-0",
+			ResourceLabel: "res-stack-0-b",
+			Operation:     "update",
+			State:         "Success",
+			NativeID:      "test-99",
+			ResourceID:    "K_NEW",
+		}},
+	}
+
+	corrected := map[struct{ stackIdx, slotIdx int }]bool{}
+	correctModelFromCommandOutcome(t, cmd, model, nil, nil, corrected, false, nil, nil)
+
+	require.Len(t, model.PendingViolations, 2, "both the NativeID and the KSUID change must be flagged")
+	for _, v := range model.PendingViolations {
+		require.Equal(t, ViolationRenameIdentityChanged, v.Kind)
+	}
+}