diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs
index 4e3a8d6f9f5b..6fe0979f08bc 100644
--- a/library/kani_macros/src/lib.rs
+++ b/library/kani_macros/src/lib.rs
@@ -103,16 +103,19 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream {
 /// 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()`**.
+/// ## Type safety specification with the `#[safety_constraint(...)]` attribute
+///
+/// When using `#[derive(Arbitrary)]` on a struct, the
+/// `#[safety_constraint(<cond>)]` attribute can be added to either the struct
+/// or its fields (but not both) to indicate a type safety invariant condition
+/// `<cond>`. Since `kani::any()` is always expected to produce type-safe
+/// values, **adding `#[safety_constraint(...)]` to the struct or any of its
+/// fields will further constrain the objects generated with `kani::any()`**.
 ///
 /// For example, the `check_positive` harness in this code is expected to
 /// pass:
 ///
-/// ```rs
+/// ```rust
 /// #[derive(kani::Arbitrary)]
 /// struct AlwaysPositive {
 ///     #[safety_constraint(*inner >= 0)]
@@ -126,11 +129,11 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream {
 /// }
 /// ```
 ///
-/// Therefore, using the `#[safety_constraint(...)]` attribute can lead to vacuous
+/// But 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
+/// ```rust
 /// #[derive(kani::Arbitrary)]
 /// struct AlwaysPositive {
 ///     #[safety_constraint(*inner >= 0 && *inner < i32::MIN)]
@@ -158,6 +161,45 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream {
 /// 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.
+///
+/// ### Adding `#[safety_constraint(...)]` to the struct as opposed to its fields
+///
+/// As mentioned earlier, the `#[safety_constraint(...)]` attribute can be added
+/// to either the struct or its fields, but not to both. Adding the
+/// `#[safety_constraint(...)]` attribute to both the struct and its fields will
+/// result in an error.
+///
+/// In practice, only one type of specification is need. If the condition for
+/// the type safety invariant involves a relation between two or more struct
+/// fields, the struct-level attribute should be used. Otherwise, using the
+/// `#[safety_constraint(...)]` on field(s) is recommended since it helps with readability.
+///
+/// For example, if we were defining a custom vector `MyVector` and wanted to
+/// specify that the inner vector's length is always less than or equal to its
+/// capacity, we should do it as follows:
+///
+/// ```rust
+/// #[derive(Arbitrary)]
+/// #[safety_constraint(vector.len() <= *capacity)]
+/// struct MyVector<T> {
+///     vector: Vec<T>,
+///     capacity: usize,
+/// }
+/// ```
+///
+/// However, if we were defining a struct whose fields are not related in any
+/// way, we would prefer using the `#[safety_constraint(...)]` attribute on its
+/// fields:
+///
+/// ```rust
+/// #[derive(Arbitrary)]
+/// struct PositivePoint {
+///     #[safety_constraint(*x >= 0)]
+///     x: i32,
+///     #[safety_constraint(*y >= 0)]
+///     y: i32,
+/// }
+/// ```
 #[proc_macro_error]
 #[proc_macro_derive(Arbitrary, attributes(safety_constraint))]
 pub fn derive_arbitrary(item: TokenStream) -> TokenStream {
@@ -167,15 +209,19 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream {
 /// 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.
+/// ## Type safety specification with the `#[safety_constraint(...)]` attribute
+///
+/// When using `#[derive(Invariant)]` on a struct, the
+/// `#[safety_constraint(<cond>)]` attribute can be added to either the struct
+/// or its fields (but not both) to indicate a type safety invariant condition
+/// `<cond>`. This will ensure that the type-safety condition gets additionally
+/// checked when using the `is_safe()` method automatically generated by the
+/// `#[derive(Invariant)]` macro.
 ///
 /// For example, the `check_positive` harness in this code is expected to
 /// fail:
 ///
-/// ```rs
+/// ```rust
 /// #[derive(kani::Invariant)]
 /// struct AlwaysPositive {
 ///     #[safety_constraint(*inner >= 0)]
@@ -200,7 +246,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream {
 /// For example, for the `AlwaysPositive` struct from above, we will generate
 /// the following implementation:
 ///
-/// ```rs
+/// ```rust
 /// impl kani::Invariant for AlwaysPositive {
 ///     fn is_safe(&self) -> bool {
 ///         let obj = self;
@@ -212,6 +258,45 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream {
 ///
 /// Note: the assignments to `obj` and `inner` are made so that we can treat the
 /// fields as if they were references.
+///
+/// ### Adding `#[safety_constraint(...)]` to the struct as opposed to its fields
+///
+/// As mentioned earlier, the `#[safety_constraint(...)]` attribute can be added
+/// to either the struct or its fields, but not to both. Adding the
+/// `#[safety_constraint(...)]` attribute to both the struct and its fields will
+/// result in an error.
+///
+/// In practice, only one type of specification is need. If the condition for
+/// the type safety invariant involves a relation between two or more struct
+/// fields, the struct-level attribute should be used. Otherwise, using the
+/// `#[safety_constraint(...)]` is recommended since it helps with readability.
+///
+/// For example, if we were defining a custom vector `MyVector` and wanted to
+/// specify that the inner vector's length is always less than or equal to its
+/// capacity, we should do it as follows:
+///
+/// ```rust
+/// #[derive(Invariant)]
+/// #[safety_constraint(vector.len() <= *capacity)]
+/// struct MyVector<T> {
+///     vector: Vec<T>,
+///     capacity: usize,
+/// }
+/// ```
+///
+/// However, if we were defining a struct whose fields are not related in any
+/// way, we would prefer using the `#[safety_constraint(...)]` attribute on its
+/// fields:
+///
+/// ```rust
+/// #[derive(Invariant)]
+/// struct PositivePoint {
+///     #[safety_constraint(*x >= 0)]
+///     x: i32,
+///     #[safety_constraint(*y >= 0)]
+///     y: i32,
+/// }
+/// ```
 #[proc_macro_error]
 #[proc_macro_derive(Invariant, attributes(safety_constraint))]
 pub fn derive_invariant(item: TokenStream) -> TokenStream {