diff --git a/library/core/src/num/flt2dec/mod.rs b/library/core/src/num/flt2dec/mod.rs
index e79a00a865969..90534bb2711e7 100644
--- a/library/core/src/num/flt2dec/mod.rs
+++ b/library/core/src/num/flt2dec/mod.rs
@@ -666,3 +666,184 @@ where
         }
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+pub mod flt2dec_verify {
+    use super::*;
+    use crate::kani;
+
+    // Upper bound on the (symbolic) digit-buffer length used by the proofs of
+    // `digits_to_dec_str` / `digits_to_exp_str`.  Their `assume_init` safety
+    // obligations depend only on control flow driven by `buf.len()`, `exp`, and
+    // the digit-count arguments, and every length-dependent branch is a
+    // comparison against a small value (`buf.len() == 1` in `digits_to_exp_str`,
+    // `exp < buf.len()` and `frac_digits > buf.len() - exp` in
+    // `digits_to_dec_str`), so a symbolic length in `1..=4` reaches every branch
+    // and therefore every distinct set of initialized `parts`; a longer buffer
+    // only adds digits to a `Part::Copy` slice.
+    const PROOF_BUFLEN: usize = 4;
+
+    // A digit buffer of symbolic length `1..=PROOF_BUFLEN` whose first digit is
+    // nonzero, as the callees require.
+    fn any_digits(buf: &[u8; PROOF_BUFLEN]) -> &[u8] {
+        kani::assume(buf[0] > b'0');
+        let n: usize = kani::any();
+        kani::assume(n >= 1 && n <= PROOF_BUFLEN);
+        &buf[..n]
+    }
+
+    // `digits_to_dec_str` writes 2, 3, or 4 `parts` depending on `exp` and
+    // `frac_digits`, then `assume_init_ref`s exactly the prefix it wrote.  Kani
+    // checks that no uninitialized `Part` is ever read and that no UB occurs.
+    #[kani::proof]
+    fn check_digits_to_dec_str() {
+        let buf: [u8; PROOF_BUFLEN] = kani::any();
+        let exp: i16 = kani::any();
+        let frac_digits: usize = kani::any();
+        let mut parts: [MaybeUninit<Part<'_>>; 4] = [const { MaybeUninit::uninit() }; 4];
+        let _ = digits_to_dec_str(any_digits(&buf), exp, frac_digits, &mut parts);
+    }
+
+    // `digits_to_exp_str` writes a variable prefix of up to 6 `parts` and
+    // `assume_init_ref`s `parts[..n + 2]` for the `n` it actually wrote; the
+    // `buf.len() == 1` case takes its own (3-part) path.
+    #[kani::proof]
+    fn check_digits_to_exp_str() {
+        let buf: [u8; PROOF_BUFLEN] = kani::any();
+        let exp: i16 = kani::any();
+        let min_ndigits: usize = kani::any();
+        let upper: bool = kani::any();
+        let mut parts: [MaybeUninit<Part<'_>>; 6] = [const { MaybeUninit::uninit() }; 6];
+        let _ = digits_to_exp_str(any_digits(&buf), exp, min_ndigits, upper, &mut parts);
+    }
+
+    // An arbitrary sign-formatting option.
+    fn any_sign() -> Sign {
+        if kani::any() { Sign::Minus } else { Sign::MinusPlus }
+    }
+
+    // A stub digit generator standing in for `grisu`/`dragon` `format_shortest`.
+    // It writes one arbitrary nonzero digit into the scratch buffer and returns
+    // it with an arbitrary exponent.  This isolates the `to_shortest_*`
+    // functions' own `unsafe` (the `assume_init` on `parts` and the delegation
+    // to the already-verified `digits_to_*_str`) from the loopy strategy code,
+    // which is verified separately.  A generic `fn` is required here rather than
+    // a closure so it satisfies the higher-ranked lifetime in the `F` bound.
+    fn stub_shortest<'a>(_d: &Decoded, buf: &'a mut [MaybeUninit<u8>]) -> (&'a [u8], i16) {
+        let digit: u8 = kani::any();
+        kani::assume(digit > b'0');
+        buf[0] = MaybeUninit::new(digit);
+        let exp: i16 = kani::any();
+        // SAFETY: we just initialized the element `..1`.
+        (unsafe { buf[..1].assume_init_ref() }, exp)
+    }
+
+    // `to_shortest_str` handles NaN/Inf/Zero by writing `parts[..1]` and the
+    // finite case by delegating to `digits_to_dec_str`.  An arbitrary `f64`
+    // reaches every `FullDecoded` arm.
+    #[kani::proof]
+    fn check_to_shortest_str() {
+        let v: f64 = kani::any();
+        let sign = any_sign();
+        let frac_digits: usize = kani::any();
+        let mut buf: [MaybeUninit<u8>; MAX_SIG_DIGITS] =
+            [const { MaybeUninit::uninit() }; MAX_SIG_DIGITS];
+        let mut parts: [MaybeUninit<Part<'_>>; 4] = [const { MaybeUninit::uninit() }; 4];
+        let _ = to_shortest_str(stub_shortest, v, sign, frac_digits, &mut buf, &mut parts);
+    }
+
+    // `to_shortest_exp_str` is the exponential-form analogue; its finite arm
+    // delegates to `digits_to_dec_str` or `digits_to_exp_str` per `dec_bounds`.
+    #[kani::proof]
+    fn check_to_shortest_exp_str() {
+        let v: f64 = kani::any();
+        let sign = any_sign();
+        let lo: i16 = kani::any();
+        let hi: i16 = kani::any();
+        kani::assume(lo <= hi);
+        let upper: bool = kani::any();
+        let mut buf: [MaybeUninit<u8>; MAX_SIG_DIGITS] =
+            [const { MaybeUninit::uninit() }; MAX_SIG_DIGITS];
+        let mut parts: [MaybeUninit<Part<'_>>; 6] = [const { MaybeUninit::uninit() }; 6];
+        let _ = to_shortest_exp_str(stub_shortest, v, sign, (lo, hi), upper, &mut buf, &mut parts);
+    }
+
+    // For `f64`, `decode` bottoms out at `decoded.exp == -1076` (normal-min,
+    // which subtracts 2 from `integer_decode`'s minimum of `-1074`), where
+    // `estimate_max_buf_len` returns 828.  1024 (the size the real `fmt` callers
+    // use) covers every reachable decoded exponent for the
+    // `buf.len() >= maxlen` assertions in both `to_exact_*` functions.
+    const PROOF_EXACT_BUFLEN: usize = 1024;
+
+    // Stub `format_exact` for `to_exact_exp_str`, which always passes the result
+    // to `digits_to_exp_str` (it calls the generator with `limit = i16::MIN`, so
+    // the real one never returns an empty buffer here).  Returns one nonzero
+    // digit with an arbitrary exponent.
+    fn stub_exact_full<'a>(
+        _d: &Decoded,
+        buf: &'a mut [MaybeUninit<u8>],
+        _limit: i16,
+    ) -> (&'a [u8], i16) {
+        let digit: u8 = kani::any();
+        kani::assume(digit > b'0');
+        buf[0] = MaybeUninit::new(digit);
+        let exp: i16 = kani::any();
+        // SAFETY: we just initialized the element `..1`.
+        (unsafe { buf[..1].assume_init_ref() }, exp)
+    }
+
+    // Stub `format_exact` for `to_exact_fixed_str`, which branches on
+    // `exp <= limit`.  That arm requires an empty result (the source
+    // `debug_assert_eq!`s `buf.len() == 0`); the other arm needs a valid nonzero
+    // digit with `exp > limit`.  Couple the result to `limit` so both caller
+    // arms are exercised soundly.
+    fn stub_exact_limited<'a>(
+        _d: &Decoded,
+        buf: &'a mut [MaybeUninit<u8>],
+        limit: i16,
+    ) -> (&'a [u8], i16) {
+        if kani::any() {
+            let exp: i16 = kani::any();
+            kani::assume(exp <= limit);
+            // SAFETY: an empty prefix is trivially initialized.
+            (unsafe { buf[..0].assume_init_ref() }, exp)
+        } else {
+            let digit: u8 = kani::any();
+            kani::assume(digit > b'0');
+            buf[0] = MaybeUninit::new(digit);
+            let exp: i16 = kani::any();
+            kani::assume(exp > limit);
+            // SAFETY: we just initialized the element `..1`.
+            (unsafe { buf[..1].assume_init_ref() }, exp)
+        }
+    }
+
+    // `to_exact_exp_str` writes `parts[..1]` for NaN/Inf, `parts[..3]`/`parts[..1]`
+    // for zero, and delegates to `digits_to_exp_str` for finite values.
+    #[kani::proof]
+    fn check_to_exact_exp_str() {
+        let v: f64 = kani::any();
+        let sign = any_sign();
+        let ndigits: usize = kani::any();
+        kani::assume(ndigits > 0);
+        let upper: bool = kani::any();
+        let mut buf: [MaybeUninit<u8>; PROOF_EXACT_BUFLEN] =
+            [const { MaybeUninit::uninit() }; PROOF_EXACT_BUFLEN];
+        let mut parts: [MaybeUninit<Part<'_>>; 6] = [const { MaybeUninit::uninit() }; 6];
+        let _ = to_exact_exp_str(stub_exact_full, v, sign, ndigits, upper, &mut buf, &mut parts);
+    }
+
+    // `to_exact_fixed_str` additionally has a finite sub-branch (`exp <= limit`)
+    // that renders like zero; `stub_exact_limited` reaches both sub-branches.
+    #[kani::proof]
+    fn check_to_exact_fixed_str() {
+        let v: f64 = kani::any();
+        let sign = any_sign();
+        let frac_digits: usize = kani::any();
+        let mut buf: [MaybeUninit<u8>; PROOF_EXACT_BUFLEN] =
+            [const { MaybeUninit::uninit() }; PROOF_EXACT_BUFLEN];
+        let mut parts: [MaybeUninit<Part<'_>>; 4] = [const { MaybeUninit::uninit() }; 4];
+        let _ = to_exact_fixed_str(stub_exact_limited, v, sign, frac_digits, &mut buf, &mut parts);
+    }
+}
diff --git a/library/core/src/num/flt2dec/strategy/grisu.rs b/library/core/src/num/flt2dec/strategy/grisu.rs
index d3bbb0934e0ff..ab7b7af93844b 100644
--- a/library/core/src/num/flt2dec/strategy/grisu.rs
+++ b/library/core/src/num/flt2dec/strategy/grisu.rs
@@ -774,3 +774,169 @@ pub fn format_exact<'a>(
         None => fallback(d, buf, limit),
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+pub mod grisu_verify {
+    use super::*;
+    use crate::kani;
+
+    // Scope of the proofs in this module.  `format_exact_opt` is called
+    // directly, unstubbed, against a 1-byte buffer: `len` is then concrete, so
+    // CBMC prunes the unreachable digit iterations and the proof closes in
+    // seconds.  With a symbolic `len` (any longer buffer) the unrolled digit
+    // loops keep every `possibly_round` instance live and the formula exceeds
+    // the 2^12 addressed objects the repository runs CBMC with
+    // (`--object-bits 12`); `format_shortest_opt`, whose digit loops are bounded
+    // only by the arithmetic (up to 17 digits, unwind 20), produces a program of
+    // ~4.7M SSA steps and ~120k verification conditions whose bit-blasting runs
+    // out of memory, and the value-dependent `debug_assert!`s of its weeding
+    // step (`round_and_weed`, a nested function that cannot be stubbed) turn the
+    // proof into a numerical-correctness obligation over the 64x64-bit `Fp`
+    // products.  Those two functions are therefore covered here through the
+    // wrapper proofs below (both callees modelled as opaque), and a direct proof
+    // needs loop contracts on the digit loops.
+    //
+    // An arbitrary `Decoded` satisfying every precondition the `grisu` entry
+    // points assert.  `mant + plus < 2^61` (and the `checked_add`/`checked_sub`
+    // assumptions) keep the scaled `Fp` arithmetic inside `u64`.
+    fn arbitrary_decoded() -> Decoded {
+        let mant: u64 = kani::any();
+        let minus: u64 = kani::any();
+        let plus: u64 = kani::any();
+        kani::assume(mant > 0);
+        kani::assume(minus > 0);
+        kani::assume(plus > 0);
+        kani::assume(mant.checked_add(plus).is_some());
+        kani::assume(mant.checked_sub(minus).is_some());
+        kani::assume(mant + plus < (1 << 61));
+        let exp: i16 = kani::any();
+        // `[-1076, 970]` is the exponent range of `decode()`; 971 is unreachable.
+        kani::assume(exp >= -1076 && exp <= 970);
+        Decoded { mant, minus, plus, exp, inclusive: kani::any() }
+    }
+
+    // An arbitrary input for the exact-mode proofs: the full documented
+    // precondition of `format_exact_opt` (`0 < mant < 2^61`), with `exp`
+    // bounded to the decoder image so `cached_power` stays in its table domain.
+    fn arbitrary_decoded_exact() -> Decoded {
+        let mant: u64 = kani::any();
+        kani::assume(mant > 0 && mant < (1 << 61));
+        let exp: i16 = kani::any();
+        kani::assume(exp >= -1076 && exp <= 970);
+        Decoded { mant, minus: 1, plus: 1, exp, inclusive: kani::any() }
+    }
+
+    // Direct proof of `format_exact_opt`: NO stubs, NO in-body assumes, over the
+    // function's full documented precondition, an arbitrary `limit`, and a
+    // 1-byte buffer.  Every buffer access in `format_exact_opt` is bounded
+    // structurally (`len` is clamped to `buf.len()` on every path, each digit
+    // write is gated by an `i == len` return, and `possibly_round`'s carry write
+    // is guarded by `len < buf.len()`); this proof exercises the `len` clamp,
+    // the `exp <= limit` early path (`possibly_round` with `len == 0`), the
+    // first digit of both the integral and the fractional loop, and the real
+    // `cached_power` / `Fp::mul` / `possibly_round` arithmetic, so the
+    // value-dependent `debug_assert!`s are discharged from the real values.
+    #[kani::proof]
+    #[kani::unwind(20)]
+    fn check_format_exact_opt_buf1() {
+        let d = arbitrary_decoded_exact();
+        let limit: i16 = kani::any();
+        let mut buf: [MaybeUninit<u8>; 1] = [const { MaybeUninit::uninit() }; 1];
+        let _ = format_exact_opt(&d, &mut buf, limit);
+    }
+
+    // Wholesale havoc stub for the dragon fallback (modelled as an opaque op that
+    // writes a digit and returns an in-bounds slice of `buf`).
+    fn stub_dragon_format_exact<'a>(
+        _d: &Decoded,
+        buf: &'a mut [MaybeUninit<u8>],
+        _limit: i16,
+    ) -> (&'a [u8], i16) {
+        let digit: u8 = kani::any();
+        kani::assume(digit >= b'0' && digit <= b'9');
+        buf[0] = MaybeUninit::new(digit);
+        // SAFETY: we just initialized element 0.
+        (unsafe { buf[..1].assume_init_ref() }, kani::any())
+    }
+
+    // Wholesale havoc stub for `format_exact_opt`: nondeterministically returns
+    // `None` (released its borrow of `buf`) or `Some` slice of `buf`.  Modelling
+    // both callees as opaque isolates the WRAPPER's only `unsafe`: the
+    // lifetime-laundering reborrow `&mut *(buf as *mut _)`, whose soundness rests
+    // on `buf` being reused only on the `None` path.
+    fn stub_format_exact_opt<'a>(
+        _d: &Decoded,
+        buf: &'a mut [MaybeUninit<u8>],
+        _limit: i16,
+    ) -> Option<(&'a [u8], i16)> {
+        if kani::any() {
+            let digit: u8 = kani::any();
+            kani::assume(digit >= b'0' && digit <= b'9');
+            buf[0] = MaybeUninit::new(digit);
+            // SAFETY: we just initialized element 0.
+            Some((unsafe { buf[..1].assume_init_ref() }, kani::any()))
+        } else {
+            // The real function writes digits before it gives up; model that
+            // dirtying so the wrapper's reuse of `buf` on the `None` path is
+            // exercised against a modified buffer.
+            buf[0] = MaybeUninit::new(kani::any());
+            None
+        }
+    }
+
+    #[kani::proof]
+    #[kani::stub(format_exact_opt, stub_format_exact_opt)]
+    #[kani::stub(crate::num::flt2dec::strategy::dragon::format_exact, stub_dragon_format_exact)]
+    fn check_format_exact() {
+        let d = arbitrary_decoded_exact();
+        let limit: i16 = kani::any();
+        let mut buf: [MaybeUninit<u8>; 4] = [const { MaybeUninit::uninit() }; 4];
+        let _ = format_exact(&d, &mut buf, limit);
+    }
+
+    // Wholesale havoc stubs for `format_shortest`'s callees (no `limit` arg).
+    fn stub_dragon_format_shortest<'a>(
+        _d: &Decoded,
+        buf: &'a mut [MaybeUninit<u8>],
+    ) -> (&'a [u8], i16) {
+        let digit: u8 = kani::any();
+        kani::assume(digit >= b'0' && digit <= b'9');
+        buf[0] = MaybeUninit::new(digit);
+        // SAFETY: we just initialized element 0.
+        (unsafe { buf[..1].assume_init_ref() }, kani::any())
+    }
+
+    fn stub_format_shortest_opt<'a>(
+        _d: &Decoded,
+        buf: &'a mut [MaybeUninit<u8>],
+    ) -> Option<(&'a [u8], i16)> {
+        if kani::any() {
+            let digit: u8 = kani::any();
+            kani::assume(digit >= b'0' && digit <= b'9');
+            buf[0] = MaybeUninit::new(digit);
+            // SAFETY: we just initialized element 0.
+            Some((unsafe { buf[..1].assume_init_ref() }, kani::any()))
+        } else {
+            // The real function writes digits before it gives up; model that
+            // dirtying so the wrapper's reuse of `buf` on the `None` path is
+            // exercised against a modified buffer.
+            buf[0] = MaybeUninit::new(kani::any());
+            None
+        }
+    }
+
+    // `format_shortest` mirrors `format_exact`: its only `unsafe` is the
+    // lifetime-laundering reborrow, verified by modelling both callees as opaque.
+    #[kani::proof]
+    #[kani::stub(format_shortest_opt, stub_format_shortest_opt)]
+    #[kani::stub(
+        crate::num::flt2dec::strategy::dragon::format_shortest,
+        stub_dragon_format_shortest
+    )]
+    fn check_format_shortest() {
+        let d = arbitrary_decoded();
+        let mut buf: [MaybeUninit<u8>; 4] = [const { MaybeUninit::uninit() }; 4];
+        let _ = format_shortest(&d, &mut buf);
+    }
+}