diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md
index f97db5d8ab6c..77392cd37fc6 100644
--- a/docs/src/rust-feature-support/intrinsics.md
+++ b/docs/src/rust-feature-support/intrinsics.md
@@ -159,8 +159,8 @@ fdiv_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809)
 float_to_int_unchecked | No | |
 floorf32 | Yes | |
 floorf64 | Yes | |
-fmaf32 | No | |
-fmaf64 | No | |
+fmaf32 | Partial | Results are overapproximated |
+fmaf64 | Partial | Results are overapproximated |
 fmul_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809) |
 forget | Yes | |
 frem_fast | No | |
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 91f7ea20c9b1..8f93a4c61553 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -447,8 +447,8 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             "floorf32" => codegen_simple_intrinsic!(Floorf),
             "floorf64" => codegen_simple_intrinsic!(Floor),
-            "fmaf32" => unstable_codegen!(codegen_simple_intrinsic!(Fmaf)),
-            "fmaf64" => unstable_codegen!(codegen_simple_intrinsic!(Fma)),
+            "fmaf32" => codegen_simple_intrinsic!(Fmaf),
+            "fmaf64" => codegen_simple_intrinsic!(Fma),
             "fmul_fast" => {
                 let fargs_clone = fargs.clone();
                 let binop_stmt = codegen_intrinsic_binop!(mul);
diff --git a/tests/kani/Intrinsics/Math/Arith/fma.rs b/tests/kani/Intrinsics/Math/Arith/fma.rs
new file mode 100644
index 000000000000..379d5aa81db5
--- /dev/null
+++ b/tests/kani/Intrinsics/Math/Arith/fma.rs
@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn verify_fma_32() {
+    let m = 10.0_f32;
+    let x = 4.0_f32;
+    let b = 60.0_f32;
+
+    // 100.0
+    let abs_difference = (m.mul_add(x, b) - ((m * x) + b)).abs();
+
+    assert!(abs_difference <= f32::EPSILON);
+}
+
+#[kani::proof]
+fn verify_fma_64() {
+    let m = 10.0_f64;
+    let x = 4.0_f64;
+    let b = 60.0_f64;
+
+    // 100.0
+    let abs_difference = (m.mul_add(x, b) - ((m * x) + b)).abs();
+
+    assert!(abs_difference < 1e-10);
+}