diff --git a/mldsa/src/ct.h b/mldsa/src/ct.h
index f7953b3b0..2c38abc85 100644
--- a/mldsa/src/ct.h
+++ b/mldsa/src/ct.h
@@ -299,7 +299,7 @@ __contract__(
   ensures((return_value == 0) == forall(i, 0, len, (a[i] == b[i]))))
 {
   uint8_t r = 0, s = 0;
-  unsigned i;
+  size_t i;
 
   for (i = 0; i < len; i++)
   __loop__(
diff --git a/mldsa/src/fips202/fips202.c b/mldsa/src/fips202/fips202.c
index fa7f682b5..0954daa3a 100644
--- a/mldsa/src/fips202/fips202.c
+++ b/mldsa/src/fips202/fips202.c
@@ -77,7 +77,9 @@ __contract__(
   assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES))
   ensures(return_value < r))
 {
-  while (inlen >= r - pos)
+  /* Safety: widen r to avoid type mismatch warning */
+  size_t rsize = r;
+  while (inlen >= rsize - pos)
   __loop__(
     assigns(pos, in, inlen,
       memory_slice(s, sizeof(uint64_t) *  MLD_KECCAK_LANES))
@@ -150,6 +152,8 @@ __contract__(
   ensures(return_value <= r))
 {
   unsigned int i;
+  /* Safety: widen r to avoid type mismatch warning */
+  size_t rsize = r;
   size_t out_offset = 0;
 
   /* Reference: This code is re-factored from the reference implementation
@@ -174,8 +178,8 @@ __contract__(
       mld_keccakf1600_permute(s);
       pos = 0;
     }
-    /* Safety: If bytes_to_go < r - pos, truncation to unsigned is safe. */
-    i = bytes_to_go < r - pos ? (unsigned)bytes_to_go : r - pos;
+    /* Safety: If bytes_to_go < rsize - pos, truncation to unsigned is safe. */
+    i = bytes_to_go < rsize - pos ? (unsigned)bytes_to_go : r - pos;
     mld_keccakf1600_extract_bytes(s, out + out_offset, pos, i);
     bytes_to_go -= i;
     pos += i;
diff --git a/mldsa/src/fips202/fips202x4.c b/mldsa/src/fips202/fips202x4.c
index 97fbd6a48..012bdb514 100644
--- a/mldsa/src/fips202/fips202x4.c
+++ b/mldsa/src/fips202/fips202x4.c
@@ -39,7 +39,9 @@ __contract__(
   requires(memory_no_alias(in3, inlen))
   assigns(memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY)))
 {
-  while (inlen >= r)
+  /* Safety: widen r to avoid type mismatch warning */
+  size_t rsize = r;
+  while (inlen >= rsize)
   __loop__(
     assigns(inlen, in0, in1, in2, in3, memory_slice(s, sizeof(uint64_t) * MLD_KECCAK_LANES * MLD_KECCAK_WAY))
     invariant(inlen <= loop_entry(inlen))
@@ -66,7 +68,7 @@ __contract__(
     mld_keccakf1600x4_xor_bytes(s, in0, in1, in2, in3, 0, (unsigned)inlen);
   }
 
-  if (inlen == r - 1)
+  if (inlen == rsize - 1)
   {
     p |= 128;
     mld_keccakf1600x4_xor_bytes(s, &p, &p, &p, &p, (unsigned)inlen, 1);