diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index f4ca557afbdb..7f5568ccf152 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -801,8 +801,30 @@ impl GotocCtx<'_> {
                 self.codegen_pointer_cast(k, e, *t, loc)
             }
             Rvalue::Cast(CastKind::Transmute, operand, ty) => {
-                let goto_typ = self.codegen_ty_stable(*ty);
-                self.codegen_operand_stable(operand).transmute_to(goto_typ, &self.symbol_table)
+                let src_ty = operand.ty(self.current_fn().locals()).unwrap();
+                // Transmute requires sized types.
+                let src_sz = LayoutOf::new(src_ty).size_of().unwrap();
+                let dst_sz = LayoutOf::new(*ty).size_of().unwrap();
+                let dst_type = self.codegen_ty_stable(*ty);
+                if src_sz != dst_sz {
+                    Expr::statement_expression(
+                        vec![
+                            self.codegen_assert_assume_false(
+                                PropertyClass::SafetyCheck,
+                                &format!(
+                                    "Cannot transmute between types of different sizes. \
+                                Transmuting from `{src_sz}` to `{dst_sz}` bytes"
+                                ),
+                                loc,
+                            ),
+                            dst_type.nondet().as_stmt(loc),
+                        ],
+                        dst_type,
+                        loc,
+                    )
+                } else {
+                    self.codegen_operand_stable(operand).transmute_to(dst_type, &self.symbol_table)
+                }
             }
             Rvalue::BinaryOp(op, e1, e2) => self.codegen_rvalue_binary_op(res_ty, op, e1, e2, loc),
             Rvalue::CheckedBinaryOp(op, e1, e2) => {
diff --git a/tests/expected/intrinsics/transmute_diff_size.expected b/tests/expected/intrinsics/transmute_diff_size.expected
new file mode 100644
index 000000000000..efc770882422
--- /dev/null
+++ b/tests/expected/intrinsics/transmute_diff_size.expected
@@ -0,0 +1,2 @@
+error[E0512]: cannot transmute between types of different sizes, or dependently-sized types
+error: aborting due to 3 previous errors
diff --git a/tests/expected/intrinsics/transmute_diff_size.rs b/tests/expected/intrinsics/transmute_diff_size.rs
new file mode 100644
index 000000000000..a38c37a379d9
--- /dev/null
+++ b/tests/expected/intrinsics/transmute_diff_size.rs
@@ -0,0 +1,33 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that compilation fails when trying to transmute with different src and target sizes.
+
+#![feature(core_intrinsics)]
+use std::intrinsics::transmute;
+
+/// This should fail due to UB detection.
+#[kani::proof]
+pub fn transmute_diff_size() {
+    let a: u32 = kani::any();
+    if kani::any() {
+        let smaller: u16 = unsafe { transmute(a) };
+        std::hint::black_box(smaller);
+    } else {
+        let bigger: (u64, isize) = unsafe { transmute(a) };
+        std::hint::black_box(bigger);
+    }
+}
+
+/// Generic transmute wrapper.
+pub unsafe fn generic_transmute<S, D>(src: S) -> D {
+    transmute(src)
+}
+
+/// This should also fail due to UB detection.
+#[kani::proof]
+pub fn transmute_wrapper_diff_size() {
+    let a: (u32, char) = kani::any();
+    let b: u128 = unsafe { generic_transmute(a) };
+    std::hint::black_box(b);
+}
diff --git a/tests/expected/intrinsics/transmute_unchecked_size.expected b/tests/expected/intrinsics/transmute_unchecked_size.expected
new file mode 100644
index 000000000000..6ff9a1f67366
--- /dev/null
+++ b/tests/expected/intrinsics/transmute_unchecked_size.expected
@@ -0,0 +1,24 @@
+Checking harness transmute_wrapper_diff_size...
+Status: UNREACHABLE\
+Description: ""Unreachable expected""
+
+Failed Checks: Cannot transmute between types of different sizes. Transmuting from `8` to `16` bytes
+
+VERIFICATION:- FAILED
+
+Checking harness transmute_diff_size...
+
+Status: UNREACHABLE\
+Description: ""This should never be reached""
+
+Status: UNREACHABLE\
+Description: ""Neither this one""
+
+Failed Checks: Cannot transmute between types of different sizes. Transmuting from `4` to `2` bytes
+Failed Checks: Cannot transmute between types of different sizes. Transmuting from `4` to `16` bytes
+
+VERIFICATION:- FAILED
+
+Verification failed for - transmute_wrapper_diff_size
+Verification failed for - transmute_diff_size
+0 successfully verified harnesses, 2 failures, 2 total
diff --git a/tests/expected/intrinsics/transmute_unchecked_size.rs b/tests/expected/intrinsics/transmute_unchecked_size.rs
new file mode 100644
index 000000000000..704448dcc6c6
--- /dev/null
+++ b/tests/expected/intrinsics/transmute_unchecked_size.rs
@@ -0,0 +1,44 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that Kani correctly identify UB when invoking `transmute_unchecked` with different sizes.
+//! See <https://github.com/model-checking/kani/issues/3839> for more details.
+
+#![feature(core_intrinsics)]
+use std::intrinsics::transmute_unchecked;
+
+/// Kani reachability checks are not currently applied to `unreachable` statements.
+macro_rules! unreachable {
+    ($msg:literal) => {
+        assert!(false, $msg)
+    };
+}
+
+/// This should fail due to UB detection.
+#[kani::proof]
+pub fn transmute_diff_size() {
+    let a: u32 = kani::any();
+    if kani::any() {
+        let smaller: u16 = unsafe { transmute_unchecked(a) };
+        std::hint::black_box(smaller);
+        unreachable!("This should never be reached");
+    } else {
+        let bigger: (u64, isize) = unsafe { transmute_unchecked(a) };
+        std::hint::black_box(bigger);
+        unreachable!("Neither this one");
+    }
+}
+
+/// Generic transmute wrapper.
+pub unsafe fn generic_transmute<S, D>(src: S) -> D {
+    transmute_unchecked(src)
+}
+
+/// This should also fail due to UB detection.
+#[kani::proof]
+pub fn transmute_wrapper_diff_size() {
+    let a: (u32, char) = kani::any();
+    let b: u128 = unsafe { generic_transmute(a) };
+    std::hint::black_box(b);
+    unreachable!("Unreachable expected");
+}