diff --git a/integration/opentitan/reduce_alloc.patch b/integration/opentitan/reduce_alloc.patch
index 1d7ab6d67..f9bc97085 100644
--- a/integration/opentitan/reduce_alloc.patch
+++ b/integration/opentitan/reduce_alloc.patch
@@ -1,7 +1,7 @@
 # Copyright (c) The mldsa-native project authors
 # SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
 diff --git a/sw/device/lib/crypto/include/mldsa.h b/sw/device/lib/crypto/include/mldsa.h
-index be11f20..26351ee 100644
+index be11f20..0000000 100644
 --- a/sw/device/lib/crypto/include/mldsa.h
 +++ b/sw/device/lib/crypto/include/mldsa.h
 @@ -41,16 +41,16 @@ enum {
@@ -10,20 +10,23 @@ index be11f20..26351ee 100644
    // Work buffer sizes in 32-bit words
 -  kOtcryptoMldsa44WorkBufferKeypairWords = 32992 / sizeof(uint32_t),
 -  kOtcryptoMldsa44WorkBufferSignWords = 32448 / sizeof(uint32_t),
+-  kOtcryptoMldsa44WorkBufferVerifyWords = 22464 / sizeof(uint32_t),
 +  kOtcryptoMldsa44WorkBufferKeypairWords = 28960 / sizeof(uint32_t),
 +  kOtcryptoMldsa44WorkBufferSignWords = 20256 / sizeof(uint32_t),
-   kOtcryptoMldsa44WorkBufferVerifyWords = 22464 / sizeof(uint32_t),
++  kOtcryptoMldsa44WorkBufferVerifyWords = 13248 / sizeof(uint32_t),
  
 -  kOtcryptoMldsa65WorkBufferKeypairWords = 46304 / sizeof(uint32_t),
 -  kOtcryptoMldsa65WorkBufferSignWords = 44768 / sizeof(uint32_t),
+-  kOtcryptoMldsa65WorkBufferVerifyWords = 30720 / sizeof(uint32_t),
 +  kOtcryptoMldsa65WorkBufferKeypairWords = 40224 / sizeof(uint32_t),
 +  kOtcryptoMldsa65WorkBufferSignWords = 27456 / sizeof(uint32_t),
-   kOtcryptoMldsa65WorkBufferVerifyWords = 30720 / sizeof(uint32_t),
++  kOtcryptoMldsa65WorkBufferVerifyWords = 18400 / sizeof(uint32_t),
  
 -  kOtcryptoMldsa87WorkBufferKeypairWords = 62688 / sizeof(uint32_t),
 -  kOtcryptoMldsa87WorkBufferSignWords = 59104 / sizeof(uint32_t),
+-  kOtcryptoMldsa87WorkBufferVerifyWords = 41216 / sizeof(uint32_t),
 +  kOtcryptoMldsa87WorkBufferKeypairWords = 54560 / sizeof(uint32_t),
 +  kOtcryptoMldsa87WorkBufferSignWords = 35648 / sizeof(uint32_t),
-   kOtcryptoMldsa87WorkBufferVerifyWords = 41216 / sizeof(uint32_t),
++  kOtcryptoMldsa87WorkBufferVerifyWords = 24800 / sizeof(uint32_t),
  };
  
diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c
index e20a82f2c..f5b60e9e8 100644
--- a/mldsa/mldsa_native.c
+++ b/mldsa/mldsa_native.c
@@ -261,8 +261,8 @@
 #undef mld_pack_sig_c_h
 #undef mld_pack_sig_z
 #undef mld_pack_sk
+#undef mld_unpack_hints
 #undef mld_unpack_pk
-#undef mld_unpack_sig
 #undef mld_unpack_sk
 /* mldsa/src/params.h */
 #undef MLDSA_BETA
diff --git a/mldsa/mldsa_native.h b/mldsa/mldsa_native.h
index de2582d02..f97458eae 100644
--- a/mldsa/mldsa_native.h
+++ b/mldsa/mldsa_native.h
@@ -932,17 +932,17 @@ int MLD_API_NAMESPACE(pk_from_sk)(
 #define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 28960
 #define MLD_TOTAL_ALLOC_44_PK_FROM_SK 32992
 #define MLD_TOTAL_ALLOC_44_SIGN 20256
-#define MLD_TOTAL_ALLOC_44_VERIFY 22464
+#define MLD_TOTAL_ALLOC_44_VERIFY 13248
 #define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 40224
 #define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 40224
 #define MLD_TOTAL_ALLOC_65_PK_FROM_SK 46304
 #define MLD_TOTAL_ALLOC_65_SIGN 27456
-#define MLD_TOTAL_ALLOC_65_VERIFY 30720
+#define MLD_TOTAL_ALLOC_65_VERIFY 18400
 #define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 54560
 #define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 54560
 #define MLD_TOTAL_ALLOC_87_PK_FROM_SK 62688
 #define MLD_TOTAL_ALLOC_87_SIGN 35648
-#define MLD_TOTAL_ALLOC_87_VERIFY 41216
+#define MLD_TOTAL_ALLOC_87_VERIFY 24800
 #endif /* !(MLD_API_LEGACY_CONFIG || !MLD_CONFIG_REDUCE_RAM) */
 /* check-magic: on */
 
diff --git a/mldsa/mldsa_native_asm.S b/mldsa/mldsa_native_asm.S
index 36296bb5e..490eb949f 100644
--- a/mldsa/mldsa_native_asm.S
+++ b/mldsa/mldsa_native_asm.S
@@ -264,8 +264,8 @@
 #undef mld_pack_sig_c_h
 #undef mld_pack_sig_z
 #undef mld_pack_sk
+#undef mld_unpack_hints
 #undef mld_unpack_pk
-#undef mld_unpack_sig
 #undef mld_unpack_sk
 /* mldsa/src/params.h */
 #undef MLDSA_BETA
diff --git a/mldsa/src/packing.c b/mldsa/src/packing.c
index c839796e5..c04d1ea3d 100644
--- a/mldsa/src/packing.c
+++ b/mldsa/src/packing.c
@@ -13,7 +13,6 @@
  * This is to facilitate building multiple instances
  * of mldsa-native (e.g. with varying parameter sets)
  * within a single compilation unit. */
-#define mld_unpack_hints MLD_ADD_PARAM_SET(mld_unpack_hints)
 /* End of parameter set namespacing */
 
 MLD_INTERNAL_API
@@ -192,17 +191,9 @@ void mld_pack_sig_z(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *zi,
  *
  * Returns 1 in case of malformed hints; otherwise 0.
  **************************************************/
-static int mld_unpack_hints(
-    mld_polyveck *h, const uint8_t packed_hints[MLDSA_POLYVECH_PACKEDBYTES])
-__contract__(
-  requires(memory_no_alias(packed_hints, MLDSA_POLYVECH_PACKEDBYTES))
-  requires(memory_no_alias(h, sizeof(mld_polyveck)))
-  assigns(memory_slice(h, sizeof(mld_polyveck)))
-  /* All returned coefficients are either 0 or 1 */
-  ensures(forall(k1, 0, MLDSA_K,
-    array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
-  ensures(return_value >= 0 && return_value <= 1)
-)
+MLD_INTERNAL_API
+int mld_unpack_hints(mld_polyveck *h,
+                     const uint8_t packed_hints[MLDSA_POLYVECH_PACKEDBYTES])
 {
   unsigned int i, j;
   unsigned int old_hint_count;
@@ -275,19 +266,5 @@ __contract__(
   return 0;
 }
 
-MLD_INTERNAL_API
-int mld_unpack_sig(uint8_t c[MLDSA_CTILDEBYTES], mld_polyvecl *z,
-                   mld_polyveck *h, const uint8_t sig[MLDSA_CRYPTO_BYTES])
-{
-  mld_memcpy(c, sig, MLDSA_CTILDEBYTES);
-  sig += MLDSA_CTILDEBYTES;
-
-  mld_polyvecl_unpack_z(z, sig);
-  sig += MLDSA_L * MLDSA_POLYZ_PACKEDBYTES;
-
-  return mld_unpack_hints(h, sig);
-}
-
 /* To facilitate single-compilation-unit (SCU) builds, undefine all macros.
  * Don't modify by hand -- this is auto-generated by scripts/autogen. */
-#undef mld_unpack_hints
diff --git a/mldsa/src/packing.h b/mldsa/src/packing.h
index 61029a5db..548f0cbe2 100644
--- a/mldsa/src/packing.h
+++ b/mldsa/src/packing.h
@@ -193,36 +193,29 @@ __contract__(
     array_abs_bound(s2->vec.vec[k2].coeffs, 0, MLDSA_N, MLD_NTT_BOUND)))
 );
 
-#define mld_unpack_sig MLD_NAMESPACE_KL(unpack_sig)
+#define mld_unpack_hints MLD_NAMESPACE_KL(unpack_hints)
 /*************************************************
- * Name:        mld_unpack_sig
+ * Name:        mld_unpack_hints
  *
- * Description: Unpack signature sig = (c, z, h).
+ * Description: Unpack hint vector h from packed hint bytes in signature.
  *
- * Arguments:   - uint8_t *c: pointer to output challenge hash
- *              - mld_polyvecl *z: pointer to output vector z
- *              - mld_polyveck *h: pointer to output hint vector h
- *              - const uint8_t sig[]: byte array containing
- *                bit-packed signature
+ * Arguments:   - mld_polyveck *h: pointer to output hint vector
+ *              - const uint8_t *packed_hints: pointer to
+ *                raw hint bytes (MLDSA_POLYVECH_PACKEDBYTES)
  *
- * Returns 1 in case of malformed signature; otherwise 0.
+ * Returns 1 in case of malformed hints; otherwise 0.
  **************************************************/
 MLD_INTERNAL_API
 MLD_MUST_CHECK_RETURN_VALUE
-int mld_unpack_sig(uint8_t c[MLDSA_CTILDEBYTES], mld_polyvecl *z,
-                   mld_polyveck *h, const uint8_t sig[MLDSA_CRYPTO_BYTES])
+int mld_unpack_hints(mld_polyveck *h,
+                     const uint8_t packed_hints[MLDSA_POLYVECH_PACKEDBYTES])
 __contract__(
-  requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES))
-  requires(memory_no_alias(c, MLDSA_CTILDEBYTES))
-  requires(memory_no_alias(z, sizeof(mld_polyvecl)))
+  requires(memory_no_alias(packed_hints, MLDSA_POLYVECH_PACKEDBYTES))
   requires(memory_no_alias(h, sizeof(mld_polyveck)))
-  assigns(memory_slice(c, MLDSA_CTILDEBYTES))
-  assigns(memory_slice(z, sizeof(mld_polyvecl)))
   assigns(memory_slice(h, sizeof(mld_polyveck)))
-  ensures(forall(k0, 0, MLDSA_L,
-    array_bound(z->vec[k0].coeffs, 0, MLDSA_N, -(MLDSA_GAMMA1 - 1), MLDSA_GAMMA1 + 1)))
   ensures(forall(k1, 0, MLDSA_K,
     array_bound(h->vec[k1].coeffs, 0, MLDSA_N, 0, 2)))
   ensures(return_value >= 0 && return_value <= 1)
 );
+
 #endif /* !MLD_PACKING_H */
diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c
index 159ea7fbf..8334e3952 100644
--- a/mldsa/src/sign.c
+++ b/mldsa/src/sign.c
@@ -1082,34 +1082,41 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
    * https://github.com/diffblue/cbmc/issues/8813 */
   typedef MLD_UNION_OR_STRUCT
   {
+    mld_polyvecl z;
+    mld_poly cp;
+  }
+  zcp_u;
+  mld_polyvecl *z;
+  mld_poly *cp;
+
+  /* TODO: Remove the following workaround for
+   * https://github.com/diffblue/cbmc/issues/8813 */
+  typedef MLD_UNION_OR_STRUCT
+  {
+    mld_polymat mat;
     mld_polyveck t1;
-    mld_polyveck w1;
+    mld_polyveck tmp;
+    mld_polyveck h;
   }
-  t1w1_u;
-  mld_polyveck *t1;
-  mld_polyveck *w1;
+  reuse_u;
 
   MLD_ALLOC(buf, uint8_t, (MLDSA_K * MLDSA_POLYW1_PACKEDBYTES), context);
   MLD_ALLOC(rho, uint8_t, MLDSA_SEEDBYTES, context);
   MLD_ALLOC(mu, uint8_t, MLDSA_CRHBYTES, context);
   MLD_ALLOC(c, uint8_t, MLDSA_CTILDEBYTES, context);
   MLD_ALLOC(c2, uint8_t, MLDSA_CTILDEBYTES, context);
-  MLD_ALLOC(cp, mld_poly, 1, context);
-  MLD_ALLOC(mat, mld_polymat, 1, context);
-  MLD_ALLOC(z, mld_polyvecl, 1, context);
-  MLD_ALLOC(t1w1, t1w1_u, 1, context);
-  MLD_ALLOC(tmp, mld_polyveck, 1, context);
-  MLD_ALLOC(h, mld_polyveck, 1, context);
+  MLD_ALLOC(zcp, zcp_u, 1, context);
+  MLD_ALLOC(w1, mld_polyveck, 1, context);
+  MLD_ALLOC(reuse, reuse_u, 1, context);
 
   if (buf == NULL || rho == NULL || mu == NULL || c == NULL || c2 == NULL ||
-      cp == NULL || mat == NULL || z == NULL || t1w1 == NULL || tmp == NULL ||
-      h == NULL)
+      zcp == NULL || w1 == NULL || reuse == NULL)
   {
     ret = MLD_ERR_OUT_OF_MEMORY;
     goto cleanup;
   }
-  t1 = &t1w1->t1;
-  w1 = &t1w1->w1;
+  z = &zcp->z;
+  cp = &zcp->cp;
 
   if (siglen != MLDSA_CRYPTO_BYTES)
   {
@@ -1117,16 +1124,11 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
     goto cleanup;
   }
 
-  mld_unpack_pk(rho, t1, pk);
+  mld_memcpy(rho, pk, MLDSA_SEEDBYTES);
+
+  mld_memcpy(c, sig, MLDSA_CTILDEBYTES);
+  mld_polyvecl_unpack_z(z, sig + MLDSA_CTILDEBYTES);
 
-  /* 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))
-  {
-    ret = MLD_ERR_FAIL;
-    goto cleanup;
-  }
   if (mld_polyvecl_chknorm(z, MLDSA_GAMMA1 - MLDSA_BETA))
   {
     ret = MLD_ERR_FAIL;
@@ -1151,23 +1153,31 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
   }
 
   /* Matrix-vector multiplication; compute Az - c2^dt1 */
+  mld_polyvecl_ntt(z);
+  mld_polyvec_matrix_expand(&reuse->mat, rho);
+  mld_polyvec_matrix_pointwise_montgomery(w1, &reuse->mat, z);
+
   mld_poly_challenge(cp, c);
   mld_poly_ntt(cp);
-  mld_polyveck_shiftl(t1);
-  mld_polyveck_ntt(t1);
-  mld_polyveck_pointwise_poly_montgomery(tmp, cp, t1);
-
-  mld_polyvec_matrix_expand(mat, rho);
-  mld_polyvecl_ntt(z);
-  mld_polyvec_matrix_pointwise_montgomery(w1, mat, z);
-  mld_polyveck_sub(w1, tmp);
+  mld_unpack_pk(rho, &reuse->t1, pk);
+  mld_polyveck_shiftl(&reuse->t1);
+  mld_polyveck_ntt(&reuse->t1);
+  mld_polyveck_pointwise_poly_montgomery(&reuse->tmp, cp, &reuse->t1);
+  mld_polyveck_sub(w1, &reuse->tmp);
   mld_polyveck_reduce(w1);
   mld_polyveck_invntt_tomont(w1);
 
   /* Reconstruct w1 */
   mld_polyveck_caddq(w1);
-  mld_polyveck_use_hint(tmp, w1, h);
-  mld_polyveck_pack_w1(buf, tmp);
+  if (mld_unpack_hints(&reuse->h, sig + MLDSA_CTILDEBYTES +
+                                      MLDSA_L * MLDSA_POLYZ_PACKEDBYTES))
+  {
+    ret = MLD_ERR_FAIL;
+    goto cleanup;
+  }
+  mld_polyveck_use_hint(&reuse->tmp, w1, &reuse->h);
+  mld_polyveck_pack_w1(buf, &reuse->tmp);
+
   /* Call random oracle and verify challenge */
   mld_H(c2, MLDSA_CTILDEBYTES, mu, MLDSA_CRHBYTES, buf,
         MLDSA_K * MLDSA_POLYW1_PACKEDBYTES, NULL, 0);
@@ -1181,12 +1191,9 @@ int mld_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, context);
-  MLD_FREE(tmp, mld_polyveck, 1, context);
-  MLD_FREE(t1w1, t1w1_u, 1, context);
-  MLD_FREE(z, mld_polyvecl, 1, context);
-  MLD_FREE(mat, mld_polymat, 1, context);
-  MLD_FREE(cp, mld_poly, 1, context);
+  MLD_FREE(reuse, reuse_u, 1, context);
+  MLD_FREE(w1, mld_polyveck, 1, context);
+  MLD_FREE(zcp, zcp_u, 1, context);
   MLD_FREE(c2, uint8_t, MLDSA_CTILDEBYTES, context);
   MLD_FREE(c, uint8_t, MLDSA_CTILDEBYTES, context);
   MLD_FREE(mu, uint8_t, MLDSA_CRHBYTES, context);
diff --git a/proofs/cbmc/sign_verify_internal/Makefile b/proofs/cbmc/sign_verify_internal/Makefile
index 2ca141a69..ac91f7a86 100644
--- a/proofs/cbmc/sign_verify_internal/Makefile
+++ b/proofs/cbmc/sign_verify_internal/Makefile
@@ -21,8 +21,9 @@ PROJECT_SOURCES += $(SRCDIR)/mldsa/src/sign.c
 
 CHECK_FUNCTION_CONTRACTS=mld_verify_internal
 USE_FUNCTION_CONTRACTS=mld_unpack_pk
-USE_FUNCTION_CONTRACTS+=mld_unpack_sig
+USE_FUNCTION_CONTRACTS+=mld_polyvecl_unpack_z
 USE_FUNCTION_CONTRACTS+=mld_polyvecl_chknorm
+USE_FUNCTION_CONTRACTS+=mld_unpack_hints
 USE_FUNCTION_CONTRACTS+=mld_H
 USE_FUNCTION_CONTRACTS+=mld_poly_challenge
 USE_FUNCTION_CONTRACTS+=mld_polyvec_matrix_expand
diff --git a/proofs/cbmc/unpack_sig/Makefile b/proofs/cbmc/unpack_sig/Makefile
deleted file mode 100644
index 96f6aab8c..000000000
--- a/proofs/cbmc/unpack_sig/Makefile
+++ /dev/null
@@ -1,56 +0,0 @@
-# Copyright (c) The mldsa-native project authors
-# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
-
-include ../Makefile_params.common
-
-HARNESS_ENTRY = harness
-HARNESS_FILE = unpack_sig_harness
-
-# This should be a unique identifier for this proof, and will appear on the
-# Litani dashboard. It can be human-readable and contain spaces if you wish.
-PROOF_UID = unpack_sig
-
-DEFINES +=
-INCLUDES +=
-
-REMOVE_FUNCTION_BODY +=
-
-PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
-PROJECT_SOURCES += $(SRCDIR)/mldsa/src/packing.c
-
-CHECK_FUNCTION_CONTRACTS=mld_unpack_sig
-USE_FUNCTION_CONTRACTS=mld_polyvecl_unpack_z
-USE_FUNCTION_CONTRACTS+=mld_unpack_hints
-APPLY_LOOP_CONTRACTS=on
-USE_DYNAMIC_FRAMES=1
-
-# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
-EXTERNAL_SAT_SOLVER=
-CBMCFLAGS=--smt2
-CBMCFLAGS+=--slice-formula
-
-FUNCTION_NAME = unpack_sig
-
-# If this proof is found to consume huge amounts of RAM, you can set the
-# EXPENSIVE variable. With new enough versions of the proof tools, this will
-# restrict the number of EXPENSIVE CBMC jobs running at once. See the
-# documentation in Makefile.common under the "Job Pools" heading for details.
-# EXPENSIVE = true
-
-# This function is large enough to need...
-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
-# ("mldsa/poly.c") in PROJECT_SOURCES).
-# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
-# include ../Makefile.common
-# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c
-# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
-# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
-# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
-# be set before including Makefile.common, but any use of variables on the
-# left-hand side requires those variables to be defined. Hence, _SOURCE,
-# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
-
-include ../Makefile.common
diff --git a/proofs/cbmc/unpack_sig/unpack_sig_harness.c b/proofs/cbmc/unpack_sig/unpack_sig_harness.c
deleted file mode 100644
index 73adbe557..000000000
--- a/proofs/cbmc/unpack_sig/unpack_sig_harness.c
+++ /dev/null
@@ -1,15 +0,0 @@
-// Copyright (c) The mldsa-native project authors
-// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
-
-#include "packing.h"
-
-
-void harness(void)
-{
-  uint8_t *c;
-  uint8_t *sig;
-  mld_polyveck *h;
-  mld_polyvecl *z;
-  int r;
-  r = mld_unpack_sig(c, z, h, sig);
-}