diff --git a/Cargo.toml b/Cargo.toml
index 06b03c0f..cf2684bc 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -18,7 +18,7 @@ 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" }
+hax-lib-macros = { git = "https://github.com/hacspec/hax", optional = true }
 
 
 [features]
@@ -26,6 +26,7 @@ default = ["api"]
 test_utils = []
 secret_integers = []
 api = []             # The streaming Rust API that everyone should use but is not hacspec.
+hax-pv = ["dep:hax-lib-macros"]
 
 [dev-dependencies]
 bertie = { path = ".", features = ["test_utils"] }
diff --git a/src/tls13cert.rs b/src/tls13cert.rs
index bcc9453f..aedc60c9 100644
--- a/src/tls13cert.rs
+++ b/src/tls13cert.rs
@@ -15,8 +15,7 @@
 //!     }
 //!     BitString // 0x03
 //! }
-//! ```
-
+#[cfg(feature = "hax-pv")]
 use hax_lib_macros::{pv_constructor, pv_handwritten};
 
 #[cfg(not(feature = "secret_integers"))]
@@ -283,7 +282,7 @@ fn read_spki(cert: &Bytes, mut offset: usize) -> Result<Spki, Asn1Error> {
 /// certificate.
 ///
 /// Returns the start offset within the `cert` bytes and length of the key.
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn verification_key_from_cert(cert: &Bytes) -> Result<Spki, Asn1Error> {
     // An x509 cert is an ASN.1 sequence of [Certificate, SignatureAlgorithm, Signature].
     // Take the first sequence inside the outer because we're interested in the
@@ -304,7 +303,7 @@ pub(crate) fn verification_key_from_cert(cert: &Bytes) -> Result<Spki, Asn1Error
 }
 
 /// Read the EC PK from the cert as uncompressed point.
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn ecdsa_public_key(
     cert: &Bytes,
     indices: CertificateKey,
@@ -317,7 +316,7 @@ pub(crate) fn ecdsa_public_key(
     Ok(cert.slice(offset + 1, len - 1)) // Drop the 0x04 here.
 }
 
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn rsa_public_key(
     cert: &Bytes,
     indices: CertificateKey,
@@ -392,7 +391,7 @@ pub(crate) fn rsa_private_key(key: &Bytes) -> Result<Bytes, Asn1Error> {
 ///
 /// On input of a `certificate` and `spki`, return a [`PublicVerificationKey`]
 /// if successful, or an [`Asn1Error`] otherwise.
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn cert_public_key(
     certificate: &Bytes,
     spki: &Spki,
diff --git a/src/tls13crypto.rs b/src/tls13crypto.rs
index 1a86eb07..97e5ec63 100644
--- a/src/tls13crypto.rs
+++ b/src/tls13crypto.rs
@@ -1,5 +1,4 @@
-use std::fmt::Display;
-
+#[cfg(feature = "hax-pv")]
 use hax_lib_macros::{pv_constructor, pv_handwritten};
 use libcrux::{
     kem::{Ct, PrivateKey, PublicKey},
@@ -7,6 +6,7 @@ use libcrux::{
     *,
 };
 use rand::{CryptoRng, RngCore};
+use std::fmt::Display;
 
 use crate::tls13utils::{
     check_mem, eq, length_u16_encoded, tlserr, Bytes, Error, TLSError, CRYPTO_ERROR,
@@ -109,7 +109,7 @@ impl HashAlgorithm {
     /// Hash `data` with the given `algorithm`.
     ///
     /// Returns the digest or an [`TLSError`].
-    #[pv_constructor]
+    #[cfg_attr(feature = "hax-pv", pv_constructor)]
     pub(crate) fn hash(&self, data: &Bytes) -> Result<Bytes, TLSError> {
         Ok(digest::hash(self.libcrux_algorithm()?, &data.declassify()).into())
     }
@@ -141,7 +141,7 @@ impl HashAlgorithm {
 /// Compute the HMAC tag.
 ///
 /// Returns the tag [`Hmac`] or a [`TLSError`].
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn hmac_tag(alg: &HashAlgorithm, mk: &MacKey, input: &Bytes) -> Result<Hmac, TLSError> {
     Ok(hmac::hmac(
         alg.hmac_algorithm()?,
@@ -155,7 +155,7 @@ pub(crate) fn hmac_tag(alg: &HashAlgorithm, mk: &MacKey, input: &Bytes) -> Resul
 /// Verify a given HMAC `tag`.
 ///
 /// Returns `()` if successful or a [`TLSError`].
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn hmac_verify(
     alg: &HashAlgorithm,
     mk: &MacKey,
@@ -186,7 +186,7 @@ fn hkdf_algorithm(alg: &HashAlgorithm) -> Result<hkdf::Algorithm, TLSError> {
 /// HKDF Extract.
 ///
 /// Returns the result as [`Bytes`] or a [`TLSError`].
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn hkdf_extract(
     alg: &HashAlgorithm,
     ikm: &Bytes,
@@ -198,7 +198,7 @@ pub(crate) fn hkdf_extract(
 /// HKDF Expand.
 ///
 /// Returns the result as [`Bytes`] or a [`TLSError`].
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn hkdf_expand(
     alg: &HashAlgorithm,
     prk: &Bytes,
@@ -316,7 +316,7 @@ impl SignatureScheme {
 }
 
 /// Sign the `input` with the provided RSA key.
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn sign_rsa(
     sk: &Bytes,
     pk_modulus: &Bytes,
@@ -350,7 +350,7 @@ pub(crate) fn sign_rsa(
 }
 
 /// Sign the bytes in `input` with the signature key `sk` and `algorithm`.
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn sign(
     algorithm: &SignatureScheme,
     sk: &Bytes,
@@ -388,7 +388,7 @@ pub(crate) fn sign(
 /// Verify the `input` bytes against the provided `signature`.
 ///
 /// Return `Ok(())` if the verification succeeds, and a [`TLSError`] otherwise.
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn verify(
     alg: &SignatureScheme,
     pk: &PublicVerificationKey,
@@ -497,7 +497,7 @@ impl KemScheme {
 }
 
 /// Generate a new KEM key pair.
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn kem_keygen(
     alg: KemScheme,
     rng: &mut (impl CryptoRng + RngCore),
@@ -541,7 +541,7 @@ fn into_raw(alg: KemScheme, point: Bytes) -> Bytes {
 }
 
 /// KEM encapsulation
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn kem_encap(
     alg: KemScheme,
     pk: &Bytes,
@@ -576,7 +576,7 @@ fn to_shared_secret(alg: KemScheme, shared_secret: Bytes) -> Bytes {
 }
 
 /// KEM decapsulation
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn kem_decap(alg: KemScheme, ct: &Bytes, sk: &Bytes) -> Result<Bytes, TLSError> {
     // event!(Level::DEBUG, "KEM Decaps with {alg:?}");
     // event!(Level::TRACE, "  with ciphertext: {}", ct.as_hex());
diff --git a/src/tls13formats.rs b/src/tls13formats.rs
index ba35701f..de3c97e0 100644
--- a/src/tls13formats.rs
+++ b/src/tls13formats.rs
@@ -24,6 +24,8 @@ pub(crate) mod handshake_data;
 use handshake_data::{HandshakeData, HandshakeType};
 #[cfg(bench)]
 pub use handshake_data::{HandshakeData, HandshakeType};
+
+#[cfg(feature = "hax-pv")]
 use hax_lib_macros::{pv_constructor, pv_handwritten};
 
 // Well Known Constants
@@ -493,7 +495,7 @@ pub fn bench_client_hello(
 }
 
 /// Build a ClientHello message.
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn client_hello(
     algorithms: &Algorithms,
     client_random: Random,
@@ -545,7 +547,7 @@ pub(crate) fn client_hello(
     Ok((client_hello, trunc_len))
 }
 
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn set_client_hello_binder(
     ciphersuite: &Algorithms,
     binder: &Option<Hmac>,
@@ -593,7 +595,7 @@ pub fn bench_parse_client_hello(
 
 /// Parse the provided `client_hello` with the given `ciphersuite`.
 #[allow(clippy::type_complexity)]
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(super) fn parse_client_hello(
     ciphersuite: &Algorithms,
     client_hello: &HandshakeData,
@@ -691,7 +693,7 @@ pub(super) fn parse_client_hello(
 }
 
 /// Build the server hello message.
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn server_hello(
     algs: &Algorithms,
     sr: Random,
@@ -733,7 +735,7 @@ pub fn bench_parse_server_hello(
     parse_server_hello(algs, server_hello)
 }
 
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn parse_server_hello(
     algs: &Algorithms,
     server_hello: &HandshakeData,
@@ -773,7 +775,7 @@ pub(crate) fn parse_server_hello(
     }
 }
 
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn encrypted_extensions(_algs: &Algorithms) -> Result<HandshakeData, TLSError> {
     let handshake_type = bytes1(HandshakeType::EncryptedExtensions as u8);
     Ok(HandshakeData(handshake_type.concat(encode_length_u24(
@@ -781,7 +783,7 @@ pub(crate) fn encrypted_extensions(_algs: &Algorithms) -> Result<HandshakeData,
     )?)))
 }
 
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn parse_encrypted_extensions(
     _algs: &Algorithms,
     encrypted_extensions: &HandshakeData,
@@ -796,7 +798,7 @@ pub(crate) fn parse_encrypted_extensions(
         encrypted_extension_bytes.raw_slice(1..encrypted_extension_bytes.len()),
     )
 }
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn server_certificate(
     _algs: &Algorithms,
     cert: &Bytes,
@@ -813,7 +815,7 @@ pub fn bench_parse_server_certificate(certificate: &HandshakeData) -> Result<Byt
     parse_server_certificate(certificate)
 }
 
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn parse_server_certificate(certificate: &HandshakeData) -> Result<Bytes, TLSError> {
     let HandshakeData(sc) = certificate.as_handshake_message(HandshakeType::Certificate)?;
     let mut next = 0;
@@ -882,7 +884,7 @@ fn parse_ecdsa_signature(sig: Bytes) -> Result<Bytes, TLSError> {
         }
     }
 }
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn certificate_verify(algs: &Algorithms, cv: &Bytes) -> Result<HandshakeData, TLSError> {
     let sv = match algs.signature {
         SignatureScheme::RsaPssRsaSha256 => cv.clone(),
@@ -902,7 +904,7 @@ pub(crate) fn certificate_verify(algs: &Algorithms, cv: &Bytes) -> Result<Handsh
     HandshakeData::from_bytes(HandshakeType::CertificateVerify, &sig)
 }
 
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn parse_certificate_verify(
     algs: &Algorithms,
     certificate_verify: &HandshakeData,
@@ -925,12 +927,12 @@ pub(crate) fn parse_certificate_verify(
     }
 }
 
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn finished(vd: &Bytes) -> Result<HandshakeData, TLSError> {
     HandshakeData::from_bytes(HandshakeType::Finished, vd)
 }
 
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn parse_finished(finished: &HandshakeData) -> Result<Bytes, TLSError> {
     let HandshakeData(fin) = finished.as_handshake_message(HandshakeType::Finished)?;
     Ok(fin)
@@ -1058,7 +1060,7 @@ impl Transcript {
     }
 
     /// Add the [`HandshakeData`] `msg` to this transcript.
-    #[pv_constructor]
+    #[cfg_attr(feature = "hax-pv", pv_constructor)]
     pub(crate) fn add(mut self, msg: &HandshakeData) -> Self {
         self.transcript = self.transcript.concat(msg);
         self
@@ -1071,7 +1073,7 @@ impl Transcript {
     }
 
     /// Get the hash of this transcript without the client hello
-    #[pv_constructor]
+    #[cfg_attr(feature = "hax-pv", pv_constructor)]
     pub(crate) fn transcript_hash_without_client_hello(
         &self,
         client_hello: &HandshakeData,
diff --git a/src/tls13formats/handshake_data.rs b/src/tls13formats/handshake_data.rs
index bdae02ac..54d2dbf1 100644
--- a/src/tls13formats/handshake_data.rs
+++ b/src/tls13formats/handshake_data.rs
@@ -1,3 +1,4 @@
+#[cfg(feature = "hax-pv")]
 use hax_lib_macros::{pv_constructor, pv_handwritten};
 
 use crate::tls13utils::{
@@ -80,7 +81,7 @@ impl HandshakeData {
 
     /// Returns a new [`HandshakeData`] that contains the bytes of
     /// `other` appended to the bytes of `self`.
-    #[pv_constructor]
+    #[cfg_attr(feature = "hax-pv", pv_constructor)]
     pub(crate) fn concat(self, other: &HandshakeData) -> HandshakeData {
         let mut message1 = self.to_bytes();
         let message2 = other.to_bytes();
@@ -134,7 +135,7 @@ impl HandshakeData {
     /// If successful, returns the parsed handshake messages. Returns a [TLSError]
     /// if parsing of either message fails or if the payload is not fully consumed
     /// by parsing two messages.
-    #[pv_handwritten]
+    #[cfg_attr(feature = "hax-pv", pv_handwritten)]
     pub(crate) fn to_two(&self) -> Result<(HandshakeData, HandshakeData), TLSError> {
         let (message1, payload_rest) = self.next_handshake_message()?;
         let (message2, payload_rest) = payload_rest.next_handshake_message()?;
@@ -150,7 +151,7 @@ impl HandshakeData {
     /// If successful, returns the parsed handshake messages. Returns a [TLSError]
     /// if parsing of any message fails or if the payload is not fully consumed
     /// by parsing four messages.
-    #[pv_handwritten]
+    #[cfg_attr(feature = "hax-pv", pv_handwritten)]
     pub(crate) fn to_four(
         &self,
     ) -> Result<(HandshakeData, HandshakeData, HandshakeData, HandshakeData), TLSError> {
diff --git a/src/tls13utils.rs b/src/tls13utils.rs
index 17569634..04dfcfea 100644
--- a/src/tls13utils.rs
+++ b/src/tls13utils.rs
@@ -188,7 +188,7 @@ impl From<Vec<u8>> for Bytes {
 
 impl Bytes {
     /// Add a prefix to these bytes and return it.
-    #[pv_handwritten]
+    #[cfg_attr(feature = "hax-pv", pv_handwritten)]
     pub(crate) fn prefix(mut self, prefix: &[U8]) -> Self {
         let mut out = Vec::with_capacity(prefix.len() + self.len());
 
@@ -255,7 +255,7 @@ impl U32 {
         self.0
     }
 }
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn u16_as_be_bytes(val: U16) -> [U8; 2] {
     #[cfg(not(feature = "secret_integers"))]
     let val = val.to_be_bytes();
@@ -328,7 +328,7 @@ impl core::ops::Index<Range<usize>> for Bytes {
 
 impl Bytes {
     /// Create new [`Bytes`].
-    #[pv_constructor]
+    #[cfg_attr(feature = "hax-pv", pv_constructor)]
     pub(crate) fn new() -> Bytes {
         Bytes(Vec::new())
     }
@@ -339,7 +339,7 @@ impl Bytes {
     }
 
     /// Generate `len` bytes of `0`.
-    #[pv_constructor]
+    #[cfg_attr(feature = "hax-pv", pv_constructor)]
     pub(crate) fn zeroes(len: usize) -> Bytes {
         Bytes(vec![U8(0); len])
     }
@@ -404,7 +404,7 @@ impl Bytes {
     }
 
     /// Concatenate `other` with these bytes and return a copy as [`Bytes`].
-    #[pv_handwritten]
+    #[cfg_attr(feature = "hax-pv", pv_handwritten)]
     pub fn concat(mut self, mut other: Bytes) -> Bytes {
         self.0.append(&mut other.0);
         self
@@ -451,6 +451,8 @@ macro_rules! bytes_concat {
     };
 }
 pub(crate) use bytes_concat;
+
+#[cfg(feature = "hax-pv")]
 use hax_lib_macros::{pv_constructor, pv_handwritten};
 
 #[cfg(test)]
@@ -511,7 +513,7 @@ pub(crate) fn eq_slice(b1: &[U8], b2: &[U8]) -> bool {
 // TODO: This function should short-circuit once hax supports returns within loops
 /// Check if [Bytes] slices `b1` and `b2` are of the same
 /// length and agree on all positions.
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub fn eq(b1: &Bytes, b2: &Bytes) -> bool {
     eq_slice(&b1.0, &b2.0)
 }
@@ -531,7 +533,7 @@ pub(crate) fn check_eq_slice(b1: &[U8], b2: &[U8]) -> Result<(), TLSError> {
 /// Parse function to check if [Bytes] slices `b1` and `b2` are of the same
 /// length and agree on all positions, returning a [TLSError] otherwise.
 #[inline(always)]
-#[pv_handwritten]
+#[cfg_attr(feature = "hax-pv", pv_handwritten)]
 pub(crate) fn check_eq(b1: &Bytes, b2: &Bytes) -> Result<(), TLSError> {
     check_eq_slice(b1.as_raw(), b2.as_raw())
 }
@@ -563,7 +565,7 @@ pub(crate) fn check_mem(b1: &[U8], b2: &[U8]) -> Result<(), TLSError> {
 /// On success, return a new [Bytes] slice such that its first byte encodes the
 /// length of `bytes` and the remainder equals `bytes`. Return a [TLSError] if
 /// the length of `bytes` exceeds what can be encoded in one byte.
-#[pv_constructor]
+#[cfg_attr(feature = "hax-pv", pv_constructor)]
 pub(crate) fn encode_length_u8(bytes: &[U8]) -> Result<Bytes, TLSError> {
     let len = bytes.len();
     if len >= 256 {