diff --git a/cprover_bindings/src/goto_program/stmt.rs b/cprover_bindings/src/goto_program/stmt.rs
index 46973cf0b0fd..76f54241665d 100644
--- a/cprover_bindings/src/goto_program/stmt.rs
+++ b/cprover_bindings/src/goto_program/stmt.rs
@@ -86,6 +86,7 @@ pub enum StmtBody {
         // applied as loop contracts in CBMC if it is a backward goto.
         loop_invariants: Option<Expr>,
         loop_modifies: Option<Vec<Expr>>,
+        loop_decreases: Option<Expr>,
     },
     /// `if (i) { t } else { e }`
     Ifthenelse {
@@ -282,7 +283,7 @@ impl Stmt {
     pub fn goto<T: Into<InternedString>>(dest: T, loc: Location) -> Self {
         let dest = dest.into();
         assert!(!dest.is_empty());
-        stmt!(Goto { dest, loop_invariants: None, loop_modifies: None }, loc)
+        stmt!(Goto { dest, loop_invariants: None, loop_modifies: None, loop_decreases: None }, loc)
     }
 
     /// `if (i) { t } else { e }` or `if (i) { t }`
@@ -327,13 +328,14 @@ impl Stmt {
 
     /// `goto dest;` with loop invariant
     pub fn with_loop_contracts(self, inv: Expr) -> Self {
-        if let Goto { dest, loop_invariants, loop_modifies } = self.body() {
+        if let Goto { dest, loop_invariants, loop_modifies, loop_decreases } = self.body() {
             assert!(loop_invariants.is_none());
             stmt!(
                 Goto {
                     dest: *dest,
                     loop_invariants: Some(inv),
-                    loop_modifies: loop_modifies.clone()
+                    loop_modifies: loop_modifies.clone(),
+                    loop_decreases: loop_decreases.clone()
                 },
                 *self.location()
             )
@@ -343,13 +345,14 @@ impl Stmt {
     }
 
     pub fn with_loop_modifies(self, asg: Vec<Expr>) -> Self {
-        if let Goto { dest, loop_invariants, loop_modifies } = self.body() {
+        if let Goto { dest, loop_invariants, loop_modifies, loop_decreases } = self.body() {
             assert!(loop_modifies.is_none());
             stmt!(
                 Goto {
                     dest: *dest,
                     loop_invariants: loop_invariants.clone(),
-                    loop_modifies: Some(asg)
+                    loop_modifies: Some(asg),
+                    loop_decreases: loop_decreases.clone()
                 },
                 *self.location()
             )
@@ -357,6 +360,23 @@ impl Stmt {
             unreachable!("Loop assigns should be annotated only to goto stmt")
         }
     }
+
+    pub fn with_loop_decreases(self, decreases: Expr) -> Self {
+        if let Goto { dest, loop_invariants, loop_modifies, loop_decreases } = self.body() {
+            assert!(loop_decreases.is_none());
+            stmt!(
+                Goto {
+                    dest: *dest,
+                    loop_invariants: loop_invariants.clone(),
+                    loop_modifies: loop_modifies.clone(),
+                    loop_decreases: Some(decreases)
+                },
+                *self.location()
+            )
+        } else {
+            unreachable!("Loop decreases should be annotated only to goto stmt")
+        }
+    }
 }
 
 /// Predicates
diff --git a/cprover_bindings/src/irep/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs
index 6477fd90e781..359a11e942c1 100644
--- a/cprover_bindings/src/irep/irep_id.rs
+++ b/cprover_bindings/src/irep/irep_id.rs
@@ -595,6 +595,7 @@ pub enum IrepId {
     Used,
     IsUsed,
     CSpecLoopInvariant,
+    CSpecDecreases,
     CSpecRequires,
     CSpecEnsures,
     CSpecAssigns,
@@ -1485,6 +1486,7 @@ impl IrepId {
             IrepId::Used => "used",
             IrepId::IsUsed => "is_used",
             IrepId::CSpecLoopInvariant => "#spec_loop_invariant",
+            IrepId::CSpecDecreases => "#spec_decreases",
             IrepId::CSpecRequires => "#spec_requires",
             IrepId::CSpecEnsures => "#spec_ensures",
             IrepId::CSpecAssigns => "#spec_assigns",
diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs
index cd263e2a3c9f..05e95eb777f1 100644
--- a/cprover_bindings/src/irep/to_irep.rs
+++ b/cprover_bindings/src/irep/to_irep.rs
@@ -556,7 +556,7 @@ impl ToIrep for StmtBody {
                     arguments_irep(arguments.iter(), mm),
                 ],
             ),
-            StmtBody::Goto { dest, loop_invariants, loop_modifies } => {
+            StmtBody::Goto { dest, loop_invariants, loop_modifies, loop_decreases } => {
                 let inv = loop_invariants
                     .clone()
                     .map(|inv| inv.clone().and(Expr::bool_true()).to_irep(mm));
@@ -565,10 +565,12 @@ impl ToIrep for StmtBody {
                         assigns.iter().map(|assign| assign.to_irep(mm)).collect(),
                     )])
                 });
+                let decreases = loop_decreases.clone().map(|dec| dec.to_irep(mm));
                 code_irep(IrepId::Goto, vec![])
                     .with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string()))
                     .with_named_sub_option(IrepId::CSpecLoopInvariant, inv)
                     .with_named_sub_option(IrepId::CSpecAssigns, assigns.clone())
+                    .with_named_sub_option(IrepId::CSpecDecreases, decreases)
             }
             StmtBody::Ifthenelse { i, t, e } => code_irep(
                 IrepId::Ifthenelse,
diff --git a/docs/src/reference/attributes.md b/docs/src/reference/attributes.md
index 53f8fb16879b..1bae1e6b9e69 100644
--- a/docs/src/reference/attributes.md
+++ b/docs/src/reference/attributes.md
@@ -248,6 +248,6 @@ There are numerous attributes for function and loop contracts. At present, these
 - Proof harness for contracts: `#[kani::proof_for_contract(name-of-function)]`
 - Verified stubbing: `#[kani::stub_verified]`
 - Function contract specification: `#[kani::requires]`, `#[kani::modifies]`, `#[kani::ensures]`, `#[kani::recursion]`
-- Loop contract specification: `#[kani::loop_invariant]`, `#[kani::loop_modifies]`.
+- Loop contract specification: `#[kani::loop_invariant]`, `#[kani::loop_modifies]`, `#[kani::loop_decreases]`.
 
 See the documentation on [function contracts](./experimental/contracts.md) and [loop contracts](./experimental/loop-contracts.md) for details.
diff --git a/docs/src/reference/experimental/loop-contracts.md b/docs/src/reference/experimental/loop-contracts.md
index b37ae6c10332..7e46ed5c8924 100644
--- a/docs/src/reference/experimental/loop-contracts.md
+++ b/docs/src/reference/experimental/loop-contracts.md
@@ -142,6 +142,29 @@ In proof path 1, we prove properties inside the loop and at last check that the
 In proof path 2, we prove properties after leaving the loop. As we leave the loop only when the loop guard is violated, the post condition of the loop can be expressed as
 `!guard && inv`, which is `x <= 1 && x >= 1` in the example. The postcondition implies `x == 1`—the property we want to prove at the end of `simple_loop_with_loop_contracts`.
 
+### Partial correctness vs. total correctness
+
+The verification steps above establish what is known as *partial correctness*: **if** the loop
+terminates, the result is correct. This is the standard guarantee provided by loop invariants alone.
+
+To establish *total correctness* — that the loop both terminates **and** produces the correct
+result — you additionally need a [decreases clause](#decreases-clauses-termination-proofs) that
+proves the loop makes progress toward termination on every iteration.
+
+In formal terms, the four steps of a complete loop correctness argument are:
+
+1. **Establishment** (base case): The invariant holds before the first iteration.
+2. **Preservation** (inductive step): If the invariant and the loop guard both hold at the start of
+   an iteration, the invariant still holds at the end of that iteration.
+3. **Postcondition**: When the loop exits (guard is false) and the invariant holds, the desired
+   result follows.
+4. **Termination**: A *variant* (also called *decrementing function* or *ranking function*) strictly
+   decreases on every iteration and is bounded from below, guaranteeing the loop eventually exits.
+
+Kani checks steps 1–3 automatically via `#[kani::loop_invariant]`. Step 4 is checked when you add
+`#[kani::loop_decreases]`. Without step 4, Kani's proofs are *partial* — they are sound assuming
+the loop terminates, but cannot rule out non-termination.
+
 ## Historic values and extra variables
 
 ### Historic values
@@ -276,6 +299,287 @@ fn main() {
 }
 ```
 
+## Decreases clauses (Termination proofs)
+
+### Why termination matters
+
+Without a proof of termination, Kani may successfully verify properties that are actually unreachable
+due to non-terminating loops. For example:
+
+```Rust
+#[kani::proof]
+fn unsound_without_termination() {
+    let mut x: u64 = kani::any_where(|i| *i >= 1);
+
+    #[kani::loop_invariant(x >= 1)]
+    while true {
+        x = x;  // infinite loop — x never changes
+    }
+
+    // This assertion is "proved" because the loop abstraction
+    // assumes we exit the loop, but we never actually do.
+    assert!(x >= 1);
+}
+```
+
+After abstracting the loop, the assertion appears to hold. But the loop never terminates, so the
+assertion is unreachable. A decreases clause prevents this class of unsound results by requiring
+the user to prove that the loop makes progress toward termination.
+
+### Background: Floyd's method
+
+The technique used here was proposed by Robert Floyd in his seminal 1967 paper
+[*Assigning Meaning to Programs*](https://people.eecs.berkeley.edu/~necula/Papers/FloydMeaning.pdf).
+The idea is to find a *variant* (also called a *ranking function* or *termination measure*) — a
+value that:
+
+1. Is bounded from below (e.g., non-negative integers), and
+2. Strictly decreases at each iteration of the loop.
+
+Since the value cannot decrease forever (it must eventually hit the lower bound), the loop must terminate.
+
+### Syntax
+
+```
+#[kani::loop_decreases(expr)]
+#[kani::loop_decreases(expr1, expr2, ..., exprN)]
+```
+
+The decreases clause accepts one or more arithmetic expressions over the variables visible at the
+same scope as the loop. It must be placed alongside the loop invariant, before the loop expression.
+
+Multiple expressions form an ordered tuple compared using
+[lexicographic ordering](https://en.wikipedia.org/wiki/Lexicographic_order) (see below).
+
+### Basic example
+
+```Rust
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+fn simple_decreases() {
+    let mut x: u8 = kani::any_where(|i| *i >= 1);
+
+    #[kani::loop_invariant(x >= 1)]
+    #[kani::loop_decreases(x)]
+    while x > 1 {
+        x = x - 1;
+    }
+
+    assert!(x == 1);
+}
+```
+
+Here, `x` strictly decreases at each iteration and is bounded below by `1` (the loop guard ensures
+`x > 1`), so the loop must terminate.
+
+### Multi-dimensional decreases (lexicographic ordering)
+
+> **Note:** Multi-dimensional decreases clauses are not yet fully supported. The syntax is
+> accepted, but CBMC does not correctly process tuple expressions passed through Kani's irep
+> encoding. This is tracked as a [known bug](#decreases-clause-limitations-and-comparison-with-other-tools).
+> Use a single integer expression for now.
+
+Some loops cannot be proved terminating with a single expression. For example, a loop with two
+counters where the inner counter resets may need a tuple `(outer, inner)`. CBMC compares tuples
+lexicographically: if the first element decreases, the remaining elements are free to increase or
+stay the same. Only if the first element stays the same must the second element decrease, and so on.
+
+This is the same principle used to prove termination of the
+[Ackermann function](https://en.wikipedia.org/wiki/Ackermann_function), which requires a
+two-dimensional decreases clause `(m, n)`.
+
+```Rust
+#[kani::proof]
+fn nested_counters() {
+    let n: u8 = kani::any_where(|i| *i >= 1 && *i <= 5);
+    let mut i: u8 = 0;
+    let mut j: u8 = 0;
+
+    #[kani::loop_invariant(i <= n && j <= n)]
+    #[kani::loop_decreases(n - i, n - j)]
+    while i < n {
+        if j < n {
+            j += 1;
+        } else {
+            i += 1;
+            j = 0;
+        }
+    }
+
+    assert!(i == n);
+}
+```
+
+When `j < n`, the first component `n - i` stays the same but the second component `n - j` decreases.
+When `j >= n`, the first component `n - i` decreases (and `n - j` resets — which is fine because
+the first component already decreased).
+
+### Semantics
+
+The decreases clause is checked by CBMC's `goto-instrument` through the following instrumentation:
+
+1. At the beginning of the loop body (after the loop guard is satisfied), the current value of the
+   measure is recorded in a temporary variable (`old_measure`).
+2. At the end of the loop body (before the back-edge), the new value of the measure is recorded
+   (`new_measure`).
+3. An assertion checks that `new_measure < old_measure` (strict decrease).
+
+For multi-dimensional decreases `(e1, e2, ..., en)`, the strict arithmetic comparison is extended
+to a strict lexicographic comparison: the tuple `(new_e1, ..., new_en)` must be lexicographically
+less than `(old_e1, ..., old_en)`.
+
+Note that CBMC does not require the measure to be non-negative at all times. It only requires that
+the loop does not execute again when the measure would go below zero. In other words, if the measure
+becomes negative but the loop guard is false, that is acceptable.
+
+### Interaction with loop invariants
+
+Decreases clauses work in conjunction with loop invariant clauses. The invariant establishes the
+context (the inductive hypothesis) under which the decreases check is performed. If a decreases
+clause is annotated on a loop without an invariant clause, the weakest possible invariant (`true`)
+is used to model an arbitrary iteration.
+
+In practice, you almost always want both: the invariant constrains the state space, and the
+decreases clause proves progress within that constrained space.
+
+### Decreases clause limitations and comparison with other tools
+
+The following limitations apply to decreases clauses in Kani. We compare with
+[Dafny](https://dafny.org/latest/OnlineTutorial/Termination) and
+[Verus](https://verus-lang.github.io/verus/guide/) to provide context.
+
+1. **Integer-only measures.** Kani (via CBMC) only supports integer-typed expressions in decreases
+   clauses. Dafny additionally supports sequences (compared by length), sets (compared by strict
+   subset inclusion), booleans, and references as termination measures. Verus similarly supports
+   richer types. In Kani, if you need to use a non-integer measure, you must manually map it to an
+   integer expression (e.g., use `slice.len() - i` instead of the slice itself).
+
+2. **No automatic inference.** Kani does not automatically guess a decreases clause. Dafny
+   automatically infers `B - A` when it sees a loop guard of the form `A < B`, and infers parameter
+   decreases for simple recursive functions. In Kani, the user must always provide an explicit
+   decreases clause.
+
+3. **No recursive function termination.** Kani's decreases clauses only apply to loops, not to
+   recursive functions. CBMC itself does not support termination proofs for recursion (as noted in
+   CBMC PR [#6236](https://github.com/diffblue/cbmc/pull/6236)). Dafny and Verus both support
+   `decreases` annotations on recursive and mutually recursive functions. In Kani, recursive
+   functions must be handled by other means (e.g., unwinding bounds).
+
+4. **No `decreases *` escape hatch.** Dafny provides `decreases *` to explicitly opt out of
+   termination checking for loops or functions where termination is unknown or intentionally
+   absent (e.g., the Collatz conjecture, stream processors). Kani has no equivalent — if you
+   cannot prove termination, simply omit the decreases clause. The loop will still be abstracted
+   by the invariant, but without a termination guarantee.
+
+5. **No side-effect checking.** Kani does not verify that decreases clause expressions are
+   side-effect free. A decreases clause with side effects (e.g., mutation of variables) could lead
+   to unsound results. The user must ensure the expression is pure.
+
+6. **Strict decrease only.** CBMC checks `new_measure < old_measure` using strict integer
+   comparison. There is no support for custom well-founded orderings or user-defined comparison
+   operators. The measure must map to integer arithmetic.
+
+## Worked example: Binary search
+
+Binary search is a classic algorithm that is deceptively tricky to get right. It is an excellent
+case study for loop contracts because the invariant, postcondition, and termination argument are
+all non-trivial and interdependent.
+
+```Rust
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+fn binary_search(arr: &[i32; 5], target: i32) -> Option<usize> {
+    let mut lo: usize = 0;
+    let mut hi: usize = arr.len();
+
+    #[kani::loop_invariant(lo <= hi && hi <= arr.len())]
+    #[kani::loop_decreases(hi - lo)]
+    while lo < hi {
+        let mid = lo + (hi - lo) / 2;
+        if arr[mid] == target {
+            return Some(mid);
+        } else if arr[mid] < target {
+            lo = mid + 1;
+        } else {
+            hi = mid;
+        }
+    }
+
+    None
+}
+```
+
+Let's walk through the four correctness steps:
+
+**1. Establishment.** Initially `lo = 0` and `hi = arr.len()`, so `0 <= lo <= hi <= arr.len()`
+holds trivially.
+
+**2. Preservation.** We need to show that if `lo <= hi <= arr.len()` and `lo < hi` (the guard),
+then after the loop body, the invariant still holds. The key insight is that
+`mid = lo + (hi - lo) / 2`, so `lo <= mid < hi`. In the `arr[mid] < target` branch, `lo` becomes
+`mid + 1`, which is at most `hi`. In the `arr[mid] >= target` branch, `hi` becomes `mid`, which is
+at least `lo`. Either way, `lo <= hi <= arr.len()` is preserved.
+
+**3. Postcondition.** When the loop exits, `lo >= hi`. Combined with the invariant `lo <= hi`, we
+get `lo == hi`. If the target was not found via early return, the search space is empty.
+
+**4. Termination.** The decreases clause is `hi - lo`. The invariant guarantees this is
+non-negative. In each branch, either `lo` increases (to `mid + 1 > lo`) or `hi` decreases (to
+`mid < hi`). Either way, `hi - lo` strictly decreases. Note how the termination argument *depends
+on the invariant* — without knowing `lo <= hi`, we couldn't guarantee the measure is non-negative.
+
+This example illustrates a general principle: the invariant and the decreases clause work together.
+The invariant constrains the state space, and the decreases clause proves progress within that
+constrained space.
+
+## Practical guidance
+
+### Choosing a loop invariant
+
+A loop invariant captures the core reason why the loop works. Think of it as an explanation of the
+loop's progress that holds at every iteration boundary. A good approach:
+
+- **Start from the postcondition.** What do you need to be true when the loop exits? The invariant
+  should generalize this to any intermediate iteration.
+- **Include bounds.** Almost every loop invariant needs bounds on the loop variable
+  (e.g., `i <= n`). Without bounds, Kani's havoc step can assign arbitrary values.
+- **Include the relationship between variables.** If the loop maintains a relationship between
+  variables (e.g., `sum == a[0] + a[1] + ... + a[i-1]`), that relationship belongs in the
+  invariant.
+
+### Common mistakes
+
+**Invariant too weak.** This is the most common error. Symptoms:
+- The *postcondition step* fails: Kani reports a failing assertion after the loop, because the
+  invariant combined with `!guard` is not strong enough to imply the desired property.
+- The *preservation step* fails: the invariant doesn't constrain the state enough to prove itself
+  inductive.
+
+**Invariant too strong.** Symptoms:
+- The *establishment step* fails: the invariant doesn't hold before the first iteration.
+- The *preservation step* fails: the loop body cannot maintain the overly strong condition.
+
+**Wrong decreases clause.** Symptoms:
+- Kani reports `FAILURE` on `"Check variant decreases after step for loop"`. This means the
+  measure did not strictly decrease on some iteration. Common causes:
+  - The measure doesn't capture the right quantity (e.g., using `i` when you should use `n - i`).
+  - The loop body has a path that doesn't make progress (e.g., a `continue` without modifying the
+    measure).
+  - The measure is a constant expression.
+
+### Tips for decreases clauses
+
+- For `while i < n` loops that increment `i`, the natural measure is `n - i`.
+- For `while x > 0` loops that decrement `x`, the natural measure is `x`.
+- For nested loops, each loop needs its own decreases clause. The inner loop's measure must
+  decrease independently of the outer loop.
+- If a single expression doesn't work, try a multi-dimensional decreases clause. Think about which
+  variable decreases "most of the time" (put it first) and which decreases "within" the first
+  (put it second).
+
 ## Limitations
 
 Loop contracts comes with the following limitations.
@@ -284,6 +588,12 @@ Loop contracts comes with the following limitations.
 2. Kani infers *loop modifies* with alias analysis. Loop modifies are those variables we assume to be arbitrary in the inductive hypothesis, and should cover all memory locations that are written to during 
    the execution of the loops. A proof will fail if the inferred loop modifies misses some targets written in the loops.
    We observed this happens when some fields of structs are modified by some other functions called in the loops.
-3. Kani doesn't check if a loop will always terminate in proofs with loop contracts. So it could be that some properties are proved successfully with Kani but actually are unreachable due to the 
-   non-termination of some loops.
-4. We don't check if loop contracts are side-effect free. A loop contract with a side effect could lead to an unsound proof result. Make sure that the specified loop contracts are side-effect free.
+3. We don't check if loop contracts (invariants, decreases clauses) are side-effect free. A loop contract with a side effect could lead to an unsound proof result. Make sure that the specified loop contracts are side-effect free.
+4. Decreases clauses only support integer-typed expressions. See the [decreases clause limitations](#decreases-clause-limitations-and-comparison-with-other-tools) section for a detailed comparison with other verification tools.
+5. Decreases clauses have the following known bugs (tracked in [#3168](https://github.com/model-checking/kani/issues/3168)):
+   - **Struct field projections** in decreases expressions (e.g., `#[kani::loop_decreases(s.field)]`) are not correctly processed by CBMC — the check always fails even when the measure genuinely decreases.
+   - **Multi-dimensional decreases** (e.g., `#[kani::loop_decreases(a, b)]`) are not correctly processed — CBMC does not perform lexicographic comparison on tuple expressions passed through Kani's irep encoding.
+   - **Combining `loop_decreases` with `loop_modifies`** causes the assigns clause check to conflict with the decreases instrumentation.
+   - **Nested loops with decreases** on both inner and outer loops can cause assigns clause conflicts.
+   
+   These limitations are documented as `fixme` tests in `tests/expected/loop-contract/`.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index b38f30e58cce..9704c8775c2e 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -97,6 +97,11 @@ impl GotocCtx<'_, '_> {
                     self.current_loop_modifies = assigns.clone();
                     return Stmt::skip(location);
                 }
+                if localname.contains("kani_loop_decreases") {
+                    let decreases_expr = self.codegen_rvalue_stable(rhs, location);
+                    self.current_loop_decreases = Some(decreases_expr);
+                    return Stmt::skip(location);
+                }
                 // we ignore assignment for all zero size types
                 if self.is_zst_stable(lty) {
                     Stmt::skip(location)
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
index a1e807ee4d28..8661e8729b95 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -96,6 +96,8 @@ pub struct GotocCtx<'tcx, 'r> {
     pub has_loop_contracts: bool,
     /// Track loop assign clause
     pub current_loop_modifies: Vec<Expr>,
+    /// Track loop decreases clause
+    pub current_loop_decreases: Option<Expr>,
 }
 
 /// Constructor
@@ -127,6 +129,7 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
             transformer,
             has_loop_contracts: false,
             current_loop_modifies: Vec::new(),
+            current_loop_decreases: None,
         }
     }
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
index 0c2bb7cce679..4a84a79c8059 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -851,6 +851,9 @@ impl GotocHook for LoopInvariantRegister {
                 stmt = stmt.with_loop_modifies(assigns.clone());
                 gcx.current_loop_modifies.clear();
             }
+            if let Some(decreases) = gcx.current_loop_decreases.take() {
+                stmt = stmt.with_loop_decreases(decreases);
+            }
 
             // Add `free(0)` to make sure the body of `free` won't be dropped to
             // satisfy the requirement of DFCC.
@@ -867,6 +870,9 @@ impl GotocHook for LoopInvariantRegister {
             // When loop-contracts is not enabled, codegen
             // assign_to = true
             // goto target
+            // Discard any decreases clause since it won't be checked without
+            // the loop-contracts flag.
+            gcx.current_loop_decreases = None;
             Stmt::block(
                 vec![
                     unwrap_or_return_codegen_unimplemented_stmt!(
diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs
index 9ceed99d114b..fb8a75f63ff6 100644
--- a/library/kani_macros/src/lib.rs
+++ b/library/kani_macros/src/lib.rs
@@ -444,6 +444,11 @@ pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream {
 pub fn loop_modifies(attr: TokenStream, item: TokenStream) -> TokenStream {
     attr_impl::loop_modifies(attr, item)
 }
+
+#[proc_macro_attribute]
+pub fn loop_decreases(attr: TokenStream, item: TokenStream) -> TokenStream {
+    attr_impl::loop_decreases(attr, item)
+}
 /// This module implements Kani attributes in a way that only Kani's compiler can understand.
 /// This code should only be activated when pre-building Kani's sysroot.
 #[cfg(kani_sysroot)]
@@ -454,7 +459,7 @@ mod sysroot {
     mod loop_contracts;
 
     pub use contracts::{ensures, modifies, proof_for_contract, requires, stub_verified};
-    pub use loop_contracts::{loop_invariant, loop_modifies};
+    pub use loop_contracts::{loop_decreases, loop_invariant, loop_modifies};
 
     use super::*;
 
@@ -634,4 +639,5 @@ mod regular {
     no_op!(stub_verified);
     no_op!(loop_invariant);
     no_op!(loop_modifies);
+    no_op!(loop_decreases);
 }
diff --git a/library/kani_macros/src/sysroot/loop_contracts/mod.rs b/library/kani_macros/src/sysroot/loop_contracts/mod.rs
index 2b0f0d54ba1e..5c927f403fa8 100644
--- a/library/kani_macros/src/sysroot/loop_contracts/mod.rs
+++ b/library/kani_macros/src/sysroot/loop_contracts/mod.rs
@@ -722,3 +722,32 @@ pub fn loop_modifies(attr: TokenStream, item: TokenStream) -> TokenStream {
     .into();
     ret
 }
+
+/// Implements the `#[kani::loop_decreases(expr1, expr2, ...)]` attribute.
+///
+/// A decreases clause specifies a measure that must strictly decrease at every
+/// iteration of a loop, proving termination. The macro creates a local binding
+/// `let kani_loop_decreases = (expr1, expr2, ...);` which the compiler detects
+/// during codegen and attaches to the loop's goto statement as a CBMC
+/// `#spec_decreases` annotation. CBMC's `goto-instrument` then instruments the
+/// termination check (record old value → execute body → assert new < old).
+///
+/// For multi-dimensional decreases, CBMC uses lexicographic ordering.
+pub fn loop_decreases(attr: TokenStream, item: TokenStream) -> TokenStream {
+    let decreases = parse_macro_input!(attr with Punctuated::<Expr, Token![,]>::parse_terminated)
+        .into_iter()
+        .collect::<Vec<Expr>>();
+    let loop_decreases_name: String = "kani_loop_decreases".to_owned();
+    let loop_decreases_ident = format_ident!("{}", loop_decreases_name);
+    let loop_decreases_stmt: Stmt = parse_quote! {
+        let #loop_decreases_ident = (#(#decreases),*);
+    };
+    let loop_stmt: Stmt = syn::parse(item.clone()).unwrap();
+    let ret: TokenStream = quote!(
+    {
+        #loop_decreases_stmt
+        #loop_stmt
+    })
+    .into();
+    ret
+}
diff --git a/tests/expected/loop-contract/decreases_binary_search.expected b/tests/expected/loop-contract/decreases_binary_search.expected
new file mode 100644
index 000000000000..34c886c358cb
--- /dev/null
+++ b/tests/expected/loop-contract/decreases_binary_search.expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/loop-contract/decreases_binary_search.rs b/tests/expected/loop-contract/decreases_binary_search.rs
new file mode 100644
index 000000000000..93ebb867a361
--- /dev/null
+++ b/tests/expected/loop-contract/decreases_binary_search.rs
@@ -0,0 +1,37 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! Binary search with decreases clause.
+//! Inspired by CBMC's binary_search example in contracts-decreases documentation.
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+fn binary_search(arr: &[i32; 5], target: i32) -> Option<usize> {
+    let mut lo: usize = 0;
+    let mut hi: usize = arr.len();
+
+    #[kani::loop_invariant(lo <= hi && hi <= arr.len())]
+    #[kani::loop_decreases(hi - lo)]
+    while lo < hi {
+        let mid = lo + (hi - lo) / 2;
+        if arr[mid] == target {
+            return Some(mid);
+        } else if arr[mid] < target {
+            lo = mid + 1;
+        } else {
+            hi = mid;
+        }
+    }
+
+    None
+}
+
+#[kani::proof]
+fn binary_search_harness() {
+    let arr = [1, 3, 5, 7, 9];
+    let result = binary_search(&arr, 5);
+    assert!(result == Some(2));
+}
diff --git a/tests/expected/loop-contract/decreases_expr.expected b/tests/expected/loop-contract/decreases_expr.expected
new file mode 100644
index 000000000000..34c886c358cb
--- /dev/null
+++ b/tests/expected/loop-contract/decreases_expr.expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/loop-contract/decreases_expr.rs b/tests/expected/loop-contract/decreases_expr.rs
new file mode 100644
index 000000000000..b39cdb1819db
--- /dev/null
+++ b/tests/expected/loop-contract/decreases_expr.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! Check decreases clause with a simple variable measure.
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+fn decreases_expr_harness() {
+    let mut x: u8 = kani::any_where(|i| *i >= 1 && *i <= 10);
+
+    #[kani::loop_invariant(x >= 1)]
+    #[kani::loop_decreases(x)]
+    while x > 1 {
+        x -= 1;
+    }
+
+    assert!(x == 1);
+}
diff --git a/tests/expected/loop-contract/decreases_fail_stale_measure.expected b/tests/expected/loop-contract/decreases_fail_stale_measure.expected
new file mode 100644
index 000000000000..a89ec00c6211
--- /dev/null
+++ b/tests/expected/loop-contract/decreases_fail_stale_measure.expected
@@ -0,0 +1,3 @@
+Status: FAILURE
+
+VERIFICATION:- FAILED
diff --git a/tests/expected/loop-contract/decreases_fail_stale_measure.rs b/tests/expected/loop-contract/decreases_fail_stale_measure.rs
new file mode 100644
index 000000000000..57f95ce2a0d1
--- /dev/null
+++ b/tests/expected/loop-contract/decreases_fail_stale_measure.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! Check that a stale measure (one that doesn't change) fails verification.
+//! The loop body modifies x but the decreases clause uses a different
+//! variable y that is never modified, so the measure is stale.
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+fn stale_measure_harness() {
+    let mut x: u16 = kani::any_where(|i| *i >= 2 && *i <= 100);
+    let y: u16 = x;
+
+    #[kani::loop_invariant(x >= 2)]
+    #[kani::loop_decreases(y)]
+    while x > 1 {
+        // x decreases, but the measure (y) never changes.
+        x = x - 1;
+    }
+}
diff --git a/tests/expected/loop-contract/decreases_fail_wrong_measure.expected b/tests/expected/loop-contract/decreases_fail_wrong_measure.expected
new file mode 100644
index 000000000000..a89ec00c6211
--- /dev/null
+++ b/tests/expected/loop-contract/decreases_fail_wrong_measure.expected
@@ -0,0 +1,3 @@
+Status: FAILURE
+
+VERIFICATION:- FAILED
diff --git a/tests/expected/loop-contract/decreases_fail_wrong_measure.rs b/tests/expected/loop-contract/decreases_fail_wrong_measure.rs
new file mode 100644
index 000000000000..92554d5b5398
--- /dev/null
+++ b/tests/expected/loop-contract/decreases_fail_wrong_measure.rs
@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! Check that a wrong decreases expression fails verification.
+//! The measure increases instead of decreasing.
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+fn wrong_decreases_harness() {
+    let mut x: u16 = kani::any_where(|i| *i >= 2 && *i <= 200);
+
+    #[kani::loop_invariant(x >= 2)]
+    #[kani::loop_decreases(x)]
+    while x > 1 {
+        // Bug: x increases instead of decreasing.
+        // Using u16 to avoid overflow obscuring the decreases failure.
+        x = x + 1;
+    }
+}
diff --git a/tests/expected/loop-contract/decreases_loop_max.expected b/tests/expected/loop-contract/decreases_loop_max.expected
new file mode 100644
index 000000000000..34c886c358cb
--- /dev/null
+++ b/tests/expected/loop-contract/decreases_loop_max.expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/loop-contract/decreases_loop_max.rs b/tests/expected/loop-contract/decreases_loop_max.rs
new file mode 100644
index 000000000000..062d6c291711
--- /dev/null
+++ b/tests/expected/loop-contract/decreases_loop_max.rs
@@ -0,0 +1,35 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! Loop max function with decreases clause.
+//! Inspired by Prusti's loop_max.rs test.
+//! Uses a countdown variable to avoid unsigned subtraction in the measure.
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+fn loop_max(x: u8, y: u8) -> u8 {
+    let mut r = x;
+    let mut remaining: u8 = y - x;
+
+    #[kani::loop_invariant(x <= r && r <= y && remaining == y - r)]
+    #[kani::loop_decreases(remaining)]
+    while r < y {
+        r += 1;
+        remaining -= 1;
+    }
+
+    r
+}
+
+#[kani::proof]
+fn loop_max_harness() {
+    let x: u8 = kani::any_where(|i| *i > 0 && *i < 100);
+    let y: u8 = kani::any_where(|i| *i > 0 && *i < 100);
+    kani::assume(x <= y);
+    let result = loop_max(x, y);
+    assert!(result >= x);
+    assert!(result >= y);
+}
diff --git a/tests/expected/loop-contract/decreases_with_function_contract.expected b/tests/expected/loop-contract/decreases_with_function_contract.expected
new file mode 100644
index 000000000000..34c886c358cb
--- /dev/null
+++ b/tests/expected/loop-contract/decreases_with_function_contract.expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/loop-contract/decreases_with_function_contract.rs b/tests/expected/loop-contract/decreases_with_function_contract.rs
new file mode 100644
index 000000000000..30a2b50f2870
--- /dev/null
+++ b/tests/expected/loop-contract/decreases_with_function_contract.rs
@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts -Z function-contracts
+
+//! Check decreases clause combined with function contracts.
+
+#![feature(proc_macro_hygiene)]
+#![feature(stmt_expr_attributes)]
+
+#[kani::requires(i >= 2)]
+#[kani::ensures(|ret| *ret == 2)]
+pub fn has_loop_with_decreases(mut i: u16) -> u16 {
+    #[kani::loop_invariant(i >= 2)]
+    #[kani::loop_decreases(i)]
+    while i > 2 {
+        i = i - 1;
+    }
+    i
+}
+
+#[kani::proof_for_contract(has_loop_with_decreases)]
+fn contract_proof() {
+    let i: u16 = kani::any();
+    let j = has_loop_with_decreases(i);
+}
diff --git a/tests/expected/loop-contract/decreases_with_old.expected b/tests/expected/loop-contract/decreases_with_old.expected
new file mode 100644
index 000000000000..34c886c358cb
--- /dev/null
+++ b/tests/expected/loop-contract/decreases_with_old.expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/loop-contract/decreases_with_old.rs b/tests/expected/loop-contract/decreases_with_old.rs
new file mode 100644
index 000000000000..61f96d3a944a
--- /dev/null
+++ b/tests/expected/loop-contract/decreases_with_old.rs
@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! Check decreases clause combined with on_entry (old) values.
+//! Inspired by Verus test_variables_not_havoc_basic.
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+fn decreases_with_old_harness() {
+    let mut x: u8 = kani::any_where(|i| *i >= 1 && *i <= 20);
+    let y: u8 = 42;
+
+    #[kani::loop_invariant(x >= 1 && on_entry(x) >= 1)]
+    #[kani::loop_decreases(x)]
+    while x > 1 {
+        x -= 1;
+    }
+
+    assert!(x == 1);
+    // y should not be havocked
+    assert!(y == 42);
+}
diff --git a/tests/expected/loop-contract/fixme_decreases_struct_field.expected b/tests/expected/loop-contract/fixme_decreases_struct_field.expected
new file mode 100644
index 000000000000..6c054dd6d82f
--- /dev/null
+++ b/tests/expected/loop-contract/fixme_decreases_struct_field.expected
@@ -0,0 +1,4 @@
+loop_decreases.1\
+	 - Status: FAILURE
+
+VERIFICATION:- FAILED
diff --git a/tests/expected/loop-contract/fixme_decreases_struct_field.rs b/tests/expected/loop-contract/fixme_decreases_struct_field.rs
new file mode 100644
index 000000000000..6f4532d6c526
--- /dev/null
+++ b/tests/expected/loop-contract/fixme_decreases_struct_field.rs
@@ -0,0 +1,29 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! FIXME: CBMC silently ignores struct field projections in decreases clauses.
+//! The `#spec_decreases` irep is emitted but goto-instrument does not process
+//! complex types — only simple integer variables/expressions are supported.
+//! Tracked in: https://github.com/model-checking/kani/issues/3168
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+struct Counter {
+    val: u8,
+}
+
+#[kani::proof]
+fn fixme_decreases_struct_field_harness() {
+    let mut c = Counter { val: kani::any_where(|i| *i >= 1 && *i <= 20) };
+
+    #[kani::loop_invariant(c.val >= 1)]
+    #[kani::loop_decreases(c.val)]
+    while c.val > 1 {
+        c.val -= 1;
+    }
+
+    assert!(c.val == 1);
+}
diff --git a/tests/expected/loop-contract/fixme_decreases_with_modifies.expected b/tests/expected/loop-contract/fixme_decreases_with_modifies.expected
new file mode 100644
index 000000000000..6c054dd6d82f
--- /dev/null
+++ b/tests/expected/loop-contract/fixme_decreases_with_modifies.expected
@@ -0,0 +1,4 @@
+loop_decreases.1\
+	 - Status: FAILURE
+
+VERIFICATION:- FAILED
diff --git a/tests/expected/loop-contract/fixme_decreases_with_modifies.rs b/tests/expected/loop-contract/fixme_decreases_with_modifies.rs
new file mode 100644
index 000000000000..ddca9ee665f3
--- /dev/null
+++ b/tests/expected/loop-contract/fixme_decreases_with_modifies.rs
@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! FIXME: Decreases clause combined with loop_modifies fails because the
+//! assigns clause checking conflicts with the decreases instrumentation.
+//! Tracked in: https://github.com/model-checking/kani/issues/3168
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+fn fixme_decreases_with_modifies_harness() {
+    let mut i: u8 = 0;
+    let mut a: [u8; 5] = [0; 5];
+
+    #[kani::loop_invariant(i <= 5)]
+    #[kani::loop_modifies(&i, &a)]
+    #[kani::loop_decreases(5 - i)]
+    while i < 5 {
+        a[i as usize] = 1;
+        i += 1;
+    }
+
+    assert!(i == 5);
+}
diff --git a/tests/expected/loop-contract/fixme_multi_dim_decreases.expected b/tests/expected/loop-contract/fixme_multi_dim_decreases.expected
new file mode 100644
index 000000000000..6c054dd6d82f
--- /dev/null
+++ b/tests/expected/loop-contract/fixme_multi_dim_decreases.expected
@@ -0,0 +1,4 @@
+loop_decreases.1\
+	 - Status: FAILURE
+
+VERIFICATION:- FAILED
diff --git a/tests/expected/loop-contract/fixme_multi_dim_decreases.rs b/tests/expected/loop-contract/fixme_multi_dim_decreases.rs
new file mode 100644
index 000000000000..7851137a5d5c
--- /dev/null
+++ b/tests/expected/loop-contract/fixme_multi_dim_decreases.rs
@@ -0,0 +1,33 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! FIXME: CBMC does not support multi-dimensional (tuple) decreases clauses
+//! when passed through Kani's `#spec_decreases` irep annotation. The tuple
+//! expression is emitted but goto-instrument does not perform lexicographic
+//! comparison on it — only single integer expressions work.
+//! Tracked in: https://github.com/model-checking/kani/issues/3168
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+fn fixme_multi_dim_decreases_harness() {
+    let n: u8 = kani::any_where(|i| *i >= 1 && *i <= 5);
+    let mut i: u8 = 0;
+    let mut j: u8 = 0;
+
+    #[kani::loop_invariant(i <= n && j <= n)]
+    #[kani::loop_decreases(n - i, n - j)]
+    while i < n {
+        if j < n {
+            j += 1;
+        } else {
+            i += 1;
+            j = 0;
+        }
+    }
+
+    assert!(i == n);
+}
diff --git a/tests/expected/loop-contract/fixme_nested_loops_decreases.expected b/tests/expected/loop-contract/fixme_nested_loops_decreases.expected
new file mode 100644
index 000000000000..a89ec00c6211
--- /dev/null
+++ b/tests/expected/loop-contract/fixme_nested_loops_decreases.expected
@@ -0,0 +1,3 @@
+Status: FAILURE
+
+VERIFICATION:- FAILED
diff --git a/tests/expected/loop-contract/fixme_nested_loops_decreases.rs b/tests/expected/loop-contract/fixme_nested_loops_decreases.rs
new file mode 100644
index 000000000000..483d146e3700
--- /dev/null
+++ b/tests/expected/loop-contract/fixme_nested_loops_decreases.rs
@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! FIXME: Nested loops with decreases clauses fail because the inner loop's
+//! assigns clause checking conflicts with the outer loop's instrumentation.
+//! Tracked in: https://github.com/model-checking/kani/issues/3168
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+fn fixme_nested_loops_decreases_harness() {
+    let mut i: u8 = 10;
+    let mut j: u8;
+
+    #[kani::loop_invariant(i <= 10)]
+    #[kani::loop_decreases(i)]
+    while i > 0 {
+        j = 5;
+        #[kani::loop_invariant(j <= 5)]
+        #[kani::loop_decreases(j)]
+        while j > 0 {
+            j -= 1;
+        }
+        i -= 1;
+    }
+
+    assert!(i == 0);
+}
diff --git a/tests/expected/loop-contract/loop_loop_decreases.expected b/tests/expected/loop-contract/loop_loop_decreases.expected
new file mode 100644
index 000000000000..34c886c358cb
--- /dev/null
+++ b/tests/expected/loop-contract/loop_loop_decreases.expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/loop-contract/loop_loop_decreases.rs b/tests/expected/loop-contract/loop_loop_decreases.rs
new file mode 100644
index 000000000000..ab990656ce7d
--- /dev/null
+++ b/tests/expected/loop-contract/loop_loop_decreases.rs
@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! Check decreases clause on a loop that counts down by 2.
+//! Note: This was originally a `loop { break }` test, but `loop` with
+//! decreases triggers an internal unreachable in the loop contract
+//! transformation. Rewritten as `while` as a workaround.
+//! Tracked in: https://github.com/model-checking/kani/issues/3168
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+fn loop_loop_decreases_harness() {
+    let mut i: u8 = 100;
+
+    #[kani::loop_invariant(i <= 100 && i >= 2 && i % 2 == 0)]
+    #[kani::loop_decreases(i)]
+    while i != 2 {
+        i = i - 2;
+    }
+
+    assert!(i == 2);
+}
diff --git a/tests/expected/loop-contract/simple_while_loop_decreases.expected b/tests/expected/loop-contract/simple_while_loop_decreases.expected
new file mode 100644
index 000000000000..34c886c358cb
--- /dev/null
+++ b/tests/expected/loop-contract/simple_while_loop_decreases.expected
@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/loop-contract/simple_while_loop_decreases.rs b/tests/expected/loop-contract/simple_while_loop_decreases.rs
new file mode 100644
index 000000000000..d50ce88a334d
--- /dev/null
+++ b/tests/expected/loop-contract/simple_while_loop_decreases.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! Check if loop contracts with decreases clause is correctly applied.
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+fn simple_while_loop_decreases_harness() {
+    let mut x: u8 = kani::any_where(|i| *i >= 1);
+
+    #[kani::loop_invariant(x >= 1)]
+    #[kani::loop_decreases(x)]
+    while x > 1 {
+        x = x - 1;
+    }
+
+    assert!(x == 1);
+}