diff --git a/prusti-contracts/prusti-specs/src/extern_spec_rewriter/common.rs b/prusti-contracts/prusti-specs/src/extern_spec_rewriter/common.rs
index d1276f2db76..481da8d340b 100644
--- a/prusti-contracts/prusti-specs/src/extern_spec_rewriter/common.rs
+++ b/prusti-contracts/prusti-specs/src/extern_spec_rewriter/common.rs
@@ -145,7 +145,7 @@ pub(crate) fn generate_extern_spec_method_stub<T: HasSignature + HasAttributes +
 
     // Build the method stub
     let stub_method =
-        generate_extern_spec_function_stub(method, &method_path, extern_spec_kind, false);
+        generate_extern_spec_function_stub(method, &method_path, extern_spec_kind, false, false);
     let stub_method: syn::ImplItemMethod = syn::parse2(stub_method)?;
 
     // Eagerly extract and process specifications
@@ -191,6 +191,7 @@ pub(crate) fn generate_extern_spec_function_stub<Input: HasSignature + HasAttrib
     fn_path: &syn::ExprPath,
     extern_spec_kind: ExternSpecKind,
     mangle_name: bool,
+    is_unsafe: bool,
 ) -> TokenStream {
     let signature = function.sig();
     let mut signature = with_explicit_lifetimes(signature).unwrap_or_else(|| signature.clone());
@@ -202,6 +203,12 @@ pub(crate) fn generate_extern_spec_function_stub<Input: HasSignature + HasAttrib
     let generic_params = &signature.generic_params_as_call_args();
     let args = &signature.params_as_call_args();
     let extern_spec_kind_string: String = extern_spec_kind.into();
+    let fn_call = quote! { #fn_path :: < #generic_params > ( #args ) };
+    let stub_body = if is_unsafe {
+        quote! { unsafe { #fn_call } }
+    } else {
+        quote! { #fn_call }
+    };
 
     quote_spanned! {function.span()=>
         #[trusted]
@@ -209,29 +216,11 @@ pub(crate) fn generate_extern_spec_function_stub<Input: HasSignature + HasAttrib
         #(#attrs)*
         #[allow(unused, dead_code)]
         #signature {
-            #fn_path :: < #generic_params > ( #args )
+            #stub_body
         }
     }
 }
 
-pub(crate) fn generate_extern_spec_foreign_function_stub<Input: HasSignature + HasAttributes + Spanned, Output: syn::parse::Parse>(
-    function: &Input,
-    extern_spec_kind: ExternSpecKind,
-) -> Output {
-    let signature = function.sig();
-    // Make elided lifetimes explicit, if necessary.
-    let signature = with_explicit_lifetimes(signature).unwrap_or_else(|| signature.clone());
-    let attrs: Vec<syn::Attribute> = function.attrs().clone();
-    let extern_spec_kind_string: String = extern_spec_kind.into();
-    
-    parse_quote_spanned! {function.span()=>
-        #[trusted]
-        #[prusti::extern_spec = #extern_spec_kind_string]
-        #(#attrs)*
-        #signature;
-    }
-}
-
 /// Given a method signature with parameters, this function returns all typed parameters
 /// as they were used as arguments for the function call.
 /// # Example
diff --git a/prusti-contracts/prusti-specs/src/extern_spec_rewriter/foreign_mods.rs b/prusti-contracts/prusti-specs/src/extern_spec_rewriter/foreign_mods.rs
index cbd75e15bb7..ab9e835eebf 100644
--- a/prusti-contracts/prusti-specs/src/extern_spec_rewriter/foreign_mods.rs
+++ b/prusti-contracts/prusti-specs/src/extern_spec_rewriter/foreign_mods.rs
@@ -1,37 +1,25 @@
 //! Process external specifications in Rust foreign modules marked with
 //! the #[extern_spec] attribute.
 
-use super::common::generate_extern_spec_foreign_function_stub;
-use crate::{
-    extract_prusti_attributes, generate_spec_and_assertions, specifications::untyped::AnyFnItem,
-    ExternSpecKind,
-};
+use super::functions::rewrite_stub;
 use proc_macro2::TokenStream;
-use quote::{quote, ToTokens};
+use quote::ToTokens;
+use syn::spanned::Spanned;
 
-pub fn rewrite_extern_spec(item_foreign_mod: &mut syn::ItemForeignMod) -> syn::Result<TokenStream> {
-    let mut specs = vec![];
-    for item in item_foreign_mod.items.iter_mut() {
-        if let syn::ForeignItem::Fn(item_fn) = item {
-            specs.extend(rewrite_fn(item_fn)?);
+pub fn rewrite_extern_spec(
+    item_foreign_mod: &syn::ItemForeignMod,
+    path: &syn::Path,
+) -> syn::Result<TokenStream> {
+    let mut res = TokenStream::new();
+    for item in item_foreign_mod.items.iter() {
+        match item {
+            syn::ForeignItem::Fn(item_fn) => {
+                let tokens = rewrite_stub(&item_fn.to_token_stream(), path, true);
+                res.extend(tokens);
+            }
+            // eventually: handle specs for foreign variables (statics)
+            _ => return Err(syn::Error::new(item.span(), "unexpected item")),
         }
-        // eventually: handle specs for foreign variables
     }
-
-    let mut res = TokenStream::new();
-    res.extend(specs.iter().map(syn::Item::to_token_stream));
-    res.extend(quote!(#item_foreign_mod));
     Ok(res)
 }
-
-fn rewrite_fn(item_fn: &mut syn::ForeignItemFn) -> Result<Vec<syn::Item>, syn::Error> {
-    let stub_fn: syn::ForeignItemFn =
-        generate_extern_spec_foreign_function_stub(item_fn, ExternSpecKind::Method);
-    let mut stub_fn = AnyFnItem::ForeignFn(stub_fn);
-    let prusti_attributes = extract_prusti_attributes(&mut stub_fn);
-    let (spec_items, generated_attributes) =
-        generate_spec_and_assertions(prusti_attributes, &stub_fn)?;
-    stub_fn.attrs_mut().extend(generated_attributes);
-    *item_fn = stub_fn.expect_foreign_item_fn();
-    Ok(spec_items)
-}
diff --git a/prusti-contracts/prusti-specs/src/extern_spec_rewriter/functions.rs b/prusti-contracts/prusti-specs/src/extern_spec_rewriter/functions.rs
index 0df7ef84aa3..c5c18764672 100644
--- a/prusti-contracts/prusti-specs/src/extern_spec_rewriter/functions.rs
+++ b/prusti-contracts/prusti-specs/src/extern_spec_rewriter/functions.rs
@@ -8,7 +8,11 @@ use proc_macro2::{Group, TokenStream, TokenTree};
 use quote::{quote, ToTokens};
 use syn::{parse_quote_spanned, spanned::Spanned};
 
-pub fn rewrite_stub(stub_tokens: &TokenStream, path: &syn::Path) -> syn::Result<TokenStream> {
+pub fn rewrite_stub(
+    stub_tokens: &TokenStream,
+    path: &syn::Path,
+    is_unsafe: bool,
+) -> syn::Result<TokenStream> {
     // Transforms function stubs (functions with a `;` after the
     // signature instead of the body) into functions, then
     // processes them.
@@ -34,7 +38,7 @@ pub fn rewrite_stub(stub_tokens: &TokenStream, path: &syn::Path) -> syn::Result<
 
     let mut item = res.unwrap();
     if let syn::Item::Fn(item_fn) = &mut item {
-        Ok(rewrite_fn(item_fn, path))
+        Ok(rewrite_fn(item_fn, path, is_unsafe))
     } else {
         Ok(quote!(#item))
     }
@@ -42,10 +46,10 @@ pub fn rewrite_stub(stub_tokens: &TokenStream, path: &syn::Path) -> syn::Result<
 
 /// Rewrite a specification function to a call to the specified function.
 /// The result of this rewriting is then parsed in `ExternSpecResolver`.
-pub fn rewrite_fn(item_fn: &syn::ItemFn, path: &syn::Path) -> TokenStream {
+pub fn rewrite_fn(item_fn: &syn::ItemFn, path: &syn::Path, is_unsafe: bool) -> TokenStream {
     let ident = &item_fn.sig.ident;
     let path_span = item_fn.sig.ident.span();
     let path = parse_quote_spanned!(path_span=> #path :: #ident);
 
-    generate_extern_spec_function_stub(item_fn, &path, ExternSpecKind::Method, true)
+    generate_extern_spec_function_stub(item_fn, &path, ExternSpecKind::Method, true, is_unsafe)
 }
diff --git a/prusti-contracts/prusti-specs/src/extern_spec_rewriter/mods.rs b/prusti-contracts/prusti-specs/src/extern_spec_rewriter/mods.rs
index b9c9ee3029c..05e998dd9bd 100644
--- a/prusti-contracts/prusti-specs/src/extern_spec_rewriter/mods.rs
+++ b/prusti-contracts/prusti-specs/src/extern_spec_rewriter/mods.rs
@@ -23,10 +23,10 @@ pub fn rewrite_mod(item_mod: &syn::ItemMod, mut path: syn::Path) -> syn::Result<
         match item {
             syn::Item::Fn(ref item_fn) => {
                 check_is_stub(&item_fn.block)?;
-                rewritten_fns.extend(rewrite_fn(item_fn, &path));
+                rewritten_fns.extend(rewrite_fn(item_fn, &path, false));
             }
             syn::Item::Mod(ref inner_mod) => rewritten_fns.extend(rewrite_mod(inner_mod, path.clone())?),
-            syn::Item::Verbatim(ref tokens) => rewritten_fns.extend(rewrite_stub(tokens, &path)?),
+            syn::Item::Verbatim(ref tokens) => rewritten_fns.extend(rewrite_stub(tokens, &path, false)?),
             syn::Item::Use(_) => rewritten_fns.extend(syn::Error::new(
                 item.span(),
                 "`use` statements have no effect in #[extern_spec] modules; module contents share the outer scope.",
diff --git a/prusti-contracts/prusti-specs/src/lib.rs b/prusti-contracts/prusti-specs/src/lib.rs
index e60490cf028..16330a4c57c 100644
--- a/prusti-contracts/prusti-specs/src/lib.rs
+++ b/prusti-contracts/prusti-specs/src/lib.rs
@@ -780,11 +780,14 @@ pub fn extern_spec(attr: TokenStream, tokens: TokenStream) -> TokenStream {
                 extern_spec_rewriter::mods::rewrite_mod(&item_mod, mod_path)
             }
             syn::Item::ForeignMod(item_foreign_mod) => {
-                extern_spec_rewriter::foreign_mods::rewrite_extern_spec(&item_foreign_mod)
+                extern_spec_rewriter::foreign_mods::rewrite_extern_spec(
+                    &item_foreign_mod,
+                    &mod_path,
+                )
             }
             // we're expecting function stubs, so they aren't represented as Item::Fn
             syn::Item::Verbatim(stub_tokens) => {
-                extern_spec_rewriter::functions::rewrite_stub(&stub_tokens, &mod_path)
+                extern_spec_rewriter::functions::rewrite_stub(&stub_tokens, &mod_path, false)
             }
             _ => Err(syn::Error::new(
                 Span::call_site(), // this covers the entire macro invocation, unlike attr.span() which changes to only cover arguments if possible
diff --git a/prusti-contracts/prusti-specs/src/specifications/untyped.rs b/prusti-contracts/prusti-specs/src/specifications/untyped.rs
index dcc5f067f2b..851ec94f050 100644
--- a/prusti-contracts/prusti-specs/src/specifications/untyped.rs
+++ b/prusti-contracts/prusti-specs/src/specifications/untyped.rs
@@ -71,7 +71,7 @@ impl AnyFnItem {
             _ => unreachable!(),
         }
     }
-    
+
     pub fn expect_foreign_item_fn(self) -> syn::ForeignItemFn {
         match self {
             AnyFnItem::ForeignFn(f) => f,
diff --git a/prusti-interface/src/specs/mod.rs b/prusti-interface/src/specs/mod.rs
index 86e50f79fa6..25b70c57e22 100644
--- a/prusti-interface/src/specs/mod.rs
+++ b/prusti-interface/src/specs/mod.rs
@@ -436,20 +436,6 @@ impl<'a, 'tcx> intravisit::Visitor<'tcx> for SpecCollector<'a, 'tcx> {
         self.env.query.hir()
     }
 
-    fn visit_foreign_item(&mut self, fi: &'tcx prusti_rustc_interface::hir::ForeignItem) {
-        intravisit::walk_foreign_item(self, fi);
-
-        let id = fi.hir_id();
-        let local_id = self.env.query.as_local_def_id(id);
-        let def_id = local_id.to_def_id();
-        let attrs = self.env.query.get_local_attributes(fi.owner_id.def_id);
-
-        // Collect procedure specifications
-        if let Some(procedure_spec_ref) = get_procedure_spec_ids(def_id, attrs) {
-            self.procedure_specs.insert(local_id, procedure_spec_ref);
-        }
-    }
-
     fn visit_trait_item(&mut self, ti: &'tcx prusti_rustc_interface::hir::TraitItem) {
         intravisit::walk_trait_item(self, ti);
 
diff --git a/prusti-tests/tests/cargo_verify/foreign_mods/Cargo.toml b/prusti-tests/tests/cargo_verify/foreign_mods/Cargo.toml
new file mode 100644
index 00000000000..bad5c5102ce
--- /dev/null
+++ b/prusti-tests/tests/cargo_verify/foreign_mods/Cargo.toml
@@ -0,0 +1,14 @@
+[package]
+name = "foreign_mods"
+version = "0.1.0"
+edition = "2021"
+build = "build.rs"
+
+[dependencies]
+prusti-contracts = { path = "prusti-contracts/prusti-contracts" } # The test suite will prepare a symbolic link for this
+
+[build-dependencies]
+cc = "1.0"
+
+# Declare that this crate is not part of a workspace
+[workspace]
diff --git a/prusti-tests/tests/cargo_verify/foreign_mods/build.rs b/prusti-tests/tests/cargo_verify/foreign_mods/build.rs
new file mode 100644
index 00000000000..d661bf98ca1
--- /dev/null
+++ b/prusti-tests/tests/cargo_verify/foreign_mods/build.rs
@@ -0,0 +1,5 @@
+fn main() {
+    cc::Build::new()
+        .file("src/clib.c")
+        .compile("clib");
+}
diff --git a/prusti-tests/tests/cargo_verify/foreign_mods/src/clib.c b/prusti-tests/tests/cargo_verify/foreign_mods/src/clib.c
new file mode 100644
index 00000000000..86624fd01e1
--- /dev/null
+++ b/prusti-tests/tests/cargo_verify/foreign_mods/src/clib.c
@@ -0,0 +1,12 @@
+#include <stdint.h>
+
+int32_t max(int32_t a, int32_t b) {
+	return a > b ? a : b;
+}
+
+void unannotated(void) {
+}
+
+int32_t abs(int32_t a) {
+	return a >= 0 ? a : -a;
+}
diff --git a/prusti-tests/tests/parse/pass/extern-spec/foreign_mods.rs b/prusti-tests/tests/cargo_verify/foreign_mods/src/main.rs
similarity index 80%
rename from prusti-tests/tests/parse/pass/extern-spec/foreign_mods.rs
rename to prusti-tests/tests/cargo_verify/foreign_mods/src/main.rs
index cefb3196f55..d1c37753bf1 100644
--- a/prusti-tests/tests/parse/pass/extern-spec/foreign_mods.rs
+++ b/prusti-tests/tests/cargo_verify/foreign_mods/src/main.rs
@@ -1,6 +1,14 @@
 use prusti_contracts::*;
 
-#[extern_spec]
+extern "C" {
+    fn max(a: i32, b: i32) -> i32;
+
+    fn unannotated();
+
+    fn abs(a: i32) -> i32;
+}
+
+#[extern_spec(crate)]
 extern "C" {
     #[ensures(a >= b ==> result == a)]
     #[ensures(b >= a ==> result == b)]
diff --git a/prusti-tests/tests/cargotest.rs b/prusti-tests/tests/cargotest.rs
index 3992d4a9c77..19d9f1c9a9c 100644
--- a/prusti-tests/tests/cargotest.rs
+++ b/prusti-tests/tests/cargotest.rs
@@ -185,6 +185,11 @@ fn test_failing_stable_toolchain() {
     test_local_project("failing_stable_toolchain");
 }
 
+#[cargo_test]
+fn test_foreign_mods() {
+    test_local_project("foreign_mods");
+}
+
 #[cargo_test]
 fn test_library_contracts_test() {
     test_local_project("library_contracts_test");
diff --git a/prusti-tests/tests/parse/fail/extern-spec/on-function.rs b/prusti-tests/tests/parse/fail/extern-spec/on-function.rs
new file mode 100644
index 00000000000..ee02feaab92
--- /dev/null
+++ b/prusti-tests/tests/parse/fail/extern-spec/on-function.rs
@@ -0,0 +1,11 @@
+use prusti_contracts::*;
+
+fn identity(a: i32) -> i32 {
+    a
+}
+
+#[extern_spec] // should be #[extern_spec(crate)] in this case
+#[ensures(a == 0 ==> result == 0)]
+fn identity(a: i32) -> i32; //~ ERROR: cannot find crate `identity` in the list of imported crates
+
+fn main() {}
diff --git a/prusti-tests/tests/parse/ui/foreign_mods.rs b/prusti-tests/tests/parse/ui/foreign_mods.rs
index 97413afe99e..e4cb5b3c454 100644
--- a/prusti-tests/tests/parse/ui/foreign_mods.rs
+++ b/prusti-tests/tests/parse/ui/foreign_mods.rs
@@ -1,6 +1,14 @@
 use prusti_contracts::*;
 
-#[extern_spec]
+extern "C" {
+    fn max(a: i32, b: i32) -> i32;
+
+    fn unannotated();
+
+    fn abs(a: i32) -> i32;
+}
+
+#[extern_spec(crate)]
 extern "C" {
     #[ensures(a >= b ==> result = a)]
     #[ensures(b >= a ==> result == b)]
diff --git a/prusti-tests/tests/parse/ui/foreign_mods.stderr b/prusti-tests/tests/parse/ui/foreign_mods.stderr
index d8ff43fc2ca..0e0f69d86c2 100644
--- a/prusti-tests/tests/parse/ui/foreign_mods.stderr
+++ b/prusti-tests/tests/parse/ui/foreign_mods.stderr
@@ -1,35 +1,39 @@
 error[E0308]: mismatched types
- --> $DIR/foreign_mods.rs:5:26
-  |
-5 |     #[ensures(a >= b ==> result = a)]
-  |                          ^^^^^^ expected `bool`, found `i32`
+  --> $DIR/foreign_mods.rs:13:26
+   |
+13 |     #[ensures(a >= b ==> result = a)]
+   |               ------     ^^^^^^ expected `bool`, found `i32`
+   |               |
+   |               expected because this is `bool`
 
 error[E0308]: mismatched types
- --> $DIR/foreign_mods.rs:5:22
-  |
-5 |     #[ensures(a >= b ==> result = a)]
-  |                      ^^^^^^^^^^^^^^ expected `bool`, found `()`
-  |
+  --> $DIR/foreign_mods.rs:13:15
+   |
+13 |     #[ensures(a >= b ==> result = a)]
+   |               ^^^^^^^^^^^^^^^^^^^^^ expected `bool`, found `()`
+   |
 help: you might have meant to compare for equality
-  |
-5 |     #[ensures(a >= b ==> result == a)]
-  |                                  +
+   |
+13 |     #[ensures(a >= b ==> result == a)]
+   |                                  +
 
 error[E0308]: mismatched types
-  --> $DIR/foreign_mods.rs:12:26
+  --> $DIR/foreign_mods.rs:20:26
    |
-12 |     #[ensures(a >= 0 ==> result = a)]
-   |                          ^^^^^^ expected `bool`, found `i32`
+20 |     #[ensures(a >= 0 ==> result = a)]
+   |               ------     ^^^^^^ expected `bool`, found `i32`
+   |               |
+   |               expected because this is `bool`
 
 error[E0308]: mismatched types
-  --> $DIR/foreign_mods.rs:12:22
+  --> $DIR/foreign_mods.rs:20:15
    |
-12 |     #[ensures(a >= 0 ==> result = a)]
-   |                      ^^^^^^^^^^^^^^ expected `bool`, found `()`
+20 |     #[ensures(a >= 0 ==> result = a)]
+   |               ^^^^^^^^^^^^^^^^^^^^^ expected `bool`, found `()`
    |
 help: you might have meant to compare for equality
    |
-12 |     #[ensures(a >= 0 ==> result == a)]
+20 |     #[ensures(a >= 0 ==> result == a)]
    |                                  +
 
 error: aborting due to 4 previous errors