diff --git a/library/core/src/num/imp/int_log10.rs b/library/core/src/num/imp/int_log10.rs
index 1da029c6a21c4..3df1d89ccdf85 100644
--- a/library/core/src/num/imp/int_log10.rs
+++ b/library/core/src/num/imp/int_log10.rs
@@ -1,10 +1,16 @@
 //! These functions compute the integer logarithm of their type, assuming
 //! that someone has already checked that the value is strictly positive.
 
+use safety::{ensures, requires};
+
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 
 // 0 < val <= u8::MAX
 #[inline]
+#[requires(val > 0)]
+#[ensures(|result: &u32| log10_correct(old(val) as u128, *result))]
 const fn u8_impl(val: u8) -> u32 {
     let val = val as u32;
 
@@ -26,6 +32,8 @@ const fn u8_impl(val: u8) -> u32 {
 
 // 0 < val < 100_000
 #[inline]
+#[requires(val > 0 && val < 100_000)]
+#[ensures(|result: &u32| log10_correct(old(val) as u128, *result))]
 const fn less_than_5(val: u32) -> u32 {
     // Similar to u8, when adding one of these constants to val,
     // we get two possible bit patterns above the low 17 bits,
@@ -47,12 +55,16 @@ const fn less_than_5(val: u32) -> u32 {
 
 // 0 < val <= u16::MAX
 #[inline]
+#[requires(val > 0)]
+#[ensures(|result: &u32| log10_correct(old(val) as u128, *result))]
 const fn u16_impl(val: u16) -> u32 {
     less_than_5(val as u32)
 }
 
 // 0 < val <= u32::MAX
 #[inline]
+#[requires(val > 0)]
+#[ensures(|result: &u32| log10_correct(old(val) as u128, *result))]
 const fn u32_impl(mut val: u32) -> u32 {
     let mut log = 0;
     if val >= 100_000 {
@@ -64,6 +76,8 @@ const fn u32_impl(mut val: u32) -> u32 {
 
 // 0 < val <= u64::MAX
 #[inline]
+#[requires(val > 0)]
+#[ensures(|result: &u32| log10_correct(old(val) as u128, *result))]
 const fn u64_impl(mut val: u64) -> u32 {
     let mut log = 0;
     if val >= 10_000_000_000 {
@@ -79,6 +93,8 @@ const fn u64_impl(mut val: u64) -> u32 {
 
 // 0 < val <= u128::MAX
 #[inline]
+#[requires(val > 0)]
+#[ensures(|result: &u32| log10_correct(old(val) as u128, *result))]
 const fn u128_impl(mut val: u128) -> u32 {
     let mut log = 0;
     if val >= 100_000_000_000_000_000_000_000_000_000_000 {
@@ -96,6 +112,7 @@ const fn u128_impl(mut val: u128) -> u32 {
 macro_rules! define_unsigned_ilog10 {
     ($($ty:ident => $impl_fn:ident,)*) => {$(
         #[inline]
+        #[ensures(|result: &u32| log10_correct(val.get() as u128, *result))]
         pub(in crate::num) const fn $ty(val: NonZero<$ty>) -> u32 {
             let result = $impl_fn(val.get());
 
@@ -117,6 +134,7 @@ define_unsigned_ilog10! {
 }
 
 #[inline]
+#[ensures(|result: &u32| log10_correct(val.get() as u128, *result))]
 pub(in crate::num) const fn usize(val: NonZero<usize>) -> u32 {
     #[cfg(target_pointer_width = "16")]
     let impl_fn = u16;
@@ -136,6 +154,10 @@ macro_rules! define_signed_ilog10 {
     ($($ty:ident => $impl_fn:ident,)*) => {$(
         // 0 < val <= $ty::MAX
         #[inline]
+        #[ensures(|result: &Option<u32>| match result {
+            Some(log) => val > 0 && log10_correct(val as u128, *log),
+            None => val <= 0,
+        })]
         pub(in crate::num) const fn $ty(val: $ty) -> Option<u32> {
             if val > 0 {
                 let result = $impl_fn(val.cast_unsigned());
@@ -169,3 +191,90 @@ define_signed_ilog10! {
 pub(in crate::num) const fn panic_for_nonpositive_argument() -> ! {
     panic!("argument of integer logarithm must be positive")
 }
+
+// For r < 128, this is exactly 2^r <= n < 2^(r+1), including r = 127.
+#[cfg(kani)]
+pub(in crate::num) const fn log2_correct(n: u128, r: u32) -> bool {
+    r < 128 && n >> r == 1
+}
+
+// Generate the powers at compile time. 10^39 exceeds every representable input.
+#[cfg(kani)]
+pub(in crate::num) const fn log10_correct(n: u128, r: u32) -> bool {
+    const POWERS: [u128; 39] = {
+        let mut powers = [1; 39];
+        let mut i = 1;
+        while i < 39 {
+            powers[i] = powers[i - 1] * 10;
+            i += 1;
+        }
+        powers
+    };
+    r < 39 && POWERS[r as usize] <= n && (r == 38 || n < POWERS[(r + 1) as usize])
+}
+
+#[cfg(kani)]
+macro_rules! check_logarithms {
+    ($($name:ident: $target:path => $arg:ty $(, $domain:expr)?;)+) => {$(
+        #[kani::proof_for_contract($target)]
+        fn $name() {
+            let n: $arg = kani::any();
+            $(kani::assume(($domain)(n));
+            kani::cover(true, "logarithm input is reachable");)?
+            let _ = $target(n);
+            kani::cover(true, "logarithm contract returns");
+        }
+    )+};
+}
+
+#[cfg(kani)]
+macro_rules! check_integer_logarithms {
+    ($($int:ident),+) => {$(
+        check_integer_logarithms!(@checked $int, checked_ilog2, checked_ilog10);
+        check_integer_logarithms!(@positive $int, ilog2, ilog10);
+    )+};
+    (@checked $int:ident, $($method:ident),+) => {
+        check_logarithms! { $(${concat($method, _, $int)}: $int::$method => $int;)+ }
+    };
+    (@positive $int:ident, $($method:ident),+) => {$(
+        check_logarithms! { ${concat($method, _, $int)}: $int::$method => $int, |n| n > 0; }
+        #[kani::proof]
+        #[kani::should_panic]
+        fn ${concat($method, _, $int, _nonpositive)}() {
+            let n: $int = kani::any();
+            kani::assume(n <= 0);
+            kani::cover(true, "nonpositive input is reachable");
+            let _ = n.$method();
+            // A safety-check failure cannot satisfy should_panic: every input must panic.
+            kani::safety_check(false, "a nonpositive logarithm must not return");
+        }
+    )+};
+}
+#[cfg(kani)]
+pub(in crate::num) use {check_integer_logarithms, check_logarithms};
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    check_logarithms! {
+        u8_impl: super::u8_impl => u8;
+        u16_impl: super::u16_impl => u16;
+        u32_impl: super::u32_impl => u32;
+        u64_impl: super::u64_impl => u64;
+        u128_impl: super::u128_impl => u128;
+        less_than_5: super::less_than_5 => u32;
+        u8: super::u8 => NonZero<u8>;
+        u16: super::u16 => NonZero<u16>;
+        u32: super::u32 => NonZero<u32>;
+        u64: super::u64 => NonZero<u64>;
+        u128: super::u128 => NonZero<u128>;
+        usize: super::usize => NonZero<usize>;
+        i8: super::i8 => i8;
+        i16: super::i16 => i16;
+        i32: super::i32 => i32;
+        i64: super::i64 => i64;
+        i128: super::i128 => i128;
+    }
+}
diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index 5ded53fbce0fd..82ddcec8ce4f8 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -3514,6 +3514,9 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline]
         #[track_caller]
+        #[ensures(|result: &u32| {
+            self > 0 && imp::int_log10::log2_correct(self as u128, *result)
+        })]
         pub const fn ilog2(self) -> u32 {
             if let Some(log) = self.checked_ilog2() {
                 log
@@ -3539,6 +3542,9 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline]
         #[track_caller]
+        #[ensures(|result: &u32| {
+            self > 0 && imp::int_log10::log10_correct(self as u128, *result)
+        })]
         pub const fn ilog10(self) -> u32 {
             if let Some(log) = self.checked_ilog10() {
                 log
@@ -3593,6 +3599,10 @@ macro_rules! int_impl {
         #[must_use = "this returns the result of the operation, \
                       without modifying the original"]
         #[inline]
+        #[ensures(|result: &Option<u32>| match result {
+            Some(log) => self > 0 && imp::int_log10::log2_correct(self as u128, *log),
+            None => self <= 0,
+        })]
         pub const fn checked_ilog2(self) -> Option<u32> {
             if self <= 0 {
                 None
@@ -3617,6 +3627,10 @@ macro_rules! int_impl {
         #[must_use = "this returns the result of the operation, \
                       without modifying the original"]
         #[inline]
+        #[ensures(|result: &Option<u32>| match result {
+            Some(log) => self > 0 && imp::int_log10::log10_correct(self as u128, *log),
+            None => self <= 0,
+        })]
         pub const fn checked_ilog10(self) -> Option<u32> {
             imp::int_log10::$ActualT(self as $ActualT)
         }
@@ -4196,3 +4210,12 @@ macro_rules! int_impl {
         }
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use crate::kani;
+    use crate::num::imp::int_log10::{check_integer_logarithms, check_logarithms};
+
+    check_integer_logarithms!(i8, i16, i32, i64, i128, isize);
+}
diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs
index d63805e401973..7f499a0f800ad 100644
--- a/library/core/src/num/nonzero.rs
+++ b/library/core/src/num/nonzero.rs
@@ -2120,6 +2120,7 @@ macro_rules! nonzero_integer_signedness_dependent_methods {
         #[must_use = "this returns the result of the operation, \
                       without modifying the original"]
         #[inline]
+        #[ensures(|result: &u32| imp::int_log10::log2_correct(self.get() as u128, *result))]
         pub const fn ilog2(self) -> u32 {
             Self::BITS - 1 - self.leading_zeros()
         }
@@ -2149,6 +2150,7 @@ macro_rules! nonzero_integer_signedness_dependent_methods {
         #[must_use = "this returns the result of the operation, \
                       without modifying the original"]
         #[inline]
+        #[ensures(|result: &u32| imp::int_log10::log10_correct(self.get() as u128, *result))]
         pub const fn ilog10(self) -> u32 {
             imp::int_log10::$Int(self)
         }
@@ -3049,6 +3051,7 @@ nonzero_integer! {
 #[cfg(kani)]
 mod verify {
     use super::*;
+    use crate::num::imp::int_log10::check_logarithms;
 
     macro_rules! nonzero_check {
         ($t:ty, $nonzero_type:ty, $nonzero_check_new_unchecked_for:ident) => {
@@ -5231,4 +5234,14 @@ mod verify {
         u128::MAX - 0xFFFFu128,
         u128::MAX
     );
+
+    macro_rules! nonzero_check_logarithms {
+        ($($int:ident),+) => {
+            check_logarithms! { $(
+                ${concat(nonzero_check_ilog2_, $int)}: NonZero::<$int>::ilog2 => NonZero<$int>;
+                ${concat(nonzero_check_ilog10_, $int)}: NonZero::<$int>::ilog10 => NonZero<$int>;
+            )+ }
+        };
+    }
+    nonzero_check_logarithms!(u8, u16, u32, u64, u128, usize);
 }
diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs
index ac72f1142c3d5..52319921bc5db 100644
--- a/library/core/src/num/uint_macros.rs
+++ b/library/core/src/num/uint_macros.rs
@@ -1834,6 +1834,9 @@ macro_rules! uint_impl {
                       without modifying the original"]
         #[inline]
         #[track_caller]
+        #[ensures(|result: &u32| {
+            self > 0 && imp::int_log10::log2_correct(self as u128, *result)
+        })]
         pub const fn ilog2(self) -> u32 {
             if let Some(log) = self.checked_ilog2() {
                 log
@@ -1859,6 +1862,9 @@ macro_rules! uint_impl {
                       without modifying the original"]
         #[inline]
         #[track_caller]
+        #[ensures(|result: &u32| {
+            self > 0 && imp::int_log10::log10_correct(self as u128, *result)
+        })]
         pub const fn ilog10(self) -> u32 {
             if let Some(log) = self.checked_ilog10() {
                 log
@@ -1957,6 +1963,10 @@ macro_rules! uint_impl {
         #[must_use = "this returns the result of the operation, \
                       without modifying the original"]
         #[inline]
+        #[ensures(|result: &Option<u32>| match result {
+            Some(log) => self > 0 && imp::int_log10::log2_correct(self as u128, *log),
+            None => self == 0,
+        })]
         pub const fn checked_ilog2(self) -> Option<u32> {
             match NonZero::new(self) {
                 Some(x) => Some(x.ilog2()),
@@ -1978,6 +1988,10 @@ macro_rules! uint_impl {
         #[must_use = "this returns the result of the operation, \
                       without modifying the original"]
         #[inline]
+        #[ensures(|result: &Option<u32>| match result {
+            Some(log) => self > 0 && imp::int_log10::log10_correct(self as u128, *log),
+            None => self == 0,
+        })]
         pub const fn checked_ilog10(self) -> Option<u32> {
             match NonZero::new(self) {
                 Some(x) => Some(x.ilog10()),
@@ -4412,3 +4426,12 @@ macro_rules! uint_impl {
         }
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use crate::kani;
+    use crate::num::imp::int_log10::{check_integer_logarithms, check_logarithms};
+
+    check_integer_logarithms!(u8, u16, u32, u64, u128, usize);
+}