diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index dea7cca60844..2267af56a684 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -470,6 +470,22 @@ impl MirVisitor for MonoItemsFnCollector<'_, '_> {
 
         self.super_terminator(terminator, location);
     }
+
+    /// Collect any function definition that may occur as a type.
+    ///
+    /// The codegen stage will require the definition to be available.
+    /// This is a conservative approach, since there are cases where the function is never
+    /// actually used, so we don't need the body.
+    ///
+    /// Another alternative would be to lazily declare functions, but it would require a bigger
+    /// change to codegen.
+    fn visit_ty(&mut self, ty: &Ty, _: Location) {
+        if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = ty.kind() {
+            let instance = Instance::resolve(def, &args).unwrap();
+            self.collect_instance(instance, true);
+        }
+        self.super_ty(ty);
+    }
 }
 
 fn extract_unsize_coercion(tcx: TyCtxt, orig_ty: Ty, dst_trait: Ty) -> (Ty, Ty) {
diff --git a/tests/kani/CodegenMisc/missing_mut_fn.rs b/tests/kani/CodegenMisc/missing_mut_fn.rs
new file mode 100644
index 000000000000..ae7bfe753bf0
--- /dev/null
+++ b/tests/kani/CodegenMisc/missing_mut_fn.rs
@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Ensure Kani can codegen code with a pointer to a function that is never used
+//! See <https://github.com/model-checking/kani/issues/3799> for more details.
+fn foo<F: Fn()>(_func: &mut F) {}
+fn foo_dyn(_func: &mut dyn Fn()) {}
+
+#[kani::proof]
+fn check_foo() {
+    fn f() {}
+
+    foo(&mut f);
+}
+
+#[kani::proof]
+fn check_foo_dyn() {
+    fn f() {}
+
+    foo_dyn(&mut f);
+}
+
+#[kani::proof]
+fn check_foo_unused() {
+    fn f() {}
+
+    let ptr = &mut f;
+}