diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs
index ba4ff7a911f6..a332b9973bb8 100644
--- a/kani_metadata/src/unstable.rs
+++ b/kani_metadata/src/unstable.rs
@@ -99,6 +99,8 @@ pub enum UnstableFeature {
     /// Allow replacing certain items with stubs (mocks).
     /// See [RFC-0002](https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html)
     Stubbing,
+    /// Enable quantifiers [RFC 10](https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html)
+    Quantifiers,
     /// Automatically check that uninitialized memory is not used.
     UninitChecks,
     /// Enable an unstable option or subcommand.
diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index fcff99c32f80..8d2f0c6605d6 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -627,6 +627,11 @@ macro_rules! kani_intrinsics {
                 assert!(cond, "{}", msg);
             }
 
+            #[crate::kani::unstable_feature(
+                feature = "quantifiers",
+                issue = 2546,
+                reason = "experimental quantifiers"
+            )]
             #[inline(never)]
             #[kanitool::fn_marker = "ForallHook"]
             pub fn kani_forall<T, F>(lower_bound: T, upper_bound: T, predicate: F) -> bool
@@ -636,6 +641,11 @@ macro_rules! kani_intrinsics {
                 predicate(lower_bound)
             }
 
+            #[crate::kani::unstable_feature(
+                feature = "quantifiers",
+                issue = 2546,
+                reason = "experimental quantifiers"
+            )]
             #[inline(never)]
             #[kanitool::fn_marker = "ExistsHook"]
             pub fn kani_exists<T, F>(lower_bound: T, upper_bound: T, predicate: F) -> bool
diff --git a/tests/expected/quantifiers/assert_with_exists_fail.rs b/tests/expected/quantifiers/assert_with_exists_fail.rs
index 3e2c6cdb3781..20a2aa8934b0 100644
--- a/tests/expected/quantifiers/assert_with_exists_fail.rs
+++ b/tests/expected/quantifiers/assert_with_exists_fail.rs
@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
 
 #[kani::proof]
 fn exists_assert_harness() {
diff --git a/tests/expected/quantifiers/assert_with_exists_pass.rs b/tests/expected/quantifiers/assert_with_exists_pass.rs
index 7d43d6117729..c364a968610c 100644
--- a/tests/expected/quantifiers/assert_with_exists_pass.rs
+++ b/tests/expected/quantifiers/assert_with_exists_pass.rs
@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
 
 #[kani::proof]
 fn exists_assert_harness() {
diff --git a/tests/expected/quantifiers/assert_with_forall_fail.rs b/tests/expected/quantifiers/assert_with_forall_fail.rs
index c9bb7bbf62dd..ec2cab5c4e98 100644
--- a/tests/expected/quantifiers/assert_with_forall_fail.rs
+++ b/tests/expected/quantifiers/assert_with_forall_fail.rs
@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
 
 #[kani::proof]
 fn forall_assert_harness() {
diff --git a/tests/expected/quantifiers/assert_with_forall_pass.rs b/tests/expected/quantifiers/assert_with_forall_pass.rs
index 5ebf73e7c0ee..1ba7d93053ff 100644
--- a/tests/expected/quantifiers/assert_with_forall_pass.rs
+++ b/tests/expected/quantifiers/assert_with_forall_pass.rs
@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
 
 #[kani::proof]
 fn forall_assert_harness() {
diff --git a/tests/expected/quantifiers/assume_with_exists_fail.rs b/tests/expected/quantifiers/assume_with_exists_fail.rs
index f6df36a6942d..0148ac991304 100644
--- a/tests/expected/quantifiers/assume_with_exists_fail.rs
+++ b/tests/expected/quantifiers/assume_with_exists_fail.rs
@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
 
 #[kani::proof]
 fn exists_assume_harness() {
diff --git a/tests/expected/quantifiers/contracts_fail.rs b/tests/expected/quantifiers/contracts_fail.rs
index a1b87ebc8633..022188f46d95 100644
--- a/tests/expected/quantifiers/contracts_fail.rs
+++ b/tests/expected/quantifiers/contracts_fail.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Z quantifiers
 
 /// Copy only first 7 elements and left the last one unchanged.
 #[kani::ensures(|ret| { unsafe{
diff --git a/tests/expected/quantifiers/quantifier_with_no_external_variable.rs b/tests/expected/quantifiers/quantifier_with_no_external_variable.rs
index dabf4d9f2137..f0c8a84362b7 100644
--- a/tests/expected/quantifiers/quantifier_with_no_external_variable.rs
+++ b/tests/expected/quantifiers/quantifier_with_no_external_variable.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-
+// kani-flags: -Z quantifiers
 /// Quantifier with no external variable in the closure
 
 #[kani::proof]
diff --git a/tests/kani/Quantifiers/array.rs b/tests/kani/Quantifiers/array.rs
index b59eccd614fb..b077d53fd6da 100644
--- a/tests/kani/Quantifiers/array.rs
+++ b/tests/kani/Quantifiers/array.rs
@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
 
 #[kani::proof]
 fn vec_assert_forall_harness() {
diff --git a/tests/kani/Quantifiers/contracts.rs b/tests/kani/Quantifiers/contracts.rs
index d8e36c194774..7df87d2996b9 100644
--- a/tests/kani/Quantifiers/contracts.rs
+++ b/tests/kani/Quantifiers/contracts.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zquantifiers
 
 #[kani::requires(i==0)]
 #[kani::ensures(|ret| {
diff --git a/tests/kani/Quantifiers/even.rs b/tests/kani/Quantifiers/even.rs
index e7f74440d85a..0fd369446baf 100644
--- a/tests/kani/Quantifiers/even.rs
+++ b/tests/kani/Quantifiers/even.rs
@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
 
 #[kani::proof]
 fn quantifier_even_harness() {
diff --git a/tests/kani/Quantifiers/from_raw_part_fixme.rs b/tests/kani/Quantifiers/from_raw_part_fixme.rs
index 2f06161847bf..88a711e963d1 100644
--- a/tests/kani/Quantifiers/from_raw_part_fixme.rs
+++ b/tests/kani/Quantifiers/from_raw_part_fixme.rs
@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
 
 //! FIXME: <https://github.com/model-checking/kani/issues/4020>
 
diff --git a/tests/kani/Quantifiers/no_array.rs b/tests/kani/Quantifiers/no_array.rs
index 9681e4ccf0fa..802dda296d64 100644
--- a/tests/kani/Quantifiers/no_array.rs
+++ b/tests/kani/Quantifiers/no_array.rs
@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
 
 #[kani::proof]
 fn forall_assert_harness() {