diff --git a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md
index 7b3d37533..c8294c694 100644
--- a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md
+++ b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md
@@ -125,6 +125,24 @@ Execution gets stuck (no matching rule) when operands have different types or un
   rule #extractOperandType(_, _) => TyUnknown [owise]
 ```
 
+#### Volatile Store (`std::intrinsics::volatile_store`, `std::ptr::write_volatile`)
+
+The `volatile_store` intrinsic writes a value to a memory location through a pointer, ensuring the write is not
+optimized away by the compiler. Unlike normal stores, volatile stores are guaranteed to occur exactly once and
+in order with respect to other volatile operations. In the semantics, this is equivalent to a regular store
+through a dereferenced pointer. We extract the place from the pointer operand, add a deref projection, and
+write the value to that location.
+
+```k
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("volatile_store")), operandCopy(place(LOCAL, PROJ)) ARG2:Operand .Operands, _DEST)
+        => #setLocalValue(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems)), ARG2)
+       ... </k>
+
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("volatile_store")), operandMove(place(LOCAL, PROJ)) ARG2:Operand .Operands, _DEST)
+        => #setLocalValue(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems)), ARG2)
+       ... </k>
+```
+
 #### Ptr Offset Computations (`std::intrinsics::ptr_offset_from`, `std::intrinsics::ptr_offset_from_unsigned`)
 
 The `ptr_offset_from[_unsigned]` calculates the distance between two pointers within the same allocation,
diff --git a/kmir/src/tests/integration/data/prove-rs/volatile_store.rs b/kmir/src/tests/integration/data/prove-rs/volatile_store.rs
new file mode 100644
index 000000000..cc187e418
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/volatile_store.rs
@@ -0,0 +1,11 @@
+#![feature(core_intrinsics)]
+fn main() {
+    let mut a: i32 = 5555;
+    let a_ptr = &mut a as *mut _;
+
+    unsafe {
+        std::intrinsics::volatile_store(a_ptr, 7777);
+    }
+
+    assert!(a == 7777);
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/write_volatile.rs b/kmir/src/tests/integration/data/prove-rs/write_volatile.rs
new file mode 100644
index 000000000..d708d8823
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/write_volatile.rs
@@ -0,0 +1,10 @@
+fn main() {
+    let mut a: i32 = 5555;
+    let a_ptr = &mut a as *mut _;
+
+    unsafe {
+        std::ptr::write_volatile(a_ptr, 7777);
+    }
+
+    assert!(a == 7777);
+}