diff --git a/.github/workflows/audit.yml b/.github/workflows/audit.yml
index 3ae9d192f376..5b75d6162c85 100644
--- a/.github/workflows/audit.yml
+++ b/.github/workflows/audit.yml
@@ -7,6 +7,7 @@
 name: Cargo Audit
 on:
   pull_request:
+  merge_group:
   push:
     # Run on changes to branches but not tags.
     branches:
diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml
index 5ab7dcb1b9c3..cc13306a4eaf 100644
--- a/.github/workflows/format-check.yml
+++ b/.github/workflows/format-check.yml
@@ -3,6 +3,7 @@
 name: Kani Format Check
 on:
   pull_request:
+  merge_group:
   push:
     # Not just any push, as that includes tags.
     # We don't want to re-trigger this workflow when tagging an existing commit.
diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index dd077eff25e1..a565c9cd4cbe 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -3,6 +3,7 @@
 name: Kani CI
 on:
   pull_request:
+  merge_group:
   push:
     # Not just any push, as that includes tags.
     # We don't want to re-trigger this workflow when tagging an existing commit.
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 72ef4e2de889..ad2e339f19e1 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -8,6 +8,7 @@
 name: Release Bundle
 on:
   pull_request:
+  merge_group:
   push:
     branches:
       - 'main'
diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md
index 501a9952f05e..ce3c9fc1b7a2 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 | |
@@ -187,8 +187,8 @@ nontemporal_store | No | |
 offset | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-2) |
 powf32 | Partial | Results are overapproximated |
 powf64 | Partial | Results are overapproximated |
-powif32 | No | |
-powif64 | No | |
+powif32 | Partial | Results are overapproximated |
+powif64 | Partial | Results are overapproximated |
 pref_align_of | Yes | |
 prefetch_read_data | No | |
 prefetch_read_instruction | No | |
@@ -211,8 +211,8 @@ sinf32 | Partial | Results are overapproximated; [this test](https://github.com/
 sinf64 | Partial | Results are overapproximated; [this test](https://github.com/model-checking/kani/blob/main/tests/kani/Intrinsics/Math/Trigonometry/sinf64.rs) explains how |
 size_of | Yes | |
 size_of_val | Yes | |
-sqrtf32 | No | |
-sqrtf64 | No | |
+sqrtf32 | Partial | Results are overapproximated |
+sqrtf64 | Partial | Results are overapproximated |
 sub_with_overflow | Yes | |
 transmute | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/nomicon/transmutes.html) |
 truncf32 | Yes | |
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 12352190e6e2..c4d5396f1fe8 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);
@@ -490,8 +490,8 @@ impl<'tcx> GotocCtx<'tcx> {
             ),
             "powf32" => codegen_simple_intrinsic!(Powf),
             "powf64" => codegen_simple_intrinsic!(Pow),
-            "powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)),
-            "powif64" => unstable_codegen!(codegen_simple_intrinsic!(Powi)),
+            "powif32" => codegen_simple_intrinsic!(Powif),
+            "powif64" => codegen_simple_intrinsic!(Powi),
             "pref_align_of" => codegen_intrinsic_const!(),
             "ptr_guaranteed_cmp" => self.codegen_ptr_guaranteed_cmp(fargs, place, loc),
             "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, place, loc),
@@ -570,8 +570,8 @@ impl<'tcx> GotocCtx<'tcx> {
             "simd_xor" => codegen_intrinsic_binop!(bitxor),
             "size_of" => unreachable!(),
             "size_of_val" => codegen_size_align!(size),
-            "sqrtf32" => unstable_codegen!(codegen_simple_intrinsic!(Sqrtf)),
-            "sqrtf64" => unstable_codegen!(codegen_simple_intrinsic!(Sqrt)),
+            "sqrtf32" => codegen_simple_intrinsic!(Sqrtf),
+            "sqrtf64" => codegen_simple_intrinsic!(Sqrt),
             "sub_with_overflow" => self.codegen_op_with_overflow(
                 BinaryOperator::OverflowResultMinus,
                 fargs,
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 8753157827b5..0c0e9e9f196c 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-08-01"
+channel = "nightly-2024-08-02"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/kani/Cast/cast_abstract_args_to_concrete_fixme2.rs b/tests/kani/Cast/cast_abstract_args_to_concrete.rs
similarity index 92%
rename from tests/kani/Cast/cast_abstract_args_to_concrete_fixme2.rs
rename to tests/kani/Cast/cast_abstract_args_to_concrete.rs
index 51067e0e0a73..6694f799493a 100644
--- a/tests/kani/Cast/cast_abstract_args_to_concrete_fixme2.rs
+++ b/tests/kani/Cast/cast_abstract_args_to_concrete.rs
@@ -1,9 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// https://github.com/model-checking/kani/issues/555
-// kani-flags: --no-undefined-function-checks
-
 // This regression test is in response to issue #135.
 // The type of the second parameter to powi is a `CInteger`, but
 // the type of `2` here is a `u32`. This test ensures that
diff --git a/tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs b/tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs
deleted file mode 100644
index faeb74c5d66a..000000000000
--- a/tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs
+++ /dev/null
@@ -1,24 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-//! This test is a modified version of cast_abstract_args_to_concrete_fixme.rs.
-//! The original test requires --no-undefined-function-checks to pass. This is an issue that
-//! require investigation. See https://github.com/model-checking/kani/issues/555.
-//!
-//! Once this issue is fixed. Please remove this test and remove the kani flag from the original
-//! test: --no-undefined-function-check
-
-fn main() {
-    let _x32 = 1.0f32.powi(2);
-    let _x64 = 1.0f64.powi(2);
-
-    unsafe {
-        let size: libc::size_t = mem::size_of::<i32>();
-        let my_num: *mut libc::c_void = libc::malloc(size);
-        if my_num.is_null() {
-            panic!("failed to allocate memory");
-        }
-        let my_num2 = libc::memset(my_num, 1, size);
-        libc::free(my_num);
-    }
-}
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);
+}
diff --git a/tests/kani/Intrinsics/Math/Arith/powi.rs b/tests/kani/Intrinsics/Math/Arith/powi.rs
new file mode 100644
index 000000000000..c7986d18a9ef
--- /dev/null
+++ b/tests/kani/Intrinsics/Math/Arith/powi.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn verify_powi32() {
+    let x: f32 = kani::any();
+    kani::assume(x.is_normal());
+    kani::assume(x >= 1e-19 || x <= -1e-19);
+    kani::assume(x <= 1.84e19 && x >= -1.84e19);
+    let x2 = x.powi(2);
+    assert!(x2 >= 0.0);
+}
+
+#[kani::proof]
+fn verify_powi64() {
+    let x: f64 = kani::any();
+    kani::assume(x.is_normal());
+    kani::assume(x >= 1e-153 || x <= -1e-153);
+    kani::assume(x <= 1.34e154 && x >= -1.34e154);
+    let x2 = x.powi(2);
+    assert!(x2 >= 0.0);
+}
diff --git a/tests/kani/Intrinsics/Math/Arith/sqrt.rs b/tests/kani/Intrinsics/Math/Arith/sqrt.rs
new file mode 100644
index 000000000000..31afaba8a740
--- /dev/null
+++ b/tests/kani/Intrinsics/Math/Arith/sqrt.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn verify_sqrt32() {
+    let positive = 4.0_f32;
+    let negative_zero = -0.0_f32;
+
+    let abs_difference = (positive.sqrt() - 2.0).abs();
+
+    assert!(abs_difference <= f32::EPSILON);
+    assert!(negative_zero.sqrt() == negative_zero);
+}
+
+#[kani::proof]
+fn verify_sqrt64() {
+    let positive = 4.0_f64;
+    let negative_zero = -0.0_f64;
+
+    let abs_difference = (positive.sqrt() - 2.0).abs();
+
+    assert!(abs_difference <= 1e-10);
+    assert!(negative_zero.sqrt() == negative_zero);
+}