diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
index 9fd89c6a9..d56cbf77f 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -248,6 +248,19 @@ A `Deref` projection in the projections list changes the target of the write ope
   rule <k> #traverseProjection(_, VAL, .ProjectionElems, _) ~> #readProjection(false) => VAL ... </k>
   rule <k> #traverseProjection(_, VAL, .ProjectionElems, _) ~> (#readProjection(true) => #writeMoved ~> VAL) ... </k>
 
+  // interior mutability permits projected writeback
+  rule <k> #traverseProjection(toLocal(I), _ORIGINAL, .ProjectionElems, CONTEXTS)
+        ~> #writeProjection(NEW)
+        => #forceSetLocal(local(I), #buildUpdate(NEW, CONTEXTS))
+       ...
+       </k>
+       <locals> LOCALS </locals>
+    requires CONTEXTS =/=K .Contexts
+     andBool 0 <=Int I andBool I <Int size(LOCALS)
+     andBool isTypedLocal(LOCALS[I])
+     andBool #allowsInteriorMutation(lookupTy(tyOfLocal({LOCALS[I]}:>TypedLocal)))
+    [priority(40), preserves-definedness]
+
   rule <k> #traverseProjection(toLocal(I), _ORIGINAL, .ProjectionElems, CONTEXTS)
         ~> #writeProjection(NEW)
         => #setLocalValue(place(local(I), .ProjectionElems), #buildUpdate(NEW, CONTEXTS))
diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/types.md b/kmir/src/kmir/kdist/mir-semantics/rt/types.md
index ee42a817c..967dda983 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/types.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/types.md
@@ -8,6 +8,8 @@ requires "value.md"
 
 module RT-TYPES
   imports BOOL
+  imports INT
+  imports STRING
   imports MAP
   imports K-EQUAL
 
@@ -146,6 +148,21 @@ To make this function total, an optional `MaybeTy` is used.
   rule elemTy(     _                  ) => TyUnknown [owise]
 ```
 
+## Interior Mutability
+
+Rust models interior mutability with `UnsafeCell`. When the runtime determines whether a projected write can observe mutation through a shared reference, it relies on `#allowsInteriorMutation` to detect that marker inside Stable MIR type metadata.
+
+```k
+  syntax Bool ::= #allowsInteriorMutation(TypeInfo) [function, total]
+  // ------------------------------------------------------
+  // Stable MIR serializes struct names as either `mirString` or a plain `String`.
+  rule #allowsInteriorMutation(typeInfoStructType(mirString(NAME), _, _, _))
+    => findString(NAME, "UnsafeCell", 0) =/=Int -1
+  rule #allowsInteriorMutation(typeInfoStructType(NAME:String, _, _, _))
+    => findString(NAME, "UnsafeCell", 0) =/=Int -1
+  rule #allowsInteriorMutation(_) => false [owise]
+```
+
 ## Static and Dynamic Metadata for Types
 
 References to data on the heap or stack may require metadata, most commonly the size of slices, which is not statically known.