diff --git a/cbmc/proofs/crypto_kem_dec/Makefile b/cbmc/proofs/crypto_kem_dec/Makefile
index f883ca965..cad79622a 100644
--- a/cbmc/proofs/crypto_kem_dec/Makefile
+++ b/cbmc/proofs/crypto_kem_dec/Makefile
@@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)dec
-USE_FUNCTION_CONTRACTS= $(FIPS202_NAMESPACE)sha3_512 $(FIPS202_NAMESPACE)sha3_256 $(MLKEM_NAMESPACE)indcpa_enc $(MLKEM_NAMESPACE)indcpa_dec $(MLKEM_NAMESPACE)mlkem_shake256_rkprf $(MLKEM_NAMESPACE)ct_memcmp $(MLKEM_NAMESPACE)ct_cmov_zero memcmp
+USE_FUNCTION_CONTRACTS= $(FIPS202_NAMESPACE)sha3_512 $(FIPS202_NAMESPACE)sha3_256 $(MLKEM_NAMESPACE)indcpa_enc $(MLKEM_NAMESPACE)indcpa_dec $(MLKEM_NAMESPACE)mlkem_shake256_rkprf ct_memcmp ct_cmov_zero memcmp
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
diff --git a/cbmc/proofs/ct_cmov_zero/Makefile b/cbmc/proofs/ct_cmov_zero/Makefile
index 06f1b2f3c..847cb2405 100644
--- a/cbmc/proofs/ct_cmov_zero/Makefile
+++ b/cbmc/proofs/ct_cmov_zero/Makefile
@@ -18,7 +18,7 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c # Dummy source
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ct_cmov_zero
+CHECK_FUNCTION_CONTRACTS=ct_cmov_zero
 USE_FUNCTION_CONTRACTS=ct_sel_uint8
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
@@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--smt2
 
-FUNCTION_NAME = $(MLKEM_NAMESPACE)ct_cmov_zero
+FUNCTION_NAME = ct_cmov_zero
 
 # 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
diff --git a/cbmc/proofs/ct_memcmp/Makefile b/cbmc/proofs/ct_memcmp/Makefile
index 452701127..917c49db1 100644
--- a/cbmc/proofs/ct_memcmp/Makefile
+++ b/cbmc/proofs/ct_memcmp/Makefile
@@ -18,7 +18,7 @@ UNWINDSET +=
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/poly.c
 
-CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)ct_memcmp
+CHECK_FUNCTION_CONTRACTS=ct_memcmp
 USE_FUNCTION_CONTRACTS=value_barrier_u8 ct_cmask_nonzero_u8
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
@@ -27,7 +27,7 @@ USE_DYNAMIC_FRAMES=1
 EXTERNAL_SAT_SOLVER=
 CBMCFLAGS=--bitwuzla
 
-FUNCTION_NAME = $(MLKEM_NAMESPACE)ct_memcmp
+FUNCTION_NAME = ct_memcmp
 
 # 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
diff --git a/mlkem/verify.h b/mlkem/verify.h
index 99d6e5f63..5c62223c3 100644
--- a/mlkem/verify.h
+++ b/mlkem/verify.h
@@ -225,7 +225,6 @@ __contract__(ensures(return_value == (cond ? a : b)))
   return b ^ (ct_cmask_nonzero_u8(cond) & (a ^ b));
 }
 
-#define ct_memcmp MLKEM_NAMESPACE(ct_memcmp)
 /*************************************************
  * Name:        ct_memcmp
  *
@@ -275,7 +274,6 @@ __contract__(
   return (value_barrier_u8(ct_cmask_nonzero_u8(r) ^ s) ^ s);
 }
 
-#define ct_cmov_zero MLKEM_NAMESPACE(ct_cmov_zero)
 /*************************************************
  * Name:        ct_cmov_zero
  *