diff --git a/mlkem/src/cbmc.h b/mlkem/src/cbmc.h
index 80e1a36fc..a6f6fa768 100644
--- a/mlkem/src/cbmc.h
+++ b/mlkem/src/cbmc.h
@@ -80,24 +80,36 @@
  * Quantifiers
  * Note that the range on qvar is _exclusive_ between qvar_lb .. qvar_ub
  * https://diffblue.github.io/cbmc/contracts-quantifiers.html
+ *
+ * The quantified variable is declared as uint32_t, so these macros
+ * quantify only over indices in [0, UINT32_MAX). Bounds larger than
+ * UINT32_MAX (4 GiB) are NOT supported: the explicit (uint32_t) casts
+ * on the bounds will trigger CBMC's conversion check if a wider bound
+ * (e.g. a size_t > UINT32_MAX) is passed.
+ *
+ * Quantifying over size_t (64-bit) was found to blow up SMT proof
+ * times, so we deliberately keep the index width at 32 bits. Callers
+ * dealing with size_t-typed buffers must add an explicit
+ *   requires(len <= UINT32_MAX)
+ * precondition.
  */
 
 /*
  * Prevent clang-format from corrupting CBMC's special ==> operator
  */
 /* clang-format off */
-#define forall(qvar, qvar_lb, qvar_ub, predicate)                 \
-  __CPROVER_forall                                                \
-  {                                                               \
-    unsigned qvar;                                                \
-    ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> (predicate)   \
+#define forall(qvar, qvar_lb, qvar_ub, predicate)                              \
+  __CPROVER_forall                                                             \
+  {                                                                            \
+    uint32_t qvar;                                                             \
+    ((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> (predicate) \
   }
 
-#define exists(qvar, qvar_lb, qvar_ub, predicate)               \
-  __CPROVER_exists                                              \
-  {                                                             \
-    unsigned qvar;                                              \
-    ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) && (predicate)  \
+#define exists(qvar, qvar_lb, qvar_ub, predicate)                              \
+  __CPROVER_exists                                                             \
+  {                                                                            \
+    uint32_t qvar;                                                             \
+    ((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) && (predicate) \
   }
 /* clang-format on */
 
@@ -126,8 +138,8 @@
                          value_lb, value_ub)                           \
   __CPROVER_forall                                                     \
   {                                                                    \
-    unsigned qvar;                                                     \
-    ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==>                    \
+    uint32_t qvar;                                                     \
+    ((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> \
         (((int)(value_lb) <= ((array_var)[(qvar)])) &&                 \
          (((array_var)[(qvar)]) < (int)(value_ub)))                    \
   }
@@ -139,8 +151,8 @@
 #define array_unchanged_core(qvar, qvar_lb, qvar_ub, array_var)        \
   __CPROVER_forall                                                     \
   {                                                                    \
-    unsigned qvar;                                                     \
-    ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==>                    \
+    uint32_t qvar;                                                     \
+    ((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> \
     ((array_var)[(qvar)]) == (old(* (int16_t (*)[(qvar_ub)])(array_var)))[(qvar)] \
   }
 
@@ -150,8 +162,8 @@
 #define array_unchanged_u64_core(qvar, qvar_lb, qvar_ub, array_var)    \
   __CPROVER_forall                                                     \
   {                                                                    \
-    unsigned qvar;                                                     \
-    ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==>                    \
+    uint32_t qvar;                                                     \
+    ((uint32_t) (qvar_lb) <= (qvar) && (qvar) < (uint32_t) (qvar_ub)) ==> \
     ((array_var)[(qvar)]) == (old(* (uint64_t (*)[(qvar_ub)])(array_var)))[(qvar)] \
   }
 
diff --git a/mlkem/src/verify.h b/mlkem/src/verify.h
index 600afa44a..9c3a40482 100644
--- a/mlkem/src/verify.h
+++ b/mlkem/src/verify.h
@@ -376,7 +376,7 @@ __contract__(
 static MLK_INLINE void mlk_ct_cmov_zero(uint8_t *r, const uint8_t *x,
                                         size_t len, uint8_t b)
 __contract__(
-  requires(len <= MLK_MAX_BUFFER_SIZE)
+  requires(len <= UINT32_MAX)
   requires(memory_no_alias(r, len))
   requires(memory_no_alias(x, len))
   assigns(memory_slice(r, len))