diff --git a/src/lean/generator.rs b/src/lean/generator.rs
index 3a38bf85..f6d44c72 100644
--- a/src/lean/generator.rs
+++ b/src/lean/generator.rs
@@ -3252,7 +3252,44 @@ impl LeanGenerator<'_, '_, '_> {
             sanitize_variable_name(self.context.def_interner.definition_name(fors.identifier.id));
 
         let start_range = Box::new(self.generate_expr(fors.start_range, out));
-        let end_range = Box::new(self.generate_expr(fors.end_range, out));
+        let end_range = self.generate_expr(fors.end_range, out);
+        // Noir's `start..=end` ranges are inclusive, while the Lean loop is
+        // half-open, so an inclusive upper bound becomes `end + 1`. This mirrors
+        // the rewrite Noir's own SSA generation performs for constant bounds
+        // below the type's maximum (see `codegen_for` in
+        // `noirc_evaluator/src/ssa/ssa_gen/mod.rs`).
+        //
+        // Note: when `end` is the maximum value of the index type, `end + 1`
+        // overflows, which the Lampe model treats as failure, whereas the real
+        // program iterates up to and including `end` (Noir generates a
+        // `break`-based loop for that case). Modelling that faithfully would
+        // require an inclusive-loop primitive in the Lean semantics; until
+        // then this diverges for that corner case.
+        let end_range = if fors.inclusive {
+            let bound_ty_noir = self.resolve_bound_type(fors.end_range);
+            let bound_type = self.generate_lean_type_value(&bound_ty_noir, None);
+            let builtin_ty = self
+                .unfold_alias(bound_ty_noir)
+                .try_into()
+                .ok()
+                .expect("Inclusive for-loop bound is not a builtin integer type");
+            let builtin_name =
+                builtin::try_infix_into_builtin_name(BinaryOpKind::Add, builtin_ty, builtin_ty)
+                    .expect("Inclusive for-loop bound type does not support addition");
+            let one = Expression::Literal(Literal::Numeric(NumericLiteral {
+                value: "1".to_string(),
+                typ:   bound_type.clone(),
+            }));
+            let add_target = Expression::builtin_call_ref(builtin_name.as_str(), &bound_type);
+            Expression::Call(Call {
+                function:    Box::new(add_target),
+                params:      vec![end_range, one],
+                return_type: bound_type,
+            })
+        } else {
+            end_range
+        };
+        let end_range = Box::new(end_range);
         let mut body_prologue = vec![];
         let body = self.generate_expr(fors.block, &mut body_prologue);
         let body = Box::new(wrap_in_block_if_needed(body_prologue, body));
diff --git a/testing/ExtractionTests/lampe/ExtractionTests-0.0.0/Extracted.lean b/testing/ExtractionTests/lampe/ExtractionTests-0.0.0/Extracted.lean
index 5fa7f832..db3cf17b 100644
--- a/testing/ExtractionTests/lampe/ExtractionTests-0.0.0/Extracted.lean
+++ b/testing/ExtractionTests/lampe/ExtractionTests-0.0.0/Extracted.lean
@@ -11,6 +11,7 @@ import «ExtractionTests-0.0.0».Extracted.Experiments
 import «ExtractionTests-0.0.0».Extracted.FieldGenerics
 import «ExtractionTests-0.0.0».Extracted.GeneratedTypes
 import «ExtractionTests-0.0.0».Extracted.ImplTraitReturn
+import «ExtractionTests-0.0.0».Extracted.InclusiveRange
 import «ExtractionTests-0.0.0».Extracted.Lib
 import «ExtractionTests-0.0.0».Extracted.MultipleGenerics
 import «ExtractionTests-0.0.0».Extracted.NestedMemberAccess
@@ -39,6 +40,7 @@ def env := AliasMemberAccess.env
   ++ Experiments.env
   ++ FieldGenerics.env
   ++ ImplTraitReturn.env
+  ++ InclusiveRange.env
   ++ Lib.env
   ++ MultipleGenerics.env
   ++ NestedMemberAccess.env
diff --git a/testing/ExtractionTests/lampe/ExtractionTests-0.0.0/Extracted/InclusiveRange.lean b/testing/ExtractionTests/lampe/ExtractionTests-0.0.0/Extracted/InclusiveRange.lean
new file mode 100644
index 00000000..1642930e
--- /dev/null
+++ b/testing/ExtractionTests/lampe/ExtractionTests-0.0.0/Extracted/InclusiveRange.lean
@@ -0,0 +1,21 @@
+-- Generated by lampe
+
+import «ExtractionTests-0.0.0».Extracted.GeneratedTypes
+import Lampe
+
+open Lampe
+
+set_option linter.unusedVariables false
+
+noir_def «ExtractionTests-0.0.0»::inclusive_range::sum_inclusive<>(n: u32) -> u32 := {
+  let sum = (#_ref returning & u32)((0: u32));
+  for i in (0: u32) .. (#_uAdd returning u32)(n, (1: u32)) do {
+    sum = (#_uAdd returning u32)((#_readRef returning u32)(sum), i);
+    #_skip
+  };
+  (#_readRef returning u32)(sum)
+}
+
+def «ExtractionTests-0.0.0».InclusiveRange.env : Env := Env.mk
+  [«ExtractionTests-0.0.0::inclusive_range::sum_inclusive»]
+  []
diff --git a/testing/ExtractionTests/src/inclusive_range.nr b/testing/ExtractionTests/src/inclusive_range.nr
new file mode 100644
index 00000000..b259ccb9
--- /dev/null
+++ b/testing/ExtractionTests/src/inclusive_range.nr
@@ -0,0 +1,9 @@
+// Inclusive ranges (`start..=end`) must extract to a loop that includes the
+// final iteration (regression test for the extractor dropping it).
+pub fn sum_inclusive(n: u32) -> u32 {
+    let mut sum = 0;
+    for i in 0..=n {
+        sum = sum + i;
+    }
+    sum
+}
diff --git a/testing/ExtractionTests/src/lib.nr b/testing/ExtractionTests/src/lib.nr
index fb5b1572..8bcdde61 100644
--- a/testing/ExtractionTests/src/lib.nr
+++ b/testing/ExtractionTests/src/lib.nr
@@ -15,6 +15,7 @@ mod reserved_keywords;
 mod shadow_mut;
 mod unit_return;
 mod bool_neq;
+mod inclusive_range;
 mod ref_member_access;
 mod array_as_vector;
 mod impl_trait_return;