diff --git a/code/jasmin/mlkem_avx2/example/api.h b/code/jasmin/mlkem_avx2/example/api.h
index 824739ab..f2d372b6 100644
--- a/code/jasmin/mlkem_avx2/example/api.h
+++ b/code/jasmin/mlkem_avx2/example/api.h
@@ -14,31 +14,31 @@
 #define JADE_KEM_mlkem_mlkem768_amd64_avx2_ARCH            "amd64"
 #define JADE_KEM_mlkem_mlkem768_amd64_avx2_IMPL            "ref"
 
-int jade_kem_mlkem_mlkem768_amd64_avx2v_keypair_derand(
+int jade_kem_mlkem_mlkem768_amd64_avx2_keypair_derand(
   uint8_t *public_key,
   uint8_t *secret_key,
   const uint8_t *coins
 );
 
-int jade_kem_mlkem_mlkem768_amd64_avx2v_keypair(
+int jade_kem_mlkem_mlkem768_amd64_avx2_keypair(
   uint8_t *public_key,
   uint8_t *secret_key
 );
 
-int jade_kem_mlkem_mlkem768_amd64_avx2v_enc_derand(
+int jade_kem_mlkem_mlkem768_amd64_avx2_enc_derand(
   uint8_t *ciphertext,
   uint8_t *shared_secret,
   const uint8_t *public_key,
   const uint8_t *coins
 );
 
-int jade_kem_mlkem_mlkem768_amd64_avx2v_enc(
+int jade_kem_mlkem_mlkem768_amd64_avx2_enc(
   uint8_t *ciphertext,
   uint8_t *shared_secret,
   const uint8_t *public_key
 );
 
-int jade_kem_mlkem_mlkem768_amd64_avx2v_dec(
+int jade_kem_mlkem_mlkem768_amd64_avx2_dec(
   uint8_t *shared_secret,
   const uint8_t *ciphertext,
   const uint8_t *secret_key
diff --git a/code/jasmin/mlkem_avx2/example/example.c b/code/jasmin/mlkem_avx2/example/example.c
index 6eb06f9f..d88c8fd3 100644
--- a/code/jasmin/mlkem_avx2/example/example.c
+++ b/code/jasmin/mlkem_avx2/example/example.c
@@ -59,12 +59,12 @@ uint8_t* randombytes(uint8_t* x, uint64_t xlen)
 #define JADE_KEM_ENCCOINBYTES JADE_KEM_mlkem_mlkem768_amd64_avx2_ENCCOINBYTES
 #define JADE_KEM_BYTES JADE_KEM_mlkem_mlkem768_amd64_avx2_BYTES
 
-#define jade_kem_keypair jade_kem_mlkem_mlkem768_amd64_avx2v_keypair
-#define jade_kem_enc jade_kem_mlkem_mlkem768_amd64_avx2v_enc
-#define jade_kem_dec jade_kem_mlkem_mlkem768_amd64_avx2v_dec
+#define jade_kem_keypair jade_kem_mlkem_mlkem768_amd64_avx2_keypair
+#define jade_kem_enc jade_kem_mlkem_mlkem768_amd64_avx2_enc
+#define jade_kem_dec jade_kem_mlkem_mlkem768_amd64_avx2_dec
 
-#define jade_kem_keypair_derand jade_kem_mlkem_mlkem768_amd64_avx2v_keypair_derand
-#define jade_kem_enc_derand jade_kem_mlkem_mlkem768_amd64_avx2v_enc_derand
+#define jade_kem_keypair_derand jade_kem_mlkem_mlkem768_amd64_avx2_keypair_derand
+#define jade_kem_enc_derand jade_kem_mlkem_mlkem768_amd64_avx2_enc_derand
 
 #define JADE_KEM_ALGNAME JADE_KEM_mlkem_mlkem768_amd64_avx2_ALGNAME
 #define JADE_KEM_ARCH JADE_KEM_mlkem_mlkem768_amd64_avx2_ARCH
diff --git a/code/jasmin/mlkem_avx2/extraction/Makefile b/code/jasmin/mlkem_avx2/extraction/Makefile
index 51ce760c..51033d90 100644
--- a/code/jasmin/mlkem_avx2/extraction/Makefile
+++ b/code/jasmin/mlkem_avx2/extraction/Makefile
@@ -11,9 +11,9 @@ all: ec
 
 ec:
 	$(JASMINC) ../jkem.jazz -oec jkem_avx2.ec \
-	  -ec jade_kem_mlkem_mlkem768_amd64_avx2v_keypair \
-	  -ec jade_kem_mlkem_mlkem768_amd64_avx2v_enc \
-	  -ec jade_kem_mlkem_mlkem768_amd64_avx2v_dec
+	  -ec jade_kem_mlkem_mlkem768_amd64_avx2_keypair \
+	  -ec jade_kem_mlkem_mlkem768_amd64_avx2_enc \
+	  -ec jade_kem_mlkem_mlkem768_amd64_avx2_dec
 
 clean:
 	rm -f *.ec
diff --git a/code/jasmin/mlkem_avx2/extraction/jkem_avx2.ec b/code/jasmin/mlkem_avx2/extraction/jkem_avx2.ec
index 104ed9a4..6ede73cd 100644
--- a/code/jasmin/mlkem_avx2/extraction/jkem_avx2.ec
+++ b/code/jasmin/mlkem_avx2/extraction/jkem_avx2.ec
@@ -5121,7 +5121,7 @@ module M(SC:Syscall_t) = {
     return ();
   }
   
-  proc jade_kem_mlkem_mlkem768_amd64_avx2v_keypair (public_key:W64.t,
+  proc jade_kem_mlkem_mlkem768_amd64_avx2_keypair (public_key:W64.t,
                                                     secret_key:W64.t) : 
   W64.t = {
     
@@ -5144,7 +5144,7 @@ module M(SC:Syscall_t) = {
     return (r);
   }
   
-  proc jade_kem_mlkem_mlkem768_amd64_avx2v_enc (ciphertext:W64.t,
+  proc jade_kem_mlkem_mlkem768_amd64_avx2_enc (ciphertext:W64.t,
                                                 shared_secret:W64.t,
                                                 public_key:W64.t) : W64.t = {
     
@@ -5169,7 +5169,7 @@ module M(SC:Syscall_t) = {
     return (r);
   }
   
-  proc jade_kem_mlkem_mlkem768_amd64_avx2v_dec (shared_secret:W64.t,
+  proc jade_kem_mlkem_mlkem768_amd64_avx2_dec (shared_secret:W64.t,
                                                 ciphertext:W64.t,
                                                 secret_key:W64.t) : W64.t = {
     
diff --git a/code/jasmin/mlkem_avx2/jkem.jazz b/code/jasmin/mlkem_avx2/jkem.jazz
index ce77dcf4..13ba3cc9 100644
--- a/code/jasmin/mlkem_avx2/jkem.jazz
+++ b/code/jasmin/mlkem_avx2/jkem.jazz
@@ -1,6 +1,6 @@
 require "kem.jinc"
 
-export fn jade_kem_mlkem_mlkem768_amd64_avx2v_keypair_derand(reg u64 public_key secret_key coins) -> reg u64
+export fn jade_kem_mlkem_mlkem768_amd64_avx2_keypair_derand(reg u64 public_key secret_key coins) -> reg u64
 {
   reg u64 r;
   stack u8[MLKEM_SYMBYTES*2] randomness;
@@ -22,7 +22,7 @@ export fn jade_kem_mlkem_mlkem768_amd64_avx2v_keypair_derand(reg u64 public_key
   return r;
 }
 
-export fn jade_kem_mlkem_mlkem768_amd64_avx2v_enc_derand(reg u64 ciphertext shared_secret public_key coins) -> reg u64
+export fn jade_kem_mlkem_mlkem768_amd64_avx2_enc_derand(reg u64 ciphertext shared_secret public_key coins) -> reg u64
 {
   reg u64 r;
   stack u8[MLKEM_SYMBYTES] randomness;
@@ -45,7 +45,7 @@ export fn jade_kem_mlkem_mlkem768_amd64_avx2v_enc_derand(reg u64 ciphertext shar
   return r;
 }
 
-export fn jade_kem_mlkem_mlkem768_amd64_avx2v_keypair(reg u64 public_key secret_key) -> reg u64
+export fn jade_kem_mlkem_mlkem768_amd64_avx2_keypair(reg u64 public_key secret_key) -> reg u64
 {
   reg u64 r;
   stack u8[MLKEM_SYMBYTES*2] randomness;
@@ -61,7 +61,7 @@ export fn jade_kem_mlkem_mlkem768_amd64_avx2v_keypair(reg u64 public_key secret_
   return r;
 }
 
-export fn jade_kem_mlkem_mlkem768_amd64_avx2v_enc(reg u64 ciphertext shared_secret public_key) -> reg u64
+export fn jade_kem_mlkem_mlkem768_amd64_avx2_enc(reg u64 ciphertext shared_secret public_key) -> reg u64
 {
   reg u64 r;
   stack u8[MLKEM_SYMBYTES] randomness;
@@ -78,7 +78,7 @@ export fn jade_kem_mlkem_mlkem768_amd64_avx2v_enc(reg u64 ciphertext shared_secr
   return r;
 }
 
-export fn jade_kem_mlkem_mlkem768_amd64_avx2v_dec(reg u64 shared_secret ciphertext secret_key) -> reg u64
+export fn jade_kem_mlkem_mlkem768_amd64_avx2_dec(reg u64 shared_secret ciphertext secret_key) -> reg u64
 {
   reg u64 r;
   __crypto_kem_dec_jazz(shared_secret, ciphertext, secret_key);
diff --git a/code/jasmin/mlkem_avx2/kem.h b/code/jasmin/mlkem_avx2/kem.h
index c86b2540..130c142d 100644
--- a/code/jasmin/mlkem_avx2/kem.h
+++ b/code/jasmin/mlkem_avx2/kem.h
@@ -16,24 +16,24 @@ void crypto_kem_dec(unsigned char *m,
                 const unsigned char *c,
                 const unsigned char *sk);
 
-void jade_kem_mlkem_mlkem768_amd64_avx2v_keypair_derand(unsigned char *pk,
+void jade_kem_mlkem_mlkem768_amd64_avx2_keypair_derand(unsigned char *pk,
                          unsigned char *sk,
                          const unsigned char *randomness);
 
-void jade_kem_mlkem_mlkem768_amd64_avx2v_enc_derand(unsigned char *c,
+void jade_kem_mlkem_mlkem768_amd64_avx2_enc_derand(unsigned char *c,
                      const unsigned char *m,
                      const unsigned char *pk,
                      const unsigned char *coins);
 
 
-void jade_kem_mlkem_mlkem768_amd64_avx2v_keypair(unsigned char *pk,
+void jade_kem_mlkem_mlkem768_amd64_avx2_keypair(unsigned char *pk,
                          unsigned char *sk);
 
-void jade_kem_mlkem_mlkem768_amd64_avx2v_enc(unsigned char *c,
+void jade_kem_mlkem_mlkem768_amd64_avx2_enc(unsigned char *c,
                      const unsigned char *m,
                      const unsigned char *pk);
 
-void jade_kem_mlkem_mlkem768_amd64_avx2v_dec(unsigned char *m,
+void jade_kem_mlkem_mlkem768_amd64_avx2_dec(unsigned char *m,
                      const unsigned char *c,
                      const unsigned char *sk);
 
diff --git a/code/jasmin/mlkem_avx2/test/test_kem.c b/code/jasmin/mlkem_avx2/test/test_kem.c
index 09f984af..1e915ab1 100644
--- a/code/jasmin/mlkem_avx2/test/test_kem.c
+++ b/code/jasmin/mlkem_avx2/test/test_kem.c
@@ -40,7 +40,7 @@ int main(void)
     assert(ri == 1);
 
     /* TEST KEYPAIR */
-    jade_kem_mlkem_mlkem768_amd64_avx2v_keypair_derand(pk1, sk1, randomness0);
+    jade_kem_mlkem_mlkem768_amd64_avx2_keypair_derand(pk1, sk1, randomness0);
     crypto_kem_keypair(pk0, sk0, randomness0);
 
     for(int i=0;i<MLKEM_SECRETKEYBYTES;i++)
@@ -61,7 +61,7 @@ int main(void)
 
     /* TEST ENCAPSULATION */
     crypto_kem_enc(ct0, shk0, pk0, randomness1);
-    jade_kem_mlkem_mlkem768_amd64_avx2v_enc_derand(ct1, shk1, pk1, randomness1);
+    jade_kem_mlkem_mlkem768_amd64_avx2_enc_derand(ct1, shk1, pk1, randomness1);
 
     for(int i=0;i<MLKEM_CIPHERTEXTBYTES;i++)
     { if(ct0[i] != ct1[i])
@@ -84,7 +84,7 @@ int main(void)
     memset(shk1, 0, MLKEM_SSBYTES);
 
     crypto_kem_dec(shk0, ct0, sk0);
-    jade_kem_mlkem_mlkem768_amd64_avx2v_dec(shk1, ct1, sk1);
+    jade_kem_mlkem_mlkem768_amd64_avx2_dec(shk1, ct1, sk1);
 
     for(int i=0;i<MLKEM_SSBYTES;i++)
     { if(shk0[i] != shk1[i])
@@ -102,7 +102,7 @@ int main(void)
     ct1[0] = ct0[0];
 
     crypto_kem_dec(shk0, ct0, sk0);
-    jade_kem_mlkem_mlkem768_amd64_avx2v_dec(shk1, ct1, sk1);
+    jade_kem_mlkem_mlkem768_amd64_avx2_dec(shk1, ct1, sk1);
 
     for(int i=0;i<MLKEM_SSBYTES;i++)
     { if(shk0[i] != shk1[i])
diff --git a/code/jasmin/test/run.jazz b/code/jasmin/test/run.jazz
index ec8b746f..2b831224 100644
--- a/code/jasmin/test/run.jazz
+++ b/code/jasmin/test/run.jazz
@@ -53,11 +53,11 @@ fn test_avx_derand() -> reg bool {
   pk, sk, ct, ss1, ss2, coins = setup(true);
 
   #[inline]
-  _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2v_keypair_derand(pk, sk, coins);
+  _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2_keypair_derand(pk, sk, coins);
   #[inline]
-  _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2v_enc_derand(ct, ss1, pk, coins + 32);
+  _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2_enc_derand(ct, ss1, pk, coins + 32);
   #[inline]
-  _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2v_dec(ss2, ct, sk);
+  _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2_dec(ss2, ct, sk);
 
   reg bool r;
   r = check(ss1, ss2);
@@ -85,11 +85,11 @@ fn test_avx() -> reg bool {
   pk, sk, ct, ss1, ss2, _ = setup(false);
 
   #[inline]
-  _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2v_keypair(pk, sk);
+  _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2_keypair(pk, sk);
   #[inline]
-  _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2v_enc(ct, ss1, pk);
+  _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2_enc(ct, ss1, pk);
   #[inline]
-  _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2v_dec(ss2, ct, sk);
+  _ = avx::jade_kem_mlkem_mlkem768_amd64_avx2_dec(ss2, ct, sk);
 
   reg bool r;
   r = check(ss1, ss2);