diff --git a/mldsa/fips202/fips202.c b/mldsa/fips202/fips202.c
index 145c2ef4..51b1078a 100644
--- a/mldsa/fips202/fips202.c
+++ b/mldsa/fips202/fips202.c
@@ -93,8 +93,6 @@ __contract__(
   {
     s[i] = 0;
   }
-
-  cassert(forall(k, 0, MLD_KECCAK_LANES, s[k] == 0));
 }
 
 /*************************************************
diff --git a/mldsa/polyvec.c b/mldsa/polyvec.c
index 228b1267..56e23dcf 100644
--- a/mldsa/polyvec.c
+++ b/mldsa/polyvec.c
@@ -269,21 +269,7 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
       t += (int64_t)u->vec[j].coeffs[i] * v->vec[j].coeffs[i];
     }
 
-    /* Substitute j == MLSDA_L into the loop invariant to get... */
-    cassert(j == MLDSA_L);
-    cassert(t >= -(int64_t)MLDSA_L * (MLDSA_Q - 1) * (MLD_NTT_BOUND - 1));
-    cassert(t <= (int64_t)MLDSA_L * (MLDSA_Q - 1) * (MLD_NTT_BOUND - 1));
-
-    /* ...and therefore... */
-    cassert(t >= -MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX);
-    cassert(t < MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX);
-
-    /* ...which meets the "strong" case of mld_montgomery_reduce() */
     r = mld_montgomery_reduce(t);
-
-    /* ...and therefore we can assert a stronger bound on r */
-    cassert(r > -MLDSA_Q);
-    cassert(r < MLDSA_Q);
     w->coeffs[i] = r;
   }
 }
diff --git a/mldsa/reduce.c b/mldsa/reduce.c
index fd0208a1..3efe614a 100644
--- a/mldsa/reduce.c
+++ b/mldsa/reduce.c
@@ -4,6 +4,7 @@
  */
 #include <stdint.h>
 
+#include "debug.h"
 #include "reduce.h"
 
 /*************************************************
@@ -65,7 +66,8 @@ int32_t mld_reduce32(int32_t a)
 
   t = (a + (1 << 22)) >> 23;
   t = a - t * MLDSA_Q;
-  cassert((t - a) % MLDSA_Q == 0);
+
+  mld_assert((t - a) % MLDSA_Q == 0);
   return t;
 }
 
diff --git a/mldsa/reduce.h b/mldsa/reduce.h
index a7acb78b..ee9a02d9 100644
--- a/mldsa/reduce.h
+++ b/mldsa/reduce.h
@@ -48,12 +48,8 @@
  **************************************************/
 int32_t mld_montgomery_reduce(int64_t a)
 __contract__(
-  requires(a >= -MONTGOMERY_REDUCE_DOMAIN_MAX && a <= MONTGOMERY_REDUCE_DOMAIN_MAX)
-  ensures(return_value >= INT32_MIN && return_value < REDUCE32_DOMAIN_MAX)
-
-  /* Special case - for stronger input bounds, we can ensure stronger bounds on the output */
-  ensures((a >= -MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX && a < MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX) ==>
-          (return_value > -MLDSA_Q && return_value < MLDSA_Q))
+  requires(a >= -MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX && a < MONTGOMERY_REDUCE_STRONG_DOMAIN_MAX)
+  ensures(return_value > -MLDSA_Q && return_value < MLDSA_Q)
 );
 
 #define mld_reduce32 MLD_NAMESPACE(reduce32)
diff --git a/mldsa/rounding.c b/mldsa/rounding.c
index 7f268aef..dee9f37b 100644
--- a/mldsa/rounding.c
+++ b/mldsa/rounding.c
@@ -4,6 +4,7 @@
  */
 #include <stdint.h>
 
+#include "debug.h"
 #include "rounding.h"
 
 
@@ -17,20 +18,20 @@ void mld_decompose(int32_t *a0, int32_t *a1, int32_t a)
 {
   *a1 = (a + 127) >> 7;
   /* We know a >= 0 and a < MLDSA_Q, so... */
-  cassert(*a1 >= 0 && *a1 <= 65472);
+  mld_assert(*a1 >= 0 && *a1 <= 65472);
 
 #if MLDSA_MODE == 2
   *a1 = (*a1 * 11275 + (1 << 23)) >> 24;
-  cassert(*a1 >= 0 && *a1 <= 44);
+  mld_assert(*a1 >= 0 && *a1 <= 44);
 
   *a1 ^= ((43 - *a1) >> 31) & *a1;
-  cassert(*a1 >= 0 && *a1 <= 43);
+  mld_assert(*a1 >= 0 && *a1 <= 43);
 #else /* MLDSA_MODE == 2 */
   *a1 = (*a1 * 1025 + (1 << 21)) >> 22;
-  cassert(*a1 >= 0 && *a1 <= 16);
+  mld_assert(*a1 >= 0 && *a1 <= 16);
 
   *a1 &= 15;
-  cassert(*a1 >= 0 && *a1 <= 15);
+  mld_assert(*a1 >= 0 && *a1 <= 15);
 
 #endif /* MLDSA_MODE != 2 */
 
diff --git a/mldsa/sign.c b/mldsa/sign.c
index 0e142c8f..9e3bb910 100644
--- a/mldsa/sign.c
+++ b/mldsa/sign.c
@@ -6,6 +6,7 @@
 #include <string.h>
 
 #include "cbmc.h"
+#include "debug.h"
 #include "fips202/fips202.h"
 #include "packing.h"
 #include "poly.h"
@@ -252,9 +253,7 @@ __contract__(
   /* If z is valid, then its coefficients are bounded by  */
   /* MLDSA_GAMMA1 - MLDSA_BETA. This will be needed below */
   /* to prove the pre-condition of pack_sig()             */
-  cassert(forall(k1, 0, MLDSA_L,
-                 array_abs_bound(z.vec[k1].coeffs, 0, MLDSA_N,
-                                 (MLDSA_GAMMA1 - MLDSA_BETA))));
+  mld_assert_abs_bound_2d(z.vec, MLDSA_L, MLDSA_N, (MLDSA_GAMMA1 - MLDSA_BETA));
 
   /* Check that subtracting cs2 does not change high bits of w and low bits
    * do not reveal secret information */