diff --git a/cbmc/proofs/basemul_cached/basemul_cached_harness.c b/cbmc/proofs/basemul_cached/basemul_cached_harness.c
index 3bf4bea8d..9ba680a66 100644
--- a/cbmc/proofs/basemul_cached/basemul_cached_harness.c
+++ b/cbmc/proofs/basemul_cached/basemul_cached_harness.c
@@ -23,7 +23,7 @@
  *
  */
 void harness(void) {
-  int16_t a[2], b[2], r[2], b_cached;
+  int16_t *a, *b, *r, b_cached;
 
   basemul_cached(r, a, b, b_cached);
 }
diff --git a/cbmc/proofs/cmov_int16/cmov_int16_harness.c b/cbmc/proofs/cmov_int16/cmov_int16_harness.c
index c739fa8ae..561039fd0 100644
--- a/cbmc/proofs/cmov_int16/cmov_int16_harness.c
+++ b/cbmc/proofs/cmov_int16/cmov_int16_harness.c
@@ -23,7 +23,7 @@
  */
 void harness(void) {
   uint16_t b;
-  int16_t r, v;
+  int16_t *r, v;
 
-  cmov_int16(&r, v, b);
+  cmov_int16(r, v, b);
 }
diff --git a/cbmc/proofs/poly_basemul_montgomery_cached/poly_basemul_montgomery_cached_harness.c b/cbmc/proofs/poly_basemul_montgomery_cached/poly_basemul_montgomery_cached_harness.c
index c2bab3c25..8a28cc572 100644
--- a/cbmc/proofs/poly_basemul_montgomery_cached/poly_basemul_montgomery_cached_harness.c
+++ b/cbmc/proofs/poly_basemul_montgomery_cached/poly_basemul_montgomery_cached_harness.c
@@ -22,8 +22,8 @@
  *
  */
 void harness(void) {
-  poly r, a, b;
-  poly_mulcache b_cached;
+  poly *r, *a, *b;
+  poly_mulcache *b_cached;
 
-  poly_basemul_montgomery_cached(&r, &a, &b, &b_cached);
+  poly_basemul_montgomery_cached(r, a, b, b_cached);
 }
diff --git a/cbmc/proofs/poly_cbd_eta1/poly_cbd_eta1_harness.c b/cbmc/proofs/poly_cbd_eta1/poly_cbd_eta1_harness.c
index f2335df25..7a6efd5c3 100644
--- a/cbmc/proofs/poly_cbd_eta1/poly_cbd_eta1_harness.c
+++ b/cbmc/proofs/poly_cbd_eta1/poly_cbd_eta1_harness.c
@@ -22,8 +22,8 @@
  *
  */
 void harness(void) {
-  uint8_t buf[MLKEM_ETA1 * MLKEM_N / 4];
-  poly a;
+  uint8_t *buf;
+  poly *a;
 
-  poly_cbd_eta1(&a, buf);
+  poly_cbd_eta1(a, buf);
 }
diff --git a/cbmc/proofs/poly_cbd_eta2/poly_cbd_eta2_harness.c b/cbmc/proofs/poly_cbd_eta2/poly_cbd_eta2_harness.c
index d8f5c257b..5ce31d8a4 100644
--- a/cbmc/proofs/poly_cbd_eta2/poly_cbd_eta2_harness.c
+++ b/cbmc/proofs/poly_cbd_eta2/poly_cbd_eta2_harness.c
@@ -22,8 +22,8 @@
  *
  */
 void harness(void) {
-  uint8_t buf[MLKEM_ETA2 * MLKEM_N / 4];
-  poly a;
+  uint8_t *buf;
+  poly *a;
 
-  poly_cbd_eta2(&a, buf);
+  poly_cbd_eta2(a, buf);
 }
diff --git a/cbmc/proofs/poly_compress/poly_compress_harness.c b/cbmc/proofs/poly_compress/poly_compress_harness.c
index 90b6f7db4..dc4832972 100644
--- a/cbmc/proofs/poly_compress/poly_compress_harness.c
+++ b/cbmc/proofs/poly_compress/poly_compress_harness.c
@@ -22,8 +22,8 @@
  *
  */
 void harness(void) {
-  poly r;
-  uint8_t a[MLKEM_POLYCOMPRESSEDBYTES];
+  poly *r;
+  uint8_t *a;
 
-  poly_compress(a, &r);
+  poly_compress(a, r);
 }
diff --git a/cbmc/proofs/poly_decompress/poly_decompress_harness.c b/cbmc/proofs/poly_decompress/poly_decompress_harness.c
index fa4b92a74..516eeca0d 100644
--- a/cbmc/proofs/poly_decompress/poly_decompress_harness.c
+++ b/cbmc/proofs/poly_decompress/poly_decompress_harness.c
@@ -22,8 +22,8 @@
  *
  */
 void harness(void) {
-  poly r;
-  uint8_t a[MLKEM_POLYCOMPRESSEDBYTES];
+  poly *r;
+  uint8_t *a;
 
-  poly_decompress(&r, a);
+  poly_decompress(r, a);
 }
diff --git a/cbmc/proofs/poly_frombytes/poly_frombytes_harness.c b/cbmc/proofs/poly_frombytes/poly_frombytes_harness.c
index cf967f3a9..bc6432cf4 100644
--- a/cbmc/proofs/poly_frombytes/poly_frombytes_harness.c
+++ b/cbmc/proofs/poly_frombytes/poly_frombytes_harness.c
@@ -22,9 +22,9 @@
  *
  */
 void harness(void) {
-  poly a;
-  uint8_t r[MLKEM_POLYBYTES];
+  poly *a;
+  uint8_t *r;
 
   /* Contracts for this function are in poly.h */
-  poly_frombytes(&a, r);
+  poly_frombytes(a, r);
 }
diff --git a/cbmc/proofs/poly_getnoise_eta1122_4x/poly_getnoise_eta1122_4x_harness.c b/cbmc/proofs/poly_getnoise_eta1122_4x/poly_getnoise_eta1122_4x_harness.c
index 6134dbb24..dceb21288 100644
--- a/cbmc/proofs/poly_getnoise_eta1122_4x/poly_getnoise_eta1122_4x_harness.c
+++ b/cbmc/proofs/poly_getnoise_eta1122_4x/poly_getnoise_eta1122_4x_harness.c
@@ -22,10 +22,10 @@
  *
  */
 void harness(void) {
-  uint8_t seed[MLKEM_SYMBYTES];
-  poly r0, r1, r2, r3;
+  uint8_t *seed;
+  poly *r0, *r1, *r2, *r3;
   uint8_t nonce0, nonce1, nonce2, nonce3;
 
-  poly_getnoise_eta1122_4x(&r0, &r1, &r2, &r3, seed, nonce0, nonce1, nonce2,
+  poly_getnoise_eta1122_4x(r0, r1, r2, r3, seed, nonce0, nonce1, nonce2,
                            nonce3);
 }
diff --git a/cbmc/proofs/poly_getnoise_eta1_4x/poly_getnoise_eta1_4x_harness.c b/cbmc/proofs/poly_getnoise_eta1_4x/poly_getnoise_eta1_4x_harness.c
index a410aae97..875ef8b4e 100644
--- a/cbmc/proofs/poly_getnoise_eta1_4x/poly_getnoise_eta1_4x_harness.c
+++ b/cbmc/proofs/poly_getnoise_eta1_4x/poly_getnoise_eta1_4x_harness.c
@@ -22,10 +22,9 @@
  *
  */
 void harness(void) {
-  uint8_t seed[MLKEM_SYMBYTES];
-  poly r0, r1, r2, r3;
+  uint8_t *seed;
+  poly *r0, *r1, *r2, *r3;
   uint8_t nonce0, nonce1, nonce2, nonce3;
 
-  poly_getnoise_eta1_4x(&r0, &r1, &r2, &r3, seed, nonce0, nonce1, nonce2,
-                        nonce3);
+  poly_getnoise_eta1_4x(r0, r1, r2, r3, seed, nonce0, nonce1, nonce2, nonce3);
 }
diff --git a/cbmc/proofs/poly_getnoise_eta2/poly_getnoise_eta2_harness.c b/cbmc/proofs/poly_getnoise_eta2/poly_getnoise_eta2_harness.c
index a9c663bfa..8324ebb3f 100644
--- a/cbmc/proofs/poly_getnoise_eta2/poly_getnoise_eta2_harness.c
+++ b/cbmc/proofs/poly_getnoise_eta2/poly_getnoise_eta2_harness.c
@@ -22,9 +22,9 @@
  *
  */
 void harness(void) {
-  uint8_t seed[MLKEM_SYMBYTES];
-  poly r;
+  uint8_t *seed;
+  poly *r;
   uint8_t nonce;
 
-  poly_getnoise_eta2(&r, seed, nonce);
+  poly_getnoise_eta2(r, seed, nonce);
 }
diff --git a/cbmc/proofs/poly_getnoise_eta2_4x/poly_getnoise_eta2_4x_harness.c b/cbmc/proofs/poly_getnoise_eta2_4x/poly_getnoise_eta2_4x_harness.c
index c4c4b8636..8abc80f40 100644
--- a/cbmc/proofs/poly_getnoise_eta2_4x/poly_getnoise_eta2_4x_harness.c
+++ b/cbmc/proofs/poly_getnoise_eta2_4x/poly_getnoise_eta2_4x_harness.c
@@ -22,10 +22,9 @@
  *
  */
 void harness(void) {
-  uint8_t seed[MLKEM_SYMBYTES];
-  poly r0, r1, r2, r3;
+  uint8_t *seed;
+  poly *r0, *r1, *r2, *r3;
   uint8_t nonce0, nonce1, nonce2, nonce3;
 
-  poly_getnoise_eta2_4x(&r0, &r1, &r2, &r3, seed, nonce0, nonce1, nonce2,
-                        nonce3);
+  poly_getnoise_eta2_4x(r0, r1, r2, r3, seed, nonce0, nonce1, nonce2, nonce3);
 }
diff --git a/cbmc/proofs/poly_mulcache_compute/poly_mulcache_compute_harness.c b/cbmc/proofs/poly_mulcache_compute/poly_mulcache_compute_harness.c
index aef25bcb2..e35498eea 100644
--- a/cbmc/proofs/poly_mulcache_compute/poly_mulcache_compute_harness.c
+++ b/cbmc/proofs/poly_mulcache_compute/poly_mulcache_compute_harness.c
@@ -23,8 +23,8 @@
  *
  */
 void harness(void) {
-  poly_mulcache x;
-  poly a;
+  poly_mulcache *x;
+  poly *a;
 
-  poly_mulcache_compute(&x, &a);
+  poly_mulcache_compute(x, a);
 }
diff --git a/cbmc/proofs/poly_reduce/poly_reduce_harness.c b/cbmc/proofs/poly_reduce/poly_reduce_harness.c
index 1240e8aa5..f077d6d95 100644
--- a/cbmc/proofs/poly_reduce/poly_reduce_harness.c
+++ b/cbmc/proofs/poly_reduce/poly_reduce_harness.c
@@ -22,8 +22,8 @@
  *
  */
 void harness(void) {
-  poly a;
+  poly *a;
 
   /* Contracts for this function are in poly.h */
-  poly_reduce(&a);
+  poly_reduce(a);
 }
diff --git a/cbmc/proofs/poly_tobytes/poly_tobytes_harness.c b/cbmc/proofs/poly_tobytes/poly_tobytes_harness.c
index 9e0a2a18f..3663e4d78 100644
--- a/cbmc/proofs/poly_tobytes/poly_tobytes_harness.c
+++ b/cbmc/proofs/poly_tobytes/poly_tobytes_harness.c
@@ -22,9 +22,9 @@
  *
  */
 void harness(void) {
-  poly a;
-  uint8_t r[MLKEM_POLYBYTES];
+  poly *a;
+  uint8_t *r;
 
   /* Contracts for this function are in poly.h */
-  poly_tobytes(r, &a);
+  poly_tobytes(r, a);
 }
diff --git a/cbmc/proofs/poly_tomont/poly_tomont_harness.c b/cbmc/proofs/poly_tomont/poly_tomont_harness.c
index 1bc93fac2..f2627e9b7 100644
--- a/cbmc/proofs/poly_tomont/poly_tomont_harness.c
+++ b/cbmc/proofs/poly_tomont/poly_tomont_harness.c
@@ -22,7 +22,7 @@
  *
  */
 void harness(void) {
-  poly a;
+  poly *a;
 
-  poly_tomont(&a);
+  poly_tomont(a);
 }
diff --git a/cbmc/proofs/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c b/cbmc/proofs/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c
index bb7111bb7..cca15dfba 100644
--- a/cbmc/proofs/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c
+++ b/cbmc/proofs/polyvec_mulcache_compute/polyvec_mulcache_compute_harness.c
@@ -22,8 +22,8 @@
  *
  */
 void harness(void) {
-  polyvec_mulcache x;
-  polyvec a;
+  polyvec_mulcache *x;
+  polyvec *a;
 
-  polyvec_mulcache_compute(&x, &a);
+  polyvec_mulcache_compute(x, a);
 }
diff --git a/mlkem/cbd.h b/mlkem/cbd.h
index 18e2d2a7c..d3309882b 100644
--- a/mlkem/cbd.h
+++ b/mlkem/cbd.h
@@ -19,8 +19,8 @@
  **************************************************/
 void poly_cbd_eta1(poly *r, const uint8_t buf[MLKEM_ETA1 * MLKEM_N / 4])
     // clang-format off
-REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
-REQUIRES(buf != NULL && IS_FRESH(buf, MLKEM_ETA1 * MLKEM_N / 4))
+REQUIRES(IS_FRESH(r, sizeof(poly)))
+REQUIRES(IS_FRESH(buf, MLKEM_ETA1 * MLKEM_N / 4))
 ASSIGNS(OBJECT_WHOLE(r))
 ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA1, MLKEM_ETA1));
 // clang-format on
@@ -38,8 +38,8 @@ ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA1, MLKEM_ET
  **************************************************/
 void poly_cbd_eta2(poly *r, const uint8_t buf[MLKEM_ETA2 * MLKEM_N / 4])
     // clang-format off
-REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
-REQUIRES(buf != NULL && IS_FRESH(buf, MLKEM_ETA2 * MLKEM_N / 4))
+REQUIRES(IS_FRESH(r, sizeof(poly)))
+REQUIRES(IS_FRESH(buf, MLKEM_ETA2 * MLKEM_N / 4))
 ASSIGNS(OBJECT_WHOLE(r))
 ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA2, MLKEM_ETA2));
 // clang-format on
diff --git a/mlkem/ntt.h b/mlkem/ntt.h
index b8c85b273..58d2eb622 100644
--- a/mlkem/ntt.h
+++ b/mlkem/ntt.h
@@ -47,9 +47,9 @@ void poly_invntt_tomont(poly *r);
 void basemul_cached(int16_t r[2], const int16_t a[2], const int16_t b[2],
                     int16_t b_cached)
     // clang-format off
-REQUIRES(r != NULL && IS_FRESH(r, 2 * sizeof(int16_t)))
-REQUIRES(a != NULL && IS_FRESH(a, 2 * sizeof(int16_t)))
-REQUIRES(b != NULL && IS_FRESH(b, 2 * sizeof(int16_t)))
+REQUIRES(IS_FRESH(r, 2 * sizeof(int16_t)))
+REQUIRES(IS_FRESH(a, 2 * sizeof(int16_t)))
+REQUIRES(IS_FRESH(b, 2 * sizeof(int16_t)))
 REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, 1, a, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
 ASSIGNS(OBJECT_UPTO(r, 2 * sizeof(int16_t)))
 ENSURES(ARRAY_IN_BOUNDS(int, k, 0, 1, r, -3 * HALF_Q + 1, 3 * HALF_Q - 1));
diff --git a/mlkem/poly.h b/mlkem/poly.h
index 873637873..bcc8dd463 100644
--- a/mlkem/poly.h
+++ b/mlkem/poly.h
@@ -70,8 +70,8 @@ ENSURES(RETURN_VALUE == (int32_t)c + (((int32_t)c < 0) * MLKEM_Q));
 #define poly_compress MLKEM_NAMESPACE(poly_compress)
 void poly_compress(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES], const poly *a)
     // clang-format off
-REQUIRES(r != NULL && IS_FRESH(r, MLKEM_POLYCOMPRESSEDBYTES))
-REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly)))
+REQUIRES(IS_FRESH(r, MLKEM_POLYCOMPRESSEDBYTES))
+REQUIRES(IS_FRESH(a, sizeof(poly)))
 REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), a->coeffs, 0, (MLKEM_Q - 1)))
 ASSIGNS(OBJECT_WHOLE(r));
 // clang-format on
@@ -188,8 +188,8 @@ static inline uint16_t scalar_signed_to_unsigned_q_16(int16_t c) {
 #define poly_decompress MLKEM_NAMESPACE(poly_decompress)
 void poly_decompress(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES])
     // clang-format off
-REQUIRES(a != NULL && IS_FRESH(a, MLKEM_POLYCOMPRESSEDBYTES))
-REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
+REQUIRES(IS_FRESH(a, MLKEM_POLYCOMPRESSEDBYTES))
+REQUIRES(IS_FRESH(r, sizeof(poly)))
 ASSIGNS(OBJECT_WHOLE(r))
 ENSURES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), r->coeffs, 0, (MLKEM_Q - 1)));
 // clang-format on
@@ -197,7 +197,8 @@ ENSURES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), r->coeffs, 0, (MLKEM_Q - 1)));
 #define poly_tobytes MLKEM_NAMESPACE(poly_tobytes)
 void poly_tobytes(uint8_t r[MLKEM_POLYBYTES], const poly *a)
     // clang-format off
-REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly)))
+REQUIRES(IS_FRESH(r, MLKEM_POLYBYTES))
+REQUIRES(IS_FRESH(a, sizeof(poly)))
 REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), a->coeffs, 0, (MLKEM_Q - 1)))
 ASSIGNS(OBJECT_WHOLE(r));
 // clang-format on
@@ -206,8 +207,8 @@ ASSIGNS(OBJECT_WHOLE(r));
 #define poly_frombytes MLKEM_NAMESPACE(poly_frombytes)
 void poly_frombytes(poly *r, const uint8_t a[MLKEM_POLYBYTES])
     // clang-format off
-REQUIRES(a != NULL && IS_FRESH(a, MLKEM_POLYBYTES))
-REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
+REQUIRES(IS_FRESH(a, MLKEM_POLYBYTES))
+REQUIRES(IS_FRESH(r, sizeof(poly)))
 ASSIGNS(OBJECT_WHOLE(r))
 ENSURES(ARRAY_IN_BOUNDS(int, k, 0, (MLKEM_N - 1), r->coeffs, 0, 4095));
 // clang-format on
@@ -234,11 +235,11 @@ void poly_getnoise_eta1_4x(poly *r0, poly *r1, poly *r2, poly *r3,
                            const uint8_t seed[MLKEM_SYMBYTES], uint8_t nonce0,
                            uint8_t nonce1, uint8_t nonce2,
                            uint8_t nonce3)  // clang-format off
-REQUIRES(r0 != NULL && IS_FRESH(r0, sizeof(poly)))
-REQUIRES(r1 != NULL && IS_FRESH(r1, sizeof(poly)))
-REQUIRES(r2 != NULL && IS_FRESH(r2, sizeof(poly)))
-REQUIRES(r3 != NULL && IS_FRESH(r3, sizeof(poly)))
-REQUIRES(seed != NULL && IS_FRESH(seed, MLKEM_SYMBYTES))
+REQUIRES(IS_FRESH(r0, sizeof(poly)))
+REQUIRES(IS_FRESH(r1, sizeof(poly)))
+REQUIRES(IS_FRESH(r2, sizeof(poly)))
+REQUIRES(IS_FRESH(r3, sizeof(poly)))
+REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
 ASSIGNS(OBJECT_WHOLE(r0), OBJECT_WHOLE(r1), OBJECT_WHOLE(r2), OBJECT_WHOLE(r3))
 ENSURES(                                                                          \
     ARRAY_IN_BOUNDS(int, k0, 0, MLKEM_N - 1, r0->coeffs, -MLKEM_ETA1, MLKEM_ETA1) \
@@ -262,8 +263,8 @@ ENSURES(
  **************************************************/
 void poly_getnoise_eta2(poly *r, const uint8_t seed[MLKEM_SYMBYTES],
                         uint8_t nonce)  // clang-format off
-REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
-REQUIRES(seed != NULL && IS_FRESH(seed, MLKEM_SYMBYTES))
+REQUIRES(IS_FRESH(r, sizeof(poly)))
+REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
 ASSIGNS(OBJECT_WHOLE(r))
 ENSURES(ARRAY_IN_BOUNDS(int, k0, 0, MLKEM_N - 1, r->coeffs, -MLKEM_ETA2, MLKEM_ETA2));
 // clang-format on
@@ -285,11 +286,11 @@ void poly_getnoise_eta2_4x(poly *r0, poly *r1, poly *r2, poly *r3,
                            const uint8_t seed[MLKEM_SYMBYTES], uint8_t nonce0,
                            uint8_t nonce1, uint8_t nonce2,
                            uint8_t nonce3)  // clang-format off
-REQUIRES(r0 != NULL && IS_FRESH(r0, sizeof(poly)))
-REQUIRES(r1 != NULL && IS_FRESH(r1, sizeof(poly)))
-REQUIRES(r2 != NULL && IS_FRESH(r2, sizeof(poly)))
-REQUIRES(r3 != NULL && IS_FRESH(r3, sizeof(poly)))
-REQUIRES(seed != NULL && IS_FRESH(seed, MLKEM_SYMBYTES))
+REQUIRES(IS_FRESH(r0, sizeof(poly)))
+REQUIRES(IS_FRESH(r1, sizeof(poly)))
+REQUIRES(IS_FRESH(r2, sizeof(poly)))
+REQUIRES(IS_FRESH(r3, sizeof(poly)))
+REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
 ASSIGNS(OBJECT_WHOLE(r0), OBJECT_WHOLE(r1), OBJECT_WHOLE(r2), OBJECT_WHOLE(r3))
 ENSURES(                                                                          \
     ARRAY_IN_BOUNDS(int, k0, 0, MLKEM_N - 1, r0->coeffs, -MLKEM_ETA2, MLKEM_ETA2) \
@@ -315,11 +316,11 @@ void poly_getnoise_eta1122_4x(poly *r0, poly *r1, poly *r2, poly *r3,
                               const uint8_t seed[MLKEM_SYMBYTES],
                               uint8_t nonce0, uint8_t nonce1, uint8_t nonce2,
                               uint8_t nonce3)  // clang-format off
-REQUIRES(r0 != NULL && IS_FRESH(r0, sizeof(poly)))
-REQUIRES(r1 != NULL && IS_FRESH(r1, sizeof(poly)))
-REQUIRES(r2 != NULL && IS_FRESH(r2, sizeof(poly)))
-REQUIRES(r3 != NULL && IS_FRESH(r3, sizeof(poly)))
-REQUIRES(seed != NULL && IS_FRESH(seed, MLKEM_SYMBYTES))
+REQUIRES(IS_FRESH(r0, sizeof(poly)))
+REQUIRES(IS_FRESH(r1, sizeof(poly)))
+REQUIRES(IS_FRESH(r2, sizeof(poly)))
+REQUIRES(IS_FRESH(r3, sizeof(poly)))
+REQUIRES(IS_FRESH(seed, MLKEM_SYMBYTES))
 ASSIGNS(OBJECT_WHOLE(r0), OBJECT_WHOLE(r1), OBJECT_WHOLE(r2), OBJECT_WHOLE(r3))
 ENSURES(                                                                          \
     ARRAY_IN_BOUNDS(int, k0, 0, MLKEM_N - 1, r0->coeffs, -MLKEM_ETA1, MLKEM_ETA1) \
@@ -351,10 +352,10 @@ ENSURES(
 void poly_basemul_montgomery_cached(poly *r, const poly *a, const poly *b,
                                     const poly_mulcache *b_cache)
     // clang-format off
-REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
-REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly)))
-REQUIRES(b != NULL && IS_FRESH(b, sizeof(poly)))
-REQUIRES(b_cache != NULL && IS_FRESH(b_cache, sizeof(poly_mulcache)))
+REQUIRES(IS_FRESH(r, sizeof(poly)))
+REQUIRES(IS_FRESH(a, sizeof(poly)))
+REQUIRES(IS_FRESH(b, sizeof(poly)))
+REQUIRES(IS_FRESH(b_cache, sizeof(poly_mulcache)))
 REQUIRES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, a->coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)))
 ASSIGNS(OBJECT_WHOLE(r))
 ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -3 * HALF_Q + 1, 3 * HALF_Q - 1));
@@ -373,7 +374,7 @@ ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -3 * HALF_Q + 1, 3 *
  **************************************************/
 void poly_tomont(poly *r)
     // clang-format off
-REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
+REQUIRES(IS_FRESH(r, sizeof(poly)))
 ASSIGNS(OBJECT_WHOLE(r))
 ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -(MLKEM_Q - 1), (MLKEM_Q - 1)));
 // clang-format on
@@ -402,7 +403,8 @@ ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, -(MLKEM_Q - 1), (MLKE
 // higher level safety proofs, and thus not part of the spec.
 void poly_mulcache_compute(poly_mulcache *x, const poly *a)
     // clang-format off
-REQUIRES(a != NULL && IS_FRESH(a, sizeof(poly)))
+REQUIRES(IS_FRESH(x, sizeof(poly_mulcache)))
+REQUIRES(IS_FRESH(a, sizeof(poly)))
 ASSIGNS(OBJECT_WHOLE(x));
 // clang-format on
 
@@ -424,7 +426,7 @@ ASSIGNS(OBJECT_WHOLE(x));
 //             use of poly_reduce() in the context of (de)serialization.
 void poly_reduce(poly *r)
     // clang-format off
-REQUIRES(r != NULL && IS_FRESH(r, sizeof(poly)))
+REQUIRES(IS_FRESH(r, sizeof(poly)))
 ASSIGNS(OBJECT_WHOLE(r))
 ENSURES(ARRAY_IN_BOUNDS(int, k, 0, MLKEM_N - 1, r->coeffs, 0, MLKEM_Q - 1));
 // clang-format on
diff --git a/mlkem/polyvec.h b/mlkem/polyvec.h
index cde038e9d..ed0d4e219 100644
--- a/mlkem/polyvec.h
+++ b/mlkem/polyvec.h
@@ -71,7 +71,8 @@ void polyvec_basemul_acc_montgomery_cached(poly *r, const polyvec *a,
 // higher level safety proofs, and thus not part of the spec.
 void polyvec_mulcache_compute(polyvec_mulcache *x, const polyvec *a)
     // clang-format off
-REQUIRES(a != NULL && IS_FRESH(a, sizeof(polyvec)))
+REQUIRES(IS_FRESH(x, sizeof(polyvec_mulcache)))
+REQUIRES(IS_FRESH(a, sizeof(polyvec)))
 ASSIGNS(OBJECT_WHOLE(x));
 // clang-format on
 
diff --git a/mlkem/rej_uniform.h b/mlkem/rej_uniform.h
index 37a52b6aa..72bca73a8 100644
--- a/mlkem/rej_uniform.h
+++ b/mlkem/rej_uniform.h
@@ -36,8 +36,8 @@
 unsigned int rej_uniform(int16_t *r, unsigned int len, const uint8_t *buf,
                          unsigned int buflen)  // clang-format off
 REQUIRES(buflen <= 4096 && buflen % 3 == 0)
-REQUIRES(r != NULL && IS_FRESH(r, sizeof(int16_t) * len))
-REQUIRES(buf != NULL && IS_FRESH(buf, buflen))
+REQUIRES(IS_FRESH(r, sizeof(int16_t) * len))
+REQUIRES(IS_FRESH(buf, buflen))
 ASSIGNS(OBJECT_UPTO(r, len * sizeof(int16_t)))
 ENSURES(RETURN_VALUE <= len &&
         (RETURN_VALUE > 0 ==> ARRAY_IN_BOUNDS(int, k, 0, RETURN_VALUE - 1, r, 0, (MLKEM_Q - 1))));
diff --git a/mlkem/verify.h b/mlkem/verify.h
index 2c0e255a7..2f20f8ea3 100644
--- a/mlkem/verify.h
+++ b/mlkem/verify.h
@@ -28,7 +28,7 @@ void cmov(uint8_t *r, const uint8_t *x, size_t len, uint8_t b);
 void cmov_int16(int16_t *r, const int16_t v, const uint16_t b)
     // clang-format off
 REQUIRES(b == 0 || b == 1)
-REQUIRES(r != NULL && IS_FRESH(r, sizeof(int16_t)))
+REQUIRES(IS_FRESH(r, sizeof(int16_t)))
 ASSIGNS(OBJECT_WHOLE(r))
 ENSURES(*r == (b ? v : OLD(*r)));
 // clang-format on