diff --git a/tests/ui/fail/mod_annot.rs b/tests/ui/fail/mod_annot.rs
new file mode 100644
index 00000000..0d66fc1b
--- /dev/null
+++ b/tests/ui/fail/mod_annot.rs
@@ -0,0 +1,18 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+mod math {
+    #[thrust_macros::requires(true)]
+    #[thrust_macros::ensures(result >= a)]
+    pub fn max(a: i64, b: i64) -> i64 {
+        if a >= b {
+            a
+        } else {
+            b
+        }
+    }
+}
+
+fn main() {
+    assert!(math::max(1, 2) >= 2);
+}
diff --git a/tests/ui/fail/mod_invariant.rs b/tests/ui/fail/mod_invariant.rs
new file mode 100644
index 00000000..3d5b43a8
--- /dev/null
+++ b/tests/ui/fail/mod_invariant.rs
@@ -0,0 +1,17 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+mod counter {
+    pub fn count_to(n: i64) -> i64 {
+        let mut i = 0_i64;
+        while i < n {
+            thrust_macros::invariant!(|i: i64| i >= 1);
+            i += 1;
+        }
+        i
+    }
+}
+
+fn main() {
+    assert!(counter::count_to(3) >= 0);
+}
diff --git a/tests/ui/pass/mod_annot.rs b/tests/ui/pass/mod_annot.rs
new file mode 100644
index 00000000..67616d33
--- /dev/null
+++ b/tests/ui/pass/mod_annot.rs
@@ -0,0 +1,18 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+mod math {
+    #[thrust_macros::requires(true)]
+    #[thrust_macros::ensures(result >= a && result >= b)]
+    pub fn max(a: i64, b: i64) -> i64 {
+        if a >= b {
+            a
+        } else {
+            b
+        }
+    }
+}
+
+fn main() {
+    assert!(math::max(1, 2) >= 2);
+}
diff --git a/tests/ui/pass/mod_invariant.rs b/tests/ui/pass/mod_invariant.rs
new file mode 100644
index 00000000..fc7a9063
--- /dev/null
+++ b/tests/ui/pass/mod_invariant.rs
@@ -0,0 +1,17 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+mod counter {
+    pub fn count_to(n: i64) -> i64 {
+        let mut i = 0_i64;
+        while i < n {
+            thrust_macros::invariant!(|i: i64| i >= 0);
+            i += 1;
+        }
+        i
+    }
+}
+
+fn main() {
+    assert!(counter::count_to(3) >= 0);
+}
diff --git a/thrust-macros/src/formula.rs b/thrust-macros/src/formula.rs
index f2112c82..77dfb06c 100644
--- a/thrust-macros/src/formula.rs
+++ b/thrust-macros/src/formula.rs
@@ -104,7 +104,7 @@ pub fn expand(input: TokenStream) -> TokenStream {
     };
 
     // Rewrites each assignment `lhs = rhs` (produced by [`desugar_arrows`] from
-    // `lhs ==> rhs`) into `thrust_models::implies(lhs, rhs)`. Visiting
+    // `lhs ==> rhs`) into `crate::thrust_models::implies(lhs, rhs)`. Visiting
     // post-order means nested implications are rewritten innermost-first, so the
     // right-associative chain `a ==> b ==> c` becomes `implies(a, implies(b, c))`.
     struct ImplicationRewriter;
@@ -115,7 +115,7 @@ pub fn expand(input: TokenStream) -> TokenStream {
             if let syn::Expr::Assign(assign) = expr {
                 let left = &assign.left;
                 let right = &assign.right;
-                *expr = syn::parse_quote!(thrust_models::implies((#left), (#right)));
+                *expr = syn::parse_quote!(crate::thrust_models::implies((#left), (#right)));
             }
         }
     }
@@ -215,22 +215,22 @@ mod tests {
     fn desugars_implication() {
         assert_eq!(
             expand_expr("a ==> b"),
-            expect("thrust_models::implies((a), (b))")
+            expect("crate::thrust_models::implies((a), (b))")
         );
         // right-associative
         assert_eq!(
             expand_expr("a ==> b ==> c"),
-            expect("thrust_models::implies((a), (thrust_models::implies((b), (c))))")
+            expect("crate::thrust_models::implies((a), (crate::thrust_models::implies((b), (c))))")
         );
         // lower precedence than `||` and `==`
         assert_eq!(
             expand_expr("a || b ==> c == d"),
-            expect("thrust_models::implies((a || b), (c == d))")
+            expect("crate::thrust_models::implies((a || b), (c == d))")
         );
         // nested inside a closure argument
         assert_eq!(
             expand_expr("exists(|x| a ==> b)"),
-            expect("exists(|x| thrust_models::implies((a), (b)))")
+            expect("exists(|x| crate::thrust_models::implies((a), (b)))")
         );
     }
 
diff --git a/thrust-macros/src/formula_fn_type_lowering.rs b/thrust-macros/src/formula_fn_type_lowering.rs
index 4c992ab6..19743a1b 100644
--- a/thrust-macros/src/formula_fn_type_lowering.rs
+++ b/thrust-macros/src/formula_fn_type_lowering.rs
@@ -35,12 +35,12 @@ impl<'a> FormulaFnTypeLowering<'a> {
         }
     }
 
-    /// Maps each function parameter `x: T` to `x: <T as thrust_models::Model>::Ty`.
+    /// Maps each function parameter `x: T` to `x: <T as crate::thrust_models::Model>::Ty`.
     ///
     /// Closure/function type parameters are first rewritten to
-    /// `thrust_models::model::Closure<F>`, including when nested in references such as `&mut F`, so
-    /// specifications can refer to the modeled closure environment while marker functions can still
-    /// recover the instantiated closure definition from `F`.
+    /// `crate::thrust_models::model::Closure<F>`, including when nested in references such as
+    /// `&mut F`, so specifications can refer to the modeled closure environment while marker
+    /// functions can still recover the instantiated closure definition from `F`.
     pub fn lower_params<'ast, I>(&self, args: I) -> TokenStream2
     where
         I: IntoIterator<Item = &'ast syn::FnArg>,
@@ -50,14 +50,16 @@ impl<'a> FormulaFnTypeLowering<'a> {
             match arg {
                 syn::FnArg::Receiver(receiver) => {
                     let ty = crate::receiver_type(receiver);
-                    model_inputs.push(syn::parse_quote!(self_: <#ty as thrust_models::Model>::Ty));
+                    model_inputs
+                        .push(syn::parse_quote!(self_: <#ty as crate::thrust_models::Model>::Ty));
                 }
                 syn::FnArg::Typed(pt) => {
                     let pat = &pt.pat;
                     let ty = &pt.ty;
                     let lowered_ty = self.lower_closure_type_params_in_ty(ty);
-                    model_inputs
-                        .push(syn::parse_quote!(#pat: <#lowered_ty as thrust_models::Model>::Ty));
+                    model_inputs.push(
+                        syn::parse_quote!(#pat: <#lowered_ty as crate::thrust_models::Model>::Ty),
+                    );
                 }
             }
         }
@@ -66,10 +68,10 @@ impl<'a> FormulaFnTypeLowering<'a> {
 
     pub fn lower_return_type(&self, ret: &syn::ReturnType) -> syn::Type {
         match ret {
-            syn::ReturnType::Default => syn::parse_quote!(<() as thrust_models::Model>::Ty),
+            syn::ReturnType::Default => syn::parse_quote!(<() as crate::thrust_models::Model>::Ty),
             syn::ReturnType::Type(_, ty) => {
                 let lowered_ty = self.lower_closure_type_params_in_ty(ty);
-                syn::parse_quote!(<#lowered_ty as thrust_models::Model>::Ty)
+                syn::parse_quote!(<#lowered_ty as crate::thrust_models::Model>::Ty)
             }
         }
     }
@@ -176,7 +178,7 @@ impl<'a> FormulaFnTypeLowering<'a> {
                         .get_ident()
                         .is_some_and(|ident| self.closure_type_params.contains(ident)) =>
             {
-                syn::parse_quote!(thrust_models::model::Closure<#ty>)
+                syn::parse_quote!(crate::thrust_models::model::Closure<#ty>)
             }
             syn::Type::Reference(tr) => {
                 let mut tr = tr.clone();
@@ -251,7 +253,7 @@ fn collect_closure_type_params(generics: &syn::Generics, result: &mut HashSet<sy
 
 fn model_predicates(ty: &impl quote::ToTokens) -> [syn::WherePredicate; 2] {
     [
-        syn::parse_quote!(#ty: thrust_models::Model),
-        syn::parse_quote!(<#ty as thrust_models::Model>::Ty: PartialEq),
+        syn::parse_quote!(#ty: crate::thrust_models::Model),
+        syn::parse_quote!(<#ty as crate::thrust_models::Model>::Ty: PartialEq),
     ]
 }
diff --git a/thrust-macros/src/ghost.rs b/thrust-macros/src/ghost.rs
index 794b173d..5fb99262 100644
--- a/thrust-macros/src/ghost.rs
+++ b/thrust-macros/src/ghost.rs
@@ -63,6 +63,6 @@ fn expand_ghost(closure: &syn::ExprClosure) -> syn::Result<syn::Expr> {
             #value == (#body)
         }
 
-        thrust_models::__ghost_marker::<_, #value_ty>(#name)
+        crate::thrust_models::__ghost_marker::<_, #value_ty>(#name)
     }))
 }
diff --git a/thrust-macros/src/invariant.rs b/thrust-macros/src/invariant.rs
index 9c519aa8..233ad141 100644
--- a/thrust-macros/src/invariant.rs
+++ b/thrust-macros/src/invariant.rs
@@ -280,7 +280,7 @@ fn expand_invariant(
             #body
         }
 
-        thrust_models::__invariant_marker(#name #turbofish)
+        crate::thrust_models::__invariant_marker(#name #turbofish)
     }))
 }
 
diff --git a/thrust-macros/src/pre_post.rs b/thrust-macros/src/pre_post.rs
index 5302e5d2..f8c7a8fd 100644
--- a/thrust-macros/src/pre_post.rs
+++ b/thrust-macros/src/pre_post.rs
@@ -18,7 +18,7 @@ pub fn expand_pre(input: TokenStream) -> TokenStream {
     let call = syn::parse_macro_input!(input as syn::ExprCall);
     let func = &*call.func;
     let args = call_args_tuple(&call.args);
-    quote::quote!(thrust_models::model::closure_precondition(#func, #args)).into()
+    quote::quote!(crate::thrust_models::model::closure_precondition(#func, #args)).into()
 }
 
 pub fn expand_post(input: TokenStream) -> TokenStream {
@@ -43,5 +43,5 @@ pub fn expand_post(input: TokenStream) -> TokenStream {
     };
     let func = &*call.func;
     let args = call_args_tuple(&call.args);
-    quote::quote!(thrust_models::model::closure_postcondition(#func, #args, #result)).into()
+    quote::quote!(crate::thrust_models::model::closure_postcondition(#func, #args, #result)).into()
 }
diff --git a/thrust-macros/src/rty.rs b/thrust-macros/src/rty.rs
index 93a49f55..5cf2ce18 100644
--- a/thrust-macros/src/rty.rs
+++ b/thrust-macros/src/rty.rs
@@ -448,7 +448,7 @@ fn build_formula_fn(
         #[allow(non_snake_case)]
         #[thrust::formula_fn]
         fn #name #def_generics(
-            #binder: <#binder_ty as thrust_models::Model>::Ty,
+            #binder: <#binder_ty as crate::thrust_models::Model>::Ty,
             #model_params
         ) -> bool #extended_where {
             #formula