diff --git a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md
index 5da5a85f2..8788d9861 100644
--- a/kmir/src/kmir/kdist/mir-semantics/intrinsics.md
+++ b/kmir/src/kmir/kdist/mir-semantics/intrinsics.md
@@ -143,6 +143,26 @@ write the value to that location.
        ... </k>
 ```
 
+#### Volatile Load (`std::intrinsics::volatile_load`, `std::ptr::read_volatile`)
+
+The `volatile_load` intrinsic reads a value from a memory location through a pointer, ensuring the read is not
+optimised away by the compiler. Unlike normal loads, volatile loads are guaranteed to occur exactly once and
+in order with respect to other volatile operations. In the semantics, this is equivalent to a regular load
+through a dereferenced pointer. We extract the place from the pointer operand, add a deref projection, and
+read the value from that location into the destination. Since `#setLocalValue` is strict in its second argument,
+the dereferenced operand is evaluated (i.e., the value is read from memory) before being written to `DEST`.
+
+```k
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("volatile_load")), operandCopy(place(LOCAL, PROJ)) .Operands, DEST, _SPAN)
+        => #setLocalValue(DEST, operandCopy(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems))))
+       ... </k>
+
+  // for `operandMove` the pointer is moved, but the pointed-to value is copied (read, not consumed)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("volatile_load")), operandMove(place(LOCAL, PROJ)) .Operands, DEST, _SPAN)
+        => #setLocalValue(DEST, operandCopy(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems))))
+       ... </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/read_volatile.rs b/kmir/src/tests/integration/data/prove-rs/read_volatile.rs
new file mode 100644
index 000000000..1d8f96587
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/read_volatile.rs
@@ -0,0 +1,11 @@
+fn main() {
+    let a: i32 = 5555;
+    let a_ptr = &a as *const _;
+
+    let b: i32;
+    unsafe {
+        b = std::ptr::read_volatile(a_ptr);
+    }
+
+    assert!(b == 5555);
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/volatile_load.rs b/kmir/src/tests/integration/data/prove-rs/volatile_load.rs
new file mode 100644
index 000000000..313adec3f
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/volatile_load.rs
@@ -0,0 +1,12 @@
+#![feature(core_intrinsics)]
+fn main() {
+    let a: i32 = 5555;
+    let a_ptr = &a as *const _;
+
+    let b: i32;
+    unsafe {
+        b = std::intrinsics::volatile_load(a_ptr);
+    }
+
+    assert!(b == 5555);
+}