diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md
index 3b117a94c..8948c0da9 100644
--- a/kmir/src/kmir/kdist/mir-semantics/kmir.md
+++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md
@@ -89,6 +89,106 @@ blocks, or call another function).
        </k>
 ```
 
+#### Special-Purpose Rule for alignment check sequence
+
+A characteristic sequence of statements and assert terminator is generated by the compiler
+when performing an alignment check before a pointer is dereferenced.
+We optionally skip the entire block since we do not use `Int`-sorted memory addresses anyway.
+
+```k
+  rule [skip-alignment-check-block]:
+    <k> #execStmts(
+          statement (... 
+            kind: statementKindAssign (... 
+              place: place (... local: PTR_UNIT , projection: .ProjectionElems ) ,
+              rvalue: rvalueCast (
+                castKindPtrToPtr ,
+                operandCopy ( place (... local: _PTR_ORIG , projection: .ProjectionElems ) ) ,
+                _UNIT_PTR_TY ) ) , // cast original to *()
+            span: SPAN )
+          statement (... 
+            kind: statementKindAssign (... 
+              place: place (... local: ADDR , projection: .ProjectionElems ) ,
+              rvalue: rvalueCast (
+                castKindTransmute ,
+                operandCopy ( place (... local: PTR_UNIT , projection: .ProjectionElems ) ) ,
+                USIZE_TY ) ) ,
+            span: SPAN )
+          statement (...
+            kind: statementKindAssign (...
+              place: place (... local: ALIGNMENT , projection: .ProjectionElems ) ,
+              rvalue: rvalueNullaryOp ( nullOpAlignOf , _ORIG_TY ) ) ,
+            span: SPAN )
+          statement (...
+            kind: statementKindAssign (... 
+              place: place (... local: ALIGN_MASK , projection: .ProjectionElems ) ,
+              rvalue: rvalueBinaryOp (
+                binOpSub ,
+                operandCopy ( place (... local: ALIGNMENT , projection: .ProjectionElems ) ) ,
+                operandConstant ( constOperand (... 
+                  span: SPAN ,
+                  userTy: noUserTypeAnnotationIndex ,
+                  const: mirConst (...
+                    kind: constantKindAllocated ( 
+                      allocation (... 
+                        bytes: b"\x01\x00\x00\x00\x00\x00\x00\x00" ,
+                        provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) ,
+                        align: align ( 8 ) ,
+                        mutability: mutabilityMut ) ) ,
+                    ty: USIZE_TY ,
+                    id: _ ) ) ) ) ) ,
+            span: SPAN )  
+          statement (... 
+            kind: statementKindAssign (...
+              place: place (... local: MASKED , projection: .ProjectionElems ) ,
+              rvalue: rvalueBinaryOp ( 
+                binOpBitAnd ,
+                operandCopy ( place (... local: ADDR , projection: .ProjectionElems ) ) ,
+                operandCopy ( place (... local: ALIGN_MASK , projection: .ProjectionElems ) ) ) ) ,
+            span: SPAN )
+          statement (... 
+            kind: statementKindAssign (... 
+              place: place (...
+                local: RESULT , projection: .ProjectionElems ) ,
+                rvalue: rvalueBinaryOp (
+                  binOpEq ,
+                  operandCopy ( place (... local: MASKED , projection: .ProjectionElems ) ) ,
+                  operandConstant ( constOperand (... 
+                    span: SPAN ,
+                    userTy: noUserTypeAnnotationIndex ,
+                    const: mirConst (...
+                      kind: constantKindAllocated (
+                        allocation (...
+                          bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" ,
+                          provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) ,
+                          align: align ( 8 ) ,
+                          mutability: mutabilityMut ) ) ,
+                      ty: USIZE_TY ,
+                      id: _ ) ) ) ) ) , 
+            span: SPAN )
+          .Statements
+        )
+      ~> #execTerminator(
+            terminator (...
+              kind: assert (... 
+                  cond: operandCopy ( place (... local: RESULT , projection: .ProjectionElems ) ) ,
+                  expected: true ,
+                  msg: assertMessageMisalignedPointerDereference (... 
+                      required: operandCopy ( place (... local: ALIGNMENT , projection: .ProjectionElems ) ) ,
+                      found: operandCopy ( place (... local: ADDR , projection: .ProjectionElems ) ) 
+                    ) ,
+                  target: TARGET,
+                  unwind: unwindActionUnreachable
+              ) ,
+              span: SPAN
+            ) 
+          )
+      ~> .K
+    => #execBlockIdx(TARGET)
+    </k>
+    [priority(40), preserves-definedness]
+```
+
 `Statement` execution handles the different `StatementKind`s. Some of
 these are irrelevant at the MIR level that this semantics is modeling
 (e.g., all statements related to compile-time checks like borrowing
diff --git a/kmir/src/tests/integration/data/prove-rs/ptr_offset.rs b/kmir/src/tests/integration/data/prove-rs/ptr_offset.rs
new file mode 100644
index 000000000..e14cb1ebc
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/ptr_offset.rs
@@ -0,0 +1,11 @@
+struct Thing {payload: i16}
+
+fn main() {
+
+    let a = [Thing{payload: 1}, Thing{payload: 2}, Thing{payload:3}];
+    let p = &a as *const Thing;
+    let p1 = unsafe { p.add(1) };
+
+    let two = unsafe { (*p1).payload };
+    assert!(two == 2);
+}