diff --git a/Cargo.lock b/Cargo.lock
index dfd7ca64..8d0f7e93 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -64,9 +64,9 @@ dependencies = [
 
 [[package]]
 name = "anstyle-query"
-version = "1.0.3"
+version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a64c907d4e79225ac72e2a354c9ce84d50ebb4586dee56c82b3ee73004f537f5"
+checksum = "ad186efb764318d35165f1758e7dcef3b10628e26d41a44bc5550652e6804391"
 dependencies = [
  "windows-sys",
 ]
@@ -95,9 +95,9 @@ checksum = "0c4b4d0bd25bd0b74681c0ad21497610ce1b7c91b1022cd21c80c6fbdd9476b0"
 
 [[package]]
 name = "backtrace"
-version = "0.3.72"
+version = "0.3.73"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "17c6a35df3749d2e8bb1b7b21a976d82b15548788d2735b9d82f329268f71a11"
+checksum = "5cc23269a4f8976d0a4d2e7109211a419fe30e8d88d677cd60b6bc79c5732e0a"
 dependencies = [
  "addr2line",
  "cc",
@@ -126,6 +126,7 @@ dependencies = [
  "hax-lib-macros 0.1.0-pre.1 (git+https://github.com/hacspec/hax)",
  "hex",
  "libcrux",
+ "libcrux-kem",
  "rand",
  "rayon",
  "serde",
@@ -135,9 +136,9 @@ dependencies = [
 
 [[package]]
 name = "bitflags"
-version = "2.5.0"
+version = "2.6.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "cf4b9d6a944f767f8e5e0db018570623c85f3d925ac718db4e06d0187adb21c1"
+checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
 
 [[package]]
 name = "bogo_shim"
@@ -164,9 +165,9 @@ checksum = "37b2a672a2cb129a2e41c10b1224bb368f9f37a2b16b612598138befd7b37eb5"
 
 [[package]]
 name = "cc"
-version = "1.0.98"
+version = "1.0.104"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "41c270e7540d725e65ac7f1b212ac8ce349719624d7bcff99f8e2e488e8cf03f"
+checksum = "74b6a57f98764a267ff415d50a25e6e166f3831a5071af4995296ea97d210490"
 dependencies = [
  "jobserver",
  "libc",
@@ -208,9 +209,9 @@ dependencies = [
 
 [[package]]
 name = "clap"
-version = "4.5.4"
+version = "4.5.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "90bc066a67923782aa8515dbaea16946c5bcc5addbd668bb80af688e53e548a0"
+checksum = "84b3edb18336f4df585bc9aa31dd99c036dfa5dc5e9a2939a722a188f3a8970d"
 dependencies = [
  "clap_builder",
  "clap_derive",
@@ -218,9 +219,9 @@ dependencies = [
 
 [[package]]
 name = "clap_builder"
-version = "4.5.2"
+version = "4.5.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ae129e2e766ae0ec03484e609954119f123cc1fe650337e155d03b022f24f7b4"
+checksum = "c1c09dd5ada6c6c78075d6fd0da3f90d8080651e2d6cc8eb2f1aaa4034ced708"
 dependencies = [
  "anstream",
  "anstyle",
@@ -230,21 +231,21 @@ dependencies = [
 
 [[package]]
 name = "clap_derive"
-version = "4.5.4"
+version = "4.5.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "528131438037fd55894f62d6e9f068b8f45ac57ffa77517819645d10aed04f64"
+checksum = "2bac35c6dafb060fd4d275d9a4ffae97917c13a6327903a8be2153cd964f7085"
 dependencies = [
  "heck",
  "proc-macro2",
  "quote",
- "syn 2.0.66",
+ "syn 2.0.68",
 ]
 
 [[package]]
 name = "clap_lex"
-version = "0.7.0"
+version = "0.7.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "98cc8fbded0c607b7ba9dd60cd98df59af97e84d24e49c8557331cfc26d301ce"
+checksum = "4b82cf0babdbd58558212896d1a4272303a57bdb245c2bf1147185fb45640e70"
 
 [[package]]
 name = "colorchoice"
@@ -337,9 +338,9 @@ dependencies = [
 
 [[package]]
 name = "either"
-version = "1.12.0"
+version = "1.13.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3dca9240753cf90908d7e4aac30f630662b02aebaa1b58a3cadabdb23385b58b"
+checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0"
 
 [[package]]
 name = "getrandom"
@@ -371,7 +372,18 @@ dependencies = [
 [[package]]
 name = "hax-lib"
 version = "0.1.0-pre.1"
-source = "git+https://github.com/hacspec/hax/?branch=main#3444df704959e5a0865bad11894fc95ada97ee5e"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1b4c24729b7608f3a2f2b798b503e18ca3d46b5287e85e42c3e2a81a6431c20e"
+dependencies = [
+ "hax-lib-macros 0.1.0-pre.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "num-bigint",
+ "num-traits",
+]
+
+[[package]]
+name = "hax-lib"
+version = "0.1.0-pre.1"
+source = "git+https://github.com/hacspec/hax/?branch=main#7be21f59fb68a39041dd135e3e6c8b23ad22b4ea"
 dependencies = [
  "hax-lib-macros 0.1.0-pre.1 (git+https://github.com/hacspec/hax/?branch=main)",
  "num-bigint",
@@ -381,7 +393,7 @@ dependencies = [
 [[package]]
 name = "hax-lib"
 version = "0.1.0-pre.1"
-source = "git+https://github.com/hacspec/hax#3444df704959e5a0865bad11894fc95ada97ee5e"
+source = "git+https://github.com/hacspec/hax#7be21f59fb68a39041dd135e3e6c8b23ad22b4ea"
 dependencies = [
  "hax-lib-macros 0.1.0-pre.1 (git+https://github.com/hacspec/hax)",
  "num-bigint",
@@ -391,31 +403,57 @@ dependencies = [
 [[package]]
 name = "hax-lib-macros"
 version = "0.1.0-pre.1"
-source = "git+https://github.com/hacspec/hax/?branch=main#3444df704959e5a0865bad11894fc95ada97ee5e"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2e537b6582ecf0d2bc9761b6c129840c9a039263e71b933850af8e24d5e3a840"
+dependencies = [
+ "hax-lib-macros-types 0.1.0-pre.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "proc-macro-error",
+ "proc-macro2",
+ "quote",
+ "syn 2.0.68",
+]
+
+[[package]]
+name = "hax-lib-macros"
+version = "0.1.0-pre.1"
+source = "git+https://github.com/hacspec/hax/?branch=main#7be21f59fb68a39041dd135e3e6c8b23ad22b4ea"
 dependencies = [
  "hax-lib-macros-types 0.1.0-pre.1 (git+https://github.com/hacspec/hax/?branch=main)",
  "proc-macro-error",
  "proc-macro2",
  "quote",
- "syn 2.0.66",
+ "syn 2.0.68",
 ]
 
 [[package]]
 name = "hax-lib-macros"
 version = "0.1.0-pre.1"
-source = "git+https://github.com/hacspec/hax#3444df704959e5a0865bad11894fc95ada97ee5e"
+source = "git+https://github.com/hacspec/hax#7be21f59fb68a39041dd135e3e6c8b23ad22b4ea"
 dependencies = [
  "hax-lib-macros-types 0.1.0-pre.1 (git+https://github.com/hacspec/hax)",
  "proc-macro-error",
  "proc-macro2",
  "quote",
- "syn 2.0.66",
+ "syn 2.0.68",
+]
+
+[[package]]
+name = "hax-lib-macros-types"
+version = "0.1.0-pre.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1025439d93a495700d7099f7bd2285845837def514b2f97b2f8a4cd93fab5bd9"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "serde",
+ "serde_json",
+ "uuid",
 ]
 
 [[package]]
 name = "hax-lib-macros-types"
 version = "0.1.0-pre.1"
-source = "git+https://github.com/hacspec/hax/?branch=main#3444df704959e5a0865bad11894fc95ada97ee5e"
+source = "git+https://github.com/hacspec/hax/?branch=main#7be21f59fb68a39041dd135e3e6c8b23ad22b4ea"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -427,7 +465,7 @@ dependencies = [
 [[package]]
 name = "hax-lib-macros-types"
 version = "0.1.0-pre.1"
-source = "git+https://github.com/hacspec/hax#3444df704959e5a0865bad11894fc95ada97ee5e"
+source = "git+https://github.com/hacspec/hax#7be21f59fb68a39041dd135e3e6c8b23ad22b4ea"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -459,7 +497,7 @@ name = "integration_tests"
 version = "0.1.0"
 dependencies = [
  "bertie",
- "libcrux-platform 0.0.2-pre.2 (registry+https://github.com/rust-lang/crates.io-index)",
+ "libcrux-platform 0.0.2-alpha.1",
  "rand",
  "tracing-subscriber",
 ]
@@ -516,9 +554,9 @@ dependencies = [
 
 [[package]]
 name = "lazy_static"
-version = "1.4.0"
+version = "1.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"
+checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe"
 
 [[package]]
 name = "libc"
@@ -529,30 +567,81 @@ checksum = "97b3888a4aecf77e811145cadf6eef5901f4782c53886191b2f693f24761847c"
 [[package]]
 name = "libcrux"
 version = "0.0.2-pre.2"
-source = "git+https://github.com/cryspen/libcrux#f86c874fb500fe6d5b245b5c89a90e42c7ab6207"
+source = "git+https://github.com/cryspen/libcrux#0f74f5a6fa7477e5dd553d6d589ab04c6fcca2bd"
 dependencies = [
  "hax-lib 0.1.0-pre.1 (git+https://github.com/hacspec/hax/?branch=main)",
  "hax-lib-macros 0.1.0-pre.1 (git+https://github.com/hacspec/hax/?branch=main)",
- "libcrux-hacl",
- "libcrux-platform 0.0.2-pre.2 (git+https://github.com/cryspen/libcrux)",
+ "libcrux-hacl 0.0.2-pre.2",
+ "libcrux-platform 0.0.2-pre.2",
  "libjade-sys",
  "rand",
 ]
 
+[[package]]
+name = "libcrux-ecdh"
+version = "0.0.2-alpha.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "914c96910c22ffcf56954b506000187a8cf04ebb799dc9a1acbec57b1627f7fb"
+dependencies = [
+ "libcrux-hacl 0.0.2-alpha.1",
+ "rand",
+]
+
+[[package]]
+name = "libcrux-hacl"
+version = "0.0.2-alpha.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "368e814a86e9442cffa12e68cb0d0b14bf8257f75be4272c25ca7851b5a12c84"
+dependencies = [
+ "cc",
+ "libcrux-platform 0.0.2-alpha.1",
+]
+
 [[package]]
 name = "libcrux-hacl"
 version = "0.0.2-pre.2"
-source = "git+https://github.com/cryspen/libcrux#f86c874fb500fe6d5b245b5c89a90e42c7ab6207"
+source = "git+https://github.com/cryspen/libcrux#0f74f5a6fa7477e5dd553d6d589ab04c6fcca2bd"
 dependencies = [
  "cc",
- "libcrux-platform 0.0.2-pre.2 (git+https://github.com/cryspen/libcrux)",
+ "libcrux-platform 0.0.2-pre.2",
+]
+
+[[package]]
+name = "libcrux-intrinsics"
+version = "0.0.2-alpha.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9b7c2ce65b529f97635fc14b10f70156e35fa658833f8fe726682ca910451f3a"
+
+[[package]]
+name = "libcrux-kem"
+version = "0.0.2-alpha.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e1b6e1aa1fd99e2b6f83476c1204ca3fd72be57a32b727a8ce4d526d9a683f1b"
+dependencies = [
+ "libcrux-ecdh",
+ "libcrux-ml-kem",
+ "libcrux-sha3",
+ "rand",
+]
+
+[[package]]
+name = "libcrux-ml-kem"
+version = "0.0.2-alpha.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fb9b5c06f556440dd6c6d29fda6809106525290cb8c20386e42a4d8f7ecee7a6"
+dependencies = [
+ "hax-lib 0.1.0-pre.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "libcrux-intrinsics",
+ "libcrux-platform 0.0.2-alpha.1",
+ "libcrux-sha3",
+ "rand_core",
 ]
 
 [[package]]
 name = "libcrux-platform"
-version = "0.0.2-pre.2"
+version = "0.0.2-alpha.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "647e39666194b11df17c19451d1154b9be79df98b9821532560c2ecad0cf3410"
+checksum = "c7ad3efa6f53977d9a56e97be561f57848cdd5151c99db19f9de820efee12df1"
 dependencies = [
  "libc",
 ]
@@ -560,18 +649,29 @@ dependencies = [
 [[package]]
 name = "libcrux-platform"
 version = "0.0.2-pre.2"
-source = "git+https://github.com/cryspen/libcrux#f86c874fb500fe6d5b245b5c89a90e42c7ab6207"
+source = "git+https://github.com/cryspen/libcrux#0f74f5a6fa7477e5dd553d6d589ab04c6fcca2bd"
 dependencies = [
  "libc",
 ]
 
+[[package]]
+name = "libcrux-sha3"
+version = "0.0.2-alpha.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8c0ef30b30ec8590b8414737fcfd0d2970add60ae249ea4a49f1ace36562abb8"
+dependencies = [
+ "hax-lib 0.1.0-pre.1 (registry+https://github.com/rust-lang/crates.io-index)",
+ "libcrux-intrinsics",
+ "libcrux-platform 0.0.2-alpha.1",
+]
+
 [[package]]
 name = "libjade-sys"
 version = "0.0.2-pre.2"
-source = "git+https://github.com/cryspen/libcrux#f86c874fb500fe6d5b245b5c89a90e42c7ab6207"
+source = "git+https://github.com/cryspen/libcrux#0f74f5a6fa7477e5dd553d6d589ab04c6fcca2bd"
 dependencies = [
  "cc",
- "libcrux-platform 0.0.2-pre.2 (git+https://github.com/cryspen/libcrux)",
+ "libcrux-platform 0.0.2-pre.2",
 ]
 
 [[package]]
@@ -586,21 +686,21 @@ dependencies = [
 
 [[package]]
 name = "log"
-version = "0.4.21"
+version = "0.4.22"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "90ed8c1e510134f979dbc4f070f87d4313098b704861a105fe34231c70a3901c"
+checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24"
 
 [[package]]
 name = "memchr"
-version = "2.7.2"
+version = "2.7.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6c8640c5d730cb13ebd907d8d04b52f55ac9a2eec55b440c8892f40d56c76c1d"
+checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3"
 
 [[package]]
 name = "miniz_oxide"
-version = "0.7.3"
+version = "0.7.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "87dfd01fe195c66b572b37921ad8803d010623c0aca821bea2302239d155cdae"
+checksum = "b8a240ddb74feaf34a79a7add65a741f3167852fba007066dcac1ca548d89c08"
 dependencies = [
  "adler",
 ]
@@ -623,9 +723,9 @@ dependencies = [
 
 [[package]]
 name = "num-bigint"
-version = "0.4.5"
+version = "0.4.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c165a9ab64cf766f73521c0dd2cfdff64f488b8f0b3e621face3462d3db536d7"
+checksum = "a5e44f723f1133c9deac646763579fdb3ac745e418f2a7af9cd0c431da1f20b9"
 dependencies = [
  "num-integer",
  "num-traits",
@@ -651,9 +751,9 @@ dependencies = [
 
 [[package]]
 name = "object"
-version = "0.35.0"
+version = "0.36.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b8ec7ab813848ba4522158d5517a6093db1ded27575b070f4177b8d12b41db5e"
+checksum = "081b846d1d56ddfc18fdf1a922e4f6e07a11768ea1b92dec44e42b72712ccfce"
 dependencies = [
  "memchr",
 ]
@@ -765,9 +865,9 @@ dependencies = [
 
 [[package]]
 name = "proc-macro2"
-version = "1.0.85"
+version = "1.0.86"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "22244ce15aa966053a896d1accb3a6e68469b97c7f33f284b99f0d576879fc23"
+checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77"
 dependencies = [
  "unicode-ident",
 ]
@@ -844,18 +944,18 @@ dependencies = [
 
 [[package]]
 name = "redox_syscall"
-version = "0.5.1"
+version = "0.5.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "469052894dcb553421e483e4209ee581a45100d31b4018de03e5a7ad86374a7e"
+checksum = "c82cf8cff14456045f55ec4241383baeff27af886adb72ffb2162f99911de0fd"
 dependencies = [
  "bitflags",
 ]
 
 [[package]]
 name = "regex"
-version = "1.10.4"
+version = "1.10.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c117dbdfde9c8308975b6a18d71f3f385c89461f7b3fb054288ecf2a2058ba4c"
+checksum = "b91213439dad192326a0d7c6ee3955910425f441d7038e0d6933b0aec5c4517f"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -865,9 +965,9 @@ dependencies = [
 
 [[package]]
 name = "regex-automata"
-version = "0.4.6"
+version = "0.4.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "86b83b8b9847f9bf95ef68afb0b8e6cdb80f498442f5179a29fad448fcc1eaea"
+checksum = "38caf58cc5ef2fed281f89292ef23f6365465ed9a41b7a7754eb4e26496c92df"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -876,9 +976,9 @@ dependencies = [
 
 [[package]]
 name = "regex-syntax"
-version = "0.8.3"
+version = "0.8.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "adad44e29e4c806119491a7f06f03de4d1af22c3a680dd47f1e6e179439d1f56"
+checksum = "7a66a03ae7c801facd77a29370b4faec201768915ac14a721ba36f20bc9c209b"
 
 [[package]]
 name = "rustc-demangle"
@@ -930,14 +1030,14 @@ checksum = "500cbc0ebeb6f46627f50f3f5811ccf6bf00643be300b4c3eabc0ef55dc5b5ba"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.66",
+ "syn 2.0.68",
 ]
 
 [[package]]
 name = "serde_json"
-version = "1.0.117"
+version = "1.0.120"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "455182ea6142b14f93f4bc5320a2b31c1f266b66a4a5c858b013302a5d8cbfc3"
+checksum = "4e0d21c9a8cae1235ad58a00c11cb40d4b1e5c784f1ef2c537876ed6ffd8b7c5"
 dependencies = [
  "itoa",
  "ryu",
@@ -1003,9 +1103,9 @@ dependencies = [
 
 [[package]]
 name = "syn"
-version = "2.0.66"
+version = "2.0.68"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c42f3f41a2de00b01c0aaad383c5a45241efc8b2d1eda5661812fda5f3cdcff5"
+checksum = "901fa70d88b9d6c98022e23b4136f9f3e54e4662c3bc1bd1d84a42a9a0f0c1e9"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -1029,7 +1129,7 @@ checksum = "46c3384250002a6d5af4d114f2845d37b57521033f30d5c3f46c4d70e1197533"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.66",
+ "syn 2.0.68",
 ]
 
 [[package]]
@@ -1077,7 +1177,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.66",
+ "syn 2.0.68",
 ]
 
 [[package]]
@@ -1123,15 +1223,15 @@ checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b"
 
 [[package]]
 name = "utf8parse"
-version = "0.2.1"
+version = "0.2.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a"
+checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821"
 
 [[package]]
 name = "uuid"
-version = "1.8.0"
+version = "1.9.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a183cf7feeba97b4dd1c0d46788634f6221d87fa961b305bed08c851829efcc0"
+checksum = "5de17fd2f7da591098415cff336e12965a28061ddace43b59cb3c430179c9439"
 dependencies = [
  "getrandom",
 ]
@@ -1185,7 +1285,7 @@ dependencies = [
  "once_cell",
  "proc-macro2",
  "quote",
- "syn 2.0.66",
+ "syn 2.0.68",
  "wasm-bindgen-shared",
 ]
 
@@ -1207,7 +1307,7 @@ checksum = "e94f17b526d0a461a191c78ea52bbce64071ed5c04c9ffe424dcb38f74171bb7"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.66",
+ "syn 2.0.68",
  "wasm-bindgen-backend",
  "wasm-bindgen-shared",
 ]
diff --git a/Cargo.toml b/Cargo.toml
index b62ef73c..47a047db 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -17,15 +17,18 @@ backtrace = "0.3.0"
 rand = "0.8.0"
 hex = "0.4.3"
 tracing = "0.1"
-libcrux = { version = "0.0.2-pre.2", features = ["rand"] }
-hax-lib-macros = { git = "https://github.com/hacspec/hax", optional = true}
+libcrux-kem = {version = "0.0.2-alpha.1", features = ["pre-verification", "kyber"]}
+libcrux = { version = "0.0.2-alpha.1", features = [
+    "rand",
+]}
+hax-lib-macros = { git = "https://github.com/hacspec/hax", optional = true }
 hax-lib = { git = "https://github.com/hacspec/hax" }
 
 [features]
 default = ["api"]
 test_utils = []
 secret_integers = []
-api = []             # The streaming Rust API that everyone should use but is not hacspec.
+api = []                           # The streaming Rust API that everyone should use but is not hacspec.
 hax-fstar = ["dep:hax-lib-macros"]
 hax-pv = ["dep:hax-lib-macros"]
 
diff --git a/integration_tests/Cargo.toml b/integration_tests/Cargo.toml
index bc1b8665..2acab70f 100644
--- a/integration_tests/Cargo.toml
+++ b/integration_tests/Cargo.toml
@@ -7,7 +7,7 @@ edition = "2021"
 
 [dependencies]
 bertie = { version = "0.1.0-pre.2", path = ".." }
-libcrux-platform = "0.0.2-pre.1"
+libcrux-platform = "0.0.2-alpha.1"
 tracing-subscriber = "0.3"
 
 [dev-dependencies]
diff --git a/integration_tests/tests/self_test.rs b/integration_tests/tests/self_test.rs
index f523430b..e2c70e03 100644
--- a/integration_tests/tests/self_test.rs
+++ b/integration_tests/tests/self_test.rs
@@ -3,16 +3,16 @@ use std::net::TcpListener;
 
 use bertie::{
     stream::BertieStream,
-    tls13crypto::SignatureScheme,
     tls13crypto::{
         SHA256_Aes128Gcm_EcdsaSecp256r1Sha256_P256, SHA256_Aes128Gcm_EcdsaSecp256r1Sha256_X25519,
         SHA256_Aes128Gcm_RsaPssRsaSha256_P256, SHA256_Aes128Gcm_RsaPssRsaSha256_X25519,
         SHA256_Chacha20Poly1305_EcdsaSecp256r1Sha256_P256,
         SHA256_Chacha20Poly1305_EcdsaSecp256r1Sha256_X25519,
+        SHA256_Chacha20Poly1305_EcdsaSecp256r1Sha256_X25519Kyber768Draft00,
         SHA256_Chacha20Poly1305_RsaPssRsaSha256_P256,
         SHA256_Chacha20Poly1305_RsaPssRsaSha256_X25519, SHA384_Aes256Gcm_EcdsaSecp256r1Sha256_P256,
         SHA384_Aes256Gcm_EcdsaSecp256r1Sha256_X25519, SHA384_Aes256Gcm_RsaPssRsaSha256_P256,
-        SHA384_Aes256Gcm_RsaPssRsaSha256_X25519,
+        SHA384_Aes256Gcm_RsaPssRsaSha256_X25519, SignatureScheme,
     },
 };
 
@@ -25,6 +25,10 @@ fn test_sha256_chacha20_poly1305_ecdsa_secp256r1_sha256_x25519() {
     self_test_algorithm(SHA256_Chacha20Poly1305_EcdsaSecp256r1Sha256_X25519);
 }
 #[test]
+fn test_sha256_chacha20_poly1305_ecdsa_secp256r1_sha256_x25519kyber768() {
+    self_test_algorithm(SHA256_Chacha20Poly1305_EcdsaSecp256r1Sha256_X25519Kyber768Draft00);
+}
+#[test]
 fn test_sha256_chacha20_poly1305_ecdsa_secp256r1_sha256_p256() {
     self_test_algorithm(SHA256_Chacha20Poly1305_EcdsaSecp256r1Sha256_P256);
 }
diff --git a/simple_https_client/src/tls13client.rs b/simple_https_client/src/tls13client.rs
index 52bb680b..1eceab01 100644
--- a/simple_https_client/src/tls13client.rs
+++ b/simple_https_client/src/tls13client.rs
@@ -35,6 +35,7 @@ struct Cli {
     ///   * SHA384_Aes256Gcm_EcdsaSecp256r1Sha256_X25519
     ///   * SHA384_Aes256Gcm_RsaPssRsaSha256_P256
     ///   * SHA384_Aes256Gcm_RsaPssRsaSha256_X25519
+    ///   * SHA256_Chacha20Poly1305_EcdsaSecp256r1Sha256_X25519Kyber768Draft00
     ///
     /// The default value is SHA256_Chacha20Poly1305_EcdsaSecp256r1Sha256_X25519.
     #[clap(verbatim_doc_comment)]
@@ -62,7 +63,7 @@ fn main() -> anyhow::Result<()> {
 
     event!(Level::INFO, "Starting new Client connection ...");
     event!(Level::DEBUG, "  {host}:{port}");
-    event!(Level::DEBUG, "  {ciphersuite:?}");
+    event!(Level::DEBUG, "  {ciphersuite:#?}");
 
     // Initiate HTTPS connection to host:port.
     let mut stream = BertieStream::client(&host, port, ciphersuite, &mut thread_rng())
diff --git a/src/tls13crypto.rs b/src/tls13crypto.rs
index 97e5ec63..2df4fb36 100644
--- a/src/tls13crypto.rs
+++ b/src/tls13crypto.rs
@@ -1,10 +1,10 @@
 #[cfg(feature = "hax-pv")]
 use hax_lib_macros::{pv_constructor, pv_handwritten};
 use libcrux::{
-    kem::{Ct, PrivateKey, PublicKey},
     signature::rsa_pss::{RsaPssKeySize, RsaPssPrivateKey, RsaPssPublicKey},
     *,
 };
+use libcrux_kem::{Ct, PrivateKey, PublicKey};
 use rand::{CryptoRng, RngCore};
 use std::fmt::Display;
 
@@ -483,14 +483,16 @@ pub enum KemScheme {
     X448,
     Secp384r1,
     Secp521r1,
+    X25519Kyber768Draft00,
 }
 
 impl KemScheme {
     /// Get the libcrux algorithm for this [`KemScheme`].
-    fn libcrux_algorithm(self) -> Result<kem::Algorithm, TLSError> {
+    fn libcrux_kem_algorithm(self) -> Result<libcrux_kem::Algorithm, TLSError> {
         match self {
-            KemScheme::X25519 => Ok(kem::Algorithm::X25519),
-            KemScheme::Secp256r1 => Ok(kem::Algorithm::Secp256r1),
+            KemScheme::X25519 => Ok(libcrux_kem::Algorithm::X25519),
+            KemScheme::Secp256r1 => Ok(libcrux_kem::Algorithm::Secp256r1),
+            KemScheme::X25519Kyber768Draft00 => Ok(libcrux_kem::Algorithm::X25519Kyber768Draft00),
             _ => tlserr(UNSUPPORTED_ALGORITHM),
         }
     }
@@ -502,7 +504,7 @@ pub(crate) fn kem_keygen(
     alg: KemScheme,
     rng: &mut (impl CryptoRng + RngCore),
 ) -> Result<(KemSk, KemPk), TLSError> {
-    let res = kem::key_gen(alg.libcrux_algorithm()?, rng);
+    let res = libcrux_kem::key_gen(alg.libcrux_kem_algorithm()?, rng);
     match res {
         Ok((sk, pk)) => {
             // event!(
@@ -551,12 +553,13 @@ pub(crate) fn kem_encap(
     // event!(Level::TRACE, "  pk:  {}", pk.as_hex());
 
     let pk = into_raw(alg, pk.clone());
-    let pk = PublicKey::decode(alg.libcrux_algorithm()?, &pk.declassify()).unwrap();
+    let pk = PublicKey::decode(alg.libcrux_kem_algorithm()?, &pk.declassify()).unwrap();
     let res = pk.encapsulate(rng);
     match res {
         Ok((shared_secret, ct)) => {
             let ct = encoding_prefix(alg).concat(Bytes::from(ct.encode()));
             let shared_secret = to_shared_secret(alg, Bytes::from(shared_secret.encode()));
+
             // event!(Level::TRACE, "  output ciphertext: {}", ct.as_hex());
             Ok((shared_secret, ct))
         }
@@ -581,7 +584,7 @@ pub(crate) fn kem_decap(alg: KemScheme, ct: &Bytes, sk: &Bytes) -> Result<Bytes,
     // event!(Level::DEBUG, "KEM Decaps with {alg:?}");
     // event!(Level::TRACE, "  with ciphertext: {}", ct.as_hex());
 
-    let librux_algorithm = alg.libcrux_algorithm()?;
+    let librux_algorithm = alg.libcrux_kem_algorithm()?;
     let sk = PrivateKey::decode(librux_algorithm, &sk.declassify()).unwrap();
     let ct = into_raw(alg, ct.clone()).declassify();
     let ct = Ct::decode(librux_algorithm, &ct).unwrap();
@@ -682,6 +685,7 @@ impl Algorithms {
             KemScheme::X448 => tlserr(UNSUPPORTED_ALGORITHM),
             KemScheme::Secp384r1 => tlserr(UNSUPPORTED_ALGORITHM),
             KemScheme::Secp521r1 => tlserr(UNSUPPORTED_ALGORITHM),
+            KemScheme::X25519Kyber768Draft00 => Ok([0x63, 0x99].into()), // same as https://github.com/google/boringssl/blob/66d274dfbab9e4f84599f06504987c418ca087d9/include/openssl/ssl.h#L2540
         }
     }
 
@@ -743,6 +747,9 @@ impl TryFrom<&str> for Algorithms {
             "SHA384_Aes256Gcm_RsaPssRsaSha256_X25519" => {
                 Ok(SHA384_Aes256Gcm_RsaPssRsaSha256_X25519)
             }
+            "SHA256_Chacha20Poly1305_EcdsaSecp256r1Sha256_X25519Kyber768Draft00" => {
+                Ok(SHA256_Chacha20Poly1305_EcdsaSecp256r1Sha256_X25519Kyber768Draft00)
+            }
             _ => Err(Error::UnknownCiphersuite(format!(
                 "Invalid ciphersuite description: {}",
                 s
@@ -787,6 +794,20 @@ pub const SHA256_Chacha20Poly1305_EcdsaSecp256r1Sha256_X25519: Algorithms = Algo
     false,
 );
 
+/// `TLS_CHACHA20_POLY1305_SHA256`
+/// with
+/// * X25519Kyber768Draft00 for key exchange (cf. https://www.ietf.org/archive/id/draft-tls-westerbaan-xyber768d00-02.html)
+/// * EcDSA P256 SHA256 for signatures
+pub const SHA256_Chacha20Poly1305_EcdsaSecp256r1Sha256_X25519Kyber768Draft00: Algorithms =
+    Algorithms::new(
+        HashAlgorithm::SHA256,
+        AeadAlgorithm::Chacha20Poly1305,
+        SignatureScheme::EcdsaSecp256r1Sha256,
+        KemScheme::X25519Kyber768Draft00,
+        false,
+        false,
+    );
+
 /// `TLS_CHACHA20_POLY1305_SHA256`
 /// with
 /// * x25519 for key exchange
diff --git a/src/tls13utils.rs b/src/tls13utils.rs
index d9c5da92..f6c99b0b 100644
--- a/src/tls13utils.rs
+++ b/src/tls13utils.rs
@@ -461,9 +461,9 @@ pub(crate) use bytes_concat;
 #[cfg(feature = "hax-pv")]
 use hax_lib_macros::{pv_constructor, pv_handwritten};
 
-#[cfg(test)]
 impl Bytes {
     /// Get a hex representation of self as [`String`].
+    #[cfg(test)]
     pub(crate) fn as_hex(&self) -> String {
         let strs: Vec<String> = self
             .0