diff --git a/mlkem/mlkem_native.S b/mlkem/mlkem_native.S
index 373235fb91..8a1aca3ef0 100644
--- a/mlkem/mlkem_native.S
+++ b/mlkem/mlkem_native.S
@@ -205,15 +205,14 @@
 #undef mlk_indcpa_enc
 #undef mlk_indcpa_keypair_derand
 /* mlkem/src/kem.h */
-#undef MLK_CONFIG_NO_SUPERCOP
 #undef MLK_KEM_H
-#undef crypto_kem_check_pk
-#undef crypto_kem_check_sk
-#undef crypto_kem_dec
-#undef crypto_kem_enc
-#undef crypto_kem_enc_derand
-#undef crypto_kem_keypair
-#undef crypto_kem_keypair_derand
+#undef mlk_kem_check_pk
+#undef mlk_kem_check_sk
+#undef mlk_kem_dec
+#undef mlk_kem_enc
+#undef mlk_kem_enc_derand
+#undef mlk_kem_keypair
+#undef mlk_kem_keypair_derand
 /* mlkem/src/params.h */
 #undef MLKEM_DU
 #undef MLKEM_DV
diff --git a/mlkem/mlkem_native.c b/mlkem/mlkem_native.c
index 121fecfdc9..22d8c6d0b4 100644
--- a/mlkem/mlkem_native.c
+++ b/mlkem/mlkem_native.c
@@ -194,15 +194,14 @@
 #undef mlk_indcpa_enc
 #undef mlk_indcpa_keypair_derand
 /* mlkem/src/kem.h */
-#undef MLK_CONFIG_NO_SUPERCOP
 #undef MLK_KEM_H
-#undef crypto_kem_check_pk
-#undef crypto_kem_check_sk
-#undef crypto_kem_dec
-#undef crypto_kem_enc
-#undef crypto_kem_enc_derand
-#undef crypto_kem_keypair
-#undef crypto_kem_keypair_derand
+#undef mlk_kem_check_pk
+#undef mlk_kem_check_sk
+#undef mlk_kem_dec
+#undef mlk_kem_enc
+#undef mlk_kem_enc_derand
+#undef mlk_kem_keypair
+#undef mlk_kem_keypair_derand
 /* mlkem/src/params.h */
 #undef MLKEM_DU
 #undef MLKEM_DV
diff --git a/mlkem/src/kem.c b/mlkem/src/kem.c
index bdb549a118..a4f52b4798 100644
--- a/mlkem/src/kem.c
+++ b/mlkem/src/kem.c
@@ -41,7 +41,7 @@
 /* Reference: Not implemented in the reference implementation @[REF]. */
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_check_pk(const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
+int mlk_kem_check_pk(const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
 {
   typedef struct
   {
@@ -78,7 +78,7 @@ int crypto_kem_check_pk(const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
 /* Reference: Not implemented in the reference implementation @[REF]. */
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_check_sk(const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
+int mlk_kem_check_sk(const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
 {
   int ret = 0;
   MLK_ALLOC(test, uint8_t, MLKEM_SYMBYTES);
@@ -154,13 +154,13 @@ static int mlk_check_pct(uint8_t const pk[MLKEM_INDCCA_PUBLICKEYBYTES],
     goto cleanup;
   }
 
-  ret = crypto_kem_enc(ws->ct, ws->ss_enc, pk);
+  ret = mlk_kem_enc(ws->ct, ws->ss_enc, pk);
   if (ret != 0)
   {
     goto cleanup;
   }
 
-  ret = crypto_kem_dec(ws->ss_dec, ws->ct, sk);
+  ret = mlk_kem_dec(ws->ss_dec, ws->ct, sk);
   if (ret != 0)
   {
     goto cleanup;
@@ -208,9 +208,9 @@ static int mlk_check_pct(uint8_t const pk[MLKEM_INDCCA_PUBLICKEYBYTES],
  *            - We optionally include PCT which is not present in
  *              the reference code. */
 MLK_EXTERNAL_API
-int crypto_kem_keypair_derand(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
-                              uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES],
-                              const uint8_t coins[2 * MLKEM_SYMBYTES])
+int mlk_kem_keypair_derand(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
+                           uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES],
+                           const uint8_t coins[2 * MLKEM_SYMBYTES])
 {
   int ret;
 
@@ -244,8 +244,8 @@ int crypto_kem_keypair_derand(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
 /* Reference: `crypto_kem_keypair()` in the reference implementation @[REF]
  *            - We zeroize the stack buffer */
 MLK_EXTERNAL_API
-int crypto_kem_keypair(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
-                       uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
+int mlk_kem_keypair(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
+                    uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
 {
   int ret = 0;
   MLK_ALLOC(coins, uint8_t, 2 * MLKEM_SYMBYTES);
@@ -260,7 +260,7 @@ int crypto_kem_keypair(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
   mlk_randombytes(coins, 2 * MLKEM_SYMBYTES);
   MLK_CT_TESTING_SECRET(coins, 2 * MLKEM_SYMBYTES);
 
-  ret = crypto_kem_keypair_derand(pk, sk, coins);
+  ret = mlk_kem_keypair_derand(pk, sk, coins);
 
 cleanup:
   /* Specification: Partially implements
@@ -274,10 +274,10 @@ int crypto_kem_keypair(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
  *            - We include public key check
  *            - We include stack buffer zeroization */
 MLK_EXTERNAL_API
-int crypto_kem_enc_derand(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
-                          uint8_t ss[MLKEM_SSBYTES],
-                          const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
-                          const uint8_t coins[MLKEM_SYMBYTES])
+int mlk_kem_enc_derand(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
+                       uint8_t ss[MLKEM_SSBYTES],
+                       const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
+                       const uint8_t coins[MLKEM_SYMBYTES])
 {
   typedef struct
   {
@@ -295,7 +295,7 @@ int crypto_kem_enc_derand(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
   }
 
   /* Specification: Implements @[FIPS203, Section 7.2, Modulus check] */
-  ret = crypto_kem_check_pk(pk);
+  ret = mlk_kem_check_pk(pk);
   if (ret != 0)
   {
     goto cleanup;
@@ -327,9 +327,9 @@ int crypto_kem_enc_derand(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
 /* Reference: `crypto_kem_enc()` in the reference implementation @[REF]
  *            - We include stack buffer zeroization */
 MLK_EXTERNAL_API
-int crypto_kem_enc(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
-                   uint8_t ss[MLKEM_SSBYTES],
-                   const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
+int mlk_kem_enc(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
+                uint8_t ss[MLKEM_SSBYTES],
+                const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
 {
   int ret = 0;
   MLK_ALLOC(coins, uint8_t, MLKEM_SYMBYTES);
@@ -343,7 +343,7 @@ int crypto_kem_enc(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
   mlk_randombytes(coins, MLKEM_SYMBYTES);
   MLK_CT_TESTING_SECRET(coins, MLKEM_SYMBYTES);
 
-  ret = crypto_kem_enc_derand(ct, ss, pk, coins);
+  ret = mlk_kem_enc_derand(ct, ss, pk, coins);
 
 cleanup:
   /* Specification: Partially implements
@@ -357,9 +357,9 @@ int crypto_kem_enc(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
  *            - We include secret key check
  *            - We include stack buffer zeroization */
 MLK_EXTERNAL_API
-int crypto_kem_dec(uint8_t ss[MLKEM_SSBYTES],
-                   const uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
-                   const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
+int mlk_kem_dec(uint8_t ss[MLKEM_SSBYTES],
+                const uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
+                const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
 {
   typedef struct
   {
@@ -380,7 +380,7 @@ int crypto_kem_dec(uint8_t ss[MLKEM_SSBYTES],
   }
 
   /* Specification: Implements @[FIPS203, Section 7.3, Hash check] */
-  ret = crypto_kem_check_sk(sk);
+  ret = mlk_kem_check_sk(sk);
   if (ret != 0)
   {
     goto cleanup;
diff --git a/mlkem/src/kem.h b/mlkem/src/kem.h
index 0967d063ec..92438ffef5 100644
--- a/mlkem/src/kem.h
+++ b/mlkem/src/kem.h
@@ -28,9 +28,7 @@
 #if defined(MLK_CHECK_APIS)
 /* Include to ensure consistency between internal kem.h
  * and external mlkem_native.h. */
-#define MLK_CONFIG_NO_SUPERCOP
 #include "mlkem_native.h"
-#undef MLK_CONFIG_NO_SUPERCOP
 
 #if MLKEM_INDCCA_SECRETKEYBYTES != \
     MLKEM_SECRETKEYBYTES(MLK_CONFIG_PARAMETER_SET)
@@ -49,18 +47,16 @@
 
 #endif /* MLK_CHECK_APIS */
 
-#define crypto_kem_keypair_derand MLK_NAMESPACE_K(keypair_derand)
-#define crypto_kem_keypair MLK_NAMESPACE_K(keypair)
-#define crypto_kem_enc_derand MLK_NAMESPACE_K(enc_derand)
-#define crypto_kem_enc MLK_NAMESPACE_K(enc)
-#define crypto_kem_dec MLK_NAMESPACE_K(dec)
-#define crypto_kem_check_pk MLK_NAMESPACE_K(check_pk)
-#define crypto_kem_check_sk MLK_NAMESPACE_K(check_sk)
-
-
+#define mlk_kem_keypair_derand MLK_NAMESPACE_K(keypair_derand)
+#define mlk_kem_keypair MLK_NAMESPACE_K(keypair)
+#define mlk_kem_enc_derand MLK_NAMESPACE_K(enc_derand)
+#define mlk_kem_enc MLK_NAMESPACE_K(enc)
+#define mlk_kem_dec MLK_NAMESPACE_K(dec)
+#define mlk_kem_check_pk MLK_NAMESPACE_K(check_pk)
+#define mlk_kem_check_sk MLK_NAMESPACE_K(check_sk)
 
 /*************************************************
- * Name:        crypto_kem_check_pk
+ * Name:        mlk_kem_check_pk
  *
  * Description: Implements modulus check mandated by FIPS 203,
  *              i.e., ensures that coefficients are in [0,q-1].
@@ -81,7 +77,7 @@
 /* Reference: Not implemented in the reference implementation @[REF]. */
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_check_pk(const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
+int mlk_kem_check_pk(const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
 __contract__(
   requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
   ensures(return_value == 0 || return_value == MLK_ERR_FAIL ||
@@ -90,7 +86,7 @@ __contract__(
 
 
 /*************************************************
- * Name:        crypto_kem_check_sk
+ * Name:        mlk_kem_check_sk
  *
  * Description: Implements public key hash check mandated by FIPS 203,
  *              i.e., ensures that
@@ -112,7 +108,7 @@ __contract__(
 /* Reference: Not implemented in the reference implementation @[REF]. */
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_check_sk(const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
+int mlk_kem_check_sk(const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
 __contract__(
   requires(memory_no_alias(sk, MLKEM_INDCCA_SECRETKEYBYTES))
   ensures(return_value == 0 || return_value == MLK_ERR_FAIL ||
@@ -120,7 +116,7 @@ __contract__(
 );
 
 /*************************************************
- * Name:        crypto_kem_keypair_derand
+ * Name:        mlk_kem_keypair_derand
  *
  * Description: Generates public and private key
  *              for CCA-secure ML-KEM key encapsulation mechanism
@@ -146,9 +142,9 @@ __contract__(
  **************************************************/
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_keypair_derand(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
-                              uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES],
-                              const uint8_t coins[2 * MLKEM_SYMBYTES])
+int mlk_kem_keypair_derand(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
+                           uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES],
+                           const uint8_t coins[2 * MLKEM_SYMBYTES])
 __contract__(
   requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
   requires(memory_no_alias(sk, MLKEM_INDCCA_SECRETKEYBYTES))
@@ -160,7 +156,7 @@ __contract__(
 );
 
 /*************************************************
- * Name:        crypto_kem_keypair
+ * Name:        mlk_kem_keypair
  *
  * Description: Generates public and private key
  *              for CCA-secure ML-KEM key encapsulation mechanism
@@ -183,8 +179,8 @@ __contract__(
  **************************************************/
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_keypair(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
-                       uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
+int mlk_kem_keypair(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
+                    uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
 __contract__(
   requires(memory_no_alias(pk, MLKEM_INDCCA_PUBLICKEYBYTES))
   requires(memory_no_alias(sk, MLKEM_INDCCA_SECRETKEYBYTES))
@@ -195,7 +191,7 @@ __contract__(
 );
 
 /*************************************************
- * Name:        crypto_kem_enc_derand
+ * Name:        mlk_kem_enc_derand
  *
  * Description: Generates cipher text and shared
  *              secret for given public key
@@ -223,10 +219,10 @@ __contract__(
  **************************************************/
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_enc_derand(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
-                          uint8_t ss[MLKEM_SSBYTES],
-                          const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
-                          const uint8_t coins[MLKEM_SYMBYTES])
+int mlk_kem_enc_derand(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
+                       uint8_t ss[MLKEM_SSBYTES],
+                       const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
+                       const uint8_t coins[MLKEM_SYMBYTES])
 __contract__(
   requires(memory_no_alias(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))
   requires(memory_no_alias(ss, MLKEM_SSBYTES))
@@ -239,7 +235,7 @@ __contract__(
 );
 
 /*************************************************
- * Name:        crypto_kem_enc
+ * Name:        mlk_kem_enc
  *
  * Description: Generates cipher text and shared
  *              secret for given public key
@@ -264,9 +260,9 @@ __contract__(
  **************************************************/
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_enc(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
-                   uint8_t ss[MLKEM_SSBYTES],
-                   const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
+int mlk_kem_enc(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
+                uint8_t ss[MLKEM_SSBYTES],
+                const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
 __contract__(
   requires(memory_no_alias(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))
   requires(memory_no_alias(ss, MLKEM_SSBYTES))
@@ -278,7 +274,7 @@ __contract__(
 );
 
 /*************************************************
- * Name:        crypto_kem_dec
+ * Name:        mlk_kem_dec
  *
  * Description: Generates shared secret for given
  *              cipher text and private key
@@ -303,9 +299,9 @@ __contract__(
  **************************************************/
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
-int crypto_kem_dec(uint8_t ss[MLKEM_SSBYTES],
-                   const uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
-                   const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
+int mlk_kem_dec(uint8_t ss[MLKEM_SSBYTES],
+                const uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
+                const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
 __contract__(
   requires(memory_no_alias(ss, MLKEM_SSBYTES))
   requires(memory_no_alias(ct, MLKEM_INDCCA_CIPHERTEXTBYTES))
diff --git a/proofs/cbmc/crypto_kem_check_pk/Makefile b/proofs/cbmc/kem_check_pk/Makefile
similarity index 96%
rename from proofs/cbmc/crypto_kem_check_pk/Makefile
rename to proofs/cbmc/kem_check_pk/Makefile
index fee43f1f0b..0a72331150 100644
--- a/proofs/cbmc/crypto_kem_check_pk/Makefile
+++ b/proofs/cbmc/kem_check_pk/Makefile
@@ -4,11 +4,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = crypto_kem_check_pk_harness
+HARNESS_FILE = kem_check_pk_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 = crypto_kem_check_pk
+PROOF_UID = kem_check_pk
 
 DEFINES +=
 INCLUDES +=
diff --git a/proofs/cbmc/crypto_kem_check_pk/crypto_kem_check_pk_harness.c b/proofs/cbmc/kem_check_pk/kem_check_pk_harness.c
similarity index 88%
rename from proofs/cbmc/crypto_kem_check_pk/crypto_kem_check_pk_harness.c
rename to proofs/cbmc/kem_check_pk/kem_check_pk_harness.c
index 6dff43ac22..2c149a6fa7 100644
--- a/proofs/cbmc/crypto_kem_check_pk/crypto_kem_check_pk_harness.c
+++ b/proofs/cbmc/kem_check_pk/kem_check_pk_harness.c
@@ -7,5 +7,5 @@
 void harness(void)
 {
   uint8_t *a;
-  crypto_kem_check_pk(a);
+  mlk_kem_check_pk(a);
 }
diff --git a/proofs/cbmc/crypto_kem_check_sk/Makefile b/proofs/cbmc/kem_check_sk/Makefile
similarity index 96%
rename from proofs/cbmc/crypto_kem_check_sk/Makefile
rename to proofs/cbmc/kem_check_sk/Makefile
index 446bdc80ba..5a25738176 100644
--- a/proofs/cbmc/crypto_kem_check_sk/Makefile
+++ b/proofs/cbmc/kem_check_sk/Makefile
@@ -4,11 +4,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = crypto_kem_check_sk_harness
+HARNESS_FILE = kem_check_sk_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 = crypto_kem_check_sk
+PROOF_UID = kem_check_sk
 
 DEFINES +=
 INCLUDES +=
diff --git a/proofs/cbmc/crypto_kem_check_sk/crypto_kem_check_sk_harness.c b/proofs/cbmc/kem_check_sk/kem_check_sk_harness.c
similarity index 88%
rename from proofs/cbmc/crypto_kem_check_sk/crypto_kem_check_sk_harness.c
rename to proofs/cbmc/kem_check_sk/kem_check_sk_harness.c
index f1ffa8a5f9..1854246822 100644
--- a/proofs/cbmc/crypto_kem_check_sk/crypto_kem_check_sk_harness.c
+++ b/proofs/cbmc/kem_check_sk/kem_check_sk_harness.c
@@ -7,5 +7,5 @@
 void harness(void)
 {
   uint8_t *a;
-  crypto_kem_check_sk(a);
+  mlk_kem_check_sk(a);
 }
diff --git a/proofs/cbmc/crypto_kem_dec/Makefile b/proofs/cbmc/kem_dec/Makefile
similarity index 96%
rename from proofs/cbmc/crypto_kem_dec/Makefile
rename to proofs/cbmc/kem_dec/Makefile
index e7a6482f19..c51b8f0866 100644
--- a/proofs/cbmc/crypto_kem_dec/Makefile
+++ b/proofs/cbmc/kem_dec/Makefile
@@ -4,11 +4,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = crypto_kem_dec_harness
+HARNESS_FILE = kem_dec_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 = crypto_kem_dec
+PROOF_UID = kem_dec
 
 DEFINES +=
 INCLUDES +=
diff --git a/proofs/cbmc/crypto_kem_dec/crypto_kem_dec_harness.c b/proofs/cbmc/kem_dec/kem_dec_harness.c
similarity index 88%
rename from proofs/cbmc/crypto_kem_dec/crypto_kem_dec_harness.c
rename to proofs/cbmc/kem_dec/kem_dec_harness.c
index c5e81e8e3c..5306751e09 100644
--- a/proofs/cbmc/crypto_kem_dec/crypto_kem_dec_harness.c
+++ b/proofs/cbmc/kem_dec/kem_dec_harness.c
@@ -7,5 +7,5 @@
 void harness(void)
 {
   uint8_t *a, *b, *c;
-  crypto_kem_dec(a, b, c);
+  mlk_kem_dec(a, b, c);
 }
diff --git a/proofs/cbmc/crypto_kem_enc/Makefile b/proofs/cbmc/kem_enc/Makefile
similarity index 96%
rename from proofs/cbmc/crypto_kem_enc/Makefile
rename to proofs/cbmc/kem_enc/Makefile
index 1ec60a762a..e7744de099 100644
--- a/proofs/cbmc/crypto_kem_enc/Makefile
+++ b/proofs/cbmc/kem_enc/Makefile
@@ -4,11 +4,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = crypto_kem_enc_harness
+HARNESS_FILE = kem_enc_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 = crypto_kem_enc
+PROOF_UID = kem_enc
 
 DEFINES +=
 INCLUDES +=
diff --git a/proofs/cbmc/crypto_kem_enc/crypto_kem_enc_harness.c b/proofs/cbmc/kem_enc/kem_enc_harness.c
similarity index 88%
rename from proofs/cbmc/crypto_kem_enc/crypto_kem_enc_harness.c
rename to proofs/cbmc/kem_enc/kem_enc_harness.c
index 0fe6b74784..22c98cf067 100644
--- a/proofs/cbmc/crypto_kem_enc/crypto_kem_enc_harness.c
+++ b/proofs/cbmc/kem_enc/kem_enc_harness.c
@@ -7,5 +7,5 @@
 void harness(void)
 {
   uint8_t *a, *b, *c;
-  crypto_kem_enc(a, b, c);
+  mlk_kem_enc(a, b, c);
 }
diff --git a/proofs/cbmc/crypto_kem_enc_derand/Makefile b/proofs/cbmc/kem_enc_derand/Makefile
similarity index 96%
rename from proofs/cbmc/crypto_kem_enc_derand/Makefile
rename to proofs/cbmc/kem_enc_derand/Makefile
index 62512cf44a..d2e0b6cafe 100644
--- a/proofs/cbmc/crypto_kem_enc_derand/Makefile
+++ b/proofs/cbmc/kem_enc_derand/Makefile
@@ -4,11 +4,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = crypto_kem_enc_derand_harness
+HARNESS_FILE = kem_enc_derand_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 = crypto_kem_enc_derand
+PROOF_UID = kem_enc_derand
 
 DEFINES +=
 INCLUDES +=
diff --git a/proofs/cbmc/crypto_kem_enc_derand/crypto_kem_enc_derand_harness.c b/proofs/cbmc/kem_enc_derand/kem_enc_derand_harness.c
similarity index 85%
rename from proofs/cbmc/crypto_kem_enc_derand/crypto_kem_enc_derand_harness.c
rename to proofs/cbmc/kem_enc_derand/kem_enc_derand_harness.c
index 5b7a492051..c87338e5f3 100644
--- a/proofs/cbmc/crypto_kem_enc_derand/crypto_kem_enc_derand_harness.c
+++ b/proofs/cbmc/kem_enc_derand/kem_enc_derand_harness.c
@@ -7,5 +7,5 @@
 void harness(void)
 {
   uint8_t *a, *b, *c, *d;
-  crypto_kem_enc_derand(a, b, c, d);
+  mlk_kem_enc_derand(a, b, c, d);
 }
diff --git a/proofs/cbmc/crypto_kem_keypair/Makefile b/proofs/cbmc/kem_keypair/Makefile
similarity index 96%
rename from proofs/cbmc/crypto_kem_keypair/Makefile
rename to proofs/cbmc/kem_keypair/Makefile
index a6f9c15670..fd9e00c658 100644
--- a/proofs/cbmc/crypto_kem_keypair/Makefile
+++ b/proofs/cbmc/kem_keypair/Makefile
@@ -4,11 +4,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = crypto_kem_keypair_harness
+HARNESS_FILE = kem_keypair_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 = crypto_kem_keypair
+PROOF_UID = kem_keypair
 
 DEFINES +=
 INCLUDES +=
diff --git a/proofs/cbmc/crypto_kem_keypair/crypto_kem_keypair_harness.c b/proofs/cbmc/kem_keypair/kem_keypair_harness.c
similarity index 88%
rename from proofs/cbmc/crypto_kem_keypair/crypto_kem_keypair_harness.c
rename to proofs/cbmc/kem_keypair/kem_keypair_harness.c
index 7adecd45ea..beb98641cd 100644
--- a/proofs/cbmc/crypto_kem_keypair/crypto_kem_keypair_harness.c
+++ b/proofs/cbmc/kem_keypair/kem_keypair_harness.c
@@ -7,5 +7,5 @@
 void harness(void)
 {
   uint8_t *a, *b;
-  crypto_kem_keypair(a, b);
+  mlk_kem_keypair(a, b);
 }
diff --git a/proofs/cbmc/crypto_kem_keypair_derand/Makefile b/proofs/cbmc/kem_keypair_derand/Makefile
similarity index 95%
rename from proofs/cbmc/crypto_kem_keypair_derand/Makefile
rename to proofs/cbmc/kem_keypair_derand/Makefile
index b723b065f1..2c46c2f04f 100644
--- a/proofs/cbmc/crypto_kem_keypair_derand/Makefile
+++ b/proofs/cbmc/kem_keypair_derand/Makefile
@@ -4,11 +4,11 @@
 include ../Makefile_params.common
 
 HARNESS_ENTRY = harness
-HARNESS_FILE = crypto_kem_keypair_derand_harness
+HARNESS_FILE = kem_keypair_derand_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 = crypto_kem_keypair_derand
+PROOF_UID = kem_keypair_derand
 
 DEFINES +=
 INCLUDES +=
diff --git a/proofs/cbmc/crypto_kem_keypair_derand/crypto_kem_keypair_derand_harness.c b/proofs/cbmc/kem_keypair_derand/kem_keypair_derand_harness.c
similarity index 85%
rename from proofs/cbmc/crypto_kem_keypair_derand/crypto_kem_keypair_derand_harness.c
rename to proofs/cbmc/kem_keypair_derand/kem_keypair_derand_harness.c
index 308a6a9be3..d8316a63c7 100644
--- a/proofs/cbmc/crypto_kem_keypair_derand/crypto_kem_keypair_derand_harness.c
+++ b/proofs/cbmc/kem_keypair_derand/kem_keypair_derand_harness.c
@@ -7,5 +7,5 @@
 void harness(void)
 {
   uint8_t *a, *b, *c;
-  crypto_kem_keypair_derand(a, b, c);
+  mlk_kem_keypair_derand(a, b, c);
 }