diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
index f76620160..c50f5783d 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -1606,6 +1606,30 @@ The first cast is reified as a `thunk`, the second one resolves it and eliminate
      andBool lookupTy(TY_DEST_INNER) ==K lookupTy(TY_SRC_OUTER) // and is well-formed (invariant)
 ```
 
+Transmuting a value `T` into a single-field wrapper struct `G<T>` (or vice versa) is sound when the struct
+has its field at zero offset and `transmute` compiled (guaranteeing equal sizes).
+These are essentially `#[repr(transparent)]` but are `#[repr(rust)]` by default without the annotation and
+thus there are no compiler optimisations to remove the transmute (there would be otherwise for downcast).
+The layout is the same for the wrapped type and so the cast in either direction is sound.
+
+```k
+  // Up: T -> Wrapper(T)
+  rule <k> #cast(VAL:Value, castKindTransmute, TY_SOURCE, TY_TARGET)
+          =>
+            Aggregate(variantIdx(0), ListItem(VAL))
+          ...
+        </k>
+      requires #transparentFieldTy(lookupTy(TY_TARGET)) ==K TY_SOURCE
+
+  // Down: Wrapper(T) -> T
+  rule <k> #cast(Aggregate(variantIdx(0), ListItem(VAL)), castKindTransmute, TY_SOURCE, TY_TARGET)
+          =>
+            VAL
+          ...
+        </k>
+      requires {#transparentFieldTy(lookupTy(TY_SOURCE))}:>Ty ==K TY_TARGET
+```
+
 Casting a byte array/slice to an integer reinterprets the bytes in little-endian order.
 
 ```k
diff --git a/kmir/src/tests/integration/data/prove-rs/box_heap_alloc-fail.rs b/kmir/src/tests/integration/data/prove-rs/box_heap_alloc-fail.rs
new file mode 100644
index 000000000..10988cbe7
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/box_heap_alloc-fail.rs
@@ -0,0 +1,4 @@
+fn main() {
+    let a = Box::new(42i32);
+    assert!(*a == 42);
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/show/box_heap_alloc-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/box_heap_alloc-fail.main.expected
new file mode 100644
index 000000000..6b316872b
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/box_heap_alloc-fail.main.expected
@@ -0,0 +1,15 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (199 steps)
+└─ 3 (stuck, leaf)
+    #execIntrinsic ( IntrinsicFunction ( symbol ( "volatile_load" ) ) , operandConst
+    span: 32
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/volatile_load_static-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/volatile_load_static-fail.main.expected
new file mode 100644
index 000000000..f792b03d2
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/volatile_load_static-fail.main.expected
@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (17 steps)
+└─ 3 (stuck, leaf)
+    #traverseProjection ( toLocal ( 3 ) , thunk ( #decodeConstant ( constantKindAllo
+    function: main
+    span: 53
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-fail.main.expected
new file mode 100644
index 000000000..0c9649cc5
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/volatile_store_static-fail.main.expected
@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (17 steps)
+└─ 3 (stuck, leaf)
+    #traverseProjection ( toLocal ( 4 ) , thunk ( #decodeConstant ( constantKindAllo
+    function: main
+    span: 57
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_down.rs b/kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_down.rs
new file mode 100644
index 000000000..7d48657eb
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_down.rs
@@ -0,0 +1,7 @@
+struct Wrapper(u64);
+
+fn main() {
+    let wrapped = Wrapper(42);
+    let val: u64 = unsafe { core::mem::transmute::<Wrapper, u64>(wrapped) };
+    assert!(val == 42);
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_up.rs b/kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_up.rs
new file mode 100644
index 000000000..043193722
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/transmute_transparent_wrapper_up.rs
@@ -0,0 +1,7 @@
+struct Wrapper(u64);
+
+fn main() {
+    let val: u64 = 42;
+    let wrapped: Wrapper = unsafe { core::mem::transmute::<u64, Wrapper>(val) };
+    assert!(wrapped.0 == 42);
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/volatile_load_static-fail.rs b/kmir/src/tests/integration/data/prove-rs/volatile_load_static-fail.rs
new file mode 100644
index 000000000..7704d6ae2
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/volatile_load_static-fail.rs
@@ -0,0 +1,11 @@
+#![feature(core_intrinsics)]
+static A: i32 = 5555;
+
+fn main() {
+    let val: i32;
+    unsafe {
+        val = std::intrinsics::volatile_load(&A as *const i32);
+    }
+
+    assert!(val == 5555);
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/volatile_store_static-fail.rs b/kmir/src/tests/integration/data/prove-rs/volatile_store_static-fail.rs
new file mode 100644
index 000000000..852d0a602
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/volatile_store_static-fail.rs
@@ -0,0 +1,12 @@
+#![feature(core_intrinsics)]
+static mut A: i32 = 5555;
+
+fn main() {
+    unsafe {
+        std::intrinsics::volatile_store(&mut A as *mut i32, 7777);
+    }
+
+    unsafe {
+        assert!(A == 7777);
+    }
+}
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index 8c59cce9b..c67f6275f 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -65,6 +65,9 @@
     'test_offset_from-fail',
     'ref-ptr-cast-elem-fail',
     'ref-ptr-cast-elem-offset-fail',
+    'volatile_store_static-fail',
+    'volatile_load_static-fail',
+    'box_heap_alloc-fail',
 ]