diff --git a/library/core/src/num/imp/int_log10.rs b/library/core/src/num/imp/int_log10.rs
index 1da029c6a21c4..da87a9597b36b 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| is_ilog(val as u128, 10, *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(0 < val && val < 100_000)]
+#[ensures(|result: &u32| is_ilog(val as u128, 10, *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| is_ilog(val as u128, 10, *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| is_ilog(old(val) as u128, 10, *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| is_ilog(old(val) as u128, 10, *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| is_ilog(old(val) as u128, 10, *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| is_ilog(val.get() as u128, 10, *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| is_ilog(val.get() as u128, 10, *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 && is_ilog(val as u128, 10, 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,63 @@ define_signed_ilog10! {
 pub(in crate::num) const fn panic_for_nonpositive_argument() -> ! {
     panic!("argument of integer logarithm must be positive")
 }
+
+/// Returns whether `log` is the largest `r` with `base^r <= value`.
+///
+/// `value / base < base^log` means `value < base^(log + 1)`, but can't overflow. This doesn't use
+/// `checked_pow` because its loop contract makes Kani lose track of the result.
+#[cfg(kani)]
+pub(in crate::num) const fn is_ilog(value: u128, base: u128, log: u32) -> bool {
+    let mut power: u128 = 1;
+    let mut i = 0;
+    while i < log {
+        power = match power.checked_mul(base) {
+            Some(power) => power,
+            None => return false,
+        };
+        i += 1;
+    }
+    power <= value && value / base < power
+}
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    macro_rules! check_contract {
+        ($($function:path => $harness:ident;)*) => {$(
+            #[kani::proof_for_contract($function)]
+            fn $harness() {
+                let _ = $function(kani::any());
+            }
+        )*};
+    }
+
+    check_contract! {
+        less_than_5 => check_less_than_5;
+
+        u8_impl => check_u8_impl;
+        u16_impl => check_u16_impl;
+        u32_impl => check_u32_impl;
+        u64_impl => check_u64_impl;
+        u128_impl => check_u128_impl;
+
+        super::u8 => check_u8;
+        super::u16 => check_u16;
+        super::u32 => check_u32;
+        super::u64 => check_u64;
+        super::u128 => check_u128;
+
+        super::i8 => check_i8;
+        super::i16 => check_i16;
+        super::i32 => check_i32;
+        super::i64 => check_i64;
+        super::i128 => check_i128;
+
+        // `usize` is 64-bit on CI; on 16- and 32-bit targets it calls `u16` or `u32`, proved above.
+        super::usize => check_usize;
+
+        // No `isize`: it calls whichever of `i16`, `i32` or `i64` matches its width.
+    }
+}
diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs
index 5ded53fbce0fd..73cb0bf4e4d82 100644
--- a/library/core/src/num/int_macros.rs
+++ b/library/core/src/num/int_macros.rs
@@ -3514,6 +3514,7 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline]
         #[track_caller]
+        #[ensures(|result: &u32| self > 0 && imp::int_log10::is_ilog(self as u128, 2, *result))]
         pub const fn ilog2(self) -> u32 {
             if let Some(log) = self.checked_ilog2() {
                 log
@@ -3539,6 +3540,7 @@ macro_rules! int_impl {
                       without modifying the original"]
         #[inline]
         #[track_caller]
+        #[ensures(|result: &u32| self > 0 && imp::int_log10::is_ilog(self as u128, 10, *result))]
         pub const fn ilog10(self) -> u32 {
             if let Some(log) = self.checked_ilog10() {
                 log
@@ -3593,6 +3595,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::is_ilog(self as u128, 2, log),
+            None => self <= 0,
+        })]
         pub const fn checked_ilog2(self) -> Option<u32> {
             if self <= 0 {
                 None
@@ -3617,6 +3623,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::is_ilog(self as u128, 10, log),
+            None => self <= 0,
+        })]
         pub const fn checked_ilog10(self) -> Option<u32> {
             imp::int_log10::$ActualT(self as $ActualT)
         }
diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs
index 852765d293731..9b2661410536b 100644
--- a/library/core/src/num/mod.rs
+++ b/library/core/src/num/mod.rs
@@ -2432,4 +2432,55 @@ mod verify {
 
         assert_eq!(result, num1 as i128);
     }
+
+    mod logarithms {
+        macro_rules! check_logarithm {
+            ($method:ident, $checked_method:ident; $($ty:ident),+) => {
+                mod $method {$(
+                    mod $ty {
+                        use crate::kani;
+
+                        #[kani::proof_for_contract($ty::$checked_method)]
+                        fn checked() {
+                            let _ = kani::any::<$ty>().$checked_method();
+                        }
+
+                        #[kani::proof_for_contract($ty::$method)]
+                        fn positive_returns_log() {
+                            let value: $ty = kani::any();
+                            kani::assume(value > 0);
+                            kani::cover(
+                                true,
+                                "non-vacuity witness: the assumed input space is non-empty",
+                            );
+                            let _ = value.$method();
+                        }
+
+                        #[kani::proof]
+                        #[kani::should_panic]
+                        fn nonpositive_panics() {
+                            let value: $ty = kani::any();
+                            kani::assume(value <= 0);
+                            kani::cover(
+                                true,
+                                "non-vacuity witness: the assumed input space is non-empty",
+                            );
+                            let _ = value.$method();
+                            // Not `kani::assert`: `should_panic` would accept that as the panic.
+                            kani::safety_check(false, "returned for a nonpositive input");
+                        }
+                    }
+                )+}
+            };
+        }
+
+        check_logarithm! {
+            ilog2, checked_ilog2;
+            i8, i16, i32, i64, i128, isize, u8, u16, u32, u64, u128, usize
+        }
+        check_logarithm! {
+            ilog10, checked_ilog10;
+            i8, i16, i32, i64, i128, isize, u8, u16, u32, u64, u128, usize
+        }
+    }
 }
diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs
index d63805e401973..c1ab1e1e50deb 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::is_ilog(self.get() as u128, 2, *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::is_ilog(self.get() as u128, 10, *result))]
         pub const fn ilog10(self) -> u32 {
             imp::int_log10::$Int(self)
         }
@@ -5231,4 +5233,27 @@ mod verify {
         u128::MAX - 0xFFFFu128,
         u128::MAX
     );
+
+    mod logarithms {
+        macro_rules! check_logarithms {
+            ($($ty:ident),+) => {$(
+                mod $ty {
+                    use crate::kani;
+                    use crate::num::NonZero;
+
+                    #[kani::proof_for_contract(NonZero::<$ty>::ilog2)]
+                    fn ilog2() {
+                        let _ = kani::any::<NonZero<$ty>>().ilog2();
+                    }
+
+                    #[kani::proof_for_contract(NonZero::<$ty>::ilog10)]
+                    fn ilog10() {
+                        let _ = kani::any::<NonZero<$ty>>().ilog10();
+                    }
+                }
+            )+};
+        }
+
+        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..899b79f3e7c0a 100644
--- a/library/core/src/num/uint_macros.rs
+++ b/library/core/src/num/uint_macros.rs
@@ -1834,6 +1834,7 @@ macro_rules! uint_impl {
                       without modifying the original"]
         #[inline]
         #[track_caller]
+        #[ensures(|result: &u32| imp::int_log10::is_ilog(self as u128, 2, *result))]
         pub const fn ilog2(self) -> u32 {
             if let Some(log) = self.checked_ilog2() {
                 log
@@ -1859,6 +1860,7 @@ macro_rules! uint_impl {
                       without modifying the original"]
         #[inline]
         #[track_caller]
+        #[ensures(|result: &u32| imp::int_log10::is_ilog(self as u128, 10, *result))]
         pub const fn ilog10(self) -> u32 {
             if let Some(log) = self.checked_ilog10() {
                 log
@@ -1957,6 +1959,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) => imp::int_log10::is_ilog(self as u128, 2, log),
+            None => self == 0,
+        })]
         pub const fn checked_ilog2(self) -> Option<u32> {
             match NonZero::new(self) {
                 Some(x) => Some(x.ilog2()),
@@ -1978,6 +1984,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) => imp::int_log10::is_ilog(self as u128, 10, log),
+            None => self == 0,
+        })]
         pub const fn checked_ilog10(self) -> Option<u32> {
             match NonZero::new(self) {
                 Some(x) => Some(x.ilog10()),