diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry
index a2747887..8f116605 100644
--- a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry
+++ b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM.cry
@@ -1,4 +1,3 @@
 
-module ml_kem where
-
-import ml_kem512
\ No newline at end of file
+module Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM where
+    import Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM512
diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM1024.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM1024.cry
index d4ca1ee1..51d5afc2 100644
--- a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM1024.cry
+++ b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM1024.cry
@@ -1,11 +1,12 @@
 /*
-@copyright Galois, Inc
-@author Marios Georgiou <marios@galois.com>
-
-@copyright Amazon.com or its affiliates.
-@editor Rod Chapman <rodchap@amazon.com>
-*/
-module ml_kem1024 = specification where
+ * @copyright Galois, Inc
+ * @author Marios Georgiou <marios@galois.com>
+ *
+ * @copyright Amazon.com or its affiliates.
+ * @editor Rod Chapman <rodchap@amazon.com>
+ */
+module Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM1024 =
+    Primitive::Asymmetric::Cipher::ML_KEM::Specification where
 
 type k = 4
 type eta_1 = 2
diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM512.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM512.cry
index b99906d4..fa4f4d12 100644
--- a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM512.cry
+++ b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM512.cry
@@ -1,12 +1,13 @@
 /*
-@copyright Galois, Inc
-@author Marios Georgiou <marios@galois.com>
+ * @copyright Galois, Inc
+ * @author Marios Georgiou <marios@galois.com>
+ *
+ * @copyright Amazon.com or its affiliates.
+ * @editor Rod Chapman <rodchap@amazon.com>
+ */
 
-@copyright Amazon.com or its affiliates.
-@editor Rod Chapman <rodchap@amazon.com>
-*/
-
-module ml_kem512 = specification where
+module Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM512 =
+    Primitive::Asymmetric::Cipher::ML_KEM::Specification where
 
 type k = 2
 type eta_1 = 3
diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM768.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM768.cry
index f75b5001..8d78e852 100644
--- a/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM768.cry
+++ b/Primitive/Asymmetric/Cipher/ML_KEM/Instantiations/ML_KEM768.cry
@@ -1,11 +1,12 @@
 /*
-@copyright Galois, Inc
-@author Marios Georgiou <marios@galois.com>
-
-@copyright Amazon.com or its affiliates.
-@editor Rod Chapman <rodchap@amazon.com>
-*/
-module ml_kem768 = specification where
+ * @copyright Galois, Inc
+ * @author Marios Georgiou <marios@galois.com>
+ *
+ * @copyright Amazon.com or its affiliates.
+ * @editor Rod Chapman <rodchap@amazon.com>
+ */
+module Primitive::Asymmetric::Cipher::ML_KEM::Instantiations::ML_KEM768 =
+    Primitive::Asymmetric::Cipher::ML_KEM::Specification where
 
 type k = 3
 type eta_1 = 2
diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry
index e039b37a..1e45054a 100644
--- a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry
+++ b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry
@@ -7,7 +7,7 @@ ML-KEM cipher with a fast NTT implementation.
 @copyright Amazon.com or its affiliates.
 @author Rod Chapman <rodchap@amazon.com>
 */
-module specification where
+module Primitive::Asymmetric::Cipher::ML_KEM::Specification where
 
 type q = 3329