diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs
index 4e99590fc6a3..a7aaa8ae334e 100644
--- a/library/kani_macros/src/derive.rs
+++ b/library/kani_macros/src/derive.rs
@@ -28,11 +28,30 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok
     let (impl_generics, ty_generics, where_clause) = generics.split_for_impl();
 
     let body = fn_any_body(&item_name, &derive_item.data);
-    let expanded = quote! {
-        // The generated implementation.
-        impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause {
-            fn any() -> Self {
-                #body
+
+    // Get the safety constraints (if any) to produce type-safe values
+    let safety_conds_opt = safety_conds(&item_name, &derive_item.data);
+
+    let expanded = if let Some(safety_cond) = safety_conds_opt {
+        let field_refs = field_refs(&item_name, &derive_item.data);
+        quote! {
+            // The generated implementation.
+            impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause {
+                fn any() -> Self {
+                    let obj = #body;
+                    #field_refs
+                    kani::assume(#safety_cond);
+                    obj
+                }
+            }
+        }
+    } else {
+        quote! {
+            // The generated implementation.
+            impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause {
+                fn any() -> Self {
+                    #body
+                }
             }
         }
     };
@@ -75,6 +94,103 @@ fn fn_any_body(ident: &Ident, data: &Data) -> TokenStream {
     }
 }
 
+/// Parse the condition expressions in `#[safety_constraint(<cond>)]` attached to struct
+/// fields and, it at least one was found, generate a conjunction to be assumed.
+///
+/// For example, if we're deriving implementations for the struct
+/// ```
+/// #[derive(Arbitrary)]
+/// #[derive(Invariant)]
+/// struct PositivePoint {
+///     #[safety_constraint(*x >= 0)]
+///     x: i32,
+///     #[safety_constraint(*y >= 0)]
+///     y: i32,
+/// }
+/// ```
+/// this function will generate the `TokenStream`
+/// ```
+/// *x >= 0 && *y >= 0
+/// ```
+/// which can be passed to `kani::assume` to constrain the values generated
+/// through the `Arbitrary` impl so that they are type-safe by construction.
+fn safety_conds(ident: &Ident, data: &Data) -> Option<TokenStream> {
+    match data {
+        Data::Struct(struct_data) => safety_conds_inner(ident, &struct_data.fields),
+        Data::Enum(_) => None,
+        Data::Union(_) => None,
+    }
+}
+
+/// Generates an expression resulting from the conjunction of conditions
+/// specified as safety constraints for each field. See `safety_conds` for more details.
+fn safety_conds_inner(ident: &Ident, fields: &Fields) -> Option<TokenStream> {
+    match fields {
+        Fields::Named(ref fields) => {
+            let conds: Vec<TokenStream> =
+                fields.named.iter().filter_map(|field| parse_safety_expr(ident, field)).collect();
+            if !conds.is_empty() { Some(quote! { #(#conds)&&* }) } else { None }
+        }
+        Fields::Unnamed(_) => None,
+        Fields::Unit => None,
+    }
+}
+
+/// Generates the sequence of expressions to initialize the variables used as
+/// references to the struct fields.
+///
+/// For example, if we're deriving implementations for the struct
+/// ```
+/// #[derive(Arbitrary)]
+/// #[derive(Invariant)]
+/// struct PositivePoint {
+///     #[safety_constraint(*x >= 0)]
+///     x: i32,
+///     #[safety_constraint(*y >= 0)]
+///     y: i32,
+/// }
+/// ```
+/// this function will generate the `TokenStream`
+/// ```
+/// let x = &obj.x;
+/// let y = &obj.y;
+/// ```
+/// which allows us to refer to the struct fields without using `self`.
+/// Note that the actual stream is generated in the `field_refs_inner` function.
+fn field_refs(ident: &Ident, data: &Data) -> TokenStream {
+    match data {
+        Data::Struct(struct_data) => field_refs_inner(ident, &struct_data.fields),
+        Data::Enum(_) => unreachable!(),
+        Data::Union(_) => unreachable!(),
+    }
+}
+
+/// Generates the sequence of expressions to initialize the variables used as
+/// references to the struct fields. See `field_refs` for more details.
+fn field_refs_inner(_ident: &Ident, fields: &Fields) -> TokenStream {
+    match fields {
+        Fields::Named(ref fields) => {
+            let field_refs: Vec<TokenStream> = fields
+                .named
+                .iter()
+                .map(|field| {
+                    let name = &field.ident;
+                    quote_spanned! {field.span()=>
+                        let #name = &obj.#name;
+                    }
+                })
+                .collect();
+            if !field_refs.is_empty() {
+                quote! { #( #field_refs )* }
+            } else {
+                quote! {}
+            }
+        }
+        Fields::Unnamed(_) => quote! {},
+        Fields::Unit => quote! {},
+    }
+}
+
 /// Generate an item initialization where an item can be a struct or a variant.
 /// For named fields, this will generate: `Item { field1: kani::any(), field2: kani::any(), .. }`
 /// For unnamed fields, this will generate: `Item (kani::any(), kani::any(), ..)`
@@ -115,6 +231,42 @@ fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream {
     }
 }
 
+/// Extract, parse and return the expression `cond` (i.e., `Some(cond)`) in the
+/// `#[safety_constraint(<cond>)]` attribute helper associated with a given field.
+/// Return `None` if the attribute isn't specified.
+fn parse_safety_expr(ident: &Ident, field: &syn::Field) -> Option<TokenStream> {
+    let name = &field.ident;
+    let mut safety_helper_attr = None;
+
+    // Keep the helper attribute if we find it
+    for attr in &field.attrs {
+        if attr.path().is_ident("safety_constraint") {
+            safety_helper_attr = Some(attr);
+        }
+    }
+
+    // Parse the arguments in the `#[safety_constraint(...)]` attribute
+    if let Some(attr) = safety_helper_attr {
+        let expr_args: Result<syn::Expr, syn::Error> = attr.parse_args();
+
+        // Check if there was an error parsing the arguments
+        if let Err(err) = expr_args {
+            abort!(Span::call_site(), "Cannot derive impl for `{}`", ident;
+            note = attr.span() =>
+            "safety constraint in field `{}` could not be parsed: {}", name.as_ref().unwrap().to_string(), err
+            )
+        }
+
+        // Return the expression associated to the safety constraint
+        let safety_expr = expr_args.unwrap();
+        Some(quote_spanned! {field.span()=>
+            #safety_expr
+        })
+    } else {
+        None
+    }
+}
+
 /// Generate the body of the function `any()` for enums. The cases are:
 /// 1. For zero-variants enumerations, this will encode a `panic!()` statement.
 /// 2. For one or more variants, the code will be something like:
@@ -176,10 +328,14 @@ pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::Tok
     let (impl_generics, ty_generics, where_clause) = generics.split_for_impl();
 
     let body = is_safe_body(&item_name, &derive_item.data);
+    let field_refs = field_refs(&item_name, &derive_item.data);
+
     let expanded = quote! {
         // The generated implementation.
         impl #impl_generics kani::Invariant for #item_name #ty_generics #where_clause {
             fn is_safe(&self) -> bool {
+                let obj = self;
+                #field_refs
                 #body
             }
         }
@@ -199,7 +355,7 @@ fn add_trait_bound_invariant(mut generics: Generics) -> Generics {
 
 fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream {
     match data {
-        Data::Struct(struct_data) => struct_safe_conjunction(ident, &struct_data.fields),
+        Data::Struct(struct_data) => struct_invariant_conjunction(ident, &struct_data.fields),
         Data::Enum(_) => {
             abort!(Span::call_site(), "Cannot derive `Invariant` for `{}` enum", ident;
                 note = ident.span() =>
@@ -215,21 +371,35 @@ fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream {
     }
 }
 
-/// Generates an expression that is the conjunction of `is_safe` calls for each field in the struct.
-fn struct_safe_conjunction(_ident: &Ident, fields: &Fields) -> TokenStream {
+/// Generates an expression that is the conjunction of safety constraints for each field in the struct.
+fn struct_invariant_conjunction(ident: &Ident, fields: &Fields) -> TokenStream {
     match fields {
         // Expands to the expression
+        // `true && <safety_cond1> && <safety_cond2> && ..`
+        // where `safety_condN` is
+        //  - `self.fieldN.is_safe() && <cond>` if a condition `<cond>` was
+        //    specified through the `#[safety_constraint(<cond>)]` helper attribute, or
+        //  - `self.fieldN.is_safe()` otherwise
+        //
+        // Therefore, if `#[safety_constraint(<cond>)]` isn't specified for any field, this expands to
         // `true && self.field1.is_safe() && self.field2.is_safe() && ..`
         Fields::Named(ref fields) => {
-            let safe_calls = fields.named.iter().map(|field| {
-                let name = &field.ident;
-                quote_spanned! {field.span()=>
-                    self.#name.is_safe()
-                }
-            });
+            let safety_conds: Vec<TokenStream> = fields
+                .named
+                .iter()
+                .map(|field| {
+                    let name = &field.ident;
+                    let default_expr = quote_spanned! {field.span()=>
+                        #name.is_safe()
+                    };
+                    parse_safety_expr(ident, field)
+                        .map(|expr| quote! { #expr && #default_expr})
+                        .unwrap_or(default_expr)
+                })
+                .collect();
             // An initial value is required for empty structs
-            safe_calls.fold(quote! { true }, |acc, call| {
-                quote! { #acc && #call }
+            safety_conds.iter().fold(quote! { true }, |acc, cond| {
+                quote! { #acc && #cond }
             })
         }
         Fields::Unnamed(ref fields) => {
diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs
index b10b8a74cdc5..4e3a8d6f9f5b 100644
--- a/library/kani_macros/src/lib.rs
+++ b/library/kani_macros/src/lib.rs
@@ -100,16 +100,120 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream {
     attr_impl::unstable(attr, item)
 }
 
-/// Allow users to auto generate Arbitrary implementations by using `#[derive(Arbitrary)]` macro.
+/// Allow users to auto generate `Arbitrary` implementations by using
+/// `#[derive(Arbitrary)]` macro.
+///
+/// When using `#[derive(Arbitrary)]` on a struct, the `#[safety_constraint(<cond>)]`
+/// attribute can be added to its fields to indicate a type safety invariant
+/// condition `<cond>`. Since `kani::any()` is always expected to produce
+/// type-safe values, **adding `#[safety_constraint(...)]` to any fields will further
+/// constrain the objects generated with `kani::any()`**.
+///
+/// For example, the `check_positive` harness in this code is expected to
+/// pass:
+///
+/// ```rs
+/// #[derive(kani::Arbitrary)]
+/// struct AlwaysPositive {
+///     #[safety_constraint(*inner >= 0)]
+///     inner: i32,
+/// }
+///
+/// #[kani::proof]
+/// fn check_positive() {
+///     let val: AlwaysPositive = kani::any();
+///     assert!(val.inner >= 0);
+/// }
+/// ```
+///
+/// Therefore, using the `#[safety_constraint(...)]` attribute can lead to vacuous
+/// results when the values are over-constrained. For example, in this code
+/// the `check_positive` harness will pass too:
+///
+/// ```rs
+/// #[derive(kani::Arbitrary)]
+/// struct AlwaysPositive {
+///     #[safety_constraint(*inner >= 0 && *inner < i32::MIN)]
+///     inner: i32,
+/// }
+///
+/// #[kani::proof]
+/// fn check_positive() {
+///     let val: AlwaysPositive = kani::any();
+///     assert!(val.inner >= 0);
+/// }
+/// ```
+///
+/// Unfortunately, we made a mistake when specifying the condition because
+/// `*inner >= 0 && *inner < i32::MIN` is equivalent to `false`. This results
+/// in the relevant assertion being unreachable:
+///
+/// ```
+/// Check 1: check_positive.assertion.1
+///         - Status: UNREACHABLE
+///         - Description: "assertion failed: val.inner >= 0"
+///         - Location: src/main.rs:22:5 in function check_positive
+/// ```
+///
+/// As usual, we recommend users to defend against these behaviors by using
+/// `kani::cover!(...)` checks and watching out for unreachable assertions in
+/// their project's code.
 #[proc_macro_error]
-#[proc_macro_derive(Arbitrary)]
+#[proc_macro_derive(Arbitrary, attributes(safety_constraint))]
 pub fn derive_arbitrary(item: TokenStream) -> TokenStream {
     derive::expand_derive_arbitrary(item)
 }
 
-/// Allow users to auto generate Invariant implementations by using `#[derive(Invariant)]` macro.
+/// Allow users to auto generate `Invariant` implementations by using
+/// `#[derive(Invariant)]` macro.
+///
+/// When using `#[derive(Invariant)]` on a struct, the `#[safety_constraint(<cond>)]`
+/// attribute can be added to its fields to indicate a type safety invariant
+/// condition `<cond>`. This will ensure that the gets additionally checked when
+/// using the `is_safe()` method generated by the `#[derive(Invariant)]` macro.
+///
+/// For example, the `check_positive` harness in this code is expected to
+/// fail:
+///
+/// ```rs
+/// #[derive(kani::Invariant)]
+/// struct AlwaysPositive {
+///     #[safety_constraint(*inner >= 0)]
+///     inner: i32,
+/// }
+///
+/// #[kani::proof]
+/// fn check_positive() {
+///     let val = AlwaysPositive { inner: -1 };
+///     assert!(val.is_safe());
+/// }
+/// ```
+///
+/// This is not too surprising since the type safety invariant that we indicated
+/// is not being taken into account when we create the `AlwaysPositive` object.
+///
+/// As mentioned, the `is_safe()` methods generated by the
+/// `#[derive(Invariant)]` macro check the corresponding `is_safe()` method for
+/// each field in addition to any type safety invariants specified through the
+/// `#[safety_constraint(...)]` attribute.
+///
+/// For example, for the `AlwaysPositive` struct from above, we will generate
+/// the following implementation:
+///
+/// ```rs
+/// impl kani::Invariant for AlwaysPositive {
+///     fn is_safe(&self) -> bool {
+///         let obj = self;
+///         let inner = &obj.inner;
+///         true && *inner >= 0 && inner.is_safe()
+///     }
+/// }
+/// ```
+///
+/// Note: the assignments to `obj` and `inner` are made so that we can treat the
+/// fields as if they were references.
 #[proc_macro_error]
-#[proc_macro_derive(Invariant)]
+#[proc_macro_derive(Invariant, attributes(safety_constraint))]
 pub fn derive_invariant(item: TokenStream) -> TokenStream {
     derive::expand_derive_invariant(item)
 }
diff --git a/tests/expected/derive-arbitrary/safety_constraint_helper/expected b/tests/expected/derive-arbitrary/safety_constraint_helper/expected
new file mode 100644
index 000000000000..f35f18084911
--- /dev/null
+++ b/tests/expected/derive-arbitrary/safety_constraint_helper/expected
@@ -0,0 +1,17 @@
+Check 1: check_invariant_helper_ok.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.x >= 0"
+
+Check 2: check_invariant_helper_ok.assertion.2\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.y >= 0"
+
+Check 1: check_invariant_helper_fail.assertion.1\
+         - Status: FAILURE\
+         - Description: "assertion failed: pos_point.x >= 0"
+
+Check 2: check_invariant_helper_fail.assertion.2\
+         - Status: FAILURE\
+         - Description: "assertion failed: pos_point.y >= 0"
+
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.
diff --git a/tests/expected/derive-arbitrary/safety_constraint_helper/safety_constraint_helper.rs b/tests/expected/derive-arbitrary/safety_constraint_helper/safety_constraint_helper.rs
new file mode 100644
index 000000000000..5b608aa2a3c0
--- /dev/null
+++ b/tests/expected/derive-arbitrary/safety_constraint_helper/safety_constraint_helper.rs
@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute helper adds the conditions provided to
+//! the attribute to the derived `Arbitrary` implementation.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+struct PositivePoint {
+    #[safety_constraint(*x >= 0)]
+    x: i32,
+    #[safety_constraint(*y >= 0)]
+    y: i32,
+}
+
+#[kani::proof]
+fn check_invariant_helper_ok() {
+    let pos_point: PositivePoint = kani::any();
+    assert!(pos_point.x >= 0);
+    assert!(pos_point.y >= 0);
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn check_invariant_helper_fail() {
+    let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() };
+    assert!(pos_point.x >= 0);
+    assert!(pos_point.y >= 0);
+}
diff --git a/tests/expected/derive-invariant/attrs_cfg_guard/attrs_cfg_guard.rs b/tests/expected/derive-invariant/attrs_cfg_guard/attrs_cfg_guard.rs
new file mode 100644
index 000000000000..546695bf3731
--- /dev/null
+++ b/tests/expected/derive-invariant/attrs_cfg_guard/attrs_cfg_guard.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute helper is picked up
+//! when it's used with `cfg_attr(kani, ...)]`.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    #[cfg_attr(kani, safety_constraint(*x >= 0))]
+    x: i32,
+    #[cfg_attr(kani, safety_constraint(*y >= 0))]
+    y: i32,
+}
+
+#[kani::proof]
+fn check_safety_constraint_cfg() {
+    let pos_point: PositivePoint = kani::any();
+    assert!(pos_point.x >= 0);
+    assert!(pos_point.y >= 0);
+}
diff --git a/tests/expected/derive-invariant/attrs_cfg_guard/expected b/tests/expected/derive-invariant/attrs_cfg_guard/expected
new file mode 100644
index 000000000000..edb3e256975d
--- /dev/null
+++ b/tests/expected/derive-invariant/attrs_cfg_guard/expected
@@ -0,0 +1,9 @@
+Check 1: check_safety_constraint_cfg.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.x >= 0"
+
+Check 2: check_safety_constraint_cfg.assertion.2\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.y >= 0"
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
diff --git a/tests/expected/derive-invariant/attrs_mixed/attrs_mixed.rs b/tests/expected/derive-invariant/attrs_mixed/attrs_mixed.rs
new file mode 100644
index 000000000000..ff58ff846c67
--- /dev/null
+++ b/tests/expected/derive-invariant/attrs_mixed/attrs_mixed.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that in the `#[safety_constraint(...)]` attribute helper it is
+//! possible to refer to other struct fields, not just the one associated with
+//! the attribute.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    #[safety_constraint(*x >= 0 && *y >= 0)]
+    x: i32,
+    y: i32,
+}
+
+#[kani::proof]
+fn check_safety_constraint_cfg() {
+    let pos_point: PositivePoint = kani::any();
+    assert!(pos_point.x >= 0);
+    assert!(pos_point.y >= 0);
+}
diff --git a/tests/expected/derive-invariant/attrs_mixed/expected b/tests/expected/derive-invariant/attrs_mixed/expected
new file mode 100644
index 000000000000..edb3e256975d
--- /dev/null
+++ b/tests/expected/derive-invariant/attrs_mixed/expected
@@ -0,0 +1,9 @@
+Check 1: check_safety_constraint_cfg.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.x >= 0"
+
+Check 2: check_safety_constraint_cfg.assertion.2\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.y >= 0"
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
diff --git a/tests/expected/derive-invariant/safety_constraint_helper/expected b/tests/expected/derive-invariant/safety_constraint_helper/expected
new file mode 100644
index 000000000000..31b6de54c647
--- /dev/null
+++ b/tests/expected/derive-invariant/safety_constraint_helper/expected
@@ -0,0 +1,13 @@
+Check 1: check_invariant_helper_ok.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.is_safe()"
+
+Check 1: check_invariant_helper_ok_manual.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.is_safe()"
+
+Check 1: check_invariant_helper_fail.assertion.1\
+         - Status: FAILURE\
+         - Description: "assertion failed: pos_point.is_safe()"
+
+Complete - 3 successfully verified harnesses, 0 failures, 3 total.
diff --git a/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs b/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs
new file mode 100644
index 000000000000..44a218f8fa63
--- /dev/null
+++ b/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs
@@ -0,0 +1,43 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute helper adds the conditions provided to
+//! the attribute to the derived `Invariant` implementation.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    #[safety_constraint(*x >= 0)]
+    x: i32,
+    #[safety_constraint(*y >= 0)]
+    y: i32,
+}
+
+#[kani::proof]
+fn check_invariant_helper_ok() {
+    let pos_point: PositivePoint = kani::any();
+    assert!(pos_point.is_safe());
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn check_invariant_helper_fail() {
+    // In this case, we build the struct from unconstrained arbitrary values
+    // that do not respect `PositivePoint`'s safety constraints.
+    let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() };
+    assert!(pos_point.is_safe());
+}
+
+#[kani::proof]
+fn check_invariant_helper_ok_manual() {
+    // In this case, we build the struct from unconstrained arbitrary values
+    // that do not respect `PositivePoint`'s safety constraints. However, we
+    // manually constrain them later.
+    let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() };
+    kani::assume(pos_point.x >= 0);
+    kani::assume(pos_point.y >= 0);
+    assert!(pos_point.is_safe());
+}
diff --git a/tests/expected/derive-invariant/safety_constraint_helper_funs/expected b/tests/expected/derive-invariant/safety_constraint_helper_funs/expected
new file mode 100644
index 000000000000..31b6de54c647
--- /dev/null
+++ b/tests/expected/derive-invariant/safety_constraint_helper_funs/expected
@@ -0,0 +1,13 @@
+Check 1: check_invariant_helper_ok.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.is_safe()"
+
+Check 1: check_invariant_helper_ok_manual.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.is_safe()"
+
+Check 1: check_invariant_helper_fail.assertion.1\
+         - Status: FAILURE\
+         - Description: "assertion failed: pos_point.is_safe()"
+
+Complete - 3 successfully verified harnesses, 0 failures, 3 total.
diff --git a/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs b/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs
new file mode 100644
index 000000000000..a2c4600eb208
--- /dev/null
+++ b/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs
@@ -0,0 +1,48 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that functions can be called in the `#[safety_constraint(...)]` attribute helpers.
+//! This is like the `invariant_helper` test but using a function instead
+//! of passing in a predicate.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    #[safety_constraint(is_coordinate_safe(x))]
+    x: i32,
+    #[safety_constraint(is_coordinate_safe(y))]
+    y: i32,
+}
+
+fn is_coordinate_safe(val: &i32) -> bool {
+    *val >= 0
+}
+
+#[kani::proof]
+fn check_invariant_helper_ok() {
+    let pos_point: PositivePoint = kani::any();
+    assert!(pos_point.is_safe());
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn check_invariant_helper_fail() {
+    // In this case, we build the struct from unconstrained arbitrary values
+    // that do not respect `PositivePoint`'s safety constraints.
+    let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() };
+    assert!(pos_point.is_safe());
+}
+
+#[kani::proof]
+fn check_invariant_helper_ok_manual() {
+    // In this case, we build the struct from unconstrained arbitrary values
+    // that do not respect `PositivePoint`'s safety constraints. However, we
+    // manually constrain them later.
+    let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() };
+    kani::assume(pos_point.x >= 0);
+    kani::assume(pos_point.y >= 0);
+    assert!(pos_point.is_safe());
+}
diff --git a/tests/expected/derive-invariant/invariant_fail/expected b/tests/expected/derive-invariant/safety_invariant_fail/expected
similarity index 100%
rename from tests/expected/derive-invariant/invariant_fail/expected
rename to tests/expected/derive-invariant/safety_invariant_fail/expected
diff --git a/tests/expected/derive-invariant/invariant_fail/invariant_fail.rs b/tests/expected/derive-invariant/safety_invariant_fail/safety_invariant_fail.rs
similarity index 100%
rename from tests/expected/derive-invariant/invariant_fail/invariant_fail.rs
rename to tests/expected/derive-invariant/safety_invariant_fail/safety_invariant_fail.rs
diff --git a/tests/expected/derive-invariant/safety_invariant_fail_mut/expected b/tests/expected/derive-invariant/safety_invariant_fail_mut/expected
new file mode 100644
index 000000000000..0853a68fa79e
--- /dev/null
+++ b/tests/expected/derive-invariant/safety_invariant_fail_mut/expected
@@ -0,0 +1,11 @@
+Check 1: check_invariant_fail_mut.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: pos_point.is_safe()"
+
+Check 2: check_invariant_fail_mut.assertion.2\
+         - Status: FAILURE\
+         - Description: "assertion failed: pos_point.is_safe()"
+
+VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
diff --git a/tests/expected/derive-invariant/safety_invariant_fail_mut/safety_invariant_fail_mut.rs b/tests/expected/derive-invariant/safety_invariant_fail_mut/safety_invariant_fail_mut.rs
new file mode 100644
index 000000000000..dc659ec66dd6
--- /dev/null
+++ b/tests/expected/derive-invariant/safety_invariant_fail_mut/safety_invariant_fail_mut.rs
@@ -0,0 +1,28 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that a verification failure is triggered if we check the invariant
+//! after mutating an object to violate it.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    #[safety_constraint(*x >= 0)]
+    x: i32,
+    #[safety_constraint(*y >= 0)]
+    y: i32,
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn check_invariant_fail_mut() {
+    let mut pos_point: PositivePoint = kani::any();
+    assert!(pos_point.is_safe());
+    // Set the `x` field to an unsafe value
+    pos_point.x = -1;
+    // The object's invariant isn't preserved anymore so the next check fails
+    assert!(pos_point.is_safe());
+}
diff --git a/tests/ui/derive-invariant/helper-empty/expected b/tests/ui/derive-invariant/helper-empty/expected
new file mode 100644
index 000000000000..d8590a9d22b8
--- /dev/null
+++ b/tests/ui/derive-invariant/helper-empty/expected
@@ -0,0 +1,6 @@
+error: Cannot derive impl for `PositivePoint`
+   |
+| #[derive(kani::Invariant)]
+   |          ^^^^^^^^^^^^^^^
+   |
+note: safety constraint in field `x` could not be parsed: expected attribute arguments in parentheses: #[safety_constraint(...)]
diff --git a/tests/ui/derive-invariant/helper-empty/helper-empty.rs b/tests/ui/derive-invariant/helper-empty/helper-empty.rs
new file mode 100644
index 000000000000..3086603cf5db
--- /dev/null
+++ b/tests/ui/derive-invariant/helper-empty/helper-empty.rs
@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check the compilation error for the `#[safety_constraint(...)]` attribute helper when an
+//! argument isn't provided.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    #[safety_constraint]
+    x: i32,
+    #[safety_constraint(*y >= 0)]
+    y: i32,
+}
diff --git a/tests/ui/derive-invariant/helper-no-expr/expected b/tests/ui/derive-invariant/helper-no-expr/expected
new file mode 100644
index 000000000000..e9ac7e3e1124
--- /dev/null
+++ b/tests/ui/derive-invariant/helper-no-expr/expected
@@ -0,0 +1,6 @@
+error: Cannot derive impl for `PositivePoint`
+   |
+| #[derive(kani::Invariant)]
+   |          ^^^^^^^^^^^^^^^
+   |
+note: safety constraint in field `x` could not be parsed: unexpected end of input, expected an expression
diff --git a/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs
new file mode 100644
index 000000000000..080c94371257
--- /dev/null
+++ b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs
@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check the compilation error for the `#[safety_constraint(...)]` attribute helper when the
+//! argument is not a proper expression.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    #[safety_constraint()]
+    x: i32,
+    #[safety_constraint(*y >= 0)]
+    y: i32,
+}
diff --git a/tests/ui/derive-invariant/helper-side-effect/expected b/tests/ui/derive-invariant/helper-side-effect/expected
new file mode 100644
index 000000000000..20b3d17efd38
--- /dev/null
+++ b/tests/ui/derive-invariant/helper-side-effect/expected
@@ -0,0 +1,9 @@
+error[E0596]: cannot borrow `*x` as mutable, as it is behind a `&` reference
+   |
+|     #[safety_constraint({*(x.as_mut()) = 0; true})]
+   |                            ^ `x` is a `&` reference, so the data it refers to cannot be borrowed as mutable
+   |
+help: consider specifying this binding's type
+   |
+|     x: &mut std::boxed::Box<i32>: Box<i32>,
+   |      +++++++++++++++++++++++++++
diff --git a/tests/ui/derive-invariant/helper-side-effect/helper-side-effect.rs b/tests/ui/derive-invariant/helper-side-effect/helper-side-effect.rs
new file mode 100644
index 000000000000..e80f2ff25796
--- /dev/null
+++ b/tests/ui/derive-invariant/helper-side-effect/helper-side-effect.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that side effect expressions in the `#[safety_constraint(...)]`
+//! attribute helpers are not allowed.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    #[safety_constraint({*(x.as_mut()) = 0; true})]
+    x: Box<i32>,
+    y: i32,
+}
+
+#[kani::proof]
+fn check_invariant_helper_ok() {
+    let pos_point: PositivePoint = kani::any();
+    assert!(pos_point.is_safe());
+}
diff --git a/tests/ui/derive-invariant/helper-wrong-expr/expected b/tests/ui/derive-invariant/helper-wrong-expr/expected
new file mode 100644
index 000000000000..3f661bce9cbb
--- /dev/null
+++ b/tests/ui/derive-invariant/helper-wrong-expr/expected
@@ -0,0 +1,9 @@
+error[E0308]: mismatched types
+   |
+|     #[safety_constraint(x >= 0)]
+   |                              ^ expected `&i32`, found integer
+   |
+help: consider dereferencing the borrow
+   |
+|     #[safety_constraint(*x >= 0)]
+   |
diff --git a/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs
new file mode 100644
index 000000000000..66b42e02fd68
--- /dev/null
+++ b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs
@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check the compilation error for the `#[safety_constraint(...)]` attribute helper when the
+//! argument cannot be evaluated in the struct's context.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+struct PositivePoint {
+    // Note: `x` is a reference in this context, we should refer to `*x`
+    #[safety_constraint(x >= 0)]
+    x: i32,
+    #[safety_constraint(*y >= 0)]
+    y: i32,
+}