diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs
index a7aaa8ae334e..cc936560e510 100644
--- a/library/kani_macros/src/derive.rs
+++ b/library/kani_macros/src/derive.rs
@@ -19,20 +19,20 @@ use syn::{
 };
 
 pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::TokenStream {
+    let trait_name = "Arbitrary";
     let derive_item = parse_macro_input!(item as DeriveInput);
     let item_name = &derive_item.ident;
 
+    let body = fn_any_body(&item_name, &derive_item.data);
+    // Get the safety constraints (if any) to produce type-safe values
+    let safety_conds_opt = safety_conds_opt(&item_name, &derive_item, trait_name);
+
     // Add a bound `T: Arbitrary` to every type parameter T.
     let generics = add_trait_bound_arbitrary(derive_item.generics);
     // Generate an expression to sum up the heap size of each field.
     let (impl_generics, ty_generics, where_clause) = generics.split_for_impl();
 
-    let body = fn_any_body(&item_name, &derive_item.data);
-
-    // 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 expanded = if let Some(safety_conds) = safety_conds_opt {
         let field_refs = field_refs(&item_name, &derive_item.data);
         quote! {
             // The generated implementation.
@@ -40,7 +40,7 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok
                 fn any() -> Self {
                     let obj = #body;
                     #field_refs
-                    kani::assume(#safety_cond);
+                    kani::assume(#safety_conds);
                     obj
                 }
             }
@@ -94,48 +94,6 @@ 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.
 ///
@@ -191,6 +149,55 @@ fn field_refs_inner(_ident: &Ident, fields: &Fields) -> TokenStream {
     }
 }
 
+fn safe_body_default(ident: &Ident, data: &Data) -> TokenStream {
+    match data {
+        Data::Struct(struct_data) => safe_body_default_inner(ident, &struct_data.fields),
+        Data::Enum(_) => unreachable!(),
+        Data::Union(_) => unreachable!(),
+    }
+}
+
+fn safe_body_default_inner(_ident: &Ident, fields: &Fields) -> TokenStream {
+    match fields {
+        Fields::Named(ref fields) => {
+            let field_safe_calls: Vec<TokenStream> = fields
+                .named
+                .iter()
+                .map(|field| {
+                    let name = &field.ident;
+                    quote_spanned! {field.span()=>
+                        #name.is_safe()
+                    }
+                })
+                .collect();
+            if !field_safe_calls.is_empty() {
+                quote! { #( #field_safe_calls )&&* }
+            } else {
+                quote! { true }
+            }
+        }
+        Fields::Unnamed(ref fields) => {
+            let field_safe_calls: Vec<TokenStream> = fields
+                .unnamed
+                .iter()
+                .enumerate()
+                .map(|(idx, field)| {
+                    let field_idx = Index::from(idx);
+                    quote_spanned! {field.span()=>
+                        #field_idx.is_safe()
+                    }
+                })
+                .collect();
+            if !field_safe_calls.is_empty() {
+                quote! { #( #field_safe_calls )&&* }
+            } else {
+                quote! { true }
+            }
+        }
+        Fields::Unit => quote! { true },
+    }
+}
+
 /// 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(), ..)`
@@ -267,6 +274,38 @@ fn parse_safety_expr(ident: &Ident, field: &syn::Field) -> Option<TokenStream> {
     }
 }
 
+fn parse_safety_expr_input(ident: &Ident, derive_input: &DeriveInput) -> Option<TokenStream> {
+    let name = ident;
+    let mut safety_attr = None;
+
+    // Keep the attribute if we find it
+    for attr in &derive_input.attrs {
+        if attr.path().is_ident("safety_constraint") {
+            safety_attr = Some(attr);
+        }
+    }
+
+    // Parse the arguments in the `#[safety_constraint(...)]` attribute
+    if let Some(attr) = safety_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 `{}` could not be parsed: {}", name.to_string(), err
+            )
+        }
+
+        // Return the expression associated to the safety constraint
+        let safety_expr = expr_args.unwrap();
+        Some(quote_spanned! {derive_input.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:
@@ -318,33 +357,112 @@ fn fn_any_enum(ident: &Ident, data: &DataEnum) -> TokenStream {
     }
 }
 
+fn safe_body_with_calls(
+    item_name: &Ident,
+    derive_input: &DeriveInput,
+    trait_name: &str,
+) -> TokenStream {
+    let safety_conds_opt = safety_conds_opt(&item_name, &derive_input, trait_name);
+    let safe_body_default = safe_body_default(&item_name, &derive_input.data);
+
+    if let Some(safety_conds) = safety_conds_opt {
+        quote! { #safe_body_default && #safety_conds }
+    } else {
+        safe_body_default
+    }
+}
+
 pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::TokenStream {
+    let trait_name = "Invariant";
     let derive_item = parse_macro_input!(item as DeriveInput);
     let item_name = &derive_item.ident;
 
+    let safe_body = safe_body_with_calls(&item_name, &derive_item, trait_name);
+    let field_refs = field_refs(&item_name, &derive_item.data);
+
     // Add a bound `T: Invariant` to every type parameter T.
     let generics = add_trait_bound_invariant(derive_item.generics);
     // Generate an expression to sum up the heap size of each field.
     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
+                #safe_body
             }
         }
     };
     proc_macro::TokenStream::from(expanded)
 }
 
+/// Looks for `#[safety_constraint(...)]` attributes used in the struct or its
+/// fields, and returns the constraints if there were any, otherwise returns
+/// `None`.
+/// Note: Errors out if the attribute is used in both the struct and its fields.
+fn safety_conds_opt(
+    item_name: &Ident,
+    derive_input: &DeriveInput,
+    trait_name: &str,
+) -> Option<TokenStream> {
+    let has_item_safety_constraint =
+        has_item_safety_constraint(&item_name, &derive_input, trait_name);
+
+    let has_field_safety_constraints = has_field_safety_constraints(&item_name, &derive_input.data);
+
+    if has_item_safety_constraint && has_field_safety_constraints {
+        abort!(Span::call_site(), "Cannot derive `{}` for `{}`", trait_name, item_name;
+        note = item_name.span() =>
+        "`#[safety_constraint(...)]` cannot be used in struct and its fields simultaneously"
+        )
+    }
+
+    if has_item_safety_constraint {
+        Some(safe_body_from_struct_attr(&item_name, &derive_input, trait_name))
+    } else if has_field_safety_constraints {
+        Some(safe_body_from_fields_attr(&item_name, &derive_input.data, trait_name))
+    } else {
+        None
+    }
+}
+
+fn has_item_safety_constraint(ident: &Ident, derive_input: &DeriveInput, trait_name: &str) -> bool {
+    let safety_constraints_in_item =
+        derive_input.attrs.iter().filter(|attr| attr.path().is_ident("safety_constraint")).count();
+    if safety_constraints_in_item > 1 {
+        abort!(Span::call_site(), "Cannot derive `{}` for `{}`", trait_name, ident;
+        note = ident.span() =>
+        "`#[safety_constraint(...)]` cannot be used more than once."
+        )
+    }
+    safety_constraints_in_item == 1
+}
+
+fn has_field_safety_constraints(ident: &Ident, data: &Data) -> bool {
+    match data {
+        Data::Struct(struct_data) => has_field_safety_constraints_inner(ident, &struct_data.fields),
+        Data::Enum(_) => false,
+        Data::Union(_) => false,
+    }
+}
+
+/// Checks if the `#[safety_constraint(...)]` attribute is attached to any
+/// field.
+fn has_field_safety_constraints_inner(_ident: &Ident, fields: &Fields) -> bool {
+    match fields {
+        Fields::Named(ref fields) => fields
+            .named
+            .iter()
+            .any(|field| field.attrs.iter().any(|attr| attr.path().is_ident("safety_constraint"))),
+        Fields::Unnamed(_) => false,
+        Fields::Unit => false,
+    }
+}
+
 /// Add a bound `T: Invariant` to every type parameter T.
-fn add_trait_bound_invariant(mut generics: Generics) -> Generics {
+pub fn add_trait_bound_invariant(mut generics: Generics) -> Generics {
     generics.params.iter_mut().for_each(|param| {
         if let GenericParam::Type(type_param) = param {
             type_param.bounds.push(parse_quote!(kani::Invariant));
@@ -353,17 +471,51 @@ fn add_trait_bound_invariant(mut generics: Generics) -> Generics {
     generics
 }
 
-fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream {
+fn safe_body_from_struct_attr(
+    ident: &Ident,
+    derive_input: &DeriveInput,
+    trait_name: &str,
+) -> TokenStream {
+    if !matches!(derive_input.data, Data::Struct(_)) {
+        abort!(Span::call_site(), "Cannot derive `{}` for `{}`", trait_name, ident;
+            note = ident.span() =>
+            "`#[safety_constraint(...)]` can only be used in structs"
+        )
+    };
+    parse_safety_expr_input(ident, derive_input).unwrap()
+}
+
+/// 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 used by the `Arbitrary` and `Invariant` to generate and check
+/// type-safe values for the struct, respectively.
+fn safe_body_from_fields_attr(ident: &Ident, data: &Data, trait_name: &str) -> TokenStream {
     match data {
-        Data::Struct(struct_data) => struct_invariant_conjunction(ident, &struct_data.fields),
+        Data::Struct(struct_data) => safe_body_from_fields_attr_inner(ident, &struct_data.fields),
         Data::Enum(_) => {
-            abort!(Span::call_site(), "Cannot derive `Invariant` for `{}` enum", ident;
+            abort!(Span::call_site(), "Cannot derive `{}` for `{}` enum", trait_name, ident;
                 note = ident.span() =>
                 "`#[derive(Invariant)]` cannot be used for enums such as `{}`", ident
             )
         }
         Data::Union(_) => {
-            abort!(Span::call_site(), "Cannot derive `Invariant` for `{}` union", ident;
+            abort!(Span::call_site(), "Cannot derive `{}` for `{}` union", trait_name, ident;
                 note = ident.span() =>
                 "`#[derive(Invariant)]` cannot be used for unions such as `{}`", ident
             )
@@ -371,50 +523,23 @@ fn is_safe_body(ident: &Ident, data: &Data) -> 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 {
+/// Generates an expression resulting from the conjunction of conditions
+/// specified as safety constraints for each field.
+/// See `safe_body_from_fields_attr` for more details.
+fn safe_body_from_fields_attr_inner(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() && ..`
+        // `<safety_cond1> && <safety_cond2> && ..`
+        // where `<safety_condN>` is the safety condition specified for the N-th field.
         Fields::Named(ref fields) => {
-            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
-            safety_conds.iter().fold(quote! { true }, |acc, cond| {
-                quote! { #acc && #cond }
-            })
+            let safety_conds: Vec<TokenStream> =
+                fields.named.iter().filter_map(|field| parse_safety_expr(ident, field)).collect();
+            quote! { #(#safety_conds)&&* }
         }
-        Fields::Unnamed(ref fields) => {
-            // Expands to the expression
-            // `true && self.0.is_safe() && self.1.is_safe() && ..`
-            let safe_calls = fields.unnamed.iter().enumerate().map(|(i, field)| {
-                let idx = syn::Index::from(i);
-                quote_spanned! {field.span()=>
-                    self.#idx.is_safe()
-                }
-            });
-            // An initial value is required for empty structs
-            safe_calls.fold(quote! { true }, |acc, call| {
-                quote! { #acc && #call }
-            })
+        Fields::Unnamed(_) => {
+            quote! {
+                true
+            }
         }
         // Expands to the expression
         // `true`
diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
index d01ca379655f..9752bec5d272 100644
--- a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
+++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts --solver minisat
 
 /// The objective of this test is to show that the contracts for double can be replaced as a stub within the contracts for quadruple.
 /// This shows that we can generate `kani::any()` for Cell.
diff --git a/tests/expected/safety-constraint-attribute/abstract-value/abstract-value.rs b/tests/expected/safety-constraint-attribute/abstract-value/abstract-value.rs
new file mode 100644
index 000000000000..6e29938d4d5a
--- /dev/null
+++ b/tests/expected/safety-constraint-attribute/abstract-value/abstract-value.rs
@@ -0,0 +1,30 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute works as expected when
+//! deriving `Arbitrary` and `Invariant` implementations.
+
+//! In this case, we test the attribute on a struct with a generic type `T`
+//! which requires the bound `From<i32>` because of the comparisons in the
+//! `#[safety_constraint(...)]` predicate. The struct represents an abstract
+//! value for which we only track its sign. The actual value is kept private.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+#[safety_constraint((*positive && *conc_value >= 0.into()) || (!*positive && *conc_value < 0.into()))]
+struct AbstractValue<T>
+where
+    T: PartialOrd + From<i32>,
+{
+    pub positive: bool,
+    conc_value: T,
+}
+
+#[kani::proof]
+fn check_abstract_value() {
+    let value: AbstractValue<i32> = kani::any();
+    assert!(value.is_safe());
+}
diff --git a/tests/expected/safety-constraint-attribute/abstract-value/expected b/tests/expected/safety-constraint-attribute/abstract-value/expected
new file mode 100644
index 000000000000..2fc76378041d
--- /dev/null
+++ b/tests/expected/safety-constraint-attribute/abstract-value/expected
@@ -0,0 +1,7 @@
+Check 1: check_abstract_value.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: value.is_safe()"
+
+VERIFICATION:- SUCCESSFUL
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
diff --git a/tests/expected/safety-constraint-attribute/check-arbitrary/check-arbitrary.rs b/tests/expected/safety-constraint-attribute/check-arbitrary/check-arbitrary.rs
new file mode 100644
index 000000000000..6e2b3ab97812
--- /dev/null
+++ b/tests/expected/safety-constraint-attribute/check-arbitrary/check-arbitrary.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute works as expected when
+//! deriving `Arbitrary` and `Invariant` implementations.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+#[safety_constraint(*x >= 0 && *y >= 0)]
+struct Point {
+    x: i32,
+    y: i32,
+}
+
+#[kani::proof]
+fn check_arbitrary() {
+    let point: Point = kani::any();
+    assert!(point.x >= 0);
+    assert!(point.y >= 0);
+    assert!(point.is_safe());
+}
diff --git a/tests/expected/safety-constraint-attribute/check-arbitrary/expected b/tests/expected/safety-constraint-attribute/check-arbitrary/expected
new file mode 100644
index 000000000000..ee1e13bb726d
--- /dev/null
+++ b/tests/expected/safety-constraint-attribute/check-arbitrary/expected
@@ -0,0 +1,11 @@
+Check 1: check_arbitrary.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: point.x >= 0"
+
+Check 2: check_arbitrary.assertion.2\
+         - Status: SUCCESS\
+         - Description: "assertion failed: point.y >= 0"
+
+Check 3: check_arbitrary.assertion.3\
+         - Status: SUCCESS\
+         - Description: "assertion failed: point.is_safe()"
diff --git a/tests/expected/safety-constraint-attribute/check-invariant/check-invariant.rs b/tests/expected/safety-constraint-attribute/check-invariant/check-invariant.rs
new file mode 100644
index 000000000000..fce7319779f0
--- /dev/null
+++ b/tests/expected/safety-constraint-attribute/check-invariant/check-invariant.rs
@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute works as expected when
+//! deriving `Arbitrary` and `Invariant` implementations.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+#[safety_constraint(*x == *y)]
+struct SameCoordsPoint {
+    x: i32,
+    y: i32,
+}
+
+#[kani::proof]
+fn check_invariant() {
+    let point: SameCoordsPoint = kani::any();
+    assert!(point.is_safe());
+
+    // Assuming `point.x != point.y` here should be like assuming `false`.
+    // The assertion should be unreachable because we're blocking the path.
+    kani::assume(point.x != point.y);
+    assert!(false, "this assertion should be unreachable");
+}
diff --git a/tests/expected/safety-constraint-attribute/check-invariant/expected b/tests/expected/safety-constraint-attribute/check-invariant/expected
new file mode 100644
index 000000000000..a4605f03b7b4
--- /dev/null
+++ b/tests/expected/safety-constraint-attribute/check-invariant/expected
@@ -0,0 +1,7 @@
+Check 1: check_invariant.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: point.is_safe()"
+
+Check 2: check_invariant.assertion.2\
+         - Status: UNREACHABLE\
+         - Description: ""this assertion should be unreachable""
diff --git a/tests/expected/safety-constraint-attribute/grade-example/expected b/tests/expected/safety-constraint-attribute/grade-example/expected
new file mode 100644
index 000000000000..fd95a713d65a
--- /dev/null
+++ b/tests/expected/safety-constraint-attribute/grade-example/expected
@@ -0,0 +1,11 @@
+Grade::check_percentage_safety.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: self.percentage <= 100"
+
+check_grade_safe.assertion.1\
+         - Status: SUCCESS\
+         - Description: "assertion failed: grade.is_safe()"
+
+VERIFICATION:- SUCCESSFUL
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
diff --git a/tests/expected/safety-constraint-attribute/grade-example/grade-example.rs b/tests/expected/safety-constraint-attribute/grade-example/grade-example.rs
new file mode 100644
index 000000000000..7998ab27df49
--- /dev/null
+++ b/tests/expected/safety-constraint-attribute/grade-example/grade-example.rs
@@ -0,0 +1,43 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute works as expected when
+//! deriving `Arbitrary` and `Invariant` implementations.
+
+//! In this case, we test the attribute on a struct that represents a hybrid
+//! grade (letter-numerical) which should keep the following equivalences:
+//!  - A for 90-100%
+//!  - B for 80-89%
+//!  - C for 70-79%
+//!  - D for 60-69%
+//!  - F for 0-59%
+//!
+//! In addition, we explicitly test that `percentage` is 0-100%
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+#[safety_constraint((*letter == 'A' && *percentage >= 90 && *percentage <= 100) ||
+                    (*letter == 'B' && *percentage >= 80 && *percentage < 90) ||
+                    (*letter == 'C' && *percentage >= 70 && *percentage < 80) ||
+                    (*letter == 'D' && *percentage >= 60 && *percentage < 70) ||
+                    (*letter == 'F' && *percentage < 60))]
+struct Grade {
+    letter: char,
+    percentage: u32,
+}
+
+impl Grade {
+    pub fn check_percentage_safety(&self) {
+        assert!(self.percentage <= 100);
+    }
+}
+
+#[kani::proof]
+fn check_grade_safe() {
+    let grade: Grade = kani::any();
+    assert!(grade.is_safe());
+    grade.check_percentage_safety();
+}
diff --git a/tests/ui/safety-constraint-attribute/double-attribute/double-attribute.rs b/tests/ui/safety-constraint-attribute/double-attribute/double-attribute.rs
new file mode 100644
index 000000000000..ef7be7fe0e03
--- /dev/null
+++ b/tests/ui/safety-constraint-attribute/double-attribute/double-attribute.rs
@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that there is a compilation error when the `#[safety_constraint(...)]`
+//! attribute is used more than once on the same struct.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(Invariant)]
+#[safety_constraint(*x >= 0)]
+#[safety_constraint(*y >= 0)]
+struct Point {
+    x: i32,
+    y: i32,
+}
diff --git a/tests/ui/safety-constraint-attribute/double-attribute/expected b/tests/ui/safety-constraint-attribute/double-attribute/expected
new file mode 100644
index 000000000000..899b85e20e9a
--- /dev/null
+++ b/tests/ui/safety-constraint-attribute/double-attribute/expected
@@ -0,0 +1,6 @@
+error: Cannot derive `Invariant` for `Point`
+   |
+| #[derive(Invariant)]
+   |          ^^^^^^^^^
+   |
+note: `#[safety_constraint(...)]` cannot be used more than once.
diff --git a/tests/ui/safety-constraint-attribute/invalid-pred-error/expected b/tests/ui/safety-constraint-attribute/invalid-pred-error/expected
new file mode 100644
index 000000000000..e15e3ff7cf7d
--- /dev/null
+++ b/tests/ui/safety-constraint-attribute/invalid-pred-error/expected
@@ -0,0 +1,19 @@
+error[E0308]: mismatched types
+   |
+| #[safety_constraint(x >= 0 && y >= 0)]
+   |                          ^ expected `&i32`, found integer
+   |
+help: consider dereferencing the borrow
+   |
+| #[safety_constraint(*x >= 0 && y >= 0)]
+   |                     +
+
+error[E0308]: mismatched types
+   |
+| #[safety_constraint(x >= 0 && y >= 0)]
+   |                                    ^ expected `&i32`, found integer
+   |
+help: consider dereferencing the borrow
+   |
+| #[safety_constraint(x >= 0 && *y >= 0)]
+   |
diff --git a/tests/ui/safety-constraint-attribute/invalid-pred-error/invalid-pred-error.rs b/tests/ui/safety-constraint-attribute/invalid-pred-error/invalid-pred-error.rs
new file mode 100644
index 000000000000..89c862bb50c3
--- /dev/null
+++ b/tests/ui/safety-constraint-attribute/invalid-pred-error/invalid-pred-error.rs
@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that there is a compilation error when the predicate passed to the
+//! `#[safety_constraint(...)]` attribute would result in a compiler error.
+//!
+//! Note: the `#[derive(kani::Invariant)]` macro is required for the compiler error,
+//! otherwise the `#[safety_constraint(...)]` attribute is ignored.
+
+extern crate kani;
+
+// Note: The struct fields `x` and `y` are references in this context, we should
+// refer to `*x` and `*y` instead.
+#[derive(kani::Invariant)]
+#[safety_constraint(x >= 0 && y >= 0)]
+struct Point {
+    x: i32,
+    y: i32,
+}
diff --git a/tests/ui/safety-constraint-attribute/mixed-attributes/expected b/tests/ui/safety-constraint-attribute/mixed-attributes/expected
new file mode 100644
index 000000000000..bca53d41bf13
--- /dev/null
+++ b/tests/ui/safety-constraint-attribute/mixed-attributes/expected
@@ -0,0 +1,6 @@
+error: Cannot derive `Invariant` for `Point`
+   |
+| #[derive(Invariant)]
+   |          ^^^^^^^^^
+   |
+note: `#[safety_constraint(...)]` cannot be used in struct and its fields simultaneously
diff --git a/tests/ui/safety-constraint-attribute/mixed-attributes/mixed-attributes.rs b/tests/ui/safety-constraint-attribute/mixed-attributes/mixed-attributes.rs
new file mode 100644
index 000000000000..931cebd4839d
--- /dev/null
+++ b/tests/ui/safety-constraint-attribute/mixed-attributes/mixed-attributes.rs
@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that there is a compilation error when the `#[safety_constraint(...)]`
+//! attribute for struct and the `#[safety_constraint(...)]` attribute for
+//! fields is used at the same time.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(Invariant)]
+#[safety_constraint(*x >= 0)]
+struct Point {
+    x: i32,
+    #[safety_constraint(*y >= 0)]
+    y: i32,
+}
diff --git a/tests/ui/safety-constraint-attribute/no-struct-error/expected b/tests/ui/safety-constraint-attribute/no-struct-error/expected
new file mode 100644
index 000000000000..df6bd82f00d6
--- /dev/null
+++ b/tests/ui/safety-constraint-attribute/no-struct-error/expected
@@ -0,0 +1,6 @@
+error: Cannot derive `Invariant` for `MyEnum`
+   |
+| #[derive(kani::Invariant)]
+   |          ^^^^^^^^^^^^^^^
+   |
+note: `#[safety_constraint(...)]` can only be used in structs
diff --git a/tests/ui/safety-constraint-attribute/no-struct-error/no-struct-error.rs b/tests/ui/safety-constraint-attribute/no-struct-error/no-struct-error.rs
new file mode 100644
index 000000000000..092bbe1319c7
--- /dev/null
+++ b/tests/ui/safety-constraint-attribute/no-struct-error/no-struct-error.rs
@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that Kani raises an error when a derive macro with the
+//! `#[safety_constraint(...)]` attribute is is used in items which are not a
+//! struct.
+//!
+//! Note: the `#[derive(kani::Invariant)]` macro is required for the compiler error,
+//! otherwise the `#[safety_constraint(...)]` attribute is ignored.
+
+extern crate kani;
+
+#[derive(kani::Invariant)]
+#[safety_constraint(true)]
+enum MyEnum {
+    A,
+    B(i32),
+}