diff --git a/dev/aarch64_clean/src/arith_native_aarch64.h b/dev/aarch64_clean/src/arith_native_aarch64.h
index c8e70f32e..ef84939c8 100644
--- a/dev/aarch64_clean/src/arith_native_aarch64.h
+++ b/dev/aarch64_clean/src/arith_native_aarch64.h
@@ -116,6 +116,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/arm/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))
@@ -123,6 +126,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 \
@@ -133,6 +137,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/arm/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))
@@ -140,6 +147,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 \
@@ -150,6 +158,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/arm/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))
@@ -157,6 +168,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 35399c8c1..b832730d4 100644
--- a/dev/aarch64_opt/src/arith_native_aarch64.h
+++ b/dev/aarch64_opt/src/arith_native_aarch64.h
@@ -116,6 +116,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/arm/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))
@@ -123,6 +126,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 \
@@ -133,6 +137,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/arm/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))
@@ -140,6 +147,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 \
@@ -150,6 +158,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/arm/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))
@@ -157,6 +168,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 556f7692e..00eb47e17 100644
--- a/mlkem/src/indcpa.c
+++ b/mlkem/src/indcpa.c
@@ -289,9 +289,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)]
  *
@@ -304,17 +306,41 @@ __contract__(
   requires(memory_no_alias(v, sizeof(mlk_polyvec)))
   requires(memory_no_alias(vc, sizeof(mlk_polyvec_mulcache)))
   requires(forall(k0, 0, MLKEM_K * MLKEM_K,
-    array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
-  assigns(object_whole(out)))
+                  array_bound(a[k0].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
+  requires(forall(k1, 0, MLKEM_K,
+     array_abs_bound(v[k1].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
+  requires(forall(k2, 0, MLKEM_K,
+     array_abs_bound(vc[k2].coeffs, 0, MLKEM_N/2, MLKEM_Q)))
+  assigns(object_whole(out))
+  ensures(forall(k3, 0, MLKEM_K,
+    array_abs_bound(out[k3].coeffs, 0, MLKEM_N, INT16_MAX/2))))
 {
-  unsigned i;
-  for (i = 0; i < MLKEM_K; i++)
-  __loop__(
-    assigns(i, object_whole(out))
-    invariant(i <= MLKEM_K))
-  {
-    mlk_polyvec_basemul_acc_montgomery_cached(&out[i], &a[MLKEM_K * i], v, vc);
-  }
+  /* Temporary on the "refine-bounds" branch - unroll to a simple
+   * sequence of calls for each possible value of MLKEM_K to
+   * simplify proof.
+   */
+  mlk_polyvec_basemul_acc_montgomery_cached(&out[0], &a[0], v, vc);
+  mlk_polyvec_basemul_acc_montgomery_cached(&out[1], &a[MLKEM_K], v, vc);
+
+#if MLKEM_K == 3
+  mlk_polyvec_basemul_acc_montgomery_cached(&out[2], &a[MLKEM_K * 2], v, vc);
+#elif MLKEM_K == 4
+  mlk_polyvec_basemul_acc_montgomery_cached(&out[2], &a[MLKEM_K * 2], v, vc);
+  mlk_polyvec_basemul_acc_montgomery_cached(&out[3], &a[MLKEM_K * 3], v, vc);
+#endif
+
+  /* unsigned i;
+   * for (i = 0; i < MLKEM_K; i++)
+   * __loop__(
+   *    assigns(i, object_whole(out))
+   *    invariant(i <= MLKEM_K)
+   *    invariant(forall(k, 0, i,
+   *     array_abs_bound(out[k].coeffs, 0, MLKEM_N, INT16_MAX/2))))
+   * {
+   *   mlk_polyvec_basemul_acc_montgomery_cached(&out[i], &a[MLKEM_K * i], v,
+   * vc);
+   * }
+   */
 }
 
 /* Reference: `indcpa_keypair_derand()` in the reference implementation @[REF].
diff --git a/mlkem/src/native/aarch64/src/arith_native_aarch64.h b/mlkem/src/native/aarch64/src/arith_native_aarch64.h
index e0978c122..6f74428ba 100644
--- a/mlkem/src/native/aarch64/src/arith_native_aarch64.h
+++ b/mlkem/src/native/aarch64/src/arith_native_aarch64.h
@@ -116,6 +116,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/arm/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))
@@ -123,6 +126,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 \
@@ -133,6 +137,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/arm/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))
@@ -140,6 +147,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 \
@@ -150,6 +158,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/arm/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))
@@ -157,6 +168,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 20f965466..6b997992c 100644
--- a/mlkem/src/native/api.h
+++ b/mlkem/src/native/api.h
@@ -155,6 +155,7 @@ __contract__(
 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))
@@ -264,6 +265,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 */
 
@@ -298,6 +300,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 */
 
@@ -332,6 +335,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 a7b087109..41cea3a13 100644
--- a/mlkem/src/poly.c
+++ b/mlkem/src/poly.c
@@ -273,6 +273,7 @@ __contract__(
   requires(memory_no_alias(x, sizeof(mlk_poly_mulcache)))
   requires(memory_no_alias(a, sizeof(mlk_poly)))
   assigns(object_whole(x))
+  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 20fb65e72..42ec24b6c 100644
--- a/mlkem/src/poly.h
+++ b/mlkem/src/poly.h
@@ -89,14 +89,16 @@ static MLK_ALWAYS_INLINE int16_t mlk_cast_uint16_to_int16(uint16_t x)
  **************************************************/
 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) */
@@ -177,17 +179,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(object_whole(x))
+  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)
@@ -339,6 +337,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 fb9779740..2ca617f2e 100644
--- a/mlkem/src/poly_k.c
+++ b/mlkem/src/poly_k.c
@@ -158,24 +158,31 @@ __contract__(
   requires(memory_no_alias(b_cache, sizeof(mlk_polyvec_mulcache)))
   requires(forall(k1, 0, MLKEM_K,
      array_bound(a[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
+  requires(forall(k2, 0, MLKEM_K,
+     array_abs_bound(b[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
+  requires(forall(k3, 0, MLKEM_K,
+     array_abs_bound(b_cache[k3].coeffs, 0, MLKEM_N/2, MLKEM_Q)))
   assigns(object_whole(r))
+  ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, INT16_MAX/2))
 )
 {
   unsigned i;
   mlk_assert_bound_2d(a, 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))
+  __loop__(
+    invariant(i <= MLKEM_N / 2)
+    invariant(array_abs_bound(r->coeffs, 0, 2 * i, INT16_MAX/2)))
   {
     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)))
+      invariant(k <= MLKEM_K && i <= MLKEM_N / 2)
+      invariant(array_abs_bound(t, 0, 2, k * 2 * MLKEM_UINT12_LIMIT * MLK_NTT_BOUND + 1)))
     {
       t[0] += (int32_t)a[k].coeffs[2 * i + 1] * b_cache[k].coeffs[i];
       t[0] += (int32_t)a[k].coeffs[2 * i] * b[k].coeffs[2 * i];
diff --git a/mlkem/src/poly_k.h b/mlkem/src/poly_k.h
index f7a40ff5f..3668a22d9 100644
--- a/mlkem/src/poly_k.h
+++ b/mlkem/src/poly_k.h
@@ -347,6 +347,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[k0].coeffs, 0, MLKEM_N, INT16_MAX/2)))
   assigns(object_whole(r))
   ensures(forall(j, 0, MLKEM_K,
   array_abs_bound(r[j].coeffs, 0, MLKEM_N, MLK_INVNTT_BOUND)))
@@ -362,7 +364,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
@@ -389,9 +395,15 @@ __contract__(
   requires(memory_no_alias(b_cache, sizeof(mlk_polyvec_mulcache)))
   requires(forall(k1, 0, MLKEM_K,
      array_bound(a[k1].coeffs, 0, MLKEM_N, 0, MLKEM_UINT12_LIMIT)))
-  assigns(object_whole(r))
+  requires(forall(k2, 0, MLKEM_K,
+     array_abs_bound(b[k2].coeffs, 0, MLKEM_N, MLK_NTT_BOUND)))
+  requires(forall(k3, 0, MLKEM_K,
+     array_abs_bound(b_cache[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
@@ -428,6 +440,8 @@ __contract__(
   requires(memory_no_alias(x, sizeof(mlk_polyvec_mulcache)))
   requires(memory_no_alias(a, sizeof(mlk_polyvec)))
   assigns(object_whole(x))
+  ensures(forall(k0, 0, MLKEM_K,
+    array_abs_bound(x[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 65fc7e878..bdc703c31 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/proofs/cbmc/matvec_mul/matvec_mul_harness.c b/proofs/cbmc/matvec_mul/matvec_mul_harness.c
index 286e47e4b..2353a403f 100644
--- a/proofs/cbmc/matvec_mul/matvec_mul_harness.c
+++ b/proofs/cbmc/matvec_mul/matvec_mul_harness.c
@@ -5,13 +5,15 @@
 #include "indcpa.h"
 #include "poly_k.h"
 
-#define mlk_matvec_mul MLK_NAMESPACE(matvec_mul)
-void mlk_matvec_mul(mlk_polyvec out, const mlk_polymat a, mlk_polyvec const v,
-                    mlk_polyvec_mulcache const vc);
+#define mlk_matvec_mul MLK_ADD_PARAM_SET(mlk_matvec_mul)
+void mlk_matvec_mul(mlk_polyvec out, const mlk_polymat a, const mlk_polyvec v,
+                    const mlk_polyvec_mulcache vc);
 
 void harness(void)
 {
-  mlk_poly *out, *a, *v;
+  mlk_poly *out;
+  mlk_poly *a;
+  mlk_poly *v;
   mlk_poly_mulcache *vc;
   mlk_matvec_mul(out, a, v, vc);
 }