diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs
index dd4306d2d9b68..df4e071e1d5ab 100644
--- a/library/core/src/slice/iter.rs
+++ b/library/core/src/slice/iter.rs
@@ -8,16 +8,14 @@ use crate::hint::assert_unchecked;
 use crate::iter::{
     FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce, UncheckedIterator,
 };
+#[cfg(kani)]
+use crate::kani;
 use crate::marker::PhantomData;
 use crate::mem::{self, SizedTypeProperties};
 use crate::num::NonZero;
 use crate::ptr::{self, without_provenance, without_provenance_mut, NonNull};
-use crate::{cmp, fmt};
-
-#[cfg(kani)]
-use crate::kani;
-
 use crate::ub_checks::Invariant;
+use crate::{cmp, fmt};
 
 #[stable(feature = "boxed_slice_into_iter", since = "1.80.0")]
 impl<T> !Iterator for [T] {}
@@ -170,7 +168,8 @@ impl<T> crate::ub_checks::Invariant for Iter<'_, T> {
         if ty_size == 0 || distance == 0 {
             self.ptr.is_aligned()
         } else {
-            let slice_ptr: *const [T] = crate::ptr::from_raw_parts(self.ptr.as_ptr(), distance / ty_size);
+            let slice_ptr: *const [T] =
+                crate::ptr::from_raw_parts(self.ptr.as_ptr(), distance / ty_size);
             crate::ub_checks::same_allocation(self.ptr.as_ptr(), self.end_or_len)
                 && self.ptr.addr().get() <= self.end_or_len as usize
                 && distance % ty_size == 0
@@ -226,7 +225,8 @@ impl<T> crate::ub_checks::Invariant for IterMut<'_, T> {
             self.ptr.is_aligned()
         } else {
             let distance = self.ptr.addr().get().abs_diff(self.end_or_len as usize);
-            let slice_ptr: *mut [T] = crate::ptr::from_raw_parts_mut(self.ptr.as_ptr(), distance / size);
+            let slice_ptr: *mut [T] =
+                crate::ptr::from_raw_parts_mut(self.ptr.as_ptr(), distance / size);
             crate::ub_checks::same_allocation(self.ptr.as_ptr(), self.end_or_len)
                 && self.ptr.addr().get() <= self.end_or_len as usize
                 && distance % size == 0
@@ -3506,7 +3506,8 @@ impl<'a, T: 'a + fmt::Debug, P> fmt::Debug for ChunkByMut<'a, T, P> {
 }
 
 /// Verify the safety of the code implemented in this module (including generated code from macros).
-#[unstable(feature = "kani", issue="none")]
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
 mod verify {
     use super::*;
     use crate::kani;
@@ -3604,17 +3605,29 @@ mod verify {
 
                 // check_safe_abstraction!(check_advance_back_by, $ty, advance_back_by, kani::any());
 
-                check_safe_abstraction!(check_is_empty, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.is_empty(); });
-                check_safe_abstraction!(check_len, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.len(); });
-                check_safe_abstraction!(check_size_hint, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.size_hint(); });
+                check_safe_abstraction!(check_is_empty, $ty, |iter: &mut Iter<'_, $ty>| {
+                    let _ = iter.is_empty();
+                });
+                check_safe_abstraction!(check_len, $ty, |iter: &mut Iter<'_, $ty>| {
+                    let _ = iter.len();
+                });
+                check_safe_abstraction!(check_size_hint, $ty, |iter: &mut Iter<'_, $ty>| {
+                    let _ = iter.size_hint();
+                });
                 //check_safe_abstraction!(check_nth, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth(kani::any()); });
                 //check_safe_abstraction!(check_advance_by, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.advance_by(kani::any()); });
-                //check_safe_abstraction!(check_next_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.next_back(); });
+                check_safe_abstraction!(check_next_back, $ty, |iter: &mut Iter<'_, $ty>| {
+                    let _ = iter.next_back();
+                });
                 //check_safe_abstraction!(check_nth_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth_back(kani::any()); });
-                check_safe_abstraction!(check_next, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.next(); });
+                check_safe_abstraction!(check_next, $ty, |iter: &mut Iter<'_, $ty>| {
+                    let _ = iter.next();
+                });
 
                 // Ensure that clone always generates a safe object.
-                check_safe_abstraction!(check_clone, $ty, |iter: &mut Iter<'_, $ty>| { kani::assert(iter.clone().is_safe(), "Clone is safe"); });
+                check_safe_abstraction!(check_clone, $ty, |iter: &mut Iter<'_, $ty>| {
+                    kani::assert(iter.clone().is_safe(), "Clone is safe");
+                });
             }
         };
     }
@@ -3623,4 +3636,4 @@ mod verify {
     check_iter_with_ty!(verify_u8, u8, u32::MAX as usize);
     check_iter_with_ty!(verify_char, char, 50);
     check_iter_with_ty!(verify_tup, (char, u8), 50);
-}
\ No newline at end of file
+}
diff --git a/library/core/src/ub_checks.rs b/library/core/src/ub_checks.rs
index a548dfee81d53..a3f3f6ee80ade 100644
--- a/library/core/src/ub_checks.rs
+++ b/library/core/src/ub_checks.rs
@@ -176,7 +176,7 @@ mod predicates {
     ///   * `src` points to a properly initialized value of type `T`.
     ///
     /// [`crate::ptr`]: https://doc.rust-lang.org/std/ptr/index.html
-    pub fn can_dereference<T>(src: *const T) -> bool {
+    pub fn can_dereference<T: ?Sized>(src: *const T) -> bool {
         let _ = src;
         true
     }
@@ -185,7 +185,7 @@ mod predicates {
     /// * `dst` must be valid for writes.
     /// * `dst` must be properly aligned. Use `write_unaligned` if this is not the
     ///    case.
-    pub fn can_write<T>(dst: *mut T) -> bool {
+    pub fn can_write<T: ?Sized>(dst: *mut T) -> bool {
         let _ = dst;
         true
     }
@@ -193,20 +193,20 @@ mod predicates {
     /// Check if a pointer can be the target of unaligned reads.
     /// * `src` must be valid for reads.
     /// * `src` must point to a properly initialized value of type `T`.
-    pub fn can_read_unaligned<T>(src: *const T) -> bool {
+    pub fn can_read_unaligned<T: ?Sized>(src: *const T) -> bool {
         let _ = src;
         true
     }
 
     /// Check if a pointer can be the target of unaligned writes.
     /// * `dst` must be valid for writes.
-    pub fn can_write_unaligned<T>(dst: *mut T) -> bool {
+    pub fn can_write_unaligned<T: ?Sized>(dst: *mut T) -> bool {
         let _ = dst;
         true
     }
 
     /// Checks if two pointers point to the same allocation.
-    pub fn same_allocation<T>(src: *const T, dst: *const T) -> bool {
+    pub fn same_allocation<T: ?Sized>(src: *const T, dst: *const T) -> bool {
         let _ = (src, dst);
         true
     }