diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs
index 69596b99262..68f739e3785 100644
--- a/kani-compiler/src/kani_middle/transform/contracts.rs
+++ b/kani-compiler/src/kani_middle/transform/contracts.rs
@@ -302,6 +302,9 @@ impl TransformPass for FunctionWithContractPass {
         match instance.ty().kind().rigid().unwrap() {
             RigidTy::FnDef(def, args) => {
                 if let Some(mode) = self.contract_mode(tcx, *def) {
+                    if mode == ContractMode::RecursiveCheck {
+                        check_mutual_recursion(tcx, *def, &body);
+                    }
                     self.mark_unused(tcx, *def, &body, mode);
                     let new_body = self.set_mode(tcx, body, mode);
                     (true, new_body)
@@ -552,3 +555,76 @@ fn find_closure(tcx: TyCtxt, fn_def: FnDef, body: &Body, name: &str) -> ClosureD
             unreachable!()
         })
 }
+
+/// Check if a function with `#[kani::recursion]` is involved in mutual recursion.
+///
+/// Scans the function's MIR body for calls to other functions that also have
+/// `#[kani::recursion]`. For each such callee, checks if the callee's body calls
+/// back to the original function (one level of indirection). If so, emits a
+/// warning because the per-function REENTRY mechanism only handles direct
+/// recursion soundly.
+///
+/// We require both `has_contract()` and `has_recursion()` on the callee because
+/// if the callee has a contract but no `#[kani::recursion]`, Kani replaces the
+/// callee with its contract abstraction — no mutual recursion occurs.
+///
+/// Limitations:
+/// - Only detects one level of indirection (f→g→f), not deeper chains (f→g→h→f).
+/// - Reports only the first mutual-recursive callee per function.
+fn check_mutual_recursion(tcx: TyCtxt, fn_def: FnDef, body: &Body) {
+    let fn_name = tcx.item_name(rustc_internal::internal(tcx, fn_def.def_id()));
+    let locals = body.locals().to_vec();
+
+    for bb in body.blocks.iter() {
+        let TerminatorKind::Call { func, .. } = &bb.terminator.kind else { continue };
+        let Ok(func_ty) = func.ty(&locals) else { continue };
+        let TyKind::RigidTy(RigidTy::FnDef(callee_def, callee_args)) = func_ty.kind() else {
+            continue;
+        };
+
+        // Skip direct recursion (that's handled correctly by REENTRY).
+        if callee_def.def_id() == fn_def.def_id() {
+            continue;
+        }
+
+        // Only warn when the callee also uses #[kani::recursion] with a contract.
+        // If the callee has a contract but no #[kani::recursion], Kani replaces
+        // the call with the contract abstraction, so no mutual recursion occurs.
+        let callee_attrs = KaniAttributes::for_def_id(tcx, callee_def.def_id());
+        if !callee_attrs.has_contract() || !callee_attrs.has_recursion() {
+            continue;
+        }
+
+        // Check if the callee calls back to us (one level deep).
+        let Ok(callee_instance) = Instance::resolve(callee_def, &callee_args) else { continue };
+        let Some(callee_body) = callee_instance.body() else { continue };
+        let callee_locals = callee_body.locals().to_vec();
+
+        for callee_bb in callee_body.blocks.iter() {
+            let TerminatorKind::Call { func: callee_func, .. } = &callee_bb.terminator.kind else {
+                continue;
+            };
+            let Ok(callee_func_ty) = callee_func.ty(&callee_locals) else { continue };
+            let TyKind::RigidTy(RigidTy::FnDef(transitive_def, _)) = callee_func_ty.kind() else {
+                continue;
+            };
+
+            if transitive_def.def_id() == fn_def.def_id() {
+                let callee_name = tcx.item_name(rustc_internal::internal(tcx, callee_def.def_id()));
+                let span = rustc_internal::internal(tcx, bb.terminator.span);
+                tcx.dcx().span_warn(
+                    span,
+                    format!(
+                        "`#[kani::recursion]` is used on `{fn_name}`, which calls \
+                         `{callee_name}` that calls back to `{fn_name}`. \
+                         Mutual recursion is not supported by contract verification \
+                         and may produce unsound results. Only direct recursion \
+                         (a function calling itself) is handled correctly."
+                    ),
+                );
+                // LIMITATION: Only report the first mutual-recursive callee.
+                return;
+            }
+        }
+    }
+}
diff --git a/tests/expected/function-contract/mutual_recursion_unsound.expected b/tests/expected/function-contract/mutual_recursion_unsound.expected
new file mode 100644
index 00000000000..24d40888f34
--- /dev/null
+++ b/tests/expected/function-contract/mutual_recursion_unsound.expected
@@ -0,0 +1 @@
+`#[kani::recursion]` is used on `mutual_a`, which calls `mutual_b` that calls back to `mutual_a`. Mutual recursion is not supported by contract verification and may produce unsound results. Only direct recursion (a function calling itself) is handled correctly.
diff --git a/tests/expected/function-contract/mutual_recursion_unsound.rs b/tests/expected/function-contract/mutual_recursion_unsound.rs
new file mode 100644
index 00000000000..6a8f73bb268
--- /dev/null
+++ b/tests/expected/function-contract/mutual_recursion_unsound.rs
@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+//! Test that Kani detects mutual recursion in functions with contracts and
+//! emits a warning about unsoundness.
+
+#[kani::requires(x < 100)]
+#[kani::ensures(|&result| result <= x)]
+#[kani::recursion]
+fn mutual_a(x: u32) -> u32 {
+    if x == 0 { 0 } else { mutual_b(x - 1) }
+}
+
+#[kani::requires(x < 100)]
+#[kani::ensures(|&result| result <= x)]
+#[kani::recursion]
+fn mutual_b(x: u32) -> u32 {
+    if x == 0 { 0 } else { mutual_a(x - 1) }
+}
+
+#[kani::proof_for_contract(mutual_a)]
+fn check_mutual_a() {
+    let x: u32 = kani::any();
+    mutual_a(x);
+}