diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs
index a50353b7c96d..1c7e9fcdf6f0 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs
@@ -46,7 +46,19 @@ pub fn codegen_in_range_expr(
     mm: &MachineModel,
 ) -> Expr {
     match float_ty {
-        FloatTy::F32 => {
+        FloatTy::F16 => {
+            let (lower, upper) = get_bounds_f16(integral_ty, mm);
+            let mut in_range = Expr::bool_true();
+            // Avoid unnecessary comparison against -∞ or ∞
+            if lower != f16::NEG_INFINITY {
+                in_range = in_range.and(float_expr.clone().gt(Expr::float16_constant(lower)));
+            }
+            if upper != f16::INFINITY {
+                in_range = in_range.and(float_expr.clone().lt(Expr::float16_constant(upper)));
+            }
+            in_range
+        }
+         FloatTy::F32 => {
             let (lower, upper) = get_bounds_f32(integral_ty, mm);
             let mut in_range = Expr::bool_true();
             // Avoid unnecessary comparison against -∞ or ∞
@@ -69,10 +81,31 @@ pub fn codegen_in_range_expr(
             }
             in_range
         }
-        _ => unimplemented!(),
+        FloatTy::F128 => {
+            let (lower, upper) = get_bounds_f128(integral_ty, mm);
+            let mut in_range = Expr::bool_true();
+            if lower != f128::NEG_INFINITY {
+                in_range = in_range.and(float_expr.clone().gt(Expr::float128_constant(lower)));
+            }
+            if upper != f128::INFINITY {
+                in_range = in_range.and(float_expr.clone().lt(Expr::float128_constant(upper)));
+            }
+            in_range
+        }
     }
 }
 
+const F16_I8_LOWER: [u8; 2] = [0x08, 0xD8];
+const F16_I8_UPPER: [u8; 2] = [0x00, 0x58];
+const F16_I16_LOWER: [u8; 2] = [0x01, 0xF8];
+const F16_I16_UPPER: [u8; 2] = [0x00, 0x78];
+const F16_I32_LOWER: [u8; 2] = [0x00, 0xFC]; // -inf
+const F16_I32_UPPER: [u8; 2] = [0x00, 0x7C]; // inf
+const F16_I64_LOWER: [u8; 2] = [0x00, 0xFC]; // -inf
+const F16_I64_UPPER: [u8; 2] = [0x00, 0x7C]; // inf
+const F16_I128_LOWER: [u8; 2] = [0x00, 0xFC]; // -inf
+const F16_I128_UPPER: [u8; 2] = [0x00, 0x7C]; // inf
+
 const F32_I8_LOWER: [u8; 4] = [0x00, 0x00, 0x01, 0xC3]; // -129.0
 const F32_I8_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x43]; // 128.0
 const F32_I16_LOWER: [u8; 4] = [0x00, 0x01, 0x00, 0xC7]; // -32769.0
@@ -97,6 +130,24 @@ const F64_I64_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x43];
 const F64_I128_LOWER: [u8; 8] = [0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0xC7]; // -170141183460469269510619166673045815296.0
 const F64_I128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x47]; // 170141183460469231731687303715884105728.0
 
+const F128_I8_LOWER: [u8; 16] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x02, 0x06, 0xC0];
+const F128_I8_UPPER: [u8; 16] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x06, 0x40];
+const F128_I16_LOWER: [u8; 16] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x02, 0x00, 0x0E, 0xC0];
+const F128_I16_UPPER: [u8; 16] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x0E, 0x40];
+const F128_I32_LOWER: [u8; 16] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x02, 0x00, 0x00, 0x00, 0x1E, 0xC0];
+const F128_I32_UPPER: [u8; 16] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x1E, 0x40];
+const F128_I64_LOWER: [u8; 16] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x02, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x3E, 0xC0];
+const F128_I64_UPPER: [u8; 16] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x3E, 0x40];
+const F128_I128_LOWER: [u8; 16] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7F, 0xC0];
+const F128_I128_UPPER: [u8; 16] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7E, 0x40];
+
+const F16_U_LOWER: [u8; 2] = [0x00, 0xBC];
+const F16_U8_UPPER: [u8; 2] = [0x00, 0x5C];
+const F16_U16_UPPER: [u8; 2] = [0x00, 0x7C]; // inf
+const F16_U32_UPPER: [u8; 2] = [0x00, 0x7C]; // inf
+const F16_U64_UPPER: [u8; 2] = [0x00, 0x7C]; // inf
+const F16_U128_UPPER: [u8; 2] = [0x00, 0x7C]; // inf
+
 const F32_U_LOWER: [u8; 4] = [0x00, 0x00, 0x80, 0xBF]; // -1.0
 const F32_U8_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x43]; // 256.0
 const F32_U16_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x47]; // 65536.0
@@ -112,6 +163,13 @@ const F64_U32_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x41];
 const F64_U64_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x43]; // 18446744073709551616.0
 const F64_U128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x47]; // 340282366920938463463374607431768211456.0
 
+const F128_U_LOWER: [u8; 16] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xFF, 0xBF];
+const F128_U8_UPPER: [u8; 16] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x07, 0x40];
+const F128_U16_UPPER: [u8; 16] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x0F, 0x40];
+const F128_U32_UPPER: [u8; 16] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x1F, 0x40];
+const F128_U64_UPPER: [u8; 16] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x3F, 0x40];
+const F128_U128_UPPER: [u8; 16] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7F, 0x40];
+
 /// upper is the smallest `f32` that after truncation is strictly larger than i<N>::MAX or u<N>::MAX
 /// lower is the largest `f32` that after truncation is strictly smaller than i<N>::MIN or u<N>::MIN
 ///
@@ -135,6 +193,14 @@ const F64_U128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x47]
 ///
 /// For all unsigned types, lower is -1.0 because the next higher number, when
 /// truncated is -0.0 (or 0.0) which is not strictly smaller than `u<N>::MIN`
+fn get_bounds_f16(integral_ty: RigidTy, mm: &MachineModel) -> (f16, f16) {
+    match integral_ty {
+        RigidTy::Int(int_ty) => get_bounds_f16_int(int_ty, mm),
+        RigidTy::Uint(uint_ty) => get_bounds_f16_uint(uint_ty, mm),
+        _ => unreachable!(),
+    }
+}
+
 fn get_bounds_f32(integral_ty: RigidTy, mm: &MachineModel) -> (f32, f32) {
     match integral_ty {
         RigidTy::Int(int_ty) => get_bounds_f32_int(int_ty, mm),
@@ -151,6 +217,31 @@ fn get_bounds_f64(integral_ty: RigidTy, mm: &MachineModel) -> (f64, f64) {
     }
 }
 
+fn get_bounds_f128(integral_ty: RigidTy, mm: &MachineModel) -> (f128, f128) {
+    match integral_ty {
+        RigidTy::Int(int_ty) => get_bounds_f128_int(int_ty, mm),
+        RigidTy::Uint(uint_ty) => get_bounds_f128_uint(uint_ty, mm),
+        _ => unreachable!(),
+    }
+}
+
+fn get_bounds_f16_uint(uint_ty: UintTy, mm: &MachineModel) -> (f16, f16) {
+    let lower: f16 = f16::from_le_bytes(F16_U_LOWER);
+    let upper: f16 = match uint_ty {
+        UintTy::U8 => f16::from_le_bytes(F16_U8_UPPER),
+        UintTy::U16 => f16::from_le_bytes(F16_U16_UPPER),
+        UintTy::U32 => f16::from_le_bytes(F16_U32_UPPER),
+        UintTy::U64 => f16::from_le_bytes(F16_U64_UPPER),
+        UintTy::U128 => f16::from_le_bytes(F16_U128_UPPER),
+        UintTy::Usize => match mm.pointer_width {
+            32 => f16::from_le_bytes(F16_U32_UPPER),
+            64 => f16::from_le_bytes(F16_U64_UPPER),
+            _ => unreachable!(),
+        },
+    };
+    (lower, upper)
+}
+
 fn get_bounds_f32_uint(uint_ty: UintTy, mm: &MachineModel) -> (f32, f32) {
     let lower: f32 = f32::from_le_bytes(F32_U_LOWER);
     let upper: f32 = match uint_ty {
@@ -185,6 +276,54 @@ fn get_bounds_f64_uint(uint_ty: UintTy, mm: &MachineModel) -> (f64, f64) {
     (lower, upper)
 }
 
+fn get_bounds_f128_uint(uint_ty: UintTy, mm: &MachineModel) -> (f128, f128) {
+    let lower = f128::from_le_bytes(F128_U_LOWER);
+    let upper = match uint_ty {
+        UintTy::U8 => f128::from_le_bytes(F128_U8_UPPER),
+        UintTy::U16 => f128::from_le_bytes(F128_U16_UPPER),
+        UintTy::U32 => f128::from_le_bytes(F128_U32_UPPER),
+        UintTy::U64 => f128::from_le_bytes(F128_U64_UPPER),
+        UintTy::U128 => f128::from_le_bytes(F128_U128_UPPER),
+        UintTy::Usize => match mm.pointer_width {
+            32 => f128::from_le_bytes(F128_U32_UPPER),
+            64 => f128::from_le_bytes(F128_U64_UPPER),
+            _ => unreachable!(),
+        },
+    };
+    (lower, upper)
+}
+
+
+fn get_bounds_f16_int(int_ty: IntTy, mm: &MachineModel) -> (f16, f16) {
+    let lower = match int_ty {
+        IntTy::I8 => f16::from_le_bytes(F16_I8_LOWER),
+        IntTy::I16 => f16::from_le_bytes(F16_I16_LOWER),
+        IntTy::I32 => f16::from_le_bytes(F16_I32_LOWER),
+        IntTy::I64 => f16::from_le_bytes(F16_I64_LOWER),
+        IntTy::I128 => f16::from_le_bytes(F16_I128_LOWER),
+        IntTy::Isize => match mm.pointer_width {
+            32 => f16::from_le_bytes(F16_I32_LOWER),
+            64 => f16::from_le_bytes(F16_I64_LOWER),
+            _ => unreachable!(),
+        },
+    };
+
+    let upper = match int_ty {
+        IntTy::I8 => f16::from_le_bytes(F16_I8_UPPER),
+        IntTy::I16 => f16::from_le_bytes(F16_I16_UPPER),
+        IntTy::I32 => f16::from_le_bytes(F16_I32_UPPER),
+        IntTy::I64 => f16::from_le_bytes(F16_I64_UPPER),
+        IntTy::I128 => f16::from_le_bytes(F16_I128_UPPER),
+        IntTy::Isize => match mm.pointer_width {
+            32 => f16::from_le_bytes(F16_I32_UPPER),
+            64 => f16::from_le_bytes(F16_I64_UPPER),
+            _ => unreachable!(),
+        },
+    };
+    (lower, upper)
+}
+
+
 fn get_bounds_f32_int(int_ty: IntTy, mm: &MachineModel) -> (f32, f32) {
     let lower = match int_ty {
         IntTy::I8 => f32::from_le_bytes(F32_I8_LOWER),
@@ -242,6 +381,34 @@ fn get_bounds_f64_int(int_ty: IntTy, mm: &MachineModel) -> (f64, f64) {
     (lower, upper)
 }
 
+fn get_bounds_f128_int(int_ty: IntTy, mm: &MachineModel) -> (f128, f128) {
+    let lower = match int_ty {
+        IntTy::I8 => f128::from_le_bytes(F128_I8_LOWER),
+        IntTy::I16 => f128::from_le_bytes(F128_I16_LOWER),
+        IntTy::I32 => f128::from_le_bytes(F128_I32_LOWER),
+        IntTy::I64 => f128::from_le_bytes(F128_I64_LOWER),
+        IntTy::I128 => f128::from_le_bytes(F128_I128_LOWER),
+        IntTy::Isize => match mm.pointer_width {
+            32 => f128::from_le_bytes(F128_I32_LOWER),
+            64 => f128::from_le_bytes(F128_I64_LOWER),
+            _ => unreachable!(),
+        },
+    };
+    let upper = match int_ty {
+        IntTy::I8 => f128::from_le_bytes(F128_I8_UPPER),
+        IntTy::I16 => f128::from_le_bytes(F128_I16_UPPER),
+        IntTy::I32 => f128::from_le_bytes(F128_I32_UPPER),
+        IntTy::I64 => f128::from_le_bytes(F128_I64_UPPER),
+        IntTy::I128 => f128::from_le_bytes(F128_I128_UPPER),
+        IntTy::Isize => match mm.pointer_width {
+            32 => f128::from_le_bytes(F128_I32_UPPER),
+            64 => f128::from_le_bytes(F128_I64_UPPER),
+            _ => unreachable!(),
+        },
+    };
+    (lower, upper)
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
diff --git a/tests/expected/intrinsics/float-to-int/oob_f128.expected b/tests/expected/intrinsics/float-to-int/oob_f128.expected
new file mode 100644
index 000000000000..020299489786
--- /dev/null
+++ b/tests/expected/intrinsics/float-to-int/oob_f128.expected
@@ -0,0 +1,13 @@
+Verification failed for - check_cast_i16
+Verification failed for - check_cast_i128
+Verification failed for - check_cast_u8
+Verification failed for - check_cast_u32
+Verification failed for - check_cast_u64
+Verification failed for - check_cast_u16
+Verification failed for - check_cast_u128
+Verification failed for - check_cast_usize
+Verification failed for - check_cast_i8
+Verification failed for - check_cast_i64
+Verification failed for - check_cast_isize
+Verification failed for - check_cast_i32
+Complete - 0 successfully verified harnesses, 12 failures, 12 total.
diff --git a/tests/expected/intrinsics/float-to-int/oob_f128.rs b/tests/expected/intrinsics/float-to-int/oob_f128.rs
new file mode 100644
index 000000000000..b28cc0360d8a
--- /dev/null
+++ b/tests/expected/intrinsics/float-to-int/oob_f128.rs
@@ -0,0 +1,29 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(f128)]
+
+// Check that `f128::MAX` does not fit in some integer types
+
+macro_rules! check_cast {
+    ($name:ident, $t:ty) => {
+        #[kani::proof]
+        fn $name() {
+            let x = f128::MAX;
+            let _u: $t = unsafe { x.to_int_unchecked() };
+        }
+    };
+}
+
+check_cast!(check_cast_u8, u8);
+check_cast!(check_cast_u16, u16);
+check_cast!(check_cast_u32, u32);
+check_cast!(check_cast_u64, u64);
+check_cast!(check_cast_u128, u128);
+check_cast!(check_cast_usize, usize);
+
+check_cast!(check_cast_i8, i8);
+check_cast!(check_cast_i16, i16);
+check_cast!(check_cast_i32, i32);
+check_cast!(check_cast_i64, i64);
+check_cast!(check_cast_i128, i128);
+check_cast!(check_cast_isize, isize);
diff --git a/tests/kani/Intrinsics/FloatToInt/float_to_int.rs b/tests/kani/Intrinsics/FloatToInt/float_to_int.rs
index 4797669b9b61..76f0a19cf58c 100644
--- a/tests/kani/Intrinsics/FloatToInt/float_to_int.rs
+++ b/tests/kani/Intrinsics/FloatToInt/float_to_int.rs
@@ -1,6 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 #![feature(core_intrinsics)]
+#![feature(f16)]
+#![feature(f128)]
 
 // Check that the `float_to_int_unchecked` intrinsic works as expected
 
@@ -16,6 +18,32 @@ macro_rules! check_float_to_int_unchecked {
     };
 }
 
+macro_rules! check_float_to_int_unchecked_no_assert {
+    ($float_ty:ty, $int_ty:ty) => {
+        let f: $float_ty = kani::any_where(|f: &$float_ty| {
+            f.is_finite() && *f > <$int_ty>::MIN as $float_ty && *f < <$int_ty>::MAX as $float_ty
+        });
+        let _u: $int_ty = unsafe { float_to_int_unchecked(f) };
+    };
+}
+
+
+#[kani::proof]
+fn check_f16_to_int_unchecked() {
+    check_float_to_int_unchecked_no_assert!(f16, u8);
+    check_float_to_int_unchecked_no_assert!(f16, u16);
+    check_float_to_int_unchecked_no_assert!(f16, u32);
+    check_float_to_int_unchecked_no_assert!(f16, u64);
+    check_float_to_int_unchecked_no_assert!(f16, u128);
+    check_float_to_int_unchecked_no_assert!(f16, usize);
+    check_float_to_int_unchecked_no_assert!(f16, i8);
+    check_float_to_int_unchecked_no_assert!(f16, i16);
+    check_float_to_int_unchecked_no_assert!(f16, i32);
+    check_float_to_int_unchecked_no_assert!(f16, i64);
+    check_float_to_int_unchecked_no_assert!(f16, i128);
+    check_float_to_int_unchecked_no_assert!(f16, isize);
+}
+
 #[kani::proof]
 fn check_f32_to_int_unchecked() {
     check_float_to_int_unchecked!(f32, u8);
@@ -47,3 +75,19 @@ fn check_f64_to_int_unchecked() {
     check_float_to_int_unchecked!(f64, i128);
     check_float_to_int_unchecked!(f64, isize);
 }
+
+#[kani::proof]
+fn check_f128_to_int_unchecked() {
+    check_float_to_int_unchecked_no_assert!(f128, u8);
+    check_float_to_int_unchecked_no_assert!(f128, u16);
+    check_float_to_int_unchecked_no_assert!(f128, u32);
+    check_float_to_int_unchecked_no_assert!(f128, u64);
+    check_float_to_int_unchecked_no_assert!(f128, u128);
+    check_float_to_int_unchecked_no_assert!(f128, usize);
+    check_float_to_int_unchecked_no_assert!(f128, i8);
+    check_float_to_int_unchecked_no_assert!(f128, i16);
+    check_float_to_int_unchecked_no_assert!(f128, i32);
+    check_float_to_int_unchecked_no_assert!(f128, i64);
+    check_float_to_int_unchecked_no_assert!(f128, i128);
+    check_float_to_int_unchecked_no_assert!(f128, isize);
+}