diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs
index 93dd351b02958..2a65b2415f7d3 100644
--- a/library/core/src/ffi/c_str.rs
+++ b/library/core/src/ffi/c_str.rs
@@ -9,6 +9,11 @@ use crate::ptr::NonNull;
 use crate::slice::memchr;
 use crate::{fmt, intrinsics, ops, slice, str};
 
+use crate::ub_checks::Invariant;
+
+#[cfg(kani)]
+use crate::kani;
+
 // FIXME: because this is doc(inline)d, we *have* to use intra-doc links because the actual link
 //   depends on where the item is being documented. however, since this is libcore, we can't
 //   actually reference libstd or liballoc in intra-doc links. so, the best we can do is remove the
@@ -207,6 +212,22 @@ impl fmt::Display for FromBytesWithNulError {
     }
 }
 
+#[unstable(feature = "ub_checks", issue = "none")]
+impl Invariant for &CStr {
+    /**
+     * Safety invariant of a valid CStr:
+     * 1. An empty CStr should have a null byte.
+     * 2. A valid CStr should end with a null-terminator and contains
+     *    no intermediate null bytes.
+     */
+    fn is_safe(&self) -> bool {
+        let bytes: &[c_char] = &self.inner;
+        let len = bytes.len();
+
+        !bytes.is_empty() && bytes[len - 1] == 0 && !bytes[..len-1].contains(&0)
+    }
+}
+
 impl CStr {
     /// Wraps a raw C string with a safe C string wrapper.
     ///
@@ -833,3 +854,25 @@ impl Iterator for Bytes<'_> {
 
 #[unstable(feature = "cstr_bytes", issue = "112115")]
 impl FusedIterator for Bytes<'_> {}
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError>
+    #[kani::proof]
+    #[kani::unwind(32)] // 7.3 seconds when 16; 33.1 seconds when 32
+    fn check_from_bytes_until_nul() {
+        const MAX_SIZE: usize = 32;
+        let string: [u8; MAX_SIZE] = kani::any();
+        // Covers the case of a single null byte at the end, no null bytes, as
+        // well as intermediate null bytes
+        let slice = kani::slice::any_slice_of_array(&string);
+
+        let result = CStr::from_bytes_until_nul(slice);
+        if let Ok(c_str) = result {
+            assert!(c_str.is_safe());
+        }
+    }
+}
\ No newline at end of file