diff --git a/dev/aarch64_clean/src/arith_native_aarch64.h b/dev/aarch64_clean/src/arith_native_aarch64.h
index fc62ac2279..f8dc4bbb89 100644
--- a/dev/aarch64_clean/src/arith_native_aarch64.h
+++ b/dev/aarch64_clean/src/arith_native_aarch64.h
@@ -115,6 +115,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(
 /* This must be kept in sync with the HOL-Light specification in
  * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
  */
+/* TODO - refine_bounds branch - Check HOL-Light specification has the
+ * INT16_MAX/2 bound on post-condition and re-prove/
+ */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
     requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
@@ -122,6 +125,7 @@ __contract__(
     requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
     requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
     assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+    ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 
 #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
@@ -132,6 +136,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(
 /* This must be kept in sync with the HOL-Light specification in
  * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
  */
+/* TODO - refine_bounds branch - Check HOL-Light specification has the
+ * INT16_MAX/2 bound on post-condition and re-prove/
+ */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
     requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
@@ -139,6 +146,7 @@ __contract__(
     requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
     requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
     assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+    ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 
 #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
@@ -149,6 +157,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(
 /* This must be kept in sync with the HOL-Light specification in
  * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
  */
+/* TODO - refine_bounds branch - Check HOL-Light specification has the
+ * INT16_MAX/2 bound on post-condition and re-prove/
+ */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
     requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
@@ -156,6 +167,7 @@ __contract__(
     requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
     requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
     assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+    ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 
 #define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
diff --git a/dev/aarch64_opt/src/arith_native_aarch64.h b/dev/aarch64_opt/src/arith_native_aarch64.h
index bce864a299..6c694bee9e 100644
--- a/dev/aarch64_opt/src/arith_native_aarch64.h
+++ b/dev/aarch64_opt/src/arith_native_aarch64.h
@@ -115,6 +115,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(
 /* This must be kept in sync with the HOL-Light specification in
  * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
  */
+/* TODO - refine_bounds branch - Check HOL-Light specification has the
+ * INT16_MAX/2 bound on post-condition and re-prove/
+ */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
     requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
@@ -122,6 +125,7 @@ __contract__(
     requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
     requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
     assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+    ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 
 #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
@@ -132,6 +136,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(
 /* This must be kept in sync with the HOL-Light specification in
  * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
  */
+/* TODO - refine_bounds branch - Check HOL-Light specification has the
+ * INT16_MAX/2 bound on post-condition and re-prove/
+ */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
     requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
@@ -139,6 +146,7 @@ __contract__(
     requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
     requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
     assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+    ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 
 #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
@@ -149,6 +157,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(
 /* This must be kept in sync with the HOL-Light specification in
  * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
  */
+/* TODO - refine_bounds branch - Check HOL-Light specification has the
+ * INT16_MAX/2 bound on post-condition and re-prove/
+ */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
     requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
@@ -156,6 +167,7 @@ __contract__(
     requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
     requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
     assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+    ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 
 #define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c
index 49cd5a1f08..eb26b97d59 100644
--- a/mlkem/src/indcpa.c
+++ b/mlkem/src/indcpa.c
@@ -336,9 +336,11 @@ void mlk_gen_matrix(mlk_polymat *a, const uint8_t seed[MLKEM_SYMBYTES],
  *              - mlk_polymat a: Input matrix. Must be in NTT domain
  *                  and have coefficients of absolute value < 4096.
  *              - mlk_polyvec v: Input polynomial vector. Must be in NTT
- *                  domain.
+ *                  domain and have coefficients of absolute value
+ *                  < MLK_NTT_BOUND.
  *              - mlk_polyvec vc: Mulcache for v, computed via
- *                  mlk_polyvec_mulcache_compute().
+ *                  mlk_polyvec_mulcache_compute(). Must have coefficients
+ *                  of absolute value < MLKEM_Q.
  *
  * Specification: Implements @[FIPS203, Section 2.4.7, Eq (2.12), (2.13)]
  *
@@ -353,14 +355,22 @@ __contract__(
   requires(forall(k0, 0, MLKEM_K,
     forall(k1, 0, MLKEM_K,
       array_bound(a->vec[k0].vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT))))
-  assigns(memory_slice(out, sizeof(mlk_polyvec))))
+  requires(forall(k1, 0, MLKEM_K,
+     array_abs_bound(v->vec[k1].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
+  requires(forall(k2, 0, MLKEM_K,
+     array_abs_bound(vc->vec[k2].coeffs, 0, MLKEM_N/2, MLKEM_Q)))
+  assigns(object_whole(out))
+  ensures(forall(k3, 0, MLKEM_K,
+    array_abs_bound(out->vec[k3].coeffs, 0, MLKEM_N, INT16_MAX/2))))
 {
   unsigned i;
   for (i = 0; i < MLKEM_K; i++)
   __loop__(
-    assigns(i, memory_slice(out, sizeof(mlk_polyvec)))
+    assigns(i, object_whole(out))
     invariant(i <= MLKEM_K)
-    decreases(MLKEM_K - i))
+    invariant(forall(k, 0, i,
+                     array_abs_bound(out->vec[k].coeffs, 0, MLKEM_N, INT16_MAX/2)))
+  )
   {
     mlk_polyvec_basemul_acc_montgomery_cached(&out->vec[i], &a->vec[i], v, vc);
   }
diff --git a/mlkem/src/native/aarch64/src/arith_native_aarch64.h b/mlkem/src/native/aarch64/src/arith_native_aarch64.h
index 2941ecbd4b..3468a0f072 100644
--- a/mlkem/src/native/aarch64/src/arith_native_aarch64.h
+++ b/mlkem/src/native/aarch64/src/arith_native_aarch64.h
@@ -115,6 +115,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(
 /* This must be kept in sync with the HOL-Light specification in
  * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
  */
+/* TODO - refine_bounds branch - Check HOL-Light specification has the
+ * INT16_MAX/2 bound on post-condition and re-prove/
+ */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
     requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
@@ -122,6 +125,7 @@ __contract__(
     requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
     requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
     assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+    ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 
 #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
@@ -132,6 +136,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(
 /* This must be kept in sync with the HOL-Light specification in
  * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
  */
+/* TODO - refine_bounds branch - Check HOL-Light specification has the
+ * INT16_MAX/2 bound on post-condition and re-prove/
+ */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
     requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
@@ -139,6 +146,7 @@ __contract__(
     requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
     requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
     assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+    ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 
 #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
@@ -149,6 +157,9 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(
 /* This must be kept in sync with the HOL-Light specification in
  * proofs/hol_light/aarch64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
  */
+/* TODO - refine_bounds branch - Check HOL-Light specification has the
+ * INT16_MAX/2 bound on post-condition and re-prove/
+ */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
     requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
@@ -156,6 +167,7 @@ __contract__(
     requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
     requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
     assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+    ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 
 #define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)
diff --git a/mlkem/src/native/api.h b/mlkem/src/native/api.h
index 0308f2bd51..47fe221fb3 100644
--- a/mlkem/src/native/api.h
+++ b/mlkem/src/native/api.h
@@ -156,6 +156,7 @@ MLK_MUST_CHECK_RETURN_VALUE
 static MLK_INLINE int mlk_intt_native(int16_t p[MLKEM_N])
 __contract__(
   requires(memory_no_alias(p, sizeof(int16_t) * MLKEM_N))
+  requires(array_abs_bound(p, 0, MLKEM_N, INT16_MAX/2))
   assigns(memory_slice(p, sizeof(int16_t) * MLKEM_N))
   ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS)
   ensures((return_value == MLK_NATIVE_FUNC_SUCCESS) ==> array_abs_bound(p, 0, MLKEM_N, MLK_INVNTT_BOUND))
@@ -269,6 +270,7 @@ __contract__(
   requires(array_bound(a, 0, 2 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
   assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
   ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS)
+  ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 #endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 2 */
 
@@ -304,6 +306,7 @@ __contract__(
   requires(array_bound(a, 0, 3 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
   assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
   ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS)
+  ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 #endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 3 */
 
@@ -339,6 +342,7 @@ __contract__(
   requires(array_bound(a, 0, 4 * MLKEM_N, 0, MLKEM_UINT12_LIMIT))
   assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
   ensures(return_value == MLK_NATIVE_FUNC_FALLBACK || return_value == MLK_NATIVE_FUNC_SUCCESS)
+  ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 #endif /* MLK_CONFIG_MULTILEVEL_WITH_SHARED || MLKEM_K == 4 */
 #endif /* MLK_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED */
diff --git a/mlkem/src/poly.c b/mlkem/src/poly.c
index 4e3900d327..08aef7f1ed 100644
--- a/mlkem/src/poly.c
+++ b/mlkem/src/poly.c
@@ -280,6 +280,7 @@ __contract__(
   requires(memory_no_alias(x, sizeof(mlk_poly_mulcache)))
   requires(memory_no_alias(a, sizeof(mlk_poly)))
   assigns(memory_slice(x, sizeof(mlk_poly_mulcache)))
+  ensures(array_abs_bound(x->coeffs, 0, MLKEM_N/2, MLKEM_Q))
 )
 {
   unsigned i;
diff --git a/mlkem/src/poly.h b/mlkem/src/poly.h
index 587062cce5..8c94627acb 100644
--- a/mlkem/src/poly.h
+++ b/mlkem/src/poly.h
@@ -60,14 +60,16 @@ typedef struct
  **************************************************/
 static MLK_ALWAYS_INLINE int16_t mlk_montgomery_reduce(int32_t a)
 __contract__(
-    requires(a < +(INT32_MAX - (((int32_t)1 << 15) * MLKEM_Q)) &&
-             a > -(INT32_MAX - (((int32_t)1 << 15) * MLKEM_Q)))
-    /* We don't attempt to express an input-dependent output bound
-     * as the post-condition here. There are two call-sites for this
-     * function:
-     * - The base multiplication: Here, we need no output bound.
-     * - mlk_fqmul: Here, we inline this function and prove another spec
-     *          for mlk_fqmul which does have a post-condition bound. */
+    /* This specification is only relevant for Montgomery reduction
+     * during base multiplication, and the input bound is tailored to that.
+     * The output bound, albeit weak, allows one addition/subtraction prior
+     * to risk of overflow; this can be useful for the inverse NTT, for example.
+     *
+     * For the use of montgomery_reduce in fqmul, we inline this
+     * function instead of calling it by contract. */
+    requires(a <= +(4 * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND) &&
+             a >= -(4 * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND))
+    ensures(return_value < (INT16_MAX / 2) && return_value > -(INT16_MAX / 2))
 )
 {
   /* check-magic: 62209 == unsigned_mod(pow(MLKEM_Q, -1, 2^16), 2^16) */
@@ -148,17 +150,13 @@ __contract__(
  * - Caches `b_1 * \gamma` in @[FIPS203, Algorithm 12, BaseCaseMultiply, L1]
  *
  ************************************************************/
-/*
- * NOTE: The default C implementation of this function populates
- * the mulcache with values in (-q,q), but this is not needed for the
- * higher level safety proofs, and thus not part of the spec.
- */
 MLK_INTERNAL_API
 void mlk_poly_mulcache_compute(mlk_poly_mulcache *x, const mlk_poly *a)
 __contract__(
   requires(memory_no_alias(x, sizeof(mlk_poly_mulcache)))
   requires(memory_no_alias(a, sizeof(mlk_poly)))
   assigns(memory_slice(x, sizeof(mlk_poly_mulcache)))
+  ensures(array_abs_bound(x->coeffs, 0, MLKEM_N/2, MLKEM_Q))
 );
 
 #define mlk_poly_reduce MLK_NAMESPACE(poly_reduce)
@@ -310,6 +308,7 @@ MLK_INTERNAL_API
 void mlk_poly_invntt_tomont(mlk_poly *r)
 __contract__(
   requires(memory_no_alias(r, sizeof(mlk_poly)))
+  requires(array_abs_bound(r->coeffs, 0, MLKEM_N, INT16_MAX/2))
   assigns(memory_slice(r, sizeof(mlk_poly)))
   ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, MLK_INVNTT_BOUND))
 );
diff --git a/mlkem/src/poly_k.c b/mlkem/src/poly_k.c
index d729d2d26f..054a3c0908 100644
--- a/mlkem/src/poly_k.c
+++ b/mlkem/src/poly_k.c
@@ -156,26 +156,35 @@ __contract__(
   requires(memory_no_alias(b_cache, sizeof(mlk_polyvec_mulcache)))
   requires(forall(k1, 0, MLKEM_K,
      array_bound(a->vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
+  requires(forall(k2, 0, MLKEM_K,
+     array_abs_bound(b->vec[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
+  requires(forall(k3, 0, MLKEM_K,
+     array_abs_bound(b_cache->vec[k3].coeffs, 0, MLKEM_N/2, MLKEM_Q)))
   assigns(memory_slice(r, sizeof(mlk_poly)))
+  ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, INT16_MAX/2))
 )
 {
   unsigned i;
   mlk_assert_bound_2d(a->vec, MLKEM_K, MLKEM_N, 0, MLKEM_UINT12_LIMIT);
 
+  mlk_assert_abs_bound_2d(b, MLKEM_K, MLKEM_N, MLK_NTT_BOUND);
+  mlk_assert_abs_bound_2d(b_cache, MLKEM_K, MLKEM_N / 2, MLKEM_Q);
+
   for (i = 0; i < MLKEM_N / 2; i++)
-  __loop__(invariant(i <= MLKEM_N / 2)
-           decreases(MLKEM_N / 2 - i))
+  __loop__(
+    invariant(i <= MLKEM_N / 2)
+    invariant(array_abs_bound(r->coeffs, 0, 2 * i, INT16_MAX/2))
+    decreases(MLKEM_N / 2 - i)
+  )
   {
     unsigned k;
     int32_t t[2] = {0};
     for (k = 0; k < MLKEM_K; k++)
     __loop__(
-      invariant(k <= MLKEM_K &&
-         t[0] <=    (int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768  &&
-         t[0] >= - ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768) &&
-         t[1] <=   ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768) &&
-         t[1] >= - ((int32_t) k * 2 * MLKEM_UINT12_LIMIT * 32768))
-      decreases(MLKEM_K - k))
+      invariant(k <= MLKEM_K && i <= MLKEM_N / 2)
+      invariant(array_abs_bound(t, 0, 2, k * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND + 1))
+      decreases(MLKEM_K - k)
+    )
     {
       t[0] += (int32_t)a->vec[k].coeffs[2 * i + 1] * b_cache->vec[k].coeffs[i];
       t[0] += (int32_t)a->vec[k].coeffs[2 * i] * b->vec[k].coeffs[2 * i];
diff --git a/mlkem/src/poly_k.h b/mlkem/src/poly_k.h
index 9089a8e431..f8b2574b1f 100644
--- a/mlkem/src/poly_k.h
+++ b/mlkem/src/poly_k.h
@@ -357,6 +357,8 @@ MLK_INTERNAL_API
 void mlk_polyvec_invntt_tomont(mlk_polyvec *r)
 __contract__(
   requires(memory_no_alias(r, sizeof(mlk_polyvec)))
+  requires(forall(k0, 0, MLKEM_K,
+    array_abs_bound(r->vec[k0].coeffs, 0, MLKEM_N, INT16_MAX/2)))
   assigns(memory_slice(r, sizeof(mlk_polyvec)))
   ensures(forall(j, 0, MLKEM_K,
   array_abs_bound(r->vec[j].coeffs, 0, MLKEM_N, MLK_INVNTT_BOUND)))
@@ -372,7 +374,11 @@ __contract__(
  *
  *              Bounds:
  *              - Every coefficient of a is assumed to be in [0..4095]
- *              - No bounds guarantees for the coefficients in the result.
+ *              - Every coefficient of b is assumed to be bound by
+ *                MLK_NTT_BOUND in absolute value.
+ *              - Every coefficient of b_cache is assumed to be bound by
+ *                MLKEM_Q in absolute value.
+ *              - The output bounds are below INT16_MAX/2 in absolute value.
  *
  * Arguments:   - mlk_poly *r: pointer to output polynomial
  *              - const mlk_polyvec a: pointer to first input polynomial vector
@@ -399,9 +405,15 @@ __contract__(
   requires(memory_no_alias(b_cache, sizeof(mlk_polyvec_mulcache)))
   requires(forall(k1, 0, MLKEM_K,
      array_bound(a->vec[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
+  requires(forall(k2, 0, MLKEM_K,
+     array_abs_bound(b->vec[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
+  requires(forall(k3, 0, MLKEM_K,
+     array_abs_bound(b_cache->vec[k3].coeffs, 0, MLKEM_N/2, MLKEM_Q)))
   assigns(memory_slice(r, sizeof(mlk_poly)))
+  ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, INT16_MAX/2))
 );
 
+
 #define mlk_polyvec_mulcache_compute MLK_NAMESPACE_K(polyvec_mulcache_compute)
 /************************************************************
  * Name: mlk_polyvec_mulcache_compute
@@ -438,6 +450,8 @@ __contract__(
   requires(memory_no_alias(x, sizeof(mlk_polyvec_mulcache)))
   requires(memory_no_alias(a, sizeof(mlk_polyvec)))
   assigns(memory_slice(x, sizeof(mlk_polyvec_mulcache)))
+  ensures(forall(k0, 0, MLKEM_K,
+    array_abs_bound(x->vec[k0].coeffs, 0, MLKEM_N/2, MLKEM_Q)))
 );
 
 #define mlk_polyvec_reduce MLK_NAMESPACE_K(polyvec_reduce)
diff --git a/proofs/cbmc/matvec_mul/Makefile b/proofs/cbmc/matvec_mul/Makefile
index 65fc7e878b..bdc703c31c 100644
--- a/proofs/cbmc/matvec_mul/Makefile
+++ b/proofs/cbmc/matvec_mul/Makefile
@@ -35,7 +35,7 @@ CBMCFLAGS=--smt2
 #
 # For functions that use large and multi-dimensional arrays, this yields
 # a substantial improvement in proof performance.
-CBMCFLAGS += --no-array-field-sensitivity
+CBMCFLAGS += --arrays-uf-always
 CBMCFLAGS += --slice-formula
 
 FUNCTION_NAME = mlk_matvec_mul
diff --git a/test/bench/bench_components_mlkem.c b/test/bench/bench_components_mlkem.c
index 6ca262b7be..82ba4ec260 100644
--- a/test/bench/bench_components_mlkem.c
+++ b/test/bench/bench_components_mlkem.c
@@ -84,7 +84,7 @@ static int bench(void)
   BENCH("mlk_poly_rej_uniform_x4",
         mlk_poly_rej_uniform_x4((mlk_poly *)data0, (mlk_poly *)data1,
                                 (mlk_poly *)data2, (mlk_poly *)data3,
-                                (uint8_t (*)[64])data4))
+                                (uint8_t(*)[64])data4))
 
   /* mlk_poly */
   /* mlk_poly_compress_du */