diff --git a/.github/workflows/all.yml b/.github/workflows/all.yml
index 1afcd318e..5d3b7ccab 100644
--- a/.github/workflows/all.yml
+++ b/.github/workflows/all.yml
@@ -20,65 +20,65 @@ jobs:
       id-token: 'write'
     uses: ./.github/workflows/base.yml
     secrets: inherit
-  lint-markdown:
-    name: Lint Markdown
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    uses: ./.github/workflows/lint_markdown.yml
-  nix:
-    name: Nix
-    permissions:
-      actions: 'write'
-      contents: 'read'
-      id-token: 'write'
-    uses: ./.github/workflows/nix.yml
-    secrets: inherit
-  ci:
-    name: Extended
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    needs: [ base, nix ]
-    uses: ./.github/workflows/ci.yml
-    secrets: inherit
+  # lint-markdown:
+  #   name: Lint Markdown
+  #   permissions:
+  #     contents: 'read'
+  #     id-token: 'write'
+  #   uses: ./.github/workflows/lint_markdown.yml
+  # nix:
+  #   name: Nix
+  #   permissions:
+  #     actions: 'write'
+  #     contents: 'read'
+  #     id-token: 'write'
+  #   uses: ./.github/workflows/nix.yml
+  #   secrets: inherit
+  # ci:
+  #   name: Extended
+  #   permissions:
+  #     contents: 'read'
+  #     id-token: 'write'
+  #   needs: [ base, nix ]
+  #   uses: ./.github/workflows/ci.yml
+  #   secrets: inherit
   cbmc:
     name: CBMC
     permissions:
       contents: 'read'
       id-token: 'write'
-    needs: [ base, nix ]
+    # needs: [ base, nix ]
     uses: ./.github/workflows/cbmc.yml
     secrets: inherit
-  oqs_integration:
-    name: libOQS
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    needs: [ base ]
-    uses: ./.github/workflows/integration-liboqs.yml
-    secrets: inherit
-  ct-test:
-    name: Constant-time
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    needs: [ base, nix ]
-    uses: ./.github/workflows/ct-tests.yml
-    secrets: inherit
-  slothy:
-    name: SLOTHY
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    needs: [ base, nix ]
-    uses: ./.github/workflows/slothy.yml
-    secrets: inherit
-  baremetal:
-    name: Baremetal
-    permissions:
-      contents: 'read'
-      id-token: 'write'
-    needs: [ base ]
-    uses: ./.github/workflows/baremetal.yml
-    secrets: inherit
+  # oqs_integration:
+  #   name: libOQS
+  #   permissions:
+  #     contents: 'read'
+  #     id-token: 'write'
+  #   needs: [ base ]
+  #   uses: ./.github/workflows/integration-liboqs.yml
+  #   secrets: inherit
+  # ct-test:
+  #   name: Constant-time
+  #   permissions:
+  #     contents: 'read'
+  #     id-token: 'write'
+  #   needs: [ base, nix ]
+  #   uses: ./.github/workflows/ct-tests.yml
+  #   secrets: inherit
+  # slothy:
+  #   name: SLOTHY
+  #   permissions:
+  #     contents: 'read'
+  #     id-token: 'write'
+  #   needs: [ base, nix ]
+  #   uses: ./.github/workflows/slothy.yml
+  #   secrets: inherit
+  # baremetal:
+  #   name: Baremetal
+  #   permissions:
+  #     contents: 'read'
+  #     id-token: 'write'
+  #   needs: [ base ]
+  #   uses: ./.github/workflows/baremetal.yml
+  #   secrets: inherit
diff --git a/BIBLIOGRAPHY.md b/BIBLIOGRAPHY.md
index 731d2350d..49e698f14 100644
--- a/BIBLIOGRAPHY.md
+++ b/BIBLIOGRAPHY.md
@@ -39,6 +39,7 @@ source code and documentation.
   - [integration/liboqs/config_x86_64.h](integration/liboqs/config_x86_64.h)
   - [mldsa/mldsa_native_config.h](mldsa/mldsa_native_config.h)
   - [mldsa/src/sign.c](mldsa/src/sign.c)
+  - [proofs/cbmc/mldsa_native_config_cbmc.h](proofs/cbmc/mldsa_native_config_cbmc.h)
   - [test/break_pct_config.h](test/break_pct_config.h)
   - [test/custom_heap_alloc_config.h](test/custom_heap_alloc_config.h)
   - [test/custom_memcpy_config.h](test/custom_memcpy_config.h)
@@ -94,6 +95,7 @@ source code and documentation.
   - [mldsa/src/rounding.h](mldsa/src/rounding.h)
   - [mldsa/src/sign.c](mldsa/src/sign.c)
   - [mldsa/src/sign.h](mldsa/src/sign.h)
+  - [proofs/cbmc/mldsa_native_config_cbmc.h](proofs/cbmc/mldsa_native_config_cbmc.h)
   - [test/break_pct_config.h](test/break_pct_config.h)
   - [test/custom_memcpy_config.h](test/custom_memcpy_config.h)
   - [test/custom_memset_config.h](test/custom_memset_config.h)
diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c
index 02dd6e192..958f7d2f8 100644
--- a/mldsa/src/sign.c
+++ b/mldsa/src/sign.c
@@ -82,23 +82,28 @@ __contract__(
 static int mld_check_pct(uint8_t const pk[MLDSA_CRYPTO_PUBLICKEYBYTES],
                          uint8_t const sk[MLDSA_CRYPTO_SECRETKEYBYTES])
 {
+  typedef struct
+  {
+    MLD_ALIGN uint8_t signature[MLDSA_CRYPTO_BYTES];
+    MLD_ALIGN uint8_t pk_test[MLDSA_CRYPTO_PUBLICKEYBYTES];
+  } workspace;
+
   MLD_ALIGN uint8_t message[1] = {0};
   size_t siglen;
   int ret;
-  MLD_ALLOC(signature, uint8_t, MLDSA_CRYPTO_BYTES);
-  MLD_ALLOC(pk_test, uint8_t, MLDSA_CRYPTO_PUBLICKEYBYTES);
 
-  if (signature == NULL || pk_test == NULL)
+  MLD_ALLOC(ws, workspace, 1);
+  if (ws == NULL)
   {
     ret = MLD_ERR_OUT_OF_MEMORY;
     goto cleanup;
   }
 
   /* Copy public key for testing */
-  mld_memcpy(pk_test, pk, MLDSA_CRYPTO_PUBLICKEYBYTES);
+  mld_memcpy(ws->pk_test, pk, MLDSA_CRYPTO_PUBLICKEYBYTES);
 
   /* Sign a test message using the original secret key */
-  ret = crypto_sign_signature(signature, &siglen, message, sizeof(message),
+  ret = crypto_sign_signature(ws->signature, &siglen, message, sizeof(message),
                               NULL, 0, sk);
   if (ret != 0)
   {
@@ -109,18 +114,17 @@ static int mld_check_pct(uint8_t const pk[MLDSA_CRYPTO_PUBLICKEYBYTES],
   /* Deliberately break public key for testing purposes */
   if (mld_break_pct())
   {
-    pk_test[0] = ~pk_test[0];
+    ws->pk_test[0] = ~ws->pk_test[0];
   }
 #endif /* MLD_CONFIG_KEYGEN_PCT_BREAKAGE_TEST */
 
   /* Verify the signature using the (potentially corrupted) public key */
-  ret = crypto_sign_verify(signature, siglen, message, sizeof(message), NULL, 0,
-                           pk_test);
+  ret = crypto_sign_verify(ws->signature, siglen, message, sizeof(message),
+                           NULL, 0, ws->pk_test);
 
 cleanup:
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
-  MLD_FREE(pk_test, uint8_t, MLDSA_CRYPTO_PUBLICKEYBYTES);
-  MLD_FREE(signature, uint8_t, MLDSA_CRYPTO_BYTES);
+  MLD_FREE(ws, workspace, 1);
 
   return ret;
 }
@@ -227,29 +231,34 @@ __contract__(
   ensures(forall(k2, 0, MLDSA_K, array_bound(t1->vec[k2].coeffs, 0, MLDSA_N, 0, 1 << 10)))
   ensures(return_value == 0 || return_value == MLD_ERR_OUT_OF_MEMORY))
 {
+  typedef struct
+  {
+    mld_polymat mat;
+    mld_polyvecl s1hat;
+    mld_polyveck t;
+  } workspace;
+
   int ret;
-  MLD_ALLOC(mat, mld_polymat, 1);
-  MLD_ALLOC(s1hat, mld_polyvecl, 1);
-  MLD_ALLOC(t, mld_polyveck, 1);
 
-  if (mat == NULL || s1hat == NULL || t == NULL)
+  MLD_ALLOC(ws, workspace, 1);
+  if (ws == NULL)
   {
     ret = MLD_ERR_OUT_OF_MEMORY;
     goto cleanup;
   }
 
   /* Expand matrix */
-  mld_polyvec_matrix_expand(mat, rho);
+  mld_polyvec_matrix_expand(&ws->mat, rho);
 
   /* Matrix-vector multiplication */
-  *s1hat = *s1;
-  mld_polyvecl_ntt(s1hat);
-  mld_polyvec_matrix_pointwise_montgomery(t, mat, s1hat);
-  mld_polyveck_reduce(t);
-  mld_polyveck_invntt_tomont(t);
+  ws->s1hat = *s1;
+  mld_polyvecl_ntt(&ws->s1hat);
+  mld_polyvec_matrix_pointwise_montgomery(&ws->t, &ws->mat, &ws->s1hat);
+  mld_polyveck_reduce(&ws->t);
+  mld_polyveck_invntt_tomont(&ws->t);
 
   /* Add error vector s2 */
-  mld_polyveck_add(t, s2);
+  mld_polyveck_add(&ws->t, s2);
 
   /* Reference: The following reduction is not present in the reference
    *            implementation. Omitting this reduction requires the output of
@@ -260,11 +269,11 @@ __contract__(
    *            reasoning. We instead add an additional reduction, and can
    *            consequently, relax the bounds requirements for the invntt.
    */
-  mld_polyveck_reduce(t);
+  mld_polyveck_reduce(&ws->t);
 
   /* Decompose to get t1, t0 */
-  mld_polyveck_caddq(t);
-  mld_polyveck_power2round(t1, t0, t);
+  mld_polyveck_caddq(&ws->t);
+  mld_polyveck_power2round(t1, t0, &ws->t);
 
   /* Pack public key and compute tr */
   mld_pack_pk(pk, rho, t1);
@@ -274,9 +283,7 @@ __contract__(
 
 cleanup:
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
-  MLD_FREE(t, mld_polyveck, 1);
-  MLD_FREE(s1hat, mld_polyvecl, 1);
-  MLD_FREE(mat, mld_polymat, 1);
+  MLD_FREE(ws, workspace, 1);
   return ret;
 }
 
@@ -286,30 +293,34 @@ int crypto_sign_keypair_internal(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES],
                                  uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES],
                                  const uint8_t seed[MLDSA_SEEDBYTES])
 {
+  typedef struct
+  {
+    MLD_ALIGN uint8_t seedbuf[2 * MLDSA_SEEDBYTES + MLDSA_CRHBYTES];
+    MLD_ALIGN uint8_t inbuf[MLDSA_SEEDBYTES + 2];
+    MLD_ALIGN uint8_t tr[MLDSA_TRBYTES];
+    mld_polyvecl s1;
+    mld_polyveck s2;
+    mld_polyveck t1;
+    mld_polyveck t0;
+  } workspace;
+
   int ret;
   const uint8_t *rho, *rhoprime, *key;
-  MLD_ALLOC(seedbuf, uint8_t, 2 * MLDSA_SEEDBYTES + MLDSA_CRHBYTES);
-  MLD_ALLOC(inbuf, uint8_t, MLDSA_SEEDBYTES + 2);
-  MLD_ALLOC(tr, uint8_t, MLDSA_TRBYTES);
-  MLD_ALLOC(s1, mld_polyvecl, 1);
-  MLD_ALLOC(s2, mld_polyveck, 1);
-  MLD_ALLOC(t1, mld_polyveck, 1);
-  MLD_ALLOC(t0, mld_polyveck, 1);
-
-  if (seedbuf == NULL || inbuf == NULL || tr == NULL || s1 == NULL ||
-      s2 == NULL || t1 == NULL || t0 == NULL)
+
+  MLD_ALLOC(ws, workspace, 1);
+  if (ws == NULL)
   {
     ret = MLD_ERR_OUT_OF_MEMORY;
     goto cleanup;
   }
 
   /* Get randomness for rho, rhoprime and key */
-  mld_memcpy(inbuf, seed, MLDSA_SEEDBYTES);
-  inbuf[MLDSA_SEEDBYTES + 0] = MLDSA_K;
-  inbuf[MLDSA_SEEDBYTES + 1] = MLDSA_L;
-  mld_shake256(seedbuf, 2 * MLDSA_SEEDBYTES + MLDSA_CRHBYTES, inbuf,
+  mld_memcpy(ws->inbuf, seed, MLDSA_SEEDBYTES);
+  ws->inbuf[MLDSA_SEEDBYTES + 0] = MLDSA_K;
+  ws->inbuf[MLDSA_SEEDBYTES + 1] = MLDSA_L;
+  mld_shake256(ws->seedbuf, 2 * MLDSA_SEEDBYTES + MLDSA_CRHBYTES, ws->inbuf,
                MLDSA_SEEDBYTES + 2);
-  rho = seedbuf;
+  rho = ws->seedbuf;
   rhoprime = rho + MLDSA_SEEDBYTES;
   key = rhoprime + MLDSA_CRHBYTES;
 
@@ -317,30 +328,25 @@ int crypto_sign_keypair_internal(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES],
   MLD_CT_TESTING_DECLASSIFY(rho, MLDSA_SEEDBYTES);
 
   /* Sample s1 and s2 */
-  mld_sample_s1_s2(s1, s2, rhoprime);
+  mld_sample_s1_s2(&ws->s1, &ws->s2, rhoprime);
 
   /* Compute t0, t1, tr, and pk from rho, s1, s2 */
-  ret = mld_compute_t0_t1_tr_from_sk_components(t0, t1, tr, pk, rho, s1, s2);
+  ret = mld_compute_t0_t1_tr_from_sk_components(&ws->t0, &ws->t1, ws->tr, pk,
+                                                rho, &ws->s1, &ws->s2);
   if (ret != 0)
   {
     goto cleanup;
   }
 
   /* Pack secret key */
-  mld_pack_sk(sk, rho, tr, key, t0, s1, s2);
+  mld_pack_sk(sk, rho, ws->tr, key, &ws->t0, &ws->s1, &ws->s2);
 
   /* Constant time: pk is the public key, inherently public data */
   MLD_CT_TESTING_DECLASSIFY(pk, MLDSA_CRYPTO_PUBLICKEYBYTES);
 
 cleanup:
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
-  MLD_FREE(t0, mld_polyveck, 1);
-  MLD_FREE(t1, mld_polyveck, 1);
-  MLD_FREE(s2, mld_polyveck, 1);
-  MLD_FREE(s1, mld_polyvecl, 1);
-  MLD_FREE(tr, uint8_t, MLDSA_TRBYTES);
-  MLD_FREE(inbuf, uint8_t, MLDSA_SEEDBYTES + 2);
-  MLD_FREE(seedbuf, uint8_t, 2 * MLDSA_SEEDBYTES + MLDSA_CRHBYTES);
+  MLD_FREE(ws, workspace, 1);
 
   if (ret != 0)
   {
@@ -486,68 +492,71 @@ __contract__(
           return_value == MLD_ERR_OUT_OF_MEMORY)
 )
 {
+  typedef struct
+  {
+    MLD_ALIGN uint8_t challenge_bytes[MLDSA_CTILDEBYTES];
+    /* TODO: Remove the following workaround for
+     * https://github.com/diffblue/cbmc/issues/8813 */
+    MLD_ALIGN MLK_UNION_OR_STRUCT
+    {
+      mld_polyvecl y;
+      mld_polyveck h;
+    }
+    yh;
+    mld_polyvecl z;
+    mld_polyveck w1;
+    mld_polyveck w0;
+    mld_poly cp;
+  } workspace;
+
   unsigned int n;
   uint32_t z_invalid, w0_invalid, h_invalid;
   int ret;
-  /* TODO: Remove the following workaround for
-   * https://github.com/diffblue/cbmc/issues/8813 */
-  typedef MLK_UNION_OR_STRUCT
-  {
-    mld_polyvecl y;
-    mld_polyveck h;
-  }
-  yh_u;
   mld_polyvecl *y;
   mld_polyveck *h;
 
-  MLD_ALLOC(challenge_bytes, uint8_t, MLDSA_CTILDEBYTES);
-  MLD_ALLOC(yh, yh_u, 1);
-  MLD_ALLOC(z, mld_polyvecl, 1);
-  MLD_ALLOC(w1, mld_polyveck, 1);
-  MLD_ALLOC(w0, mld_polyveck, 1);
-  MLD_ALLOC(cp, mld_poly, 1);
-
-  if (challenge_bytes == NULL || yh == NULL || z == NULL || w1 == NULL ||
-      w0 == NULL || cp == NULL)
+  MLD_ALLOC(ws, workspace, 1);
+  if (ws == NULL)
   {
     ret = MLD_ERR_OUT_OF_MEMORY;
     goto cleanup;
   }
-  y = &yh->y;
-  h = &yh->h;
+
+  y = &ws->yh.y;
+  h = &ws->yh.h;
 
   /* Sample intermediate vector y */
   mld_polyvecl_uniform_gamma1(y, rhoprime, nonce);
 
   /* Matrix-vector multiplication */
-  *z = *y;
-  mld_polyvecl_ntt(z);
-  mld_polyvec_matrix_pointwise_montgomery(w0, mat, z);
-  mld_polyveck_reduce(w0);
-  mld_polyveck_invntt_tomont(w0);
+  ws->z = *y;
+  mld_polyvecl_ntt(&ws->z);
+  mld_polyvec_matrix_pointwise_montgomery(&ws->w0, mat, &ws->z);
+  mld_polyveck_reduce(&ws->w0);
+  mld_polyveck_invntt_tomont(&ws->w0);
 
   /* Decompose w and call the random oracle */
-  mld_polyveck_caddq(w0);
-  mld_polyveck_decompose(w1, w0);
-  mld_polyveck_pack_w1(sig, w1);
+  mld_polyveck_caddq(&ws->w0);
+  mld_polyveck_decompose(&ws->w1, &ws->w0);
+  mld_polyveck_pack_w1(sig, &ws->w1);
 
-  mld_H(challenge_bytes, MLDSA_CTILDEBYTES, mu, MLDSA_CRHBYTES, sig,
+  mld_H(ws->challenge_bytes, MLDSA_CTILDEBYTES, mu, MLDSA_CRHBYTES, sig,
         MLDSA_K * MLDSA_POLYW1_PACKEDBYTES, NULL, 0);
   /* Constant time: Leaking challenge_bytes does not reveal any information
    * about the secret key as H() is modelled as random oracle.
    * This also applies to challenges for rejected signatures.
    * See Section 5.5 of @[Round3_Spec]. */
-  MLD_CT_TESTING_DECLASSIFY(challenge_bytes, MLDSA_CTILDEBYTES);
-  mld_poly_challenge(cp, challenge_bytes);
-  mld_poly_ntt(cp);
+  MLD_CT_TESTING_DECLASSIFY(ws->challenge_bytes, MLDSA_CTILDEBYTES);
+  mld_poly_challenge(&ws->cp, ws->challenge_bytes);
+  mld_poly_ntt(&ws->cp);
 
   /* Compute z, reject if it reveals secret */
-  mld_polyvecl_pointwise_poly_montgomery(z, cp, s1);
-  mld_polyvecl_invntt_tomont(z);
-  mld_polyvecl_add(z, y);
-  mld_polyvecl_reduce(z);
+  mld_polyvecl_pointwise_poly_montgomery(&ws->z, &ws->cp, s1);
+  mld_polyvecl_invntt_tomont(&ws->z);
+  mld_polyvecl_add(&ws->z, y);
+  mld_polyvecl_reduce(&ws->z);
 
-  z_invalid = mld_polyvecl_chknorm(z, MLDSA_GAMMA1 - MLDSA_BETA);
+  z_invalid = mld_polyvecl_chknorm(&ws->z, MLDSA_GAMMA1 - MLDSA_BETA);
   /* Constant time: It is fine (and prohibitively expensive to avoid)
    * leaking the result of the norm check. In case of rejection it
    * would even be okay to leak which coefficient led to rejection
@@ -563,17 +572,17 @@ __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()             */
-  mld_assert_abs_bound_2d(z->vec, MLDSA_L, MLDSA_N,
+  mld_assert_abs_bound_2d(ws->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 */
-  mld_polyveck_pointwise_poly_montgomery(h, cp, s2);
+  mld_polyveck_pointwise_poly_montgomery(h, &ws->cp, s2);
   mld_polyveck_invntt_tomont(h);
-  mld_polyveck_sub(w0, h);
-  mld_polyveck_reduce(w0);
+  mld_polyveck_sub(&ws->w0, h);
+  mld_polyveck_reduce(&ws->w0);
 
-  w0_invalid = mld_polyveck_chknorm(w0, MLDSA_GAMMA2 - MLDSA_BETA);
+  w0_invalid = mld_polyveck_chknorm(&ws->w0, MLDSA_GAMMA2 - MLDSA_BETA);
   /* Constant time: w0_invalid may be leaked - see comment for z_invalid. */
   MLD_CT_TESTING_DECLASSIFY(&w0_invalid, sizeof(uint32_t));
   if (w0_invalid)
@@ -583,7 +592,7 @@ __contract__(
   }
 
   /* Compute hints for w1 */
-  mld_polyveck_pointwise_poly_montgomery(h, cp, t0);
+  mld_polyveck_pointwise_poly_montgomery(h, &ws->cp, t0);
   mld_polyveck_invntt_tomont(h);
   mld_polyveck_reduce(h);
 
@@ -596,7 +605,7 @@ __contract__(
     goto cleanup;
   }
 
-  mld_polyveck_add(w0, h);
+  mld_polyveck_add(&ws->w0, h);
 
   /* Constant time: At this point all norm checks have passed and we, hence,
    * know that the signature does not leak any secret information.
@@ -606,9 +615,9 @@ __contract__(
    * h=c*t0 is public as both c and t0 are public.
    * For a more detailed discussion, refer to https://eprint.iacr.org/2022/1406.
    */
-  MLD_CT_TESTING_DECLASSIFY(w0, sizeof(*w0));
-  MLD_CT_TESTING_DECLASSIFY(w1, sizeof(*w1));
-  n = mld_polyveck_make_hint(h, w0, w1);
+  MLD_CT_TESTING_DECLASSIFY(&ws->w0, sizeof(ws->w0));
+  MLD_CT_TESTING_DECLASSIFY(&ws->w1, sizeof(ws->w1));
+  n = mld_polyveck_make_hint(h, &ws->w0, &ws->w1);
   if (n > MLDSA_OMEGA)
   {
     ret = MLD_ERR_FAIL; /* reject */
@@ -619,19 +628,14 @@ __contract__(
   /* Constant time: At this point it is clear that the signature is valid - it
    * can, hence, be considered public. */
   MLD_CT_TESTING_DECLASSIFY(h, sizeof(*h));
-  MLD_CT_TESTING_DECLASSIFY(z, sizeof(*z));
-  mld_pack_sig(sig, challenge_bytes, z, h, n);
+  MLD_CT_TESTING_DECLASSIFY(&ws->z, sizeof(ws->z));
+  mld_pack_sig(sig, ws->challenge_bytes, &ws->z, h, n);
 
   ret = 0; /* success */
 
 cleanup:
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
-  MLD_FREE(cp, mld_poly, 1);
-  MLD_FREE(w0, mld_polyveck, 1);
-  MLD_FREE(w1, mld_polyveck, 1);
-  MLD_FREE(z, mld_polyvecl, 1);
-  MLD_FREE(yh, yh_u, 1);
-  MLD_FREE(challenge_bytes, uint8_t, MLDSA_CTILDEBYTES);
+  MLD_FREE(ws, workspace, 1);
 
   return ret;
 }
@@ -643,28 +647,33 @@ int crypto_sign_signature_internal(
     const uint8_t rnd[MLDSA_RNDBYTES],
     const uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES], int externalmu)
 {
+  typedef struct
+  {
+    MLD_ALIGN uint8_t
+        seedbuf[2 * MLDSA_SEEDBYTES + MLDSA_TRBYTES + 2 * MLDSA_CRHBYTES];
+    mld_polymat mat;
+    mld_polyvecl s1;
+    mld_polyveck t0;
+    mld_polyveck s2;
+  } workspace;
+
   int ret;
   uint8_t *rho, *tr, *key, *mu, *rhoprime;
   uint16_t nonce = 0;
-  MLD_ALLOC(seedbuf, uint8_t,
-            2 * MLDSA_SEEDBYTES + MLDSA_TRBYTES + 2 * MLDSA_CRHBYTES);
-  MLD_ALLOC(mat, mld_polymat, 1);
-  MLD_ALLOC(s1, mld_polyvecl, 1);
-  MLD_ALLOC(t0, mld_polyveck, 1);
-  MLD_ALLOC(s2, mld_polyveck, 1);
-
-  if (seedbuf == NULL || mat == NULL || s1 == NULL || t0 == NULL || s2 == NULL)
+
+  MLD_ALLOC(ws, workspace, 1);
+  if (ws == NULL)
   {
     ret = MLD_ERR_OUT_OF_MEMORY;
     goto cleanup;
   }
 
-  rho = seedbuf;
+  rho = ws->seedbuf;
   tr = rho + MLDSA_SEEDBYTES;
   key = tr + MLDSA_TRBYTES;
   mu = key + MLDSA_SEEDBYTES;
   rhoprime = mu + MLDSA_CRHBYTES;
-  mld_unpack_sk(rho, tr, key, t0, s1, s2, sk);
+  mld_unpack_sk(rho, tr, key, &ws->t0, &ws->s1, &ws->s2, sk);
 
   if (!externalmu)
   {
@@ -684,10 +693,10 @@ int crypto_sign_signature_internal(
   /* Constant time: rho is part of the public key and, hence, public. */
   MLD_CT_TESTING_DECLASSIFY(rho, MLDSA_SEEDBYTES);
   /* Expand matrix and transform vectors */
-  mld_polyvec_matrix_expand(mat, rho);
-  mld_polyvecl_ntt(s1);
-  mld_polyveck_ntt(s2);
-  mld_polyveck_ntt(t0);
+  mld_polyvec_matrix_expand(&ws->mat, rho);
+  mld_polyvecl_ntt(&ws->s1);
+  mld_polyveck_ntt(&ws->s2);
+  mld_polyveck_ntt(&ws->t0);
 
   /* By default, return failure. Flip to success and write output
    * once signature generation succeeds. */
@@ -705,10 +714,10 @@ int crypto_sign_signature_internal(
     /* loop. We can therefore re-assert their bounds here as part of the     */
     /* loop invariant. This makes proof noticeably faster with CBMC          */
     invariant(forall(k1, 0, MLDSA_K, forall(l1, 0, MLDSA_L,
-              array_bound(mat->vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
-    invariant(forall(k2, 0, MLDSA_K, array_abs_bound(t0->vec[k2].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
-    invariant(forall(k3, 0, MLDSA_L, array_abs_bound(s1->vec[k3].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
-    invariant(forall(k4, 0, MLDSA_K, array_abs_bound(s2->vec[k4].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
+              array_bound(ws->mat.vec[k1].vec[l1].coeffs, 0, MLDSA_N, 0, MLDSA_Q))))
+    invariant(forall(k2, 0, MLDSA_K, array_abs_bound(ws->t0.vec[k2].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
+    invariant(forall(k3, 0, MLDSA_L, array_abs_bound(ws->s1.vec[k3].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
+    invariant(forall(k4, 0, MLDSA_K, array_abs_bound(ws->s2.vec[k4].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
     invariant(ret == MLD_ERR_FAIL)
   )
   {
@@ -723,8 +732,8 @@ int crypto_sign_signature_internal(
       break;
     }
 
-    ret = mld_attempt_signature_generation(sig, mu, rhoprime, nonce, mat, s1,
-                                           s2, t0);
+    ret = mld_attempt_signature_generation(sig, mu, rhoprime, nonce, &ws->mat,
+                                           &ws->s1, &ws->s2, &ws->t0);
     nonce++;
     if (ret == 0)
     {
@@ -750,12 +759,7 @@ int crypto_sign_signature_internal(
   }
 
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
-  MLD_FREE(s2, mld_polyveck, 1);
-  MLD_FREE(t0, mld_polyveck, 1);
-  MLD_FREE(s1, mld_polyvecl, 1);
-  MLD_FREE(mat, mld_polymat, 1);
-  MLD_FREE(seedbuf, uint8_t,
-           2 * MLDSA_SEEDBYTES + MLDSA_TRBYTES + 2 * MLDSA_CRHBYTES);
+  MLD_FREE(ws, workspace, 1);
   return ret;
 }
 
@@ -767,19 +771,24 @@ int crypto_sign_signature(uint8_t sig[MLDSA_CRYPTO_BYTES], size_t *siglen,
                           size_t ctxlen,
                           const uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES])
 {
+  typedef struct
+  {
+    MLD_ALIGN uint8_t pre[MLD_DOMAIN_SEPARATION_MAX_BYTES];
+    MLD_ALIGN uint8_t rnd[MLDSA_RNDBYTES];
+  } workspace;
+
   size_t pre_len;
   int ret;
-  MLD_ALLOC(pre, uint8_t, MLD_DOMAIN_SEPARATION_MAX_BYTES);
-  MLD_ALLOC(rnd, uint8_t, MLDSA_RNDBYTES);
 
-  if (pre == NULL || rnd == NULL)
+  MLD_ALLOC(ws, workspace, 1);
+  if (ws == NULL)
   {
     ret = MLD_ERR_OUT_OF_MEMORY;
     goto cleanup;
   }
 
   /* Prepare domain separation prefix for pure ML-DSA */
-  pre_len = mld_prepare_domain_separation_prefix(pre, NULL, 0, ctx, ctxlen,
+  pre_len = mld_prepare_domain_separation_prefix(ws->pre, NULL, 0, ctx, ctxlen,
                                                  MLD_PREHASH_NONE);
   if (pre_len == 0)
   {
@@ -789,11 +798,11 @@ int crypto_sign_signature(uint8_t sig[MLDSA_CRYPTO_BYTES], size_t *siglen,
 
   /* Randomized variant of ML-DSA. If you need the deterministic variant,
    * call crypto_sign_signature_internal directly with all-zero rnd. */
-  mld_randombytes(rnd, MLDSA_RNDBYTES);
-  MLD_CT_TESTING_SECRET(rnd, sizeof(rnd));
+  mld_randombytes(ws->rnd, MLDSA_RNDBYTES);
+  MLD_CT_TESTING_SECRET(ws->rnd, sizeof(ws->rnd));
 
-  ret = crypto_sign_signature_internal(sig, siglen, m, mlen, pre, pre_len, rnd,
-                                       sk, 0);
+  ret = crypto_sign_signature_internal(sig, siglen, m, mlen, ws->pre, pre_len,
+                                       ws->rnd, sk, 0);
 
 cleanup:
   if (ret != 0)
@@ -809,8 +818,7 @@ int crypto_sign_signature(uint8_t sig[MLDSA_CRYPTO_BYTES], size_t *siglen,
   }
 
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
-  MLD_FREE(rnd, uint8_t, MLDSA_RNDBYTES);
-  MLD_FREE(pre, uint8_t, MLD_DOMAIN_SEPARATION_MAX_BYTES);
+  MLD_FREE(ws, workspace, 1);
 
   return ret;
 }
@@ -874,24 +882,27 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
                                 const uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES],
                                 int externalmu)
 {
+  typedef struct
+  {
+    MLD_ALIGN uint8_t buf[MLDSA_K * MLDSA_POLYW1_PACKEDBYTES];
+    MLD_ALIGN uint8_t rho[MLDSA_SEEDBYTES];
+    MLD_ALIGN uint8_t mu[MLDSA_CRHBYTES];
+    MLD_ALIGN uint8_t c[MLDSA_CTILDEBYTES];
+    MLD_ALIGN uint8_t c2[MLDSA_CTILDEBYTES];
+    mld_poly cp;
+    mld_polymat mat;
+    mld_polyvecl z;
+    mld_polyveck t1;
+    mld_polyveck w1;
+    mld_polyveck tmp;
+    mld_polyveck h;
+  } workspace;
+
   unsigned int i;
   int ret;
-  MLD_ALLOC(buf, uint8_t, (MLDSA_K * MLDSA_POLYW1_PACKEDBYTES));
-  MLD_ALLOC(rho, uint8_t, MLDSA_SEEDBYTES);
-  MLD_ALLOC(mu, uint8_t, MLDSA_CRHBYTES);
-  MLD_ALLOC(c, uint8_t, MLDSA_CTILDEBYTES);
-  MLD_ALLOC(c2, uint8_t, MLDSA_CTILDEBYTES);
-  MLD_ALLOC(cp, mld_poly, 1);
-  MLD_ALLOC(mat, mld_polymat, 1);
-  MLD_ALLOC(z, mld_polyvecl, 1);
-  MLD_ALLOC(t1, mld_polyveck, 1);
-  MLD_ALLOC(w1, mld_polyveck, 1);
-  MLD_ALLOC(tmp, mld_polyveck, 1);
-  MLD_ALLOC(h, mld_polyveck, 1);
-
-  if (buf == NULL || rho == NULL || mu == NULL || c == NULL || c2 == NULL ||
-      cp == NULL || mat == NULL || z == NULL || t1 == NULL || w1 == NULL ||
-      tmp == NULL || h == NULL)
+
+  MLD_ALLOC(ws, workspace, 1);
+  if (ws == NULL)
   {
     ret = MLD_ERR_OUT_OF_MEMORY;
     goto cleanup;
@@ -903,17 +914,17 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
     goto cleanup;
   }
 
-  mld_unpack_pk(rho, t1, pk);
+  mld_unpack_pk(ws->rho, &ws->t1, pk);
 
   /* mld_unpack_sig and mld_polyvecl_chknorm signal failure through a
    * single non-zero error code that's not yet aligned with MLD_ERR_XXX.
    * Map it to MLD_ERR_FAIL explicitly. */
-  if (mld_unpack_sig(c, z, h, sig))
+  if (mld_unpack_sig(ws->c, &ws->z, &ws->h, sig))
   {
     ret = MLD_ERR_FAIL;
     goto cleanup;
   }
-  if (mld_polyvecl_chknorm(z, MLDSA_GAMMA1 - MLDSA_BETA))
+  if (mld_polyvecl_chknorm(&ws->z, MLDSA_GAMMA1 - MLDSA_BETA))
   {
     ret = MLD_ERR_FAIL;
     goto cleanup;
@@ -925,7 +936,7 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
     MLD_ALIGN uint8_t hpk[MLDSA_CRHBYTES];
     mld_H(hpk, MLDSA_TRBYTES, pk, MLDSA_CRYPTO_PUBLICKEYBYTES, NULL, 0, NULL,
           0);
-    mld_H(mu, MLDSA_CRHBYTES, hpk, MLDSA_TRBYTES, pre, prelen, m, mlen);
+    mld_H(ws->mu, MLDSA_CRHBYTES, hpk, MLDSA_TRBYTES, pre, prelen, m, mlen);
 
     /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
     mld_zeroize(hpk, sizeof(hpk));
@@ -933,32 +944,32 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
   else
   {
     /* mu has been provided directly */
-    mld_memcpy(mu, m, MLDSA_CRHBYTES);
+    mld_memcpy(ws->mu, m, MLDSA_CRHBYTES);
   }
 
   /* Matrix-vector multiplication; compute Az - c2^dt1 */
-  mld_poly_challenge(cp, c);
-  mld_polyvec_matrix_expand(mat, rho);
+  mld_poly_challenge(&ws->cp, ws->c);
+  mld_polyvec_matrix_expand(&ws->mat, ws->rho);
 
-  mld_polyvecl_ntt(z);
-  mld_polyvec_matrix_pointwise_montgomery(w1, mat, z);
+  mld_polyvecl_ntt(&ws->z);
+  mld_polyvec_matrix_pointwise_montgomery(&ws->w1, &ws->mat, &ws->z);
 
-  mld_poly_ntt(cp);
-  mld_polyveck_shiftl(t1);
-  mld_polyveck_ntt(t1);
+  mld_poly_ntt(&ws->cp);
+  mld_polyveck_shiftl(&ws->t1);
+  mld_polyveck_ntt(&ws->t1);
 
-  mld_polyveck_pointwise_poly_montgomery(tmp, cp, t1);
+  mld_polyveck_pointwise_poly_montgomery(&ws->tmp, &ws->cp, &ws->t1);
 
-  mld_polyveck_sub(w1, tmp);
-  mld_polyveck_reduce(w1);
-  mld_polyveck_invntt_tomont(w1);
+  mld_polyveck_sub(&ws->w1, &ws->tmp);
+  mld_polyveck_reduce(&ws->w1);
+  mld_polyveck_invntt_tomont(&ws->w1);
 
   /* Reconstruct w1 */
-  mld_polyveck_caddq(w1);
-  mld_polyveck_use_hint(tmp, w1, h);
-  mld_polyveck_pack_w1(buf, tmp);
+  mld_polyveck_caddq(&ws->w1);
+  mld_polyveck_use_hint(&ws->tmp, &ws->w1, &ws->h);
+  mld_polyveck_pack_w1(ws->buf, &ws->tmp);
   /* Call random oracle and verify challenge */
-  mld_H(c2, MLDSA_CTILDEBYTES, mu, MLDSA_CRHBYTES, buf,
+  mld_H(ws->c2, MLDSA_CTILDEBYTES, ws->mu, MLDSA_CRHBYTES, ws->buf,
         MLDSA_K * MLDSA_POLYW1_PACKEDBYTES, NULL, 0);
 
   /* Constant time: All data in verification is usually considered public.
@@ -969,14 +980,14 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
    * a hash call (that should behave like a random oracle), it is safe to
    * declassify here even with a secret message.
    */
-  MLD_CT_TESTING_DECLASSIFY(c2, MLDSA_CTILDEBYTES);
+  MLD_CT_TESTING_DECLASSIFY(ws->c2, MLDSA_CTILDEBYTES);
   ret = MLD_ERR_FAIL;
   for (i = 0; i < MLDSA_CTILDEBYTES; ++i)
   __loop__(
     invariant(i <= MLDSA_CTILDEBYTES)
   )
   {
-    if (c[i] != c2[i])
+    if (ws->c[i] != ws->c2[i])
     {
       goto cleanup;
     }
@@ -986,18 +997,7 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen,
 
 cleanup:
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
-  MLD_FREE(h, mld_polyveck, 1);
-  MLD_FREE(tmp, mld_polyveck, 1);
-  MLD_FREE(w1, mld_polyveck, 1);
-  MLD_FREE(t1, mld_polyveck, 1);
-  MLD_FREE(z, mld_polyvecl, 1);
-  MLD_FREE(mat, mld_polymat, 1);
-  MLD_FREE(cp, mld_poly, 1);
-  MLD_FREE(c2, uint8_t, MLDSA_CTILDEBYTES);
-  MLD_FREE(c, uint8_t, MLDSA_CTILDEBYTES);
-  MLD_FREE(mu, uint8_t, MLDSA_CRHBYTES);
-  MLD_FREE(rho, uint8_t, MLDSA_SEEDBYTES);
-  MLD_FREE(buf, uint8_t, (MLDSA_K * MLDSA_POLYW1_PACKEDBYTES));
+  MLD_FREE(ws, workspace, 1);
   return ret;
 }
 
@@ -1314,40 +1314,44 @@ MLD_EXTERNAL_API
 int crypto_sign_pk_from_sk(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES],
                            const uint8_t sk[MLDSA_CRYPTO_SECRETKEYBYTES])
 {
+  typedef struct
+  {
+    MLD_ALIGN uint8_t rho[MLDSA_SEEDBYTES];
+    MLD_ALIGN uint8_t tr[MLDSA_TRBYTES];
+    MLD_ALIGN uint8_t tr_computed[MLDSA_TRBYTES];
+    MLD_ALIGN uint8_t key[MLDSA_SEEDBYTES];
+    mld_polyvecl s1;
+    mld_polyveck s2;
+    mld_polyveck t0;
+    mld_polyveck t0_computed;
+    mld_polyveck t1;
+  } workspace;
+
   uint8_t cmp, cmp0, cmp1;
   int ret;
-  MLD_ALLOC(rho, uint8_t, MLDSA_SEEDBYTES);
-  MLD_ALLOC(tr, uint8_t, MLDSA_TRBYTES);
-  MLD_ALLOC(tr_computed, uint8_t, MLDSA_TRBYTES);
-  MLD_ALLOC(key, uint8_t, MLDSA_SEEDBYTES);
-  MLD_ALLOC(s1, mld_polyvecl, 1);
-  MLD_ALLOC(s2, mld_polyveck, 1);
-  MLD_ALLOC(t0, mld_polyveck, 1);
-  MLD_ALLOC(t0_computed, mld_polyveck, 1);
-  MLD_ALLOC(t1, mld_polyveck, 1);
-
-  if (rho == NULL || tr == NULL || tr_computed == NULL || key == NULL ||
-      s1 == NULL || s2 == NULL || t0 == NULL || t0_computed == NULL ||
-      t1 == NULL)
+
+  MLD_ALLOC(ws, workspace, 1);
+  if (ws == NULL)
   {
     ret = MLD_ERR_OUT_OF_MEMORY;
     goto cleanup;
   }
 
   /* Unpack secret key */
-  mld_unpack_sk(rho, tr, key, t0, s1, s2, sk);
+  mld_unpack_sk(ws->rho, ws->tr, ws->key, &ws->t0, &ws->s1, &ws->s2, sk);
 
   /* Recompute t0, t1, tr, and pk from rho, s1, s2 */
-  ret = mld_compute_t0_t1_tr_from_sk_components(t0_computed, t1, tr_computed,
-                                                pk, rho, s1, s2);
+  ret = mld_compute_t0_t1_tr_from_sk_components(&ws->t0_computed, &ws->t1,
+                                                ws->tr_computed, pk, ws->rho,
+                                                &ws->s1, &ws->s2);
   if (ret != 0)
   {
     goto cleanup;
   }
 
   /* Validate t0 and tr using constant-time comparisons */
-  cmp0 = mld_ct_memcmp(t0, t0_computed, sizeof(mld_polyveck));
-  cmp1 = mld_ct_memcmp(tr, tr_computed, MLDSA_TRBYTES);
+  cmp0 = mld_ct_memcmp(&ws->t0, &ws->t0_computed, sizeof(mld_polyveck));
+  cmp1 = mld_ct_memcmp(ws->tr, ws->tr_computed, MLDSA_TRBYTES);
   cmp = mld_value_barrier_u8(cmp0 | cmp1);
 
   /* Declassify the final result of the validity check. */
@@ -1365,15 +1369,7 @@ int crypto_sign_pk_from_sk(uint8_t pk[MLDSA_CRYPTO_PUBLICKEYBYTES],
   MLD_CT_TESTING_DECLASSIFY(pk, MLDSA_CRYPTO_PUBLICKEYBYTES);
 
   /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */
-  MLD_FREE(t1, mld_polyveck, 1);
-  MLD_FREE(t0_computed, mld_polyveck, 1);
-  MLD_FREE(t0, mld_polyveck, 1);
-  MLD_FREE(s2, mld_polyveck, 1);
-  MLD_FREE(s1, mld_polyvecl, 1);
-  MLD_FREE(key, uint8_t, MLDSA_SEEDBYTES);
-  MLD_FREE(tr_computed, uint8_t, MLDSA_TRBYTES);
-  MLD_FREE(tr, uint8_t, MLDSA_TRBYTES);
-  MLD_FREE(rho, uint8_t, MLDSA_SEEDBYTES);
+  MLD_FREE(ws, workspace, 1);
 
   return ret;
 }
diff --git a/proofs/cbmc/H/H_harness.c b/proofs/cbmc/H/H_harness.c
index 8cbbb48af..5e1eb4164 100644
--- a/proofs/cbmc/H/H_harness.c
+++ b/proofs/cbmc/H/H_harness.c
@@ -9,6 +9,11 @@ void mld_H(uint8_t *out, size_t outlen, const uint8_t *in1, size_t in1len,
 
 void harness(void)
 {
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
   uint8_t *out;
   size_t outlen;
   const uint8_t *in1;
diff --git a/proofs/cbmc/Makefile.common b/proofs/cbmc/Makefile.common
index 867888cfa..ce3df0a8e 100644
--- a/proofs/cbmc/Makefile.common
+++ b/proofs/cbmc/Makefile.common
@@ -247,7 +247,7 @@ endif
 #   * an entire project when added to Makefile-project-defines
 #   * a specific proof when added to the harness Makefile
 
-CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-fail-assert
+CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-may-fail --malloc-fail-null # alloc may fail with returning NULL
 CBMC_FLAG_BOUNDS_CHECK ?= # set to --no-bounds-check to disable
 CBMC_FLAG_CONVERSION_CHECK ?= --conversion-check
 CBMC_FLAG_DIV_BY_ZERO_CHECK ?= # set to --no-div-by-zero-check to disable
@@ -555,6 +555,7 @@ ifndef MLD_CONFIG_PARAMETER_SET
     $(error MLD_CONFIG_PARAMETER_SET not set)
 endif
 
+DEFINES += -DMLD_CONFIG_FILE="\"mldsa_native_config_cbmc.h\""
 DEFINES += -DMLD_CONFIG_PARAMETER_SET=$(MLD_CONFIG_PARAMETER_SET)
 # Give visibility to all static functions
 DEFINES += -Dstatic=
diff --git a/proofs/cbmc/check_pct/Makefile b/proofs/cbmc/check_pct/Makefile
index 06d1eda47..21d975d08 100644
--- a/proofs/cbmc/check_pct/Makefile
+++ b/proofs/cbmc/check_pct/Makefile
@@ -10,7 +10,7 @@ HARNESS_FILE = check_pct_harness
 # Litani dashboard. It can be human-readable and contain spaces if you wish.
 PROOF_UID = mld_check_pct
 
-DEFINES += -DMLD_CONFIG_KEYGEN_PCT
+DEFINES +=
 INCLUDES +=
 
 REMOVE_FUNCTION_BODY +=
diff --git a/proofs/cbmc/crypto_sign_signature_internal/Makefile b/proofs/cbmc/crypto_sign_signature_internal/Makefile
index 9fefe5f9d..fe4acb632 100644
--- a/proofs/cbmc/crypto_sign_signature_internal/Makefile
+++ b/proofs/cbmc/crypto_sign_signature_internal/Makefile
@@ -46,7 +46,7 @@ FUNCTION_NAME = crypto_sign_signature_internal
 # EXPENSIVE = true
 
 # This function is large enough to need...
-CBMC_OBJECT_BITS = 8
+CBMC_OBJECT_BITS = 9
 
 # If you require access to a file-local ("static") function or object to conduct
 # your proof, set the following (and do not include the original source file
diff --git a/proofs/cbmc/mldsa_native_config_cbmc.h b/proofs/cbmc/mldsa_native_config_cbmc.h
new file mode 100644
index 000000000..b25de479d
--- /dev/null
+++ b/proofs/cbmc/mldsa_native_config_cbmc.h
@@ -0,0 +1,715 @@
+/*
+ * Copyright (c) The mldsa-native project authors
+ * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+ */
+
+/* References
+ * ==========
+ *
+ * - [FIPS140_3_IG]
+ *   Implementation Guidance for FIPS 140-3 and the Cryptographic Module
+ *   Validation Program
+ *   National Institute of Standards and Technology
+ *   https://csrc.nist.gov/projects/cryptographic-module-validation-program/fips-140-3-ig-announcements
+ *
+ * - [FIPS204]
+ *   FIPS 204 Module-Lattice-Based Digital Signature Standard
+ *   National Institute of Standards and Technology
+ *   https://csrc.nist.gov/pubs/fips/204/final
+ */
+
+/*
+ * WARNING: This file is auto-generated from scripts/autogen
+ *          in the mldsa-native repository.
+ *          Do not modify it directly.
+ */
+
+/*
+ * Test configuration: mldsa-native configuration used for CBMC proofs, using
+ * instrumented alloc/free
+ *
+ * This configuration differs from the default mldsa/mldsa_native_config.h in
+ * the following places:
+ *   - MLD_CONFIG_KEYGEN_PCT
+ *   - MLD_CONFIG_CUSTOM_ALLOC_FREE
+ */
+
+
+#ifndef MLD_CONFIG_H
+#define MLD_CONFIG_H
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_PARAMETER_SET
+ *
+ * Description: Specifies the parameter set for ML-DSA
+ *              - MLD_CONFIG_PARAMETER_SET=44 corresponds to ML-DSA-44
+ *              - MLD_CONFIG_PARAMETER_SET=65 corresponds to ML-DSA-65
+ *              - MLD_CONFIG_PARAMETER_SET=87 corresponds to ML-DSA-87
+ *
+ *              If you want to support multiple parameter sets, build the
+ *              library multiple times and set MLD_CONFIG_MULTILEVEL_BUILD.
+ *              See MLD_CONFIG_MULTILEVEL_BUILD for how to do this while
+ *              minimizing code duplication.
+ *
+ *              This can also be set using CFLAGS.
+ *
+ *****************************************************************************/
+#ifndef MLD_CONFIG_PARAMETER_SET
+#define MLD_CONFIG_PARAMETER_SET \
+  44 /* Change this for different security strengths */
+#endif
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_FILE
+ *
+ * Description: If defined, this is a header that will be included instead
+ *              of the default configuration file mldsa/mldsa_native_config.h.
+ *
+ *              When you need to build mldsa-native in multiple configurations,
+ *              using varying MLD_CONFIG_FILE can be more convenient
+ *              then configuring everything through CFLAGS.
+ *
+ *              To use, MLD_CONFIG_FILE _must_ be defined prior
+ *              to the inclusion of any mldsa-native headers. For example,
+ *              it can be set by passing `-DMLD_CONFIG_FILE="..."`
+ *              on the command line.
+ *
+ *****************************************************************************/
+/* No need to set this -- we _are_ already in a custom config */
+/* #define MLD_CONFIG_FILE "mldsa_native_config.h" */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_NAMESPACE_PREFIX
+ *
+ * Description: The prefix to use to namespace global symbols from mldsa/.
+ *
+ *              In a multi-level build, level-dependent symbols will
+ *              additionally be prefixed with the parameter set (44/65/87).
+ *
+ *              This can also be set using CFLAGS.
+ *
+ *****************************************************************************/
+#if !defined(MLD_CONFIG_NAMESPACE_PREFIX)
+#define MLD_CONFIG_NAMESPACE_PREFIX MLD_DEFAULT_NAMESPACE_PREFIX
+#endif
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_MULTILEVEL_BUILD
+ *
+ * Description: Set this if the build is part of a multi-level build supporting
+ *              multiple parameter sets.
+ *
+ *              If you need only a single parameter set, keep this unset.
+ *
+ *              To build mldsa-native with support for all parameter sets,
+ *              build it three times -- once per parameter set -- and set the
+ *              option MLD_CONFIG_MULTILEVEL_WITH_SHARED for exactly one of
+ *              them, and MLD_CONFIG_MULTILEVEL_NO_SHARED for the others.
+ *              MLD_CONFIG_MULTILEVEL_BUILD should be set for all of them.
+ *
+ *              See examples/multilevel_build for an example.
+ *
+ *              This can also be set using CFLAGS.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_MULTILEVEL_BUILD */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_EXTERNAL_API_QUALIFIER
+ *
+ * Description: If set, this option provides an additional function
+ *              qualifier to be added to declarations of mldsa-native's
+ *              public API.
+ *
+ *              The primary use case for this option are single-CU builds
+ *              where the public API exposed by mldsa-native is wrapped by
+ *              another API in the consuming application. In this case,
+ *              even mldsa-native's public API can be marked `static`.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_EXTERNAL_API_QUALIFIER */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_NO_RANDOMIZED_API
+ *
+ * Description: If this option is set, mldsa-native will be built without the
+ *              randomized API functions (crypto_sign_keypair,
+ *              crypto_sign, crypto_sign_signature, and
+ *              crypto_sign_signature_extmu).
+ *              This allows users to build mldsa-native without providing a
+ *              randombytes() implementation if they only need the
+ *              internal deterministic API
+ *              (crypto_sign_keypair_internal, crypto_sign_signature_internal).
+ *
+ *              NOTE: This option is incompatible with MLD_CONFIG_KEYGEN_PCT
+ *              as the current PCT implementation requires
+ *              crypto_sign_signature().
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_NO_RANDOMIZED_API */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_NO_SUPERCOP
+ *
+ * Description: By default, mldsa_native.h exposes the mldsa-native API in the
+ *              SUPERCOP naming convention (crypto_sign_xxx). If you don't need
+ *              this, set MLD_CONFIG_NO_SUPERCOP.
+ *
+ *              NOTE: You must set this for a multi-level build as the SUPERCOP
+ *              naming does not disambiguate between the parameter sets.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_NO_SUPERCOP */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_CONSTANTS_ONLY
+ *
+ * Description: If you only need the size constants (MLDSA_PUBLICKEYBYTES, etc.)
+ *              but no function declarations, set MLD_CONFIG_CONSTANTS_ONLY.
+ *
+ *              This only affects the public header mldsa_native.h, not
+ *              the implementation.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_CONSTANTS_ONLY */
+
+/******************************************************************************
+ *
+ * Build-only configuration options
+ *
+ * The remaining configurations are build-options only.
+ * They do not affect the API described in mldsa_native.h.
+ *
+ *****************************************************************************/
+
+#if defined(MLD_BUILD_INTERNAL)
+/******************************************************************************
+ * Name:        MLD_CONFIG_MULTILEVEL_WITH_SHARED
+ *
+ * Description: This is for multi-level builds of mldsa-native only. If you
+ *              need only a single parameter set, keep this unset.
+ *
+ *              If this is set, all MLD_CONFIG_PARAMETER_SET-independent
+ *              code will be included in the build, including code needed only
+ *              for other parameter sets.
+ *
+ *              Example: TODO: add example
+ *
+ *              To build mldsa-native with support for all parameter sets,
+ *              build it three times -- once per parameter set -- and set the
+ *              option MLD_CONFIG_MULTILEVEL_WITH_SHARED for exactly one of
+ *              them, and MLD_CONFIG_MULTILEVEL_NO_SHARED for the others.
+ *
+ *              See examples/multilevel_build_mldsa for an example.
+ *
+ *              This can also be set using CFLAGS.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_MULTILEVEL_WITH_SHARED */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_MULTILEVEL_NO_SHARED
+ *
+ * Description: This is for multi-level builds of mldsa-native only. If you
+ *              need only a single parameter set, keep this unset.
+ *
+ *              If this is set, no MLD_CONFIG_PARAMETER_SET-independent code
+ *              will be included in the build.
+ *
+ *              To build mldsa-native with support for all parameter sets,
+ *              build it three times -- once per parameter set -- and set the
+ *              option MLD_CONFIG_MULTILEVEL_WITH_SHARED for exactly one of
+ *              them, and MLD_CONFIG_MULTILEVEL_NO_SHARED for the others.
+ *
+ *              See examples/multilevel_build_mldsa for an example.
+ *
+ *              This can also be set using CFLAGS.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_MULTILEVEL_NO_SHARED */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_MONOBUILD_KEEP_SHARED_HEADERS
+ *
+ * Description: This is only relevant for single compilation unit (SCU)
+ *              builds of mldsa-native. In this case, it determines whether
+ *              directives defined in parameter-set-independent headers should
+ *              be #undef'ined or not at the of the SCU file. This is needed
+ *              in multilevel builds.
+ *
+ *              See examples/multilevel_build_native for an example.
+ *
+ *              This can also be set using CFLAGS.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_MONOBUILD_KEEP_SHARED_HEADERS */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_USE_NATIVE_BACKEND_ARITH
+ *
+ * Description: Determines whether an native arithmetic backend should be used.
+ *
+ *              The arithmetic backend covers performance critical functions
+ *              such as the number-theoretic transform (NTT).
+ *
+ *              If this option is unset, the C backend will be used.
+ *
+ *              If this option is set, the arithmetic backend to be use is
+ *              determined by MLD_CONFIG_ARITH_BACKEND_FILE: If the latter is
+ *              unset, the default backend for your the target architecture
+ *              will be used. If set, it must be the name of a backend metadata
+ *              file.
+ *
+ *              This can also be set using CFLAGS.
+ *
+ *****************************************************************************/
+#if !defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH)
+/* #define MLD_CONFIG_USE_NATIVE_BACKEND_ARITH */
+#endif
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_ARITH_BACKEND_FILE
+ *
+ * Description: The arithmetic backend to use.
+ *
+ *              If MLD_CONFIG_USE_NATIVE_BACKEND_ARITH is unset, this option
+ *              is ignored.
+ *
+ *              If MLD_CONFIG_USE_NATIVE_BACKEND_ARITH is set, this option must
+ *              either be undefined or the filename of an arithmetic backend.
+ *              If unset, the default backend will be used.
+ *
+ *              This can be set using CFLAGS.
+ *
+ *****************************************************************************/
+#if defined(MLD_CONFIG_USE_NATIVE_BACKEND_ARITH) && \
+    !defined(MLD_CONFIG_ARITH_BACKEND_FILE)
+#define MLD_CONFIG_ARITH_BACKEND_FILE "native/meta.h"
+#endif
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202
+ *
+ * Description: Determines whether an native FIPS202 backend should be used.
+ *
+ *              The FIPS202 backend covers 1x/2x/4x-fold Keccak-f1600, which is
+ *              the performance bottleneck of SHA3 and SHAKE.
+ *
+ *              If this option is unset, the C backend will be used.
+ *
+ *              If this option is set, the FIPS202 backend to be use is
+ *              determined by MLD_CONFIG_FIPS202_BACKEND_FILE: If the latter is
+ *              unset, the default backend for your the target architecture
+ *              will be used. If set, it must be the name of a backend metadata
+ *              file.
+ *
+ *              This can also be set using CFLAGS.
+ *
+ *****************************************************************************/
+#if !defined(MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202)
+/* #define MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 */
+#endif
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_FIPS202_BACKEND_FILE
+ *
+ * Description: The FIPS-202 backend to use.
+ *
+ *              If MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 is set, this option
+ *              must either be undefined or the filename of a FIPS202 backend.
+ *              If unset, the default backend will be used.
+ *
+ *              This can be set using CFLAGS.
+ *
+ *****************************************************************************/
+#if defined(MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202) && \
+    !defined(MLD_CONFIG_FIPS202_BACKEND_FILE)
+#define MLD_CONFIG_FIPS202_BACKEND_FILE "fips202/native/auto.h"
+#endif
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_FIPS202_CUSTOM_HEADER
+ *
+ * Description: Custom header to use for FIPS-202
+ *
+ *              This should only be set if you intend to use a custom
+ *              FIPS-202 implementation, different from the one shipped
+ *              with mldsa-native.
+ *
+ *              If set, it must be the name of a file serving as the
+ *              replacement for mldsa/src/fips202/fips202.h, and exposing
+ *              the same API (see FIPS202.md).
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_FIPS202_CUSTOM_HEADER "SOME_FILE.h" */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_FIPS202X4_CUSTOM_HEADER
+ *
+ * Description: Custom header to use for FIPS-202-X4
+ *
+ *              This should only be set if you intend to use a custom
+ *              FIPS-202 implementation, different from the one shipped
+ *              with mldsa-native.
+ *
+ *              If set, it must be the name of a file serving as the
+ *              replacement for mldsa/src/fips202/fips202x4.h, and exposing
+ *              the same API (see FIPS202.md).
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_FIPS202X4_CUSTOM_HEADER "SOME_FILE.h" */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_CUSTOM_ZEROIZE
+ *
+ * Description: In compliance with @[FIPS204, Section 3.6.3], mldsa-native,
+ *              zeroizes intermediate stack buffers before returning from
+ *              function calls.
+ *
+ *              Set this option and define `mld_zeroize_native` if you want to
+ *              use a custom method to zeroize intermediate stack buffers.
+ *              The default implementation uses SecureZeroMemory on Windows
+ *              and a memset + compiler barrier otherwise. If neither of those
+ *              is available on the target platform, compilation will fail,
+ *              and you will need to use MLD_CONFIG_CUSTOM_ZEROIZE to provide
+ *              a custom implementation of `mld_zeroize_native()`.
+ *
+ *              WARNING:
+ *              The explicit stack zeroization conducted by mldsa-native
+ *              reduces the likelihood of data leaking on the stack, but
+ *              does not eliminate it! The C standard makes no guarantee about
+ *              where a compiler allocates structures and whether/where it makes
+ *              copies of them. Also, in addition to entire structures, there
+ *              may also be potentially exploitable leakage of individual values
+ *              on the stack.
+ *
+ *              If you need bullet-proof zeroization of the stack, you need to
+ *              consider additional measures instead of what this feature
+ *              provides. In this case, you can set mld_zeroize_native to a
+ *              no-op.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_CUSTOM_ZEROIZE
+   #if !defined(__ASSEMBLER__)
+   #include <stdint.h>
+   #include "src/src.h"
+   static MLD_INLINE void mld_zeroize_native(void *ptr, size_t len)
+   {
+       ... your implementation ...
+   }
+   #endif
+*/
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_CUSTOM_RANDOMBYTES
+ *
+ * Description: mldsa-native does not provide a secure randombytes
+ *              implementation. Such an implementation has to provided by the
+ *              consumer.
+ *
+ *              If this option is not set, mldsa-native expects a function
+ *              void randombytes(uint8_t *out, size_t outlen).
+ *
+ *              Set this option and define `mld_randombytes` if you want to
+ *              use a custom method to sample randombytes with a different name
+ *              or signature.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_CUSTOM_RANDOMBYTES
+   #if !defined(__ASSEMBLER__)
+   #include <stdint.h>
+   #include "src/src.h"
+   static MLD_INLINE void mld_randombytes(uint8_t *ptr, size_t len)
+   {
+       ... your implementation ...
+   }
+   #endif
+*/
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_CUSTOM_CAPABILITY_FUNC
+ *
+ * Description: mldsa-native backends may rely on specific hardware features.
+ *              Those backends will only be included in an mldsa-native build
+ *              if support for the respective features is enabled at
+ *              compile-time. However, when building for a heteroneous set
+ *              of CPUs to run the resulting binary/library on, feature
+ *              detection at _runtime_ is needed to decided whether a backend
+ *              can be used or not.
+ *
+ *              Set this option and define `mld_sys_check_capability` if you
+ *              want to use a custom method to dispatch between implementations.
+ *
+ *              Return value 1 indicates that a capability is supported.
+ *              Return value 0 indicates that a capability is not supported.
+ *
+ *              If this option is not set, mldsa-native uses compile-time
+ *              feature detection only to decide which backend to use.
+ *
+ *              If you compile mldsa-native on a system with different
+ *              capabilities than the system that the resulting binary/library
+ *              will be run on, you must use this option.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_CUSTOM_CAPABILITY_FUNC
+   static MLD_INLINE int mld_sys_check_capability(mld_sys_cap cap)
+   {
+       ... your implementation ...
+   }
+*/
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_CUSTOM_ALLOC_FREE [EXPERIMENTAL]
+ *
+ * Description: Set this option and define `MLD_CUSTOM_ALLOC` and
+ *              `MLD_CUSTOM_FREE` if you want to use custom allocation for
+ *              large local structures or buffers.
+ *
+ *              By default, all buffers/structures are allocated on the stack.
+ *              If this option is set, most of them will be allocated via
+ *              MLD_CUSTOM_ALLOC.
+ *
+ *              Parameters to MLD_CUSTOM_ALLOC:
+ *              - T* v: Target pointer to declare.
+ *              - T: Type of structure to be allocated
+ *              - N: Number of elements to be allocated.
+ *
+ *              Parameters to MLD_CUSTOM_FREE:
+ *              - T* v: Target pointer to free. May be NULL.
+ *              - T: Type of structure to be freed.
+ *              - N: Number of elements to be freed.
+ *
+ *              WARNING: This option is experimental!
+ *              Its scope, configuration and function/macro signatures may
+ *              change at any time. We expect a stable API for v2.
+ *
+ *              NOTE: Even if this option is set, some allocations further down
+ *              the call stack will still be made from the stack. Those will
+ *              likely be added to the scope of this option in the future.
+ *
+ *              NOTE: MLD_CUSTOM_ALLOC need not guarantee a successful
+ *              allocation nor include error handling. Upon failure, the
+ *              target pointer should simply be set to NULL. The calling
+ *              code will handle this case and invoke MLD_CUSTOM_FREE.
+ *
+ *****************************************************************************/
+#define MLD_CONFIG_CUSTOM_ALLOC_FREE
+#if !defined(__ASSEMBLER__)
+#include <stdlib.h>
+#define MLD_CUSTOM_ALLOC(v, T, N) T *v = (T *)malloc(sizeof(T) * (N))
+#define MLD_CUSTOM_FREE(v, T, N) free(v)
+#endif
+
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_CUSTOM_MEMCPY
+ *
+ * Description: Set this option and define `mld_memcpy` if you want to
+ *              use a custom method to copy memory instead of the standard
+ *              library memcpy function.
+ *
+ *              The custom implementation must have the same signature and
+ *              behavior as the standard memcpy function:
+ *              void *mld_memcpy(void *dest, const void *src, size_t n)
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_CUSTOM_MEMCPY
+   #if !defined(__ASSEMBLER__)
+   #include <stdint.h>
+   #include "src/src.h"
+   static MLD_INLINE void *mld_memcpy(void *dest, const void *src, size_t n)
+   {
+       ... your implementation ...
+   }
+   #endif
+*/
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_CUSTOM_MEMSET
+ *
+ * Description: Set this option and define `mld_memset` if you want to
+ *              use a custom method to set memory instead of the standard
+ *              library memset function.
+ *
+ *              The custom implementation must have the same signature and
+ *              behavior as the standard memset function:
+ *              void *mld_memset(void *s, int c, size_t n)
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_CUSTOM_MEMSET
+   #if !defined(__ASSEMBLER__)
+   #include <stdint.h>
+   #include "src/src.h"
+   static MLD_INLINE void *mld_memset(void *s, int c, size_t n)
+   {
+       ... your implementation ...
+   }
+   #endif
+*/
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_INTERNAL_API_QUALIFIER
+ *
+ * Description: If set, this option provides an additional function
+ *              qualifier to be added to declarations of internal API.
+ *
+ *              The primary use case for this option are single-CU builds,
+ *              in which case this option can be set to `static`.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_INTERNAL_API_QUALIFIER */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_CT_TESTING_ENABLED
+ *
+ * Description: If set, mldsa-native annotates data as secret / public using
+ *              valgrind's annotations VALGRIND_MAKE_MEM_UNDEFINED and
+ *              VALGRIND_MAKE_MEM_DEFINED, enabling various checks for secret-
+ *              dependent control flow of variable time execution (depending
+ *              on the exact version of valgrind installed).
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_CT_TESTING_ENABLED */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_NO_ASM
+ *
+ * Description: If this option is set, mldsa-native will be built without
+ *              use of native code or inline assembly.
+ *
+ *              By default, inline assembly is used to implement value barriers.
+ *              Without inline assembly, mldsa-native will use a global volatile
+ *              'opt blocker' instead; see ct.h.
+ *
+ *              Inline assembly is also used to implement a secure zeroization
+ *              function on non-Windows platforms. If this option is set and
+ *              the target platform is not Windows, you MUST set
+ *              MLD_CONFIG_CUSTOM_ZEROIZE and provide a custom zeroization
+ *              function.
+ *
+ *              If this option is set, MLD_CONFIG_USE_NATIVE_BACKEND_FIPS202 and
+ *              and MLD_CONFIG_USE_NATIVE_BACKEND_ARITH will be ignored, and no
+ *              native backends will be used.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_NO_ASM */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_NO_ASM_VALUE_BARRIER
+ *
+ * Description: If this option is set, mldsa-native will be built without
+ *              use of native code or inline assembly for value barriers.
+ *
+ *              By default, inline assembly (if available) is used to implement
+ *              value barriers.
+ *              Without inline assembly, mldsa-native will use a global volatile
+ *              'opt blocker' instead; see ct.h.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_NO_ASM_VALUE_BARRIER */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_KEYGEN_PCT
+ *
+ * Description: Compliance with @[FIPS140_3_IG, p.87] requires a
+ *              Pairwise Consistency Test (PCT) to be carried out on a freshly
+ *              generated keypair before it can be exported.
+ *
+ *              Set this option if such a check should be implemented.
+ *              In this case, crypto_sign_keypair_internal and
+ *              crypto_sign_keypair will return a non-zero error code if the
+ *              PCT failed.
+ *
+ *              NOTE: This feature will drastically lower the performance of
+ *              key generation.
+ *
+ *****************************************************************************/
+#define MLD_CONFIG_KEYGEN_PCT
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_KEYGEN_PCT_BREAKAGE_TEST
+ *
+ * Description: If this option is set, the user must provide a runtime
+ *              function `static inline int mld_break_pct() { ... }` to
+ *              indicate whether the PCT should be made fail.
+ *
+ *              This option only has an effect if MLD_CONFIG_KEYGEN_PCT is set.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_KEYGEN_PCT_BREAKAGE_TEST
+   #if !defined(__ASSEMBLER__)
+   #include "src/src.h"
+   static MLD_INLINE int mld_break_pct(void)
+   {
+       ... return 0/1 depending on whether PCT should be broken ...
+   }
+   #endif
+*/
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_SERIAL_FIPS202_ONLY
+ *
+ * Description: Set this to use a FIPS202 implementation with global state
+ *              that supports only one active Keccak computation at a time
+ *              (e.g. some hardware accelerators).
+ *
+ *              If this option is set, ML-DSA will use FIPS202 operations
+ *              serially, ensuring that only one SHAKE context is active
+ *              at any given time.
+ *
+ *              This allows offloading Keccak computations to a hardware
+ *              accelerator that holds only a single Keccak state locally,
+ *              rather than requiring support for multiple concurrent
+ *              Keccak states.
+ *
+ *              NOTE: Depending on the target CPU, this may reduce
+ *              performance when using software FIPS202 implementations.
+ *              Only enable this when you have to.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_SERIAL_FIPS202_ONLY */
+
+/******************************************************************************
+ * Name:        MLD_CONFIG_REDUCE_RAM [EXPERIMENTAL]
+ *
+ * Description: Set this to reduce RAM usage.
+ *              This trades memory for performance.
+ *
+ *              For detailed expected memory savings, see the
+ *              mldsa-native README.
+ *
+ *              This option is useful for embedded systems with tight RAM
+ *              constraints but relaxed performance requirements.
+ *
+ *              WARNING: This option is experimental!
+ *              CBMC proofs do not currently cover this configuration option.
+ *              Its scope and configuration may change at any time.
+ *
+ *****************************************************************************/
+/* #define MLD_CONFIG_REDUCE_RAM */
+
+/*************************  Config internals  ********************************/
+
+#endif /* MLD_BUILD_INTERNAL */
+
+/* Default namespace
+ *
+ * Don't change this. If you need a different namespace, re-define
+ * MLD_CONFIG_NAMESPACE_PREFIX above instead, and remove the following.
+ *
+ * The default MLDSA namespace is
+ *
+ *   PQCP_MLDSA_NATIVE_MLDSA<LEVEL>_
+ *
+ * e.g., PQCP_MLDSA_NATIVE_MLDSA44_
+ */
+
+#if MLD_CONFIG_PARAMETER_SET == 44
+#define MLD_DEFAULT_NAMESPACE_PREFIX PQCP_MLDSA_NATIVE_MLDSA44
+#elif MLD_CONFIG_PARAMETER_SET == 65
+#define MLD_DEFAULT_NAMESPACE_PREFIX PQCP_MLDSA_NATIVE_MLDSA65
+#elif MLD_CONFIG_PARAMETER_SET == 87
+#define MLD_DEFAULT_NAMESPACE_PREFIX PQCP_MLDSA_NATIVE_MLDSA87
+#endif
+
+#endif /* !MLD_CONFIG_H */
diff --git a/proofs/cbmc/prepare_domain_separation_prefix/prepare_domain_separation_prefix_harness.c b/proofs/cbmc/prepare_domain_separation_prefix/prepare_domain_separation_prefix_harness.c
index e77ae4af9..7adf717d4 100644
--- a/proofs/cbmc/prepare_domain_separation_prefix/prepare_domain_separation_prefix_harness.c
+++ b/proofs/cbmc/prepare_domain_separation_prefix/prepare_domain_separation_prefix_harness.c
@@ -5,6 +5,11 @@
 
 void harness(void)
 {
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
   uint8_t *prefix;
   const uint8_t *ph;
   size_t phlen;
diff --git a/proofs/cbmc/sample_s1_s2/sample_s1_s2_harness.c b/proofs/cbmc/sample_s1_s2/sample_s1_s2_harness.c
index 84a392a09..eaf2d404c 100644
--- a/proofs/cbmc/sample_s1_s2/sample_s1_s2_harness.c
+++ b/proofs/cbmc/sample_s1_s2/sample_s1_s2_harness.c
@@ -8,6 +8,11 @@ static void mld_sample_s1_s2(mld_polyvecl *s1, mld_polyveck *s2,
 
 void harness(void)
 {
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
   mld_polyvecl *s1;
   mld_polyveck *s2;
   uint8_t *seed;
diff --git a/proofs/cbmc/sample_s1_s2_serial/sample_s1_s2_harness.c b/proofs/cbmc/sample_s1_s2_serial/sample_s1_s2_harness.c
index 84a392a09..eaf2d404c 100644
--- a/proofs/cbmc/sample_s1_s2_serial/sample_s1_s2_harness.c
+++ b/proofs/cbmc/sample_s1_s2_serial/sample_s1_s2_harness.c
@@ -8,6 +8,11 @@ static void mld_sample_s1_s2(mld_polyvecl *s1, mld_polyveck *s2,
 
 void harness(void)
 {
+  {
+    /* Dummy use of `free` to work around CBMC issue #8814. */
+    free(NULL);
+  }
+
   mld_polyvecl *s1;
   mld_polyveck *s2;
   uint8_t *seed;
diff --git a/test/configs.yml b/test/configs.yml
index 2e8ba5cf1..b2099e4dd 100644
--- a/test/configs.yml
+++ b/test/configs.yml
@@ -426,3 +426,18 @@ configs:
           #endif /* !__ASSEMBLER__ */
       MLD_CONFIG_FILE:
         comment: "/* No need to set this -- we _are_ already in a custom config */"
+
+  - path: proofs/cbmc/mldsa_native_config_cbmc.h
+    description: "mldsa-native configuration used for CBMC proofs, using instrumented alloc/free"
+    defines:
+      MLD_CONFIG_KEYGEN_PCT: true
+      MLD_CONFIG_CUSTOM_ALLOC_FREE:
+        content: |
+          #define MLD_CONFIG_CUSTOM_ALLOC_FREE
+          #if !defined(__ASSEMBLER__)
+          #include <stdlib.h>
+          #define MLD_CUSTOM_ALLOC(v, T, N) T* v = (T *)malloc(sizeof(T) * (N))
+          #define MLD_CUSTOM_FREE(v, T, N) free(v)
+          #endif /* !__ASSEMBLER__ */
+      MLD_CONFIG_FILE:
+        comment: "/* No need to set this -- we _are_ already in a custom config */"