diff --git a/Cargo.lock b/Cargo.lock
index e4c5835..558963b 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -282,6 +282,17 @@ dependencies = [
  "arbitrary",
 ]
 
+[[package]]
+name = "core-models"
+version = "0.0.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "657f625ff361906f779745d08375ae3cc9fef87a35fba5f22874cf773010daf4"
+dependencies = [
+ "hax-lib",
+ "pastey",
+ "rand 0.9.4",
+]
+
 [[package]]
 name = "core2"
 version = "0.4.0"
@@ -317,8 +328,8 @@ dependencies = [
  "p256",
  "p384",
  "pkcs8",
- "rand_chacha",
- "rand_core",
+ "rand_chacha 0.3.1",
+ "rand_core 0.6.4",
  "rsa",
  "sha1",
  "sha2",
@@ -331,6 +342,15 @@ dependencies = [
  "zeroize",
 ]
 
+[[package]]
+name = "cosmian_libcrux_provider"
+version = "1.0.0"
+dependencies = [
+ "cosmian_crypto_core",
+ "libcrux-ml-kem",
+ "zeroize",
+]
+
 [[package]]
 name = "cosmian_openssl_provider"
 version = "1.0.0"
@@ -449,7 +469,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0dc92fb57ca44df6db8059111ab3af99a63d5d0f8375d9972e319a379c6bab76"
 dependencies = [
  "generic-array",
- "rand_core",
+ "rand_core 0.6.4",
  "subtle",
  "zeroize",
 ]
@@ -461,7 +481,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "78c8292055d1c1df0cce5d180393dc8cce0abec0a7102adb6c7b1eef6016d60a"
 dependencies = [
  "generic-array",
- "rand_core",
+ "rand_core 0.6.4",
  "typenum",
 ]
 
@@ -515,7 +535,7 @@ dependencies = [
  "curve25519-dalek-derive",
  "digest",
  "fiat-crypto",
- "rand_core",
+ "rand_core 0.6.4",
  "rustc_version",
  "subtle",
  "zeroize",
@@ -645,7 +665,7 @@ dependencies = [
  "hkdf",
  "pem-rfc7468",
  "pkcs8",
- "rand_core",
+ "rand_core 0.6.4",
  "sec1",
  "subtle",
  "zeroize",
@@ -679,7 +699,7 @@ version = "0.13.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "c0b50bfb653653f9ca9095b427bed08ab8d75a137839d9ad64eb11810d5b6393"
 dependencies = [
- "rand_core",
+ "rand_core 0.6.4",
  "subtle",
 ]
 
@@ -809,7 +829,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f0f9ef7462f7c099f518d754361858f86d8a07af53ba9af0fe635bbccb151a63"
 dependencies = [
  "ff",
- "rand_core",
+ "rand_core 0.6.4",
  "subtle",
 ]
 
@@ -835,6 +855,43 @@ dependencies = [
  "foldhash",
 ]
 
+[[package]]
+name = "hax-lib"
+version = "0.3.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "543f93241d32b3f00569201bfce9d7a93c92c6421b23c77864ac929dc947b9fc"
+dependencies = [
+ "hax-lib-macros",
+ "num-bigint",
+ "num-traits",
+]
+
+[[package]]
+name = "hax-lib-macros"
+version = "0.3.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f8755751e760b11021765bb04cb4a6c4e24742688d9f3aa14c2079638f537b0f"
+dependencies = [
+ "hax-lib-macros-types",
+ "proc-macro-error2",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
+[[package]]
+name = "hax-lib-macros-types"
+version = "0.3.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f177c9ae8ea456e2f71ff3c1ea47bf4464f772a05133fcbba56cd5ba169035a2"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "serde",
+ "serde_json",
+ "uuid",
+]
+
 [[package]]
 name = "hkdf"
 version = "0.12.4"
@@ -953,6 +1010,72 @@ version = "0.2.180"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "bcc35a38544a891a5f7c865aca548a982ccb3b8650a5b06d0fd33a10283c56fc"
 
+[[package]]
+name = "libcrux-intrinsics"
+version = "0.0.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0aa4779454e853d1de200cd12f19a8185aac47d99a5ec404cea3295c943d48f1"
+dependencies = [
+ "core-models",
+ "hax-lib",
+]
+
+[[package]]
+name = "libcrux-ml-kem"
+version = "0.0.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a930ff130a63e9d89648d0e22203ca034995191cbfa606b9f3c151ba67306963"
+dependencies = [
+ "hax-lib",
+ "libcrux-intrinsics",
+ "libcrux-platform",
+ "libcrux-secrets",
+ "libcrux-sha3",
+ "libcrux-traits",
+ "rand 0.9.4",
+ "tls_codec",
+]
+
+[[package]]
+name = "libcrux-platform"
+version = "0.0.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1d9e21d7ed31a92ac539bd69a8c970b183ee883872d2d19ce27036e24cb8ecc4"
+dependencies = [
+ "libc",
+]
+
+[[package]]
+name = "libcrux-secrets"
+version = "0.0.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1ce650f3041b44ba40d4263852347d007cd2cd9d1cc856a6f6c8b2e10c3fd40b"
+dependencies = [
+ "hax-lib",
+]
+
+[[package]]
+name = "libcrux-sha3"
+version = "0.0.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e3dabce2795479bd7294f853f7966a678cadf7a26d3d29f61cf15f5123e7ba4f"
+dependencies = [
+ "hax-lib",
+ "libcrux-intrinsics",
+ "libcrux-platform",
+ "libcrux-traits",
+]
+
+[[package]]
+name = "libcrux-traits"
+version = "0.0.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "695ff2fb97627e4d57315a2fdfbfe50df1c80c6ef7d91ba34216169bd6f41c00"
+dependencies = [
+ "libcrux-secrets",
+ "rand 0.9.4",
+]
+
 [[package]]
 name = "libflate"
 version = "2.2.1"
@@ -1045,6 +1168,16 @@ dependencies = [
  "simd-adler32",
 ]
 
+[[package]]
+name = "num-bigint"
+version = "0.4.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a5e44f723f1133c9deac646763579fdb3ac745e418f2a7af9cd0c431da1f20b9"
+dependencies = [
+ "num-integer",
+ "num-traits",
+]
+
 [[package]]
 name = "num-bigint-dig"
 version = "0.8.6"
@@ -1056,7 +1189,7 @@ dependencies = [
  "num-integer",
  "num-iter",
  "num-traits",
- "rand",
+ "rand 0.8.5",
  "smallvec",
  "zeroize",
 ]
@@ -1195,6 +1328,12 @@ dependencies = [
  "sha2",
 ]
 
+[[package]]
+name = "pastey"
+version = "0.2.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2ee67f1008b1ba2321834326597b8e186293b049a023cdef258527550b9935b4"
+
 [[package]]
 name = "pbkdf2"
 version = "0.12.2"
@@ -1254,7 +1393,7 @@ checksum = "f950b2377845cebe5cf8b5165cb3cc1a5e0fa5cfa3e1f7f55707d8fd82e0a7b7"
 dependencies = [
  "der",
  "pkcs5",
- "rand_core",
+ "rand_core 0.6.4",
  "spki",
 ]
 
@@ -1333,6 +1472,28 @@ dependencies = [
  "elliptic-curve",
 ]
 
+[[package]]
+name = "proc-macro-error-attr2"
+version = "2.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "96de42df36bb9bba5542fe9f1a054b8cc87e172759a1868aa05c1f3acc89dfc5"
+dependencies = [
+ "proc-macro2",
+ "quote",
+]
+
+[[package]]
+name = "proc-macro-error2"
+version = "2.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "11ec05c52be0a07b08061f7dd003e7d7092e0472bc731b4af7bb1ef876109802"
+dependencies = [
+ "proc-macro-error-attr2",
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
 [[package]]
 name = "proc-macro2"
 version = "1.0.106"
@@ -1363,8 +1524,18 @@ version = "0.8.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404"
 dependencies = [
- "rand_chacha",
- "rand_core",
+ "rand_chacha 0.3.1",
+ "rand_core 0.6.4",
+]
+
+[[package]]
+name = "rand"
+version = "0.9.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "44c5af06bb1b7d3216d91932aed5265164bf384dc89cd6ba05cf59a35f5f76ea"
+dependencies = [
+ "rand_chacha 0.9.0",
+ "rand_core 0.9.5",
 ]
 
 [[package]]
@@ -1374,7 +1545,17 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88"
 dependencies = [
  "ppv-lite86",
- "rand_core",
+ "rand_core 0.6.4",
+]
+
+[[package]]
+name = "rand_chacha"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb"
+dependencies = [
+ "ppv-lite86",
+ "rand_core 0.9.5",
 ]
 
 [[package]]
@@ -1386,6 +1567,15 @@ dependencies = [
  "getrandom 0.2.17",
 ]
 
+[[package]]
+name = "rand_core"
+version = "0.9.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "76afc826de14238e6e8c374ddcc1fa19e374fd8dd986b0d2af0d02377261d83c"
+dependencies = [
+ "getrandom 0.3.4",
+]
+
 [[package]]
 name = "rayon"
 version = "1.11.0"
@@ -1473,7 +1663,7 @@ dependencies = [
  "num-traits",
  "pkcs1",
  "pkcs8",
- "rand_core",
+ "rand_core 0.6.4",
  "signature",
  "spki",
  "subtle",
@@ -1645,7 +1835,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "77549399552de45a898a580c1b41d445bf730df867cc44e6c0233bbc4b8329de"
 dependencies = [
  "digest",
- "rand_core",
+ "rand_core 0.6.4",
 ]
 
 [[package]]
diff --git a/Cargo.toml b/Cargo.toml
index a0aef35..07afa9b 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,9 +1,10 @@
 [workspace]
 members = [
   "crates/core",
+  "crates/libcrux",
   "crates/openssl_provider",
   "crates/rust_nist_ec",
-  "crates/rust_curve25519"
+  "crates/rust_curve25519",
 ]
 resolver = "2"
 
diff --git a/crates/libcrux/Cargo.toml b/crates/libcrux/Cargo.toml
new file mode 100644
index 0000000..6c7eeff
--- /dev/null
+++ b/crates/libcrux/Cargo.toml
@@ -0,0 +1,24 @@
+[package]
+name = "cosmian_libcrux_provider"
+version = "1.0.0"
+description = "Verified, pure-Rust provider."
+
+authors = { workspace = true }
+categories = { workspace = true }
+edition = { workspace = true }
+keywords = { workspace = true }
+license = { workspace = true }
+repository = { workspace = true }
+
+[lib]
+crate-type = ["lib", "staticlib"]
+name = "cosmian_libcrux_provider"
+path = "src/lib.rs"
+
+[dependencies]
+cosmian_crypto_core = { path = "../core", version = "11", default-features = false }
+libcrux-ml-kem = { version = "0.0.6" }
+zeroize = { workspace = true }
+
+[dev-dependencies]
+cosmian_crypto_core = { path = "../core", version = "11", default-features = false, features = ["sha3"] }
diff --git a/crates/libcrux/src/lib.rs b/crates/libcrux/src/lib.rs
new file mode 100644
index 0000000..3275da1
--- /dev/null
+++ b/crates/libcrux/src/lib.rs
@@ -0,0 +1,2 @@
+pub mod mlkem;
+// mod r25519;
diff --git a/crates/libcrux/src/mlkem.rs b/crates/libcrux/src/mlkem.rs
new file mode 100644
index 0000000..25eaee1
--- /dev/null
+++ b/crates/libcrux/src/mlkem.rs
@@ -0,0 +1,183 @@
+macro_rules! make_mlkem {
+    ($module:tt, $mlkem:ident,
+     ($enc:ident, $ctx:ident, $enc_size:tt),
+     ($ek:ident, $pk:ident, $ek_size:tt),
+     ($dk:ident, $sk:ident, $dk_size:tt)) => {
+        pub mod $module {
+
+            use core::ops::IndexMut;
+            use std::pin::Pin;
+
+            use cosmian_crypto_core::{
+                bytes_ser_de::{Deserializer, Serializable, Serializer},
+                traits::KEM,
+                CryptoCoreError, Secret, SymmetricKey,
+            };
+            use libcrux_ml_kem::$module;
+            use zeroize::{Zeroize, ZeroizeOnDrop};
+
+            pub struct $enc($module::$ctx);
+
+            impl $enc {
+                pub const LENGTH: usize = $enc_size;
+            }
+
+            impl Serializable for $enc {
+                type Error = CryptoCoreError;
+
+                fn length(&self) -> usize {
+                    Self::LENGTH
+                }
+
+                fn write(&self, ser: &mut Serializer) -> Result<usize, Self::Error> {
+                    ser.write_array(self.0.as_slice())
+                }
+
+                fn read(de: &mut Deserializer) -> Result<Self, Self::Error> {
+                    Ok(Self(
+                        $module::$ctx::try_from(de.read_array::<{ Self::LENGTH }>()?).map_err(
+                            |e| CryptoCoreError::GenericDeserializationError(e.to_string()),
+                        )?,
+                    ))
+                }
+            }
+
+            pub struct $ek($module::$pk);
+
+            impl $ek {
+                pub const LENGTH: usize = $ek_size;
+            }
+
+            impl Serializable for $ek {
+                type Error = CryptoCoreError;
+
+                fn length(&self) -> usize {
+                    Self::LENGTH
+                }
+
+                fn write(&self, ser: &mut Serializer) -> Result<usize, Self::Error> {
+                    ser.write_array(self.0.as_slice())
+                }
+
+                fn read(de: &mut Deserializer) -> Result<Self, Self::Error> {
+                    Ok(Self(
+                        $module::$pk::try_from(de.read_array::<{ Self::LENGTH }>()?).map_err(
+                            |e| CryptoCoreError::GenericDeserializationError(e.to_string()),
+                        )?,
+                    ))
+                }
+            }
+
+            pub struct $dk(Pin<Box<$module::$sk>>);
+
+            impl $dk {
+                pub const LENGTH: usize = $dk_size;
+            }
+
+            impl Drop for $dk {
+                fn drop(&mut self) {
+                    self.0.index_mut(..Self::LENGTH).zeroize();
+                }
+            }
+
+            impl ZeroizeOnDrop for $dk {}
+
+            impl Serializable for $dk {
+                type Error = CryptoCoreError;
+
+                fn length(&self) -> usize {
+                    Self::LENGTH
+                }
+
+                fn write(&self, ser: &mut Serializer) -> Result<usize, Self::Error> {
+                    ser.write_array(self.0.as_slice())
+                }
+
+                fn read(de: &mut Deserializer) -> Result<Self, Self::Error> {
+                    let mut bytes = de.read_array::<{ Self::LENGTH }>()?;
+                    let dk = Self(Box::pin($module::$sk::try_from(&bytes).map_err(|e| {
+                        CryptoCoreError::GenericDeserializationError(e.to_string())
+                    })?));
+                    bytes.zeroize();
+                    Ok(dk)
+                }
+            }
+
+            pub struct $mlkem;
+
+            impl KEM<32> for $mlkem {
+                type Encapsulation = $enc;
+
+                type EncapsulationKey = $ek;
+
+                type DecapsulationKey = $dk;
+
+                type Error = CryptoCoreError;
+
+                fn keygen(
+                    rng: &mut impl cosmian_crypto_core::reexport::rand_core::CryptoRngCore,
+                ) -> Result<(Self::DecapsulationKey, Self::EncapsulationKey), Self::Error> {
+                    let mut randomness = [0; libcrux_ml_kem::KEY_GENERATION_SEED_SIZE];
+                    rng.fill_bytes(&mut randomness);
+                    let (dk, ek) = $module::generate_key_pair(randomness).into_parts();
+                    Ok(($dk(Box::pin(dk)), $ek(ek)))
+                }
+
+                fn enc(
+                    ek: &Self::EncapsulationKey,
+                    rng: &mut impl cosmian_crypto_core::reexport::rand_core::CryptoRngCore,
+                ) -> Result<(SymmetricKey<32>, Self::Encapsulation), Self::Error> {
+                    let mut randomness = [0; libcrux_ml_kem::SHARED_SECRET_SIZE];
+                    rng.fill_bytes(&mut randomness);
+                    let (enc, mut ss) = $module::encapsulate(&ek.0, randomness);
+                    Ok((Secret::from_unprotected_bytes(&mut ss).into(), $enc(enc)))
+                }
+
+                fn dec(
+                    dk: &Self::DecapsulationKey,
+                    enc: &Self::Encapsulation,
+                ) -> Result<cosmian_crypto_core::SymmetricKey<32>, Self::Error> {
+                    let mut ss = $module::decapsulate(&dk.0, &enc.0);
+                    Ok(Secret::from_unprotected_bytes(&mut ss).into())
+                }
+            }
+        }
+    };
+}
+
+make_mlkem!(
+    mlkem512,
+    MlKem512,
+    (MlKem512Encapsulation, MlKem512Ciphertext, 768),
+    (MlKem512EncapsulationKey, MlKem512PublicKey, 800),
+    (MlKem512DecapsulationKey, MlKem512PrivateKey, 1632)
+);
+
+make_mlkem!(
+    mlkem768,
+    MlKem768,
+    (MlKem768Encapsulation, MlKem768Ciphertext, 1088),
+    (MlKem768EncapsulationKey, MlKem768PublicKey, 1184),
+    (MlKem768DecapsulationKey, MlKem768PrivateKey, 2400)
+);
+
+make_mlkem!(
+    mlkem1024,
+    MlKem1024,
+    (MlKem1024Encapsulation, MlKem1024Ciphertext, 1568),
+    (MlKem1024EncapsulationKey, MlKem1024PublicKey, 1568),
+    (MlKem1024DecapsulationKey, MlKem1024PrivateKey, 3168)
+);
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use cosmian_crypto_core::traits::tests::test_kem;
+
+    #[test]
+    fn test_mlkem() {
+        test_kem::<32, mlkem512::MlKem512>();
+        test_kem::<32, mlkem768::MlKem768>();
+        test_kem::<32, mlkem1024::MlKem1024>();
+    }
+}