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 a8acb5bf4..b5769a562 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
diff --git a/proofs/cbmc/check_pct/Makefile b/proofs/cbmc/check_pct/Makefile
index 99bb0d174..9a09a4157 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/mldsa_native_config_cbmc.h b/proofs/cbmc/mldsa_native_config_cbmc.h
index 47b8a4141..236a3f1a9 100644
--- a/proofs/cbmc/mldsa_native_config_cbmc.h
+++ b/proofs/cbmc/mldsa_native_config_cbmc.h
@@ -25,11 +25,14 @@
  */
 
 /*
- * Test configuration: mldsa-native configuration used for CBMC proofs
+ * 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_NAMESPACE_PREFIX
+ *   - MLD_CONFIG_KEYGEN_PCT
+ *   - MLD_CONFIG_CUSTOM_ALLOC_FREE
  */
 
 
@@ -541,15 +544,13 @@
  *              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 *)aligned_alloc(MLD_DEFAULT_ALIGN,               \
-                                 MLD_ALIGN_UP(sizeof(T) * (N)))
-   #define MLD_CUSTOM_FREE(v, T, N) free(v)
-   #endif
-*/
+#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
@@ -678,7 +679,7 @@
  *              requires crypto_sign_signature() and crypto_sign_verify().
  *
  *****************************************************************************/
-/* #define MLD_CONFIG_KEYGEN_PCT */
+#define MLD_CONFIG_KEYGEN_PCT
 
 /******************************************************************************
  * Name:        MLD_CONFIG_KEYGEN_PCT_BREAKAGE_TEST
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/proofs/cbmc/sign_signature_internal/Makefile b/proofs/cbmc/sign_signature_internal/Makefile
index e282030c1..134a89828 100644
--- a/proofs/cbmc/sign_signature_internal/Makefile
+++ b/proofs/cbmc/sign_signature_internal/Makefile
@@ -43,7 +43,7 @@ FUNCTION_NAME = 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/test/configs/configs.yml b/test/configs/configs.yml
index 5583ebbf4..47bf6acf9 100644
--- a/test/configs/configs.yml
+++ b/test/configs/configs.yml
@@ -472,8 +472,17 @@ configs:
         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"
+    description: "mldsa-native configuration used for CBMC proofs, using instrumented alloc/free"
     defines:
       MLD_CONFIG_NAMESPACE_PREFIX: mld
+      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 */"