diff --git a/tests/ui/fail/closure_ensures_only.rs b/tests/ui/fail/closure_ensures_only.rs
new file mode 100644
index 00000000..7ec22b2c
--- /dev/null
+++ b/tests/ui/fail/closure_ensures_only.rs
@@ -0,0 +1,20 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+// The declared postcondition `result > x` hides the body's exact result, so `r == 4`
+// is not provable. Were the postcondition inferred instead, it would be exact and the
+// assertion would hold.
+#[thrust_macros::requires(thrust_macros::pre!(f(x)))]
+#[thrust_macros::ensures(thrust_macros::post!(f(x), result))]
+fn apply<F: FnOnce(i32) -> i32>(x: i32, f: F) -> i32 {
+    f(x)
+}
+
+fn main() {
+    let f = thrust_macros::closure!(
+        ensures(result > x),
+        |x: i32| -> i32 { x + 1 },
+    );
+    let r = apply(3, f);
+    assert!(r == 4);
+}
diff --git a/tests/ui/fail/closure_requires_ensures.rs b/tests/ui/fail/closure_requires_ensures.rs
new file mode 100644
index 00000000..e9f79ae2
--- /dev/null
+++ b/tests/ui/fail/closure_requires_ensures.rs
@@ -0,0 +1,21 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+// The declared postcondition `result > x` hides the body's exact result, so `r == 4`
+// is not provable. Were the postcondition inferred instead, it would be exact and the
+// assertion would hold.
+#[thrust_macros::requires(thrust_macros::pre!(f(x)))]
+#[thrust_macros::ensures(thrust_macros::post!(f(x), result))]
+fn apply<F: FnOnce(i32) -> i32>(x: i32, f: F) -> i32 {
+    f(x)
+}
+
+fn main() {
+    let f = thrust_macros::closure!(
+        requires(x > 0),
+        ensures(result > x),
+        |x: i32| -> i32 { x + 1 },
+    );
+    let r = apply(3, f);
+    assert!(r == 4);
+}
diff --git a/tests/ui/fail/closure_requires_only.rs b/tests/ui/fail/closure_requires_only.rs
new file mode 100644
index 00000000..8aa8bcad
--- /dev/null
+++ b/tests/ui/fail/closure_requires_only.rs
@@ -0,0 +1,19 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+
+// `-1` violates the declared precondition `x > 0`. Were the precondition inferred
+// instead, it would be weak enough to admit the call.
+#[thrust_macros::requires(thrust_macros::pre!(f(x)))]
+#[thrust_macros::ensures(thrust_macros::post!(f(x), result))]
+fn apply<F: FnOnce(i32) -> i32>(x: i32, f: F) -> i32 {
+    f(x)
+}
+
+fn main() {
+    let f = thrust_macros::closure!(
+        requires(x > 0),
+        |x: i32| -> i32 { x + 1 },
+    );
+    let r = apply(-1, f);
+    assert!(r == 0);
+}
diff --git a/tests/ui/pass/closure_ensures_only.rs b/tests/ui/pass/closure_ensures_only.rs
new file mode 100644
index 00000000..83e5e8b5
--- /dev/null
+++ b/tests/ui/pass/closure_ensures_only.rs
@@ -0,0 +1,19 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+// A closure that declares only `ensures`; its precondition stays inferred as a
+// predicate variable, so the caller has nothing to establish.
+#[thrust_macros::requires(thrust_macros::pre!(f(x)))]
+#[thrust_macros::ensures(thrust_macros::post!(f(x), result))]
+fn apply<F: FnOnce(i32) -> i32>(x: i32, f: F) -> i32 {
+    f(x)
+}
+
+fn main() {
+    let f = thrust_macros::closure!(
+        ensures(result > x),
+        |x: i32| -> i32 { x + 1 },
+    );
+    let r = apply(3, f);
+    assert!(r > 3);
+}
diff --git a/tests/ui/pass/closure_requires_ensures.rs b/tests/ui/pass/closure_requires_ensures.rs
new file mode 100644
index 00000000..a0d9118a
--- /dev/null
+++ b/tests/ui/pass/closure_requires_ensures.rs
@@ -0,0 +1,20 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+// The declared postcondition `result > x` is weaker than what the body computes, and
+// the caller sees only the declared one.
+#[thrust_macros::requires(thrust_macros::pre!(f(x)))]
+#[thrust_macros::ensures(thrust_macros::post!(f(x), result))]
+fn apply<F: FnOnce(i32) -> i32>(x: i32, f: F) -> i32 {
+    f(x)
+}
+
+fn main() {
+    let f = thrust_macros::closure!(
+        requires(x > 0),
+        ensures(result > x),
+        |x: i32| -> i32 { x + 1 },
+    );
+    let r = apply(3, f);
+    assert!(r > 3);
+}
diff --git a/tests/ui/pass/closure_requires_only.rs b/tests/ui/pass/closure_requires_only.rs
new file mode 100644
index 00000000..eeea3067
--- /dev/null
+++ b/tests/ui/pass/closure_requires_only.rs
@@ -0,0 +1,19 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+
+// A closure that declares only `requires`; its postcondition stays inferred as a
+// predicate variable, so the caller still learns the body's exact result.
+#[thrust_macros::requires(thrust_macros::pre!(f(x)))]
+#[thrust_macros::ensures(thrust_macros::post!(f(x), result))]
+fn apply<F: FnOnce(i32) -> i32>(x: i32, f: F) -> i32 {
+    f(x)
+}
+
+fn main() {
+    let f = thrust_macros::closure!(
+        requires(x > 0),
+        |x: i32| -> i32 { x + 1 },
+    );
+    let r = apply(3, f);
+    assert!(r == 4);
+}
diff --git a/thrust-macros/src/closure.rs b/thrust-macros/src/closure.rs
new file mode 100644
index 00000000..9c154544
--- /dev/null
+++ b/thrust-macros/src/closure.rs
@@ -0,0 +1,175 @@
+//! Expansion of `thrust_macros::closure!`, which attaches an explicit
+//! `requires`/`ensures` specification to a closure expression.
+//!
+//! ```ignore
+//! let f = thrust_macros::closure!(
+//!     requires(x > 0),
+//!     ensures(result > x),
+//!     |x: i32| -> i32 { x + 1 },
+//! );
+//! ```
+//!
+//! Rust attributes cannot sit on a closure expression, so the clauses are written
+//! inside the macro. The expansion prepends `#[thrust::formula_fn]` companions and
+//! `#[thrust::requires_path]` / `#[thrust::ensures_path]` path statements to the
+//! closure body — the markers the plugin already reads for named `fn` specs (see
+//! `spec.rs`). Each clause is optional (an omitted one leaves that side inferred)
+//! and may be repeated, in which case its predicates are conjoined.
+//!
+//! A clause sees no threaded generic or `Self` context, so a closure in a generic
+//! context cannot refer to generic- or `Self`-typed values.
+
+use proc_macro::TokenStream;
+use proc_macro2::TokenStream as TokenStream2;
+use quote::{quote, ToTokens};
+use syn::{
+    parenthesized,
+    parse::{Parse, ParseStream},
+    FnArg,
+};
+
+use crate::FormulaFnTypeLowering;
+
+mod kw {
+    syn::custom_keyword!(requires);
+    syn::custom_keyword!(ensures);
+}
+
+struct ClosureSpec {
+    requires: Vec<TokenStream2>,
+    ensures: Vec<TokenStream2>,
+    closure: syn::ExprClosure,
+}
+
+impl Parse for ClosureSpec {
+    fn parse(input: ParseStream) -> syn::Result<Self> {
+        let mut requires = Vec::new();
+        let mut ensures = Vec::new();
+
+        loop {
+            let clause = if input.peek(kw::requires) {
+                input.parse::<kw::requires>()?;
+                &mut requires
+            } else if input.peek(kw::ensures) {
+                input.parse::<kw::ensures>()?;
+                &mut ensures
+            } else {
+                break;
+            };
+            let content;
+            parenthesized!(content in input);
+            clause.push(content.parse()?);
+            input.parse::<Option<syn::Token![,]>>()?;
+        }
+
+        let closure: syn::ExprClosure = input.parse()?;
+        input.parse::<Option<syn::Token![,]>>()?;
+
+        Ok(Self {
+            requires,
+            ensures,
+            closure,
+        })
+    }
+}
+
+pub fn expand(input: TokenStream) -> TokenStream {
+    let spec = match syn::parse::<ClosureSpec>(input) {
+        Ok(spec) => spec,
+        Err(e) => return e.to_compile_error().into(),
+    };
+    match expand_closure(spec) {
+        Ok(expr) => expr.into_token_stream().into(),
+        Err(e) => e.to_compile_error().into(),
+    }
+}
+
+fn expand_closure(spec: ClosureSpec) -> syn::Result<syn::ExprClosure> {
+    let ClosureSpec {
+        requires,
+        ensures,
+        mut closure,
+    } = spec;
+
+    // A closure's parameters are `[env, arg1, .., argN]`, the environment being the
+    // closure value itself. A clause names only the arguments, so the companions take
+    // a dummy parameter in the environment's place to keep the positions aligned.
+    let mut fn_params: Vec<FnArg> = vec![syn::parse_quote!(_thrust_closure_env: ())];
+    for param in &closure.inputs {
+        let syn::Pat::Type(pt) = param else {
+            return Err(syn::Error::new_spanned(
+                param,
+                "closure! requires explicitly typed closure parameters, e.g. `|x: i32| ...`",
+            ));
+        };
+        let pat = &pt.pat;
+        let ty = &pt.ty;
+        fn_params.push(syn::parse_quote!(#pat: #ty));
+    }
+
+    if !ensures.is_empty() && matches!(closure.output, syn::ReturnType::Default) {
+        return Err(syn::Error::new_spanned(
+            &closure,
+            "closure! with `ensures` requires an explicit return type, e.g. `|x: i32| -> i32 { .. }`",
+        ));
+    }
+
+    // The lowering reads generics off a signature to spot `Fn`-bounded type params; a
+    // clause has none of its own.
+    let spec_sig: syn::Signature = syn::parse_quote!(fn closure_spec());
+    let type_lowering = FormulaFnTypeLowering::new(&spec_sig);
+    let model_params = type_lowering.lower_params(&fn_params);
+
+    let mut prelude: Vec<TokenStream2> = Vec::new();
+    if let Some(body) = conjoin(requires) {
+        prelude.push(quote! {
+            #[allow(unused_variables, non_snake_case)]
+            #[thrust::formula_fn]
+            fn _thrust_closure_requires(#model_params) -> bool {
+                #body
+            }
+
+            #[thrust::requires_path]
+            _thrust_closure_requires;
+        });
+    }
+    if let Some(body) = conjoin(ensures) {
+        let ret_model = type_lowering.lower_return_type(&closure.output);
+        prelude.push(quote! {
+            #[allow(unused_variables, non_snake_case)]
+            #[thrust::formula_fn]
+            fn _thrust_closure_ensures(result: #ret_model, #model_params) -> bool {
+                #body
+            }
+
+            #[thrust::ensures_path]
+            _thrust_closure_ensures;
+        });
+    }
+
+    // Splice into the body's own block rather than nesting it inside a new one, which
+    // would warn `unused_braces`. A block carrying a label or attributes has to stay
+    // whole, so it becomes the tail expression of the new block instead.
+    let body_stmts = match *closure.body {
+        syn::Expr::Block(ref block) if block.attrs.is_empty() && block.label.is_none() => {
+            block.block.stmts.clone()
+        }
+        ref body => vec![syn::Stmt::Expr(body.clone(), None)],
+    };
+    closure.body = Box::new(syn::parse_quote!({
+        #(#prelude)*
+        #(#body_stmts)*
+    }));
+
+    Ok(closure)
+}
+
+fn conjoin(preds: Vec<TokenStream2>) -> Option<TokenStream2> {
+    preds
+        .into_iter()
+        .map(|pred| {
+            let pred = crate::formula::expand(pred);
+            quote!((#pred))
+        })
+        .reduce(|acc, pred| quote!(#acc && #pred))
+}
diff --git a/thrust-macros/src/lib.rs b/thrust-macros/src/lib.rs
index 429be63a..ddda2388 100644
--- a/thrust-macros/src/lib.rs
+++ b/thrust-macros/src/lib.rs
@@ -1,6 +1,7 @@
 use proc_macro::TokenStream;
 use proc_macro2::{TokenStream as TokenStream2, TokenTree as TokenTree2};
 
+mod closure;
 mod context;
 mod fn_outer_item;
 mod formula;
@@ -28,6 +29,15 @@ pub fn post(input: TokenStream) -> TokenStream {
     pre_post::expand_post(input)
 }
 
+/// `closure!(requires(..), ensures(..), |x: T| -> R { .. })` attaches an
+/// explicit pre-/post-condition to a closure expression. Each clause is optional
+/// (omitting one leaves that side inferred) and may be repeated (conjoined).
+/// See [`mod@closure`].
+#[proc_macro]
+pub fn closure(input: TokenStream) -> TokenStream {
+    closure::expand(input)
+}
+
 #[proc_macro_attribute]
 pub fn context(_attr: TokenStream, item: TokenStream) -> TokenStream {
     context::expand(item)