diff --git a/.gitignore b/.gitignore
index 777dce3a..76f14337 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,4 @@
 .ci
 *.tar.gz
 libjade-*
+.vscode
\ No newline at end of file
diff --git a/proof/crypto_kem/xwing/amd64/.gitkeep b/proof/crypto_kem/xwing/amd64/.gitkeep
new file mode 100644
index 00000000..e69de29b
diff --git a/src/common/keccak/common/fips202_DIRTY.jinc b/src/common/keccak/common/fips202_DIRTY.jinc
index 9988b10a..92698c60 100644
--- a/src/common/keccak/common/fips202_DIRTY.jinc
+++ b/src/common/keccak/common/fips202_DIRTY.jinc
@@ -84,6 +84,63 @@ fn _sha3_256_32(reg ptr u8[32] out, reg ptr u8[KYBER_SYMBYTES] in) -> reg ptr u8
   return out;
 }
 
+#[returnaddress="stack"]
+fn _sha3_256_134(reg ptr u8[32] out, reg ptr u8[134] in) -> reg ptr u8[32]
+{
+  reg u256[7] state;
+  stack u64[28] s_state;
+  stack u64[25] a_jagged_p;
+  reg u64 t l;
+  reg u8 c;
+  inline int i;
+
+  a_jagged_p = KECCAK_A_JAGGED;
+  s_state = __init_s_state_avx2();
+
+  state[0] = #VPBROADCAST_4u64(in[u64 0]);
+
+  for i=1 to 16
+  {
+    t = in[u64 i];
+    l = a_jagged_p[i];
+    s_state[(int) l] = t;
+  }
+
+  c = in[u8 128];
+  l = a_jagged_p[(int) 16];
+  l <<= 3;
+  s_state[u8 (int)l] = c;
+
+  for i = 129 to 134{
+    c = in[i];
+    l += 1;
+    s_state[u8 (int)l] = c;
+  }
+
+  l += 1;
+  s_state[u8 (int)l] = 0x06;
+
+  l = a_jagged_p[(SHA3_256_RATE-1)/8];
+  l <<= 3;
+  t = SHA3_256_RATE - 1; t &= 0x7;
+  l += t;
+  s_state[u8 (int)l] ^= 0x80;
+
+  for i=1 to 7 { state[i] = s_state[u256 i]; }
+  
+  state = __keccakf1600_avx2(state);
+
+  for i=0 to 7 { s_state[u256 i] = state[i]; }
+
+  for i=0 to 4
+  {
+    l = a_jagged_p[i];
+    t = s_state[(int)l];
+    out[u64 i] = t;
+  }
+
+  return out;
+}
 
 #[returnaddress="stack"]
 fn _shake256_64(reg u64 out outlen, reg const ptr u8[64] in)
diff --git a/src/common/keccak/common/fips202_ref_DIRTY.jinc b/src/common/keccak/common/fips202_ref_DIRTY.jinc
index dcb4480c..d8dd1d63 100644
--- a/src/common/keccak/common/fips202_ref_DIRTY.jinc
+++ b/src/common/keccak/common/fips202_ref_DIRTY.jinc
@@ -235,6 +235,40 @@ fn _sha3_256_32(reg ptr u8[32] out, reg ptr u8[KYBER_SYMBYTES] in) -> reg ptr u8
   return out;
 }
 
+
+#[returnaddress="stack"]
+fn _sha3_256_134(reg ptr u8[32] out, reg ptr u8[134] in) -> reg ptr u8[32]
+{
+  stack u64[25] state;
+  stack ptr u8[32] s_out;
+  reg u64 t64;
+  inline int i;
+
+  s_out = out;
+
+  state = __keccak_init_ref1(state);
+
+  for i=0 to 134
+  {
+    state[u8 i] = in[i];
+  }
+
+  state[u8 134] ^= 0x06;
+  state[u8 SHA3_256_RATE - 1] = 0x80;
+
+  state = __keccakf1600_ref1(state);
+
+  out = s_out;
+
+  for i=0 to 4
+  {
+    t64 = state[i];
+    out[u64 i] = t64;
+  }
+
+  return out;
+}
+
 #[returnaddress="stack"]
 fn _sha3_512_64(reg ptr u8[64] out, reg const ptr u8[64] in) -> stack u8[64]
 {
diff --git a/src/common/tofromstack.jinc b/src/common/tofromstack.jinc
index 8f03272c..493842ca 100644
--- a/src/common/tofromstack.jinc
+++ b/src/common/tofromstack.jinc
@@ -13,6 +13,21 @@ fn __tostack64u8(reg ptr u8[64] out, reg u64 inp) -> reg ptr u8[64]
   return out;
 }
 
+inline 
+fn __tostack96u8(reg ptr u8[96] out, reg u64 inp) -> reg ptr u8[96] 
+{
+  reg u8 t;
+  inline int i;
+
+  for i=0 to 96 
+  {
+    t = (u8)[inp + i];
+    out[i] = t;
+  }
+  return out;
+}
+
+
 inline 
 fn __tostack32u8(reg ptr u8[32] out, reg u64 inp) -> reg ptr u8[32] 
 {
@@ -40,3 +55,29 @@ fn __fromstack32u8(reg u64 outp, reg ptr u8[32] in)
     (u8)[outp + i] = t;
   }
 }
+
+inline 
+fn __fromstack134u8(reg u64 outp, reg ptr u8[134] in)
+{
+  reg u8 t;
+  inline int i;
+
+  for i=0 to 134
+  {
+    t = in[i];
+    (u8)[outp + i] = t;
+  }
+}
+
+inline 
+fn __fromstack64u8(reg u64 outp, reg ptr u8[64] in)
+{
+  reg u8 t;
+  inline int i;
+
+  for i=0 to 64
+  {
+    t = in[i];
+    (u8)[outp + i] = t;
+  }
+}
\ No newline at end of file
diff --git a/src/crypto_kem/mlkem/mlkem768/amd64/ref/params.jinc b/src/crypto_kem/mlkem/mlkem768/amd64/ref/params.jinc
index 085e975c..9e38ad46 100644
--- a/src/crypto_kem/mlkem/mlkem768/amd64/ref/params.jinc
+++ b/src/crypto_kem/mlkem/mlkem768/amd64/ref/params.jinc
@@ -14,3 +14,10 @@ param int MLKEM_CT_LEN = MLKEM_POLYVECCOMPRESSEDBYTES + MLKEM_POLYCOMPRESSEDBYTE
 param int MLKEM_INDCPA_PUBLICKEYBYTES = MLKEM_POLYVECBYTES + MLKEM_SYMBYTES;
 param int MLKEM_PUBLICKEYBYTES = MLKEM_INDCPA_PUBLICKEYBYTES;
 param int MLKEM_SSBYTES = 32;
+
+// the following is a patch to handle inconsistencies between ref/params.jinc and avx2/params.jinc (motivated by xwing);
+// this needs to be fixed upstream, in formosa-mlkem
+param int MLKEM_INDCPA_CIPHERTEXTBYTES = MLKEM_POLYVECCOMPRESSEDBYTES + MLKEM_POLYCOMPRESSEDBYTES;
+param int MLKEM_INDCPA_SECRETKEYBYTES = MLKEM_POLYVECBYTES;
+param int MLKEM_SECRETKEYBYTES = MLKEM_INDCPA_SECRETKEYBYTES + MLKEM_INDCPA_PUBLICKEYBYTES + 2*MLKEM_SYMBYTES;
+param int MLKEM_CIPHERTEXTBYTES = MLKEM_INDCPA_CIPHERTEXTBYTES;
diff --git a/src/crypto_kem/xwing/META.yml b/src/crypto_kem/xwing/META.yml
new file mode 100644
index 00000000..21c2b0e6
--- /dev/null
+++ b/src/crypto_kem/xwing/META.yml
@@ -0,0 +1,26 @@
+name: X-Wing
+type: kem
+checksumsmall: d80f0bfdf6d38a189cfffe48c048973521c02456bde1934475c38e0819c4afae
+checksumbig: 607234d1da70d4441c64c8bb3deff3f22728a38942500457c92dbcdaf393d0c0
+claimed-nist-level: 3
+claimed-security: IND-CCA2
+length-public-key: 1216
+length-ciphertext: 1120
+length-secret-key: 2464
+length-shared-secret: 32
+principal-submitters:
+  - TODO
+auxiliary-submitters:
+  - TODO
+implementations:
+    - name: amd64/ref
+      version: TODO
+      supported_platforms:
+        - architecture: x86_64
+          operating_systems:
+              - Linux
+              - Darwin
+          required_flags: # FIXME
+              - avx2
+              - bmi2
+              - popcnt
diff --git a/src/crypto_kem/xwing/amd64/avx2/Makefile b/src/crypto_kem/xwing/amd64/avx2/Makefile
new file mode 100644
index 00000000..578d38fd
--- /dev/null
+++ b/src/crypto_kem/xwing/amd64/avx2/Makefile
@@ -0,0 +1,3 @@
+SAFETY_FLAGS := -nocheckalignment
+SRCS := kem.jazz
+include ../../../../Makefile.common
\ No newline at end of file
diff --git a/src/crypto_kem/xwing/amd64/avx2/include/api.h b/src/crypto_kem/xwing/amd64/avx2/include/api.h
new file mode 100644
index 00000000..a8331912
--- /dev/null
+++ b/src/crypto_kem/xwing/amd64/avx2/include/api.h
@@ -0,0 +1,47 @@
+#ifndef JADE_KEM_xwing_amd64_avx2_API_H
+#define JADE_KEM_xwing_amd64_avx2_API_H
+
+#include <stdint.h>
+
+#define JADE_KEM_xwing_amd64_avx2_PUBLICKEYBYTES   1216
+#define JADE_KEM_xwing_amd64_avx2_SECRETKEYBYTES   2464
+#define JADE_KEM_xwing_amd64_avx2_CIPHERTEXTBYTES  1120
+#define JADE_KEM_xwing_amd64_avx2_KEYPAIRCOINBYTES 96
+#define JADE_KEM_xwing_amd64_avx2_ENCCOINBYTES     64
+#define JADE_KEM_xwing_amd64_avx2_BYTES            32
+
+#define JADE_KEM_xwing_amd64_avx2_ALGNAME         "X-Wing"
+#define JADE_KEM_xwing_amd64_avx2_ARCH            "amd64"
+#define JADE_KEM_xwing_amd64_avx2_IMPL            "ref"
+
+int jade_kem_xwing_amd64_avx2_keypair_derand(
+  uint8_t *public_key,
+  uint8_t *secret_key,
+  const uint8_t *coins
+);
+
+int jade_kem_xwing_amd64_avx2_keypair(
+  uint8_t *public_key,
+  uint8_t *secret_key
+);
+
+int jade_kem_xwing_amd64_avx2_enc_derand(
+  uint8_t *ciphertext,
+  uint8_t *shared_secret,
+  const uint8_t *public_key,
+  const uint8_t *coins
+);
+
+int jade_kem_xwing_amd64_avx2_enc(
+  uint8_t *ciphertext,
+  uint8_t *shared_secret,
+  const uint8_t *public_key
+);
+
+int jade_kem_xwing_amd64_avx2_dec(
+  uint8_t *shared_secret,
+  const uint8_t *ciphertext,
+  const uint8_t *secret_key
+);
+
+#endif
diff --git a/src/crypto_kem/xwing/amd64/avx2/kem.jazz b/src/crypto_kem/xwing/amd64/avx2/kem.jazz
new file mode 100644
index 00000000..21b5056c
--- /dev/null
+++ b/src/crypto_kem/xwing/amd64/avx2/kem.jazz
@@ -0,0 +1,92 @@
+from Jade require "common/tofromstack.jinc"
+
+from Jade require "crypto_kem/mlkem/mlkem768/amd64/avx2/kem.jinc"
+from Jade require "crypto_kem/xwing/amd64/ref/kem.jinc"
+from Jade require "crypto_kem/xwing/amd64/ref/params.jinc"
+
+export fn jade_kem_xwing_amd64_avx2_keypair_derand(reg u64 public_key secret_key coins) -> reg u64
+{
+  reg u64 r;
+  stack u8[XWING_KEYPAIRCOINBYTES] stack_coins;
+
+  _ = #init_msf();
+
+  public_key = public_key;
+  secret_key = secret_key;
+  stack_coins = __tostack96u8(stack_coins, coins);
+
+  _crypto_xkem_keypair_derand_jazz(public_key, secret_key, stack_coins);
+
+  ?{}, r = #set0();
+  return r;
+}
+
+export fn jade_kem_xwing_amd64_avx2_keypair(reg u64 public_key secret_key) -> reg u64
+{
+  reg u64 r;
+  stack u8[XWING_KEYPAIRCOINBYTES] stack_coins;
+
+  _ = #init_msf();
+
+  public_key = public_key;
+  secret_key = secret_key;
+  stack_coins = #randombytes(stack_coins);
+
+  _crypto_xkem_keypair_derand_jazz(public_key, secret_key, stack_coins);
+
+  ?{}, r = #set0();
+  return r;
+}
+
+export fn jade_kem_xwing_amd64_avx2_enc_derand(reg u64 ciphertext shared_secret public_key coins) -> reg u64
+{
+  reg u64 r;
+  stack u8[XWING_ENCCOINBYTES] stack_coins;
+
+  _ = #init_msf();
+
+  ciphertext = ciphertext;
+  shared_secret = shared_secret;
+  public_key = public_key;
+  stack_coins = __tostack64u8(stack_coins, coins);
+
+  _crypto_xkem_enc_derand_jazz(ciphertext, shared_secret, public_key, stack_coins);
+
+  ?{}, r = #set0();
+  return r;
+}
+
+export fn jade_kem_xwing_amd64_avx2_enc(reg u64 ciphertext shared_secret public_key) -> reg u64
+{
+  reg u64 r;
+  stack u8[XWING_ENCCOINBYTES] stack_coins;
+
+  _ = #init_msf();
+
+  ciphertext = ciphertext;
+  shared_secret = shared_secret;
+  public_key = public_key;
+  stack_coins = #randombytes(stack_coins);
+
+  _crypto_xkem_enc_derand_jazz(ciphertext, shared_secret, public_key, stack_coins);
+
+  ?{}, r = #set0();
+  return r;
+}
+
+export fn jade_kem_xwing_amd64_avx2_dec(reg u64 shared_secret ciphertext secret_key) -> reg u64
+{
+  reg u64 r;
+
+  _ = #init_msf();
+
+  shared_secret = shared_secret;
+  ciphertext = ciphertext;
+  secret_key = secret_key;
+
+  _crypto_xkem_dec_jazz(shared_secret, ciphertext, secret_key);
+
+  ?{}, r = #set0();
+  return r;
+}
+
diff --git a/src/crypto_kem/xwing/amd64/ref/Makefile b/src/crypto_kem/xwing/amd64/ref/Makefile
new file mode 100644
index 00000000..578d38fd
--- /dev/null
+++ b/src/crypto_kem/xwing/amd64/ref/Makefile
@@ -0,0 +1,3 @@
+SAFETY_FLAGS := -nocheckalignment
+SRCS := kem.jazz
+include ../../../../Makefile.common
\ No newline at end of file
diff --git a/src/crypto_kem/xwing/amd64/ref/include/api.h b/src/crypto_kem/xwing/amd64/ref/include/api.h
new file mode 100644
index 00000000..073ed620
--- /dev/null
+++ b/src/crypto_kem/xwing/amd64/ref/include/api.h
@@ -0,0 +1,47 @@
+#ifndef JADE_KEM_xwing_amd64_ref_API_H
+#define JADE_KEM_xwing_amd64_ref_API_H
+
+#include <stdint.h>
+
+#define JADE_KEM_xwing_amd64_ref_PUBLICKEYBYTES   1216
+#define JADE_KEM_xwing_amd64_ref_SECRETKEYBYTES   2464
+#define JADE_KEM_xwing_amd64_ref_CIPHERTEXTBYTES  1120
+#define JADE_KEM_xwing_amd64_ref_KEYPAIRCOINBYTES 96
+#define JADE_KEM_xwing_amd64_ref_ENCCOINBYTES     64
+#define JADE_KEM_xwing_amd64_ref_BYTES            32
+
+#define JADE_KEM_xwing_amd64_ref_ALGNAME         "X-Wing"
+#define JADE_KEM_xwing_amd64_ref_ARCH            "amd64"
+#define JADE_KEM_xwing_amd64_ref_IMPL            "ref"
+
+int jade_kem_xwing_amd64_ref_keypair_derand(
+  uint8_t *public_key,
+  uint8_t *secret_key,
+  const uint8_t *coins
+);
+
+int jade_kem_xwing_amd64_ref_keypair(
+  uint8_t *public_key,
+  uint8_t *secret_key
+);
+
+int jade_kem_xwing_amd64_ref_enc_derand(
+  uint8_t *ciphertext,
+  uint8_t *shared_secret,
+  const uint8_t *public_key,
+  const uint8_t *coins
+);
+
+int jade_kem_xwing_amd64_ref_enc(
+  uint8_t *ciphertext,
+  uint8_t *shared_secret,
+  const uint8_t *public_key
+);
+
+int jade_kem_xwing_amd64_ref_dec(
+  uint8_t *shared_secret,
+  const uint8_t *ciphertext,
+  const uint8_t *secret_key
+);
+
+#endif
diff --git a/src/crypto_kem/xwing/amd64/ref/kem.jazz b/src/crypto_kem/xwing/amd64/ref/kem.jazz
new file mode 100644
index 00000000..34d81363
--- /dev/null
+++ b/src/crypto_kem/xwing/amd64/ref/kem.jazz
@@ -0,0 +1,92 @@
+from Jade require "common/tofromstack.jinc"
+
+from Jade require "crypto_kem/mlkem/mlkem768/amd64/ref/kem.jinc"
+require "kem.jinc"
+require "params.jinc"
+
+export fn jade_kem_xwing_amd64_ref_keypair_derand(reg u64 public_key secret_key coins) -> reg u64
+{
+  reg u64 r;
+  stack u8[XWING_KEYPAIRCOINBYTES] stack_coins;
+
+  _ = #init_msf();
+
+  public_key = public_key;
+  secret_key = secret_key;
+  stack_coins = __tostack96u8(stack_coins, coins);
+
+  _crypto_xkem_keypair_derand_jazz(public_key, secret_key, stack_coins);
+
+  ?{}, r = #set0();
+  return r;
+}
+
+export fn jade_kem_xwing_amd64_ref_keypair(reg u64 public_key secret_key) -> reg u64
+{
+  reg u64 r;
+  stack u8[XWING_KEYPAIRCOINBYTES] stack_coins;
+
+  _ = #init_msf();
+
+  public_key = public_key;
+  secret_key = secret_key;
+  stack_coins = #randombytes(stack_coins);
+
+  _crypto_xkem_keypair_derand_jazz(public_key, secret_key, stack_coins);
+
+  ?{}, r = #set0();
+  return r;
+}
+
+export fn jade_kem_xwing_amd64_ref_enc_derand(reg u64 ciphertext shared_secret public_key coins) -> reg u64
+{
+  reg u64 r;
+  stack u8[XWING_ENCCOINBYTES] stack_coins;
+
+  _ = #init_msf();
+
+  ciphertext = ciphertext;
+  shared_secret = shared_secret;
+  public_key = public_key;
+  stack_coins = __tostack64u8(stack_coins, coins);
+
+  _crypto_xkem_enc_derand_jazz(ciphertext, shared_secret, public_key, stack_coins);
+
+  ?{}, r = #set0();
+  return r;
+}
+
+export fn jade_kem_xwing_amd64_ref_enc(reg u64 ciphertext shared_secret public_key) -> reg u64
+{
+  reg u64 r;
+  stack u8[XWING_ENCCOINBYTES] stack_coins;
+
+  _ = #init_msf();
+
+  ciphertext = ciphertext;
+  shared_secret = shared_secret;
+  public_key = public_key;
+  stack_coins = #randombytes(stack_coins);
+
+  _crypto_xkem_enc_derand_jazz(ciphertext, shared_secret, public_key, stack_coins);
+
+  ?{}, r = #set0();
+  return r;
+}
+
+export fn jade_kem_xwing_amd64_ref_dec(reg u64 shared_secret ciphertext secret_key) -> reg u64
+{
+  reg u64 r;
+
+  _ = #init_msf();
+
+  shared_secret = shared_secret;
+  ciphertext = ciphertext;
+  secret_key = secret_key;
+
+  _crypto_xkem_dec_jazz(shared_secret, ciphertext, secret_key);
+
+  ?{}, r = #set0();
+  return r;
+}
+
diff --git a/src/crypto_kem/xwing/amd64/ref/kem.jinc b/src/crypto_kem/xwing/amd64/ref/kem.jinc
new file mode 100644
index 00000000..409e35da
--- /dev/null
+++ b/src/crypto_kem/xwing/amd64/ref/kem.jinc
@@ -0,0 +1,133 @@
+// paper: https://eprint.iacr.org/2024/039.pdf
+// note: the require from mlkem768 is missing on purpose
+
+require "params.jinc"
+require "scalarmult.jinc"
+require "sha3.jinc"
+
+// sct: at this level there are no more #mmx register to spend
+//      as such, after unspill, an init_msf (lfence) is needed
+//      to "promote" transient variables to public; in this
+//      particular case, there is no advantage in patching the
+//      implementations to preserve the misspeculation register.
+//      Some performance data next.
+//
+// - cpu cycles of the following code without lfences, 11700K:
+//   keypair       , 345740
+//   keypair_derand, 343532
+//   enc           , 518594
+//   enc_derand    , 516238
+//   dec           , 462404
+//
+// - and with the lfences, 11700K:
+//   keypair       , 345744
+//   keypair_derand, 343496
+//   enc           , 518260
+//   enc_derand    , 515878
+//   dec           , 462904
+//
+// So, minus the usual noise, its pretty much the same
+
+
+// note: 
+// - (MLKEM_SYMBYTES*2) was copy pasted from params.jinc file from mlkem768 implementation
+// - for simplicity and efficiency of the last for loop, 32 is hardcoded: if the caller of
+//   of this function provides something different from (MLKEM_SYMBYTES*2) + 32 then 
+//   then the compilation should fail.
+
+fn _crypto_xkem_keypair_derand_jazz(reg u64 pkp skp, reg ptr u8[(MLKEM_SYMBYTES*2) + 32] randomness)
+{
+  inline int i;
+  reg u64 pk2;
+  reg ptr u8[32] sk2;
+
+  // spill all
+  () = #spill(pkp, skp, randomness);
+
+  // (sk1, pk1) <- KEM.KeyGen() // skp, pkp <- KEM.KeyGen(randomness[0:64])
+  __crypto_kem_keypair_jazz(pkp, skp, randomness[0:(MLKEM_SYMBYTES*2)]);
+
+  // sk2 <-$ // randomness[64:32]
+  // pk2 <- exp(G, sk2)
+    ()  = #unspill(pkp, randomness); _ = #init_msf();
+    pk2 = #LEA(pkp + MLKEM_PUBLICKEYBYTES);
+  xwing_x25519_base_p_rp(pk2, randomness[(MLKEM_SYMBYTES*2):32]);
+
+  // pk <- (pk1, pk2)
+  // done.
+
+  // sk <- (sk1, sk2, pk2)
+    ()  = #unspill(pkp, skp, randomness); _ = #init_msf();
+    sk2 = randomness[(MLKEM_SYMBYTES*2):32];
+    pk2 = #LEA(pkp + MLKEM_PUBLICKEYBYTES);
+
+  for i=0 to 4 // assumes: sk2 with 32 bytes; pk2 with 32 bytes
+  { (u64)[skp + MLKEM_SECRETKEYBYTES + i*8] = sk2[u64 i];
+    (u64)[skp + MLKEM_SECRETKEYBYTES + 32 + i*8] = (u64)[pk2 + i*8];
+  }
+}
+
+
+fn _crypto_xkem_enc_derand_jazz(reg u64 ctp shkp pkp, reg ptr u8[MLKEM_SYMBYTES + 32] randomness)
+{
+  reg u64 k k1 c2 pk2;
+  reg ptr u8[32] ske;
+  stack u8[32] k2;
+
+  // spill all
+  () = #spill(pkp, ctp, shkp, randomness);
+
+  // k1, c1 <- KEM.Enc(pk1) // shkp+0 (as aux), ctp+0 <- KEM.Enc(pkp+0, randomness[0:32])
+  __crypto_kem_enc_jazz(ctp, shkp, pkp, randomness[0:32]);
+
+  // ske <-$ // randomness[32:32]
+  // c2 <- exp(G, ske) // ctp+MLKEM_CIPHERTEXTBYTES <- exp(G, randomness[32:32])
+    ()  = #unspill(ctp, randomness); _ = #init_msf();
+    c2  = #LEA(ctp + MLKEM_CIPHERTEXTBYTES);
+    ske = randomness[MLKEM_SYMBYTES:32];
+  xwing_x25519_base_p_rp(c2, ske);
+
+  // k2 <- exp(pk2, ske) // k2 <- exp(pkp + MLKEM_PUBLICKEYBYTES, randomness[32:32])
+    ()  = #unspill(randomness, pkp); _ = #init_msf();
+    ske = randomness[MLKEM_SYMBYTES:32];
+    pk2 = #LEA(pkp + MLKEM_PUBLICKEYBYTES);
+  k2 = xwing_x25519_rp_rp_p(k2, ske, pk2);
+
+  // k <- H(label || k1 || k2 || c2 || pk2)
+    ()   = #unspill(shkp, ctp, pkp); _ = #init_msf();
+     k   = shkp;
+     k1  = shkp;
+     c2  = #LEA(ctp + MLKEM_CIPHERTEXTBYTES);
+     pk2 = #LEA(pkp + MLKEM_PUBLICKEYBYTES);
+  _xwing_sha3(k, k1, k2, c2, pk2);
+}
+
+
+fn _crypto_xkem_dec_jazz(reg u64 shkp ctp skp)
+{
+  reg u64 k k1 c2 sk2 pk2;
+  stack u8[32] k2;
+
+  // spill all
+  () = #spill(shkp, ctp, skp);
+
+  // (sk1, sk2, pk2) <- sk
+  // (c1, c2) <- c
+  // k1 <- KEM.Dec(c1, sk1) // shkp+0 (as aux) <- KEM.Dec(ctp, skp)
+  __crypto_kem_dec_jazz(shkp, ctp, skp);
+
+  // k2 <- exp(c2, sk2) // k2 <- exp(ctp + MLKEM_CIPHERTEXTBYTES, skp + MLKEM_SECRETKEYBYTES);
+    () = #unspill(skp, ctp); _ = #init_msf();
+    sk2 = #LEA(skp + MLKEM_SECRETKEYBYTES);
+    c2  = #LEA(ctp + MLKEM_CIPHERTEXTBYTES);
+  k2 = xwing_x25519_rp_p_p(k2, sk2, c2);
+
+  // k <- H(label || k1 || k2 || c2 || pk2)
+    ()  = #unspill(shkp, ctp, skp); _ = #init_msf();
+    k   = shkp;
+    k1  = shkp;
+    c2  = #LEA(ctp + MLKEM_CIPHERTEXTBYTES);
+    pk2 = #LEA(skp + MLKEM_SECRETKEYBYTES + 32);
+  _xwing_sha3(k, k1, k2, c2, pk2);
+}
+
diff --git a/src/crypto_kem/xwing/amd64/ref/params.jinc b/src/crypto_kem/xwing/amd64/ref/params.jinc
new file mode 100644
index 00000000..d45117a3
--- /dev/null
+++ b/src/crypto_kem/xwing/amd64/ref/params.jinc
@@ -0,0 +1,9 @@
+u8[6] XWING_LABEL = {0x5c,0x2e,0x2f,0x2f,0x5e,0x5c};
+
+param int XWING_PUBLICKEYBYTES   = MLKEM_PUBLICKEYBYTES  + 32;
+param int XWING_SECRETKEYBYTES   = MLKEM_SECRETKEYBYTES  + 64;
+param int XWING_CIPHERTEXTBYTES  = MLKEM_CIPHERTEXTBYTES + 32;
+param int XWING_KEYPAIRCOINBYTES = MLKEM_SYMBYTES*2      + 32;
+param int XWING_ENCCOINBYTES     = MLKEM_SYMBYTES        + 32;
+param int XWING_BYTES            = 32;
+
diff --git a/src/crypto_kem/xwing/amd64/ref/scalarmult.jinc b/src/crypto_kem/xwing/amd64/ref/scalarmult.jinc
new file mode 100644
index 00000000..98a12c78
--- /dev/null
+++ b/src/crypto_kem/xwing/amd64/ref/scalarmult.jinc
@@ -0,0 +1,50 @@
+from Jade require "crypto_scalarmult/curve25519/amd64/ref4/curve25519.jinc"
+
+fn xwing_x25519_base_p_rp(#spill_to_mmx reg u64 qp, reg ptr u8[32] _n)
+{
+  reg u64[4] q n;
+  inline int i;
+
+  () = #spill(qp);
+  for i=0 to 4 { n[i] = _n[u64 i]; }
+
+  q = _curve25519_ref4_base(n); // q = nG
+
+  () = #unspill(qp);
+  __store4(qp, q);
+}
+
+fn xwing_x25519_rp_rp_p(#spill_to_mmx reg ptr u8[32] _q, reg ptr u8[32] _n, reg u64 pp) -> reg ptr u8[32]
+{
+  reg u64[4] q n p;
+  inline int i;
+
+  () = #spill(_q);
+  for i=0 to 4 { n[i] = _n[u64 i]; }
+  for i=0 to 4 { p[i] = (u64)[pp + 8*i]; }
+
+  q = _curve25519_ref4(n, p); // q = nP
+
+  () = #unspill(_q);
+  for i=0 to 4 { _q[u64 i] = q[i]; }
+
+  return _q;
+}
+
+fn xwing_x25519_rp_p_p(#spill_to_mmx reg ptr u8[32] _q, reg u64 np, reg u64 pp) -> reg ptr u8[32]
+{
+  reg u64[4] q n p;
+  inline int i;
+
+  () = #spill(_q);
+  for i=0 to 4 { n[i] = (u64)[np + 8*i]; }
+  for i=0 to 4 { p[i] = (u64)[pp + 8*i]; }
+
+  q = _curve25519_ref4(n, p); // q = nP
+
+  () = #unspill(_q);
+  for i=0 to 4 { _q[u64 i] = q[i]; }
+
+  return _q;
+}
+
diff --git a/src/crypto_kem/xwing/amd64/ref/sha3.jinc b/src/crypto_kem/xwing/amd64/ref/sha3.jinc
new file mode 100644
index 00000000..5e3ea21e
--- /dev/null
+++ b/src/crypto_kem/xwing/amd64/ref/sha3.jinc
@@ -0,0 +1,44 @@
+
+fn _xwing_sha3(
+  #spill_to_mmx
+  reg u64 k,         // writes: 32 bytes
+  reg u64 k1,        // reads:  32 bytes
+  reg ptr u8[32] k2, // reads:  32 bytes
+  reg u64 c2,        // reads:  32 bytes
+  reg u64 pk2)       // reads:  32 bytes
+{
+  stack u64[25] state;
+  inline int i;
+
+  () = #spill(k);
+
+  // copy label
+  for i=0 to 6
+  { state[u8 i] = XWING_LABEL[i]; }
+
+  // copy k1, k2, c2, pk2
+  for i=0 to 4
+  { state.[6 + 0  + i*8] = (u64)[k1 + i*8];
+    state.[6 + 32 + i*8] = k2[u64 i];
+    state.[6 + 64 + i*8] = (u64)[c2 + i*8];
+    state.[6 + 96 + i*8] = (u64)[pk2 + i*8];
+  }
+  // 6 + 96 + 3*8 = 126 (and +8 byte write, 134)
+
+  // zero the remaining state
+  state.[u16 134] = 0;
+  for i=17 to 25
+  { state[i] = 0; }
+
+  state[u8 134] ^= 0x06;
+  state[u8 SHA3_256_RATE - 1] = 0x80;
+
+  // it uses the same keccakf1600 as mlkem768
+  state = _keccakf1600_(state);
+
+  () = #unspill(k);
+
+  for i=0 to 4
+  { (u64)[k + 8*i] = state[i]; }
+}
+
diff --git a/src/crypto_scalarmult/curve25519/amd64/ref4/curve25519.jinc b/src/crypto_scalarmult/curve25519/amd64/ref4/curve25519.jinc
index 38ddbb8a..abc13cd7 100644
--- a/src/crypto_scalarmult/curve25519/amd64/ref4/curve25519.jinc
+++ b/src/crypto_scalarmult/curve25519/amd64/ref4/curve25519.jinc
@@ -1,5 +1,6 @@
 from Jade require "crypto_scalarmult/curve25519/amd64/common/bit.jinc"
 from Jade require "crypto_scalarmult/curve25519/amd64/common/decode_scalar.jinc"
+from Jade require "crypto_scalarmult/curve25519/amd64/common/load_store4.jinc"
 
 from Jade require "crypto_scalarmult/curve25519/amd64/common/64/decode_u4.jinc"
 from Jade require "crypto_scalarmult/curve25519/amd64/common/64/init_points4.jinc"
@@ -143,7 +144,7 @@ inline fn __curve25519_internal_ref4(stack u8[32] k, reg u64[4] u) -> reg u64[4]
   return r;
 }
 
-inline fn __curve25519_ref4(reg u64[4] _k _u) -> reg u64[4]
+fn _curve25519_ref4(reg u64[4] _k _u) -> reg u64[4]
 {
   stack u8[32] k;
   reg u64[4] u r;
@@ -155,7 +156,23 @@ inline fn __curve25519_ref4(reg u64[4] _k _u) -> reg u64[4]
   return r;
 }
 
-inline fn __curve25519_ref4_base(reg u64[4] _k) -> reg u64[4]
+inline fn __curve25519_ref4_ptr(#spill_to_mmx reg u64 rp, reg u64 kp up)
+{
+  reg u64[4] r k u;
+
+  ()  = #spill(rp);
+
+  k = __load4(kp);
+  u = __load4(up);
+  r = _curve25519_ref4(k, u);
+
+  ()  = #unspill(rp);
+
+  __store4(rp, r);
+}
+
+
+fn _curve25519_ref4_base(reg u64[4] _k) -> reg u64[4]
 {
   stack u8[32] k;
   reg u64[4] u r;
@@ -167,3 +184,17 @@ inline fn __curve25519_ref4_base(reg u64[4] _k) -> reg u64[4]
   return r;
 }
 
+inline fn __curve25519_ref4_base_ptr(#spill_to_mmx reg u64 rp, reg u64 kp)
+{
+  reg u64[4] r k;
+
+  () = #spill(rp);
+
+  k = __load4(kp);
+  r = _curve25519_ref4_base(k);
+
+  ()  = #unspill(rp);
+
+  __store4(rp, r);
+}
+
diff --git a/src/crypto_scalarmult/curve25519/amd64/ref4/scalarmult.jazz b/src/crypto_scalarmult/curve25519/amd64/ref4/scalarmult.jazz
index 70e3a1f9..261848dd 100644
--- a/src/crypto_scalarmult/curve25519/amd64/ref4/scalarmult.jazz
+++ b/src/crypto_scalarmult/curve25519/amd64/ref4/scalarmult.jazz
@@ -4,18 +4,10 @@ require "curve25519.jinc"
 export fn jade_scalarmult_curve25519_amd64_ref4(#spill_to_mmx reg u64 qp np pp) -> reg u64
 {
   reg u64 r;
-  reg u64[4] q n p;
 
   _ = #init_msf();
 
-  ()  = #spill(qp);
-  n   = __load4(np);
-  p   = __load4(pp);
-
-  q = __curve25519_ref4(n, p);
-
-  ()  = #unspill(qp);
-  __store4(qp, q);
+  __curve25519_ref4_ptr(qp, np, pp);
 
   ?{}, r = #set0();
   return r;
@@ -24,17 +16,10 @@ export fn jade_scalarmult_curve25519_amd64_ref4(#spill_to_mmx reg u64 qp np pp)
 export fn jade_scalarmult_curve25519_amd64_ref4_base(#spill_to_mmx reg u64 qp np) -> reg u64
 {
   reg u64 r;
-  reg u64[4] q n;
 
   _ = #init_msf();
 
-  ()  = #spill(qp);
-  n   = __load4(np);
-
-  q = __curve25519_ref4_base(n);
-
-  ()  = #unspill(qp);
-  __store4(qp, q);
+  __curve25519_ref4_base_ptr(qp, np);
 
   ?{}, r = #set0();
   return r;
diff --git a/submodules/crypto-specs b/submodules/crypto-specs
index c07ff650..a91aef66 160000
--- a/submodules/crypto-specs
+++ b/submodules/crypto-specs
@@ -1 +1 @@
-Subproject commit c07ff6501d73e2e2ed64e8017ace31b637b5b2f2
+Subproject commit a91aef66f94ee722888e109771b5713f0056f9fe