diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
index 75eb18df0abb..16f33115e0ff 100644
--- a/cprover_bindings/src/goto_program/expr.rs
+++ b/cprover_bindings/src/goto_program/expr.rs
@@ -98,7 +98,11 @@ pub enum ExprValue {
     // {}
     EmptyUnion,
     /// `1.0f`
+    Float16Constant(f16),
+    /// `1.0f`
     FloatConstant(f32),
+    /// `Float 128 example`
+    Float128Constant(f128),
     /// `function(arguments)`
     FunctionCall {
         function: Expr,
@@ -581,6 +585,28 @@ impl Expr {
         expr!(EmptyUnion, typ)
     }
 
+    /// `3.14f`
+    pub fn float16_constant(c: f16) -> Self {
+        expr!(Float16Constant(c), Type::float16())
+    }
+
+    /// `union {_Float16 f; uint16_t bp} u = {.bp = 0x1234}; >>> u.f <<<`
+    pub fn float16_constant_from_bitpattern(bp: u16) -> Self {
+        let c = f16::from_bits(bp);
+        Self::float16_constant(c)
+    }
+
+    /// `3.14159265358979323846264338327950288L`
+    pub fn float128_constant(c: f128) -> Self {
+        expr!(Float128Constant(c), Type::float128())
+    }
+
+    /// `union {_Float128 f; __uint128_t bp} u = {.bp = 0x1234}; >>> u.f <<<`
+    pub fn float128_constant_from_bitpattern(bp: u128) -> Self {
+        let c = f128::from_bits(bp);
+        Self::float128_constant(c)
+    }
+
     /// `1.0f`
     pub fn float_constant(c: f32) -> Self {
         expr!(FloatConstant(c), Type::float())
diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs
index da943b26ab19..d0cc8821a447 100644
--- a/cprover_bindings/src/goto_program/typ.rs
+++ b/cprover_bindings/src/goto_program/typ.rs
@@ -41,6 +41,10 @@ pub enum Type {
     FlexibleArray { typ: Box<Type> },
     /// `float`
     Float,
+    /// `_Float16`
+    Float16,
+    /// `_Float128`
+    Float128,
     /// `struct x {}`
     IncompleteStruct { tag: InternedString },
     /// `union x {}`
@@ -166,6 +170,8 @@ impl DatatypeComponent {
             | Double
             | FlexibleArray { .. }
             | Float
+            | Float16
+            | Float128
             | Integer
             | Pointer { .. }
             | Signedbv { .. }
@@ -363,6 +369,8 @@ impl Type {
             Double => st.machine_model().double_width,
             Empty => 0,
             FlexibleArray { .. } => 0,
+            Float16 => 16,
+            Float128 => 128,
             Float => st.machine_model().float_width,
             IncompleteStruct { .. } => unreachable!("IncompleteStruct doesn't have a sizeof"),
             IncompleteUnion { .. } => unreachable!("IncompleteUnion doesn't have a sizeof"),
@@ -532,6 +540,22 @@ impl Type {
         }
     }
 
+    pub fn is_float_16(&self) -> bool {
+        let concrete = self.unwrap_typedef();
+        match concrete {
+            Float16 => true,
+            _ => false,
+        }
+    }
+
+    pub fn is_float_128(&self) -> bool {
+        let concrete = self.unwrap_typedef();
+        match concrete {
+            Float128 => true,
+            _ => false,
+        }
+    }
+
     pub fn is_float(&self) -> bool {
         let concrete = self.unwrap_typedef();
         match concrete {
@@ -543,7 +567,7 @@ impl Type {
     pub fn is_floating_point(&self) -> bool {
         let concrete = self.unwrap_typedef();
         match concrete {
-            Double | Float => true,
+            Double | Float | Float16 | Float128 => true,
             _ => false,
         }
     }
@@ -577,6 +601,8 @@ impl Type {
             | CInteger(_)
             | Double
             | Float
+            | Float16
+            | Float128
             | Integer
             | Pointer { .. }
             | Signedbv { .. }
@@ -632,6 +658,8 @@ impl Type {
             | Double
             | Empty
             | Float
+            | Float16
+            | Float128
             | Integer
             | Pointer { .. }
             | Signedbv { .. }
@@ -918,6 +946,8 @@ impl Type {
             | CInteger(_)
             | Double
             | Float
+            | Float16
+            | Float128
             | Integer
             | Pointer { .. }
             | Signedbv { .. }
@@ -1042,6 +1072,14 @@ impl Type {
         FlexibleArray { typ: Box::new(self) }
     }
 
+    pub fn float16() -> Self {
+        Float16
+    }
+
+    pub fn float128() -> Self {
+        Float128
+    }
+
     pub fn float() -> Self {
         Float
     }
@@ -1275,6 +1313,10 @@ impl Type {
             Expr::c_true()
         } else if self.is_float() {
             Expr::float_constant(1.0)
+        } else if self.is_float_16() {
+            Expr::float16_constant(1.0)
+        } else if self.is_float_128() {
+            Expr::float128_constant(1.0)
         } else if self.is_double() {
             Expr::double_constant(1.0)
         } else {
@@ -1291,6 +1333,10 @@ impl Type {
             Expr::c_false()
         } else if self.is_float() {
             Expr::float_constant(0.0)
+        } else if self.is_float_16() {
+            Expr::float16_constant(0.0)
+        } else if self.is_float_128() {
+            Expr::float128_constant(0.0)
         } else if self.is_double() {
             Expr::double_constant(0.0)
         } else if self.is_pointer() {
@@ -1309,6 +1355,8 @@ impl Type {
             | CInteger(_)
             | Double
             | Float
+            | Float16
+            | Float128
             | Integer
             | Pointer { .. }
             | Signedbv { .. }
@@ -1413,6 +1461,8 @@ impl Type {
             Type::Empty => "empty".to_string(),
             Type::FlexibleArray { typ } => format!("flexarray_of_{}", typ.to_identifier()),
             Type::Float => "float".to_string(),
+            Type::Float16 => "float16".to_string(),
+            Type::Float128 => "float128".to_string(),
             Type::IncompleteStruct { tag } => tag.to_string(),
             Type::IncompleteUnion { tag } => tag.to_string(),
             Type::InfiniteArray { typ } => {
@@ -1512,6 +1562,8 @@ mod type_tests {
         assert_eq!(type_def.is_unsigned(&mm), src_type.is_unsigned(&mm));
         assert_eq!(type_def.is_scalar(), src_type.is_scalar());
         assert_eq!(type_def.is_float(), src_type.is_float());
+        assert_eq!(type_def.is_float_16(), src_type.is_float_16());
+        assert_eq!(type_def.is_float_128(), src_type.is_float_128());
         assert_eq!(type_def.is_floating_point(), src_type.is_floating_point());
         assert_eq!(type_def.width(), src_type.width());
         assert_eq!(type_def.can_be_lvalue(), src_type.can_be_lvalue());
diff --git a/cprover_bindings/src/irep/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs
index 119aecb8887c..9d52f4ef32fa 100644
--- a/cprover_bindings/src/irep/irep_id.rs
+++ b/cprover_bindings/src/irep/irep_id.rs
@@ -283,6 +283,8 @@ pub enum IrepId {
     Short,
     Long,
     Float,
+    Float16,
+    Float128,
     Double,
     Byte,
     Boolean,
@@ -1157,6 +1159,8 @@ impl Display for IrepId {
             IrepId::Short => "short",
             IrepId::Long => "long",
             IrepId::Float => "float",
+            IrepId::Float16 => "float16",
+            IrepId::Float128 => "float128",
             IrepId::Double => "double",
             IrepId::Byte => "byte",
             IrepId::Boolean => "boolean",
diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs
index 8716c16d88e0..4b5c86350172 100644
--- a/cprover_bindings/src/irep/to_irep.rs
+++ b/cprover_bindings/src/irep/to_irep.rs
@@ -254,6 +254,25 @@ impl ToIrep for ExprValue {
                     )],
                 }
             }
+            ExprValue::Float16Constant(i) => {
+                let c: u16 = i.to_bits();
+                Irep {
+                    id: IrepId::Constant,
+                    sub: vec![],
+                    named_sub: linear_map![(IrepId::Value, Irep::just_bitpattern_id(c, 16, false))],
+                }
+            }
+            ExprValue::Float128Constant(i) => {
+                let c: u128 = i.to_bits();
+                Irep {
+                    id: IrepId::Constant,
+                    sub: vec![],
+                    named_sub: linear_map![(
+                        IrepId::Value,
+                        Irep::just_bitpattern_id(c, 128, false)
+                    )],
+                }
+            }
             ExprValue::FunctionCall { function, arguments } => side_effect_irep(
                 IrepId::FunctionCall,
                 vec![function.to_irep(mm), arguments_irep(arguments.iter(), mm)],
@@ -695,6 +714,30 @@ impl ToIrep for Type {
                     (IrepId::CCType, Irep::just_id(IrepId::Float)),
                 ],
             },
+            Type::Float16 => Irep {
+                id: IrepId::Floatbv,
+                sub: vec![],
+                // Fraction bits: 10
+                // Exponent width bits: 5
+                // Sign bit: 1
+                named_sub: linear_map![
+                    (IrepId::F, Irep::just_int_id(10)),
+                    (IrepId::Width, Irep::just_int_id(16)),
+                    (IrepId::CCType, Irep::just_id(IrepId::Float16)),
+                ],
+            },
+            Type::Float128 => Irep {
+                id: IrepId::Floatbv,
+                sub: vec![],
+                // Fraction bits: 112
+                // Exponent width bits: 15
+                // Sign bit: 1
+                named_sub: linear_map![
+                    (IrepId::F, Irep::just_int_id(112)),
+                    (IrepId::Width, Irep::just_int_id(128)),
+                    (IrepId::CCType, Irep::just_id(IrepId::Float128)),
+                ],
+            },
             Type::IncompleteStruct { tag } => Irep {
                 id: IrepId::Struct,
                 sub: vec![],
diff --git a/cprover_bindings/src/lib.rs b/cprover_bindings/src/lib.rs
index cd87dffd75a6..e77b29a24ca2 100644
--- a/cprover_bindings/src/lib.rs
+++ b/cprover_bindings/src/lib.rs
@@ -29,6 +29,9 @@
 //! Speical [irep::Irep::id]s include:
 //! 1. [irep::IrepId::Empty] and [irep::IrepId::Nil] behaves like \[null\].
 
+#![feature(f128)]
+#![feature(f16)]
+
 mod env;
 pub mod goto_program;
 pub mod irep;
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
index 7388ca44a5b7..5549edcced25 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -184,12 +184,18 @@ impl<'tcx> GotocCtx<'tcx> {
             // Instead, we use integers with the right width to represent the bit pattern.
             {
                 match k {
+                    FloatTy::F16 => Some(Expr::float16_constant_from_bitpattern(
+                        alloc.read_uint().unwrap() as u16,
+                    )),
                     FloatTy::F32 => Some(Expr::float_constant_from_bitpattern(
                         alloc.read_uint().unwrap() as u32,
                     )),
                     FloatTy::F64 => Some(Expr::double_constant_from_bitpattern(
                         alloc.read_uint().unwrap() as u64,
                     )),
+                    FloatTy::F128 => {
+                        Some(Expr::float128_constant_from_bitpattern(alloc.read_uint().unwrap()))
+                    }
                 }
             }
             TyKind::RigidTy(RigidTy::RawPtr(inner_ty, _))
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 6d00bda5bce4..6e6547295ff9 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -130,6 +130,8 @@ impl<'tcx> GotocCtx<'tcx> {
                 Type::Empty => todo!(),
                 Type::FlexibleArray { .. } => todo!(),
                 Type::Float => write!(out, "f32")?,
+                Type::Float16 => write!(out, "f16")?,
+                Type::Float128 => write!(out, "f128")?,
                 Type::IncompleteStruct { .. } => todo!(),
                 Type::IncompleteUnion { .. } => todo!(),
                 Type::InfiniteArray { .. } => todo!(),
@@ -542,9 +544,8 @@ impl<'tcx> GotocCtx<'tcx> {
             ty::Float(k) => match k {
                 FloatTy::F32 => Type::float(),
                 FloatTy::F64 => Type::double(),
-                // `F16` and `F128` are not yet handled.
-                // Tracked here: <https://github.com/model-checking/kani/issues/3069>
-                FloatTy::F16 | FloatTy::F128 => unimplemented!(),
+                FloatTy::F16 => Type::float16(),
+                FloatTy::F128 => Type::float128(),
             },
             ty::Adt(def, _) if def.repr().simd() => self.codegen_vector(ty),
             ty::Adt(def, subst) => {
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index b7d8feeee886..84ec8d627c59 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -1034,10 +1034,9 @@ fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option<KaniAttributeKind> {
                     .intersperse("::")
                     .collect::<String>();
                 KaniAttributeKind::try_from(ident_str.as_str())
-                    .map_err(|err| {
+                    .inspect_err(|&err| {
                         debug!(?err, "attr_kind_failed");
                         tcx.dcx().span_err(attr.span, format!("unknown attribute `{ident_str}`"));
-                        err
                     })
                     .ok()
             } else {
diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs
index a5cfa347a85e..d2f8cf17e9e7 100644
--- a/kani-compiler/src/main.rs
+++ b/kani-compiler/src/main.rs
@@ -13,6 +13,8 @@
 #![feature(more_qualified_paths)]
 #![feature(iter_intersperse)]
 #![feature(let_chains)]
+#![feature(f128)]
+#![feature(f16)]
 extern crate rustc_abi;
 extern crate rustc_ast;
 extern crate rustc_ast_pretty;
diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs
index 3f1adc787b79..424ca2485d57 100644
--- a/library/kani/src/arbitrary.rs
+++ b/library/kani/src/arbitrary.rs
@@ -71,6 +71,10 @@ trivial_arbitrary!(isize);
 trivial_arbitrary!(f32);
 trivial_arbitrary!(f64);
 
+// Similarly, we do not constraint values for non-standard floating types.
+trivial_arbitrary!(f16);
+trivial_arbitrary!(f128);
+
 trivial_arbitrary!(());
 
 impl Arbitrary for bool {
diff --git a/library/kani/src/invariant.rs b/library/kani/src/invariant.rs
index f118f94e995c..068cdedc277e 100644
--- a/library/kani/src/invariant.rs
+++ b/library/kani/src/invariant.rs
@@ -96,6 +96,8 @@ trivial_invariant!(isize);
 // invariant that checks for NaN, infinite, or subnormal values.
 trivial_invariant!(f32);
 trivial_invariant!(f64);
+trivial_invariant!(f16);
+trivial_invariant!(f128);
 
 trivial_invariant!(());
 trivial_invariant!(bool);
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index acf1e08e0441..0a52a9516398 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -18,6 +18,8 @@
 #![allow(internal_features)]
 // Required for implementing memory predicates.
 #![feature(ptr_metadata)]
+#![feature(f16)]
+#![feature(f128)]
 
 pub mod arbitrary;
 #[cfg(feature = "concrete_playback")]
diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs
index d202df4ead1d..a8271ad758cf 100644
--- a/library/kani_core/src/arbitrary.rs
+++ b/library/kani_core/src/arbitrary.rs
@@ -88,6 +88,15 @@ macro_rules! generate_arbitrary {
         trivial_arbitrary!(i128);
         trivial_arbitrary!(isize);
 
+        // We do not constrain floating points values per type spec. Users must add assumptions to their
+        // verification code if they want to eliminate NaN, infinite, or subnormal.
+        trivial_arbitrary!(f32);
+        trivial_arbitrary!(f64);
+
+        // Similarly, we do not constraint values for non-standard floating types.
+        trivial_arbitrary!(f16);
+        trivial_arbitrary!(f128);
+
         nonzero_arbitrary!(NonZeroU8, u8);
         nonzero_arbitrary!(NonZeroU16, u16);
         nonzero_arbitrary!(NonZeroU32, u32);
diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index de808ffaf918..143fbb7ef825 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -17,6 +17,8 @@
 
 #![feature(no_core)]
 #![no_core]
+#![feature(f16)]
+#![feature(f128)]
 
 mod arbitrary;
 mod mem;
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index c620752b423a..5f02b82a51d2 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-06-27"
+channel = "nightly-2024-06-28"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/expected/arbitrary/floats/non_standard_floats/expected b/tests/expected/arbitrary/floats/non_standard_floats/expected
new file mode 100644
index 000000000000..26db615201a6
--- /dev/null
+++ b/tests/expected/arbitrary/floats/non_standard_floats/expected
@@ -0,0 +1,31 @@
+Checking harness check_f128...
+
+Status: SATISFIED\
+Description: "This may be true"\
+in function check_f128
+
+Status: SATISFIED\
+Description: "This may also be true"\
+in function check_f128
+
+Status: SATISFIED\
+Description: "NaN should be valid float"\
+in function check_f128
+
+Checking harness check_f16...
+
+Status: SATISFIED\
+Description: "This may be true"\
+in function check_f16
+
+Status: SATISFIED\
+Description: "This may also be true"\
+in function check_f16
+
+Status: SATISFIED\
+Description: "NaN should be valid float"\
+in function check_f16
+
+VERIFICATION:- SUCCESSFUL
+
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.
diff --git a/tests/expected/arbitrary/floats/non_standard_floats/main.rs b/tests/expected/arbitrary/floats/non_standard_floats/main.rs
new file mode 100644
index 000000000000..ebea6535b3d5
--- /dev/null
+++ b/tests/expected/arbitrary/floats/non_standard_floats/main.rs
@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Ensure that kani::any and kani::any_raw can be used with non-standard floats i.e f16 and f128.
+
+#![feature(f16)]
+#![feature(f128)]
+
+macro_rules! test_non_standard_floats {
+    ( $type: ty ) => {{
+        let v1 = kani::any::<$type>();
+        let v2 = kani::any::<$type>();
+        kani::cover!(v1 == v2, "This may be true");
+        kani::cover!(v1 != v2, "This may also be true");
+        kani::cover!(v1.is_nan(), "NaN should be valid float");
+    }};
+}
+
+#[kani::proof]
+fn check_f16() {
+    test_non_standard_floats!(f16);
+}
+
+#[kani::proof]
+fn check_f128() {
+    test_non_standard_floats!(f128);
+}
diff --git a/tests/expected/arbitrary/floats/expected b/tests/expected/arbitrary/floats/standard_floats/expected
similarity index 99%
rename from tests/expected/arbitrary/floats/expected
rename to tests/expected/arbitrary/floats/standard_floats/expected
index 4bb2fadacd7f..de3b67f28578 100644
--- a/tests/expected/arbitrary/floats/expected
+++ b/tests/expected/arbitrary/floats/standard_floats/expected
@@ -51,10 +51,8 @@ Status: SATISFIED\
 Description: "Non-finite numbers are valid float"\
 in function check_f32
 
-
  ** 6 of 6 cover properties satisfied
 
-
 VERIFICATION:- SUCCESSFUL
 
 Complete - 2 successfully verified harnesses, 0 failures, 2 total.
diff --git a/tests/expected/arbitrary/floats/main.rs b/tests/expected/arbitrary/floats/standard_floats/main.rs
similarity index 74%
rename from tests/expected/arbitrary/floats/main.rs
rename to tests/expected/arbitrary/floats/standard_floats/main.rs
index 1ad4de3ef3f7..c204643e9ab8 100644
--- a/tests/expected/arbitrary/floats/main.rs
+++ b/tests/expected/arbitrary/floats/standard_floats/main.rs
@@ -1,9 +1,12 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// Ensure that kani::any and kani::any_raw can be used with floats.
+// Ensure that kani::any and kani::any_raw can be used with standard floats i.e f32 and f64.
 
-macro_rules! test {
+#![feature(f16)]
+#![feature(f128)]
+
+macro_rules! test_standard_floats {
     ( $type: ty ) => {{
         let v1 = kani::any::<$type>();
         let v2 = kani::any::<$type>();
@@ -18,10 +21,10 @@ macro_rules! test {
 
 #[kani::proof]
 fn check_f32() {
-    test!(f32);
+    test_standard_floats!(f32);
 }
 
 #[kani::proof]
 fn check_f64() {
-    test!(f64);
+    test_standard_floats!(f64);
 }
diff --git a/tests/kani/FloatingPoint/main.rs b/tests/kani/FloatingPoint/main.rs
index c04bd9b305f8..f8ebccdac02a 100644
--- a/tests/kani/FloatingPoint/main.rs
+++ b/tests/kani/FloatingPoint/main.rs
@@ -1,5 +1,9 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#![feature(f16)]
+#![feature(f128)]
+
 macro_rules! test_floats {
     ($ty:ty) => {
         let a: $ty = kani::any();
@@ -26,6 +30,8 @@ fn main() {
     assert!(1.1 == 1.1 * 1.0);
     assert!(1.1 != 1.11 / 1.0);
 
+    test_floats!(f16);
     test_floats!(f32);
     test_floats!(f64);
+    test_floats!(f128);
 }
diff --git a/tests/kani/Invariant/invariant_impls.rs b/tests/kani/Invariant/invariant_impls.rs
index 4f00f4134956..146c9731370d 100644
--- a/tests/kani/Invariant/invariant_impls.rs
+++ b/tests/kani/Invariant/invariant_impls.rs
@@ -3,6 +3,10 @@
 
 //! Check the `Invariant` implementations that we include in the Kani library
 //! with respect to the underlying type invariants.
+
+#![feature(f16)]
+#![feature(f128)]
+
 extern crate kani;
 use kani::Invariant;
 
@@ -29,6 +33,9 @@ fn check_safe_impls() {
     check_safe_type!(i128);
     check_safe_type!(isize);
 
+    check_safe_type!(f16);
+    check_safe_type!(f128);
+
     check_safe_type!(f32);
     check_safe_type!(f64);