diff --git a/Cargo.lock b/Cargo.lock
index 78a064964..541c7a6b7 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -688,6 +688,14 @@ dependencies = [
  "subtle",
 ]
 
+[[package]]
+name = "hacl-rs"
+version = "0.1.0"
+source = "git+https://github.com/hacl-star/hacl-star.git?branch=afromher_rs#e83275b78cb4144254b2097fe36e6d2602f87cd7"
+dependencies = [
+ "krml",
+]
+
 [[package]]
 name = "half"
 version = "2.4.1"
@@ -701,7 +709,7 @@ dependencies = [
 [[package]]
 name = "hax-lib"
 version = "0.1.0-pre.1"
-source = "git+https://github.com/hacspec/hax/?branch=main#d6cc1888b7633df221e388823f9f9e5bebf42b9e"
+source = "git+https://github.com/hacspec/hax/?branch=main#cd6e258cb2fbc65b97901092b07bfdee02fe4808"
 dependencies = [
  "hax-lib-macros 0.1.0-pre.1 (git+https://github.com/hacspec/hax/?branch=main)",
  "num-bigint",
@@ -711,7 +719,7 @@ dependencies = [
 [[package]]
 name = "hax-lib"
 version = "0.1.0-pre.1"
-source = "git+https://github.com/hacspec/hax/#d6cc1888b7633df221e388823f9f9e5bebf42b9e"
+source = "git+https://github.com/hacspec/hax/#cd6e258cb2fbc65b97901092b07bfdee02fe4808"
 dependencies = [
  "hax-lib-macros 0.1.0-pre.1 (git+https://github.com/hacspec/hax/)",
  "num-bigint",
@@ -721,7 +729,7 @@ dependencies = [
 [[package]]
 name = "hax-lib-macros"
 version = "0.1.0-pre.1"
-source = "git+https://github.com/hacspec/hax/?branch=main#d6cc1888b7633df221e388823f9f9e5bebf42b9e"
+source = "git+https://github.com/hacspec/hax/?branch=main#cd6e258cb2fbc65b97901092b07bfdee02fe4808"
 dependencies = [
  "hax-lib-macros-types 0.1.0-pre.1 (git+https://github.com/hacspec/hax/?branch=main)",
  "proc-macro-error",
@@ -733,7 +741,7 @@ dependencies = [
 [[package]]
 name = "hax-lib-macros"
 version = "0.1.0-pre.1"
-source = "git+https://github.com/hacspec/hax/#d6cc1888b7633df221e388823f9f9e5bebf42b9e"
+source = "git+https://github.com/hacspec/hax/#cd6e258cb2fbc65b97901092b07bfdee02fe4808"
 dependencies = [
  "hax-lib-macros-types 0.1.0-pre.1 (git+https://github.com/hacspec/hax/)",
  "proc-macro-error",
@@ -745,7 +753,7 @@ dependencies = [
 [[package]]
 name = "hax-lib-macros-types"
 version = "0.1.0-pre.1"
-source = "git+https://github.com/hacspec/hax/?branch=main#d6cc1888b7633df221e388823f9f9e5bebf42b9e"
+source = "git+https://github.com/hacspec/hax/?branch=main#cd6e258cb2fbc65b97901092b07bfdee02fe4808"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -757,7 +765,7 @@ dependencies = [
 [[package]]
 name = "hax-lib-macros-types"
 version = "0.1.0-pre.1"
-source = "git+https://github.com/hacspec/hax/#d6cc1888b7633df221e388823f9f9e5bebf42b9e"
+source = "git+https://github.com/hacspec/hax/#cd6e258cb2fbc65b97901092b07bfdee02fe4808"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -897,6 +905,11 @@ dependencies = [
  "cpufeatures",
 ]
 
+[[package]]
+name = "krml"
+version = "0.1.0"
+source = "git+https://github.com/hacl-star/hacl-star.git?branch=afromher_rs#e83275b78cb4144254b2097fe36e6d2602f87cd7"
+
 [[package]]
 name = "lazy_static"
 version = "1.5.0"
@@ -958,6 +971,7 @@ dependencies = [
 name = "libcrux-ecdh"
 version = "0.0.2-alpha.3"
 dependencies = [
+ "hacl-rs",
  "hex",
  "libcrux-hacl",
  "pretty_env_logger",
diff --git a/libcrux-ecdh/Cargo.toml b/libcrux-ecdh/Cargo.toml
index a94d69e58..ac8df473c 100644
--- a/libcrux-ecdh/Cargo.toml
+++ b/libcrux-ecdh/Cargo.toml
@@ -15,6 +15,10 @@ path = "src/ecdh.rs"
 [dependencies]
 rand = { version = "0.8" }
 libcrux-hacl = { version = "=0.0.2-alpha.3", path = "../sys/hacl" }
+hacl-rs = { git = "https://github.com/hacl-star/hacl-star.git", branch = "afromher_rs", optional = true }
+
+[features]
+hacl-rs = ["dep:hacl-rs"]
 
 [dev-dependencies]
 rand_core = { version = "0.6" }
@@ -22,3 +26,4 @@ hex = { version = "0.4.3", features = ["serde"] }
 serde_json = { version = "1.0" }
 serde = { version = "1.0", features = ["derive"] }
 pretty_env_logger = "0.5"
+
diff --git a/libcrux-ecdh/src/hacl/curve25519.rs b/libcrux-ecdh/src/hacl/curve25519.rs
index 8ee631669..b19e98a14 100644
--- a/libcrux-ecdh/src/hacl/curve25519.rs
+++ b/libcrux-ecdh/src/hacl/curve25519.rs
@@ -1,3 +1,4 @@
+#[cfg(not(feature = "hacl-rs"))]
 use libcrux_hacl::{Hacl_Curve25519_51_ecdh, Hacl_Curve25519_51_secret_to_public};
 
 #[derive(Debug, PartialEq, Eq, Clone, Copy)]
@@ -14,6 +15,7 @@ pub fn ecdh(
     public_key: impl AsRef<[u8; 32]>,
 ) -> Result<[u8; 32], Error> {
     let mut shared = [0u8; 32];
+    #[cfg(not(feature = "hacl-rs"))]
     let ok = unsafe {
         Hacl_Curve25519_51_ecdh(
             shared.as_mut_ptr(),
@@ -21,6 +23,9 @@ pub fn ecdh(
             public_key.as_ref().as_ptr() as _,
         )
     };
+    #[cfg(feature = "hacl-rs")]
+    let ok =
+        hacl_rs::hacl::curve25519_51::ecdh(&mut shared, private_key.as_ref(), public_key.as_ref());
     if !ok {
         Err(Error::InvalidInput)
     } else {
@@ -32,13 +37,17 @@ pub fn ecdh(
 /// with the base point).
 ///
 /// Returns the 32 bytes shared key.
+
 #[must_use]
 #[inline(always)]
 pub fn secret_to_public(private_key: impl AsRef<[u8; 32]>) -> [u8; 32] {
     let mut public = [0u8; 32];
+    #[cfg(not(feature = "hacl-rs"))]
     unsafe {
         Hacl_Curve25519_51_secret_to_public(public.as_mut_ptr(), private_key.as_ref().as_ptr() as _)
     };
+    #[cfg(feature = "hacl-rs")]
+    hacl_rs::hacl::curve25519_51::secret_to_public(&mut public, private_key.as_ref());
     public
 }
 
diff --git a/libcrux-ecdh/src/hacl/p256.rs b/libcrux-ecdh/src/hacl/p256.rs
index f8cfe25e7..65d6f4667 100644
--- a/libcrux-ecdh/src/hacl/p256.rs
+++ b/libcrux-ecdh/src/hacl/p256.rs
@@ -1,3 +1,4 @@
+#[cfg(not(feature = "hacl-rs"))]
 use libcrux_hacl::{
     Hacl_P256_compressed_to_raw, Hacl_P256_dh_initiator, Hacl_P256_dh_responder,
     Hacl_P256_uncompressed_to_raw, Hacl_P256_validate_private_key, Hacl_P256_validate_public_key,
@@ -19,9 +20,13 @@ pub enum Error {
 pub fn uncompressed_to_coordinates(point: &[u8]) -> Result<[u8; 64], Error> {
     let mut concat_point = [0u8; 64];
     if point.len() >= 65 {
+        #[cfg(not(feature = "hacl-rs"))]
         let ok = unsafe {
             Hacl_P256_uncompressed_to_raw(point.as_ptr() as _, concat_point.as_mut_ptr())
         };
+
+        #[cfg(feature = "hacl-rs")]
+        let ok = hacl_rs::hacl::p256::uncompressed_to_raw(point, &mut concat_point);
         if ok {
             Ok(concat_point)
         } else {
@@ -37,8 +42,11 @@ pub fn uncompressed_to_coordinates(point: &[u8]) -> Result<[u8; 64], Error> {
 pub fn compressed_to_coordinates(point: &[u8]) -> Result<[u8; 64], Error> {
     let mut concat_point = [0u8; 64];
     if point.len() >= 33 {
+        #[cfg(not(feature = "hacl-rs"))]
         let ok =
             unsafe { Hacl_P256_compressed_to_raw(point.as_ptr() as _, concat_point.as_mut_ptr()) };
+        #[cfg(feature = "hacl-rs")]
+        let ok = hacl_rs::hacl::p256::compressed_to_raw(point, &mut concat_point);
         if ok {
             Ok(concat_point)
         } else {
@@ -54,7 +62,12 @@ pub fn compressed_to_coordinates(point: &[u8]) -> Result<[u8; 64], Error> {
 ///
 /// Returns [`Error::InvalidPoint`] if the `point` is not valid.
 pub fn validate_point(point: impl AsRef<[u8; 64]>) -> Result<(), Error> {
-    if unsafe { Hacl_P256_validate_public_key(point.as_ref().as_ptr() as _) } {
+    #[cfg(not(feature = "hacl-rs"))]
+    let valid_point = unsafe { Hacl_P256_validate_public_key(point.as_ref().as_ptr() as _) };
+    #[cfg(feature = "hacl-rs")]
+    let valid_point = hacl_rs::hacl::p256::validate_public_key(point.as_ref());
+
+    if valid_point {
         Ok(())
     } else {
         Err(Error::InvalidPoint)
@@ -75,9 +88,12 @@ pub fn validate_scalar_(scalar: &[u8; 32]) -> Result<(), Error> {
     if scalar.as_ref().iter().all(|b| *b == 0) {
         return Err(Error::InvalidScalar);
     }
-
+    #[cfg(not(feature = "hacl-rs"))]
+    let valid_scalar = unsafe { Hacl_P256_validate_private_key(scalar.as_ref().as_ptr() as _) };
+    #[cfg(feature = "hacl-rs")]
+    let valid_scalar = hacl_rs::hacl::p256::validate_private_key(scalar);
     // Ensure that the key is in range  [1, p-1]
-    if unsafe { Hacl_P256_validate_private_key(scalar.as_ref().as_ptr() as _) } {
+    if valid_scalar {
         Ok(())
     } else {
         Err(Error::InvalidScalar)
@@ -108,6 +124,7 @@ pub fn ecdh(
     public_key: impl AsRef<[u8; 64]>,
 ) -> Result<[u8; 64], Error> {
     let mut shared = [0u8; 64];
+    #[cfg(not(feature = "hacl-rs"))]
     let ok = unsafe {
         Hacl_P256_dh_responder(
             shared.as_mut_ptr(),
@@ -115,6 +132,10 @@ pub fn ecdh(
             private_key.as_ref().as_ptr() as _,
         )
     };
+    #[cfg(feature = "hacl-rs")]
+    let ok =
+        hacl_rs::hacl::p256::dh_responder(&mut shared, public_key.as_ref(), private_key.as_ref());
+
     if !ok {
         Err(Error::InvalidInput)
     } else {
@@ -129,7 +150,11 @@ pub fn secret_to_public(s: impl AsRef<[u8; 32]>) -> Result<[u8; 64], Error> {
     validate_scalar(&s)?;
 
     let mut out = [0u8; 64];
-    if unsafe { Hacl_P256_dh_initiator(out.as_mut_ptr(), s.as_ref().as_ptr() as _) } {
+    #[cfg(not(feature = "hacl-rs"))]
+    let ok = unsafe { Hacl_P256_dh_initiator(out.as_mut_ptr(), s.as_ref().as_ptr() as _) };
+    #[cfg(feature = "hacl-rs")]
+    let ok = hacl_rs::hacl::p256::dh_initiator(&mut out, s.as_ref());
+    if ok {
         Ok(out)
     } else {
         Err(Error::InvalidScalar)