diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs
index 34a05ac38884d..14ac03f4bd535 100644
--- a/library/core/src/ascii/ascii_char.rs
+++ b/library/core/src/ascii/ascii_char.rs
@@ -3,9 +3,13 @@
 //! suggestions from rustc if you get anything slightly wrong in here, and overall
 //! helps with clarity as we're also referring to `char` intentionally in here.
 
+use safety::{ensures, requires};
 use crate::fmt::{self, Write};
 use crate::mem::transmute;
 
+#[cfg(kani)]
+use crate::kani;
+
 /// One of the 128 Unicode characters from U+0000 through U+007F,
 /// often known as the [ASCII] subset.
 ///
@@ -449,6 +453,7 @@ impl AsciiChar {
     /// or returns `None` if it's too large.
     #[unstable(feature = "ascii_char", issue = "110998")]
     #[inline]
+    #[ensures(|result| (b <= 127) == result.is_some())]
     pub const fn from_u8(b: u8) -> Option<Self> {
         if b <= 127 {
             // SAFETY: Just checked that `b` is in-range
@@ -466,6 +471,7 @@ impl AsciiChar {
     /// `b` must be in `0..=127`, or else this is UB.
     #[unstable(feature = "ascii_char", issue = "110998")]
     #[inline]
+    #[requires(b <= 127)]
     pub const unsafe fn from_u8_unchecked(b: u8) -> Self {
         // SAFETY: Our safety precondition is that `b` is in-range.
         unsafe { transmute(b) }
@@ -616,3 +622,22 @@ impl fmt::Debug for AsciiChar {
         f.write_char('\'')
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+    use AsciiChar;
+
+    #[kani::proof_for_contract(AsciiChar::from_u8)]
+    fn check_from_u8() {
+        let b: u8 = kani::any();
+        unsafe { AsciiChar::from_u8(b) };
+    }
+
+    #[kani::proof_for_contract(AsciiChar::from_u8_unchecked)]
+    fn check_from_u8_unchecked() {
+        let b: u8 = kani::any();
+        unsafe { AsciiChar::from_u8_unchecked(b) };
+    }
+}
diff --git a/library/core/src/char/convert.rs b/library/core/src/char/convert.rs
index f0c2636307fcf..573fbc40c8fc7 100644
--- a/library/core/src/char/convert.rs
+++ b/library/core/src/char/convert.rs
@@ -1,5 +1,6 @@
 //! Character conversions.
 
+use safety::requires;
 use crate::char::TryFromCharError;
 use crate::error::Error;
 use crate::fmt;
@@ -7,6 +8,9 @@ use crate::mem::transmute;
 use crate::str::FromStr;
 use crate::ub_checks::assert_unsafe_precondition;
 
+#[cfg(kani)]
+use crate::kani;
+
 /// Converts a `u32` to a `char`. See [`char::from_u32`].
 #[must_use]
 #[inline]
@@ -21,6 +25,7 @@ pub(super) const fn from_u32(i: u32) -> Option<char> {
 /// Converts a `u32` to a `char`, ignoring validity. See [`char::from_u32_unchecked`].
 #[inline]
 #[must_use]
+#[requires(char_try_from_u32(i).is_ok())]
 pub(super) const unsafe fn from_u32_unchecked(i: u32) -> char {
     // SAFETY: the caller must guarantee that `i` is a valid char value.
     unsafe {
@@ -290,3 +295,15 @@ pub(super) const fn from_digit(num: u32, radix: u32) -> Option<char> {
         None
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    #[kani::proof_for_contract(from_u32_unchecked)]
+    fn check_from_u32_unchecked() {
+        let i: u32 = kani::any();
+        unsafe { from_u32_unchecked(i) };
+    }
+}
diff --git a/library/core/src/char/methods.rs b/library/core/src/char/methods.rs
index 4186565c131ed..4df90d462b5d0 100644
--- a/library/core/src/char/methods.rs
+++ b/library/core/src/char/methods.rs
@@ -1,10 +1,14 @@
 //! impl char {}
 
+use safety::ensures;
 use crate::slice;
 use crate::str::from_utf8_unchecked_mut;
 use crate::unicode::printable::is_printable;
 use crate::unicode::{self, conversions};
 
+#[cfg(kani)]
+use crate::kani;
+
 use super::*;
 
 impl char {
@@ -1836,3 +1840,30 @@ pub fn encode_utf16_raw(mut code: u32, dst: &mut [u16]) -> &mut [u16] {
         }
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    #[ensures(|result| c.is_ascii() == result.is_some())]
+    fn as_ascii_clone(c: &char) -> Option<ascii::Char> {
+        c.as_ascii()
+    }
+
+    #[kani::proof_for_contract(as_ascii_clone)]
+    fn check_as_ascii_ascii_char() {
+        let ascii: char = kani::any_where(|c : &char| c.is_ascii());
+        unsafe { 
+            as_ascii_clone(&ascii);
+        };
+    }
+
+    #[kani::proof_for_contract(as_ascii_clone)]
+    fn check_as_ascii_non_ascii_char() {
+        let non_ascii: char = kani::any_where(|c: &char| !c.is_ascii());
+        unsafe {
+            as_ascii_clone(&non_ascii);
+        }
+    }
+}