diff --git a/.github/workflows/tls_codec.yml b/.github/workflows/tls_codec.yml
index d41e20d14..09ce78329 100644
--- a/.github/workflows/tls_codec.yml
+++ b/.github/workflows/tls_codec.yml
@@ -86,7 +86,8 @@ jobs:
         uses: hacspec/hax-actions@main
         with:
           fstar: v2025.08.07
+          hax_reference: tls-codec-panic-freedom
       - name: 🏃 Extract F*
         run: cargo hax into fstar
-      - name: 🏃 Lax-check extracted F*
-        run: OTHERFLAGS="--admit_smt_queries true" make -C proofs/fstar/extraction/
\ No newline at end of file
+      - name: 🏃 Type-check extracted F*
+        run: make -C proofs/fstar/extraction/
\ No newline at end of file
diff --git a/Cargo.lock b/Cargo.lock
index e4151a471..d777d20a3 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -739,8 +739,8 @@ checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1"
 
 [[package]]
 name = "hax-lib"
-version = "0.3.1"
-source = "git+https://github.com/cryspen/hax?branch=tls-codec-lib#89146496aa29fff2137635020f58a03a1ffb7caa"
+version = "0.3.5"
+source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#445f3a0ba8863b43287d10c0e8ed30052d3db747"
 dependencies = [
  "hax-lib-macros",
  "num-bigint",
@@ -749,8 +749,8 @@ dependencies = [
 
 [[package]]
 name = "hax-lib-macros"
-version = "0.3.1"
-source = "git+https://github.com/cryspen/hax?branch=tls-codec-lib#89146496aa29fff2137635020f58a03a1ffb7caa"
+version = "0.3.5"
+source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#445f3a0ba8863b43287d10c0e8ed30052d3db747"
 dependencies = [
  "hax-lib-macros-types",
  "proc-macro-error2",
@@ -761,8 +761,8 @@ dependencies = [
 
 [[package]]
 name = "hax-lib-macros-types"
-version = "0.3.1"
-source = "git+https://github.com/cryspen/hax?branch=tls-codec-lib#89146496aa29fff2137635020f58a03a1ffb7caa"
+version = "0.3.5"
+source = "git+https://github.com/cryspen/hax?branch=tls-codec-panic-freedom#445f3a0ba8863b43287d10c0e8ed30052d3db747"
 dependencies = [
  "proc-macro2",
  "quote",
diff --git a/tls_codec/Cargo.toml b/tls_codec/Cargo.toml
index 672892caf..50dd14128 100644
--- a/tls_codec/Cargo.toml
+++ b/tls_codec/Cargo.toml
@@ -16,7 +16,7 @@ zeroize = { version = "1.8", default-features = false, features = [
     "alloc",
     "zeroize_derive",
 ] }
-hax-lib = {git = "https://github.com/cryspen/hax", branch = "tls-codec-lib"}
+hax-lib = {git = "https://github.com/cryspen/hax", branch = "tls-codec-panic-freedom"}
 
 # optional dependencies
 arbitrary = { version = "1.4", features = ["derive"], optional = true }
diff --git a/tls_codec/derive/src/lib.rs b/tls_codec/derive/src/lib.rs
index f132943a2..c3925a1c0 100644
--- a/tls_codec/derive/src/lib.rs
+++ b/tls_codec/derive/src/lib.rs
@@ -90,6 +90,10 @@
 //!         TlsByteSliceU32(v).tls_serialized_len()
 //!     }
 //!
+//!     pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {
+//!         TlsByteSliceU32(v).tls_serialized_len_checked()
+//!     }
+//!
 //!     pub fn tls_serialize<W: Write>(v: &[u8], writer: &mut W) -> Result<usize, tls_codec::Error> {
 //!         TlsByteSliceU32(v).tls_serialize(writer)
 //!     }
@@ -787,6 +791,11 @@ fn impl_tls_size(parsed_ast: TlsStruct) -> TokenStream2 {
                         #(#prefixes::tls_serialized_len(&self.#members) + )*
                         0
                     }
+                    #[inline]
+                    #[allow(clippy::needless_question_mark)]
+                    fn tls_serialized_len_checked(&self) -> Option<usize> {
+                        Some(0usize#(.checked_add(#prefixes::tls_serialized_len_checked(&self.#members)?)?)*)
+                    }
                 }
 
                 impl #impl_generics tls_codec::Size for &#ident #ty_generics #where_clause {
@@ -794,6 +803,10 @@ fn impl_tls_size(parsed_ast: TlsStruct) -> TokenStream2 {
                     fn tls_serialized_len(&self) -> usize {
                         tls_codec::Size::tls_serialized_len(*self)
                     }
+                    #[inline]
+                    fn tls_serialized_len_checked(&self) -> Option<usize> {
+                        tls_codec::Size::tls_serialized_len_checked(*self)
+                    }
                 }
             }
         }
@@ -827,6 +840,13 @@ fn impl_tls_size(parsed_ast: TlsStruct) -> TokenStream2 {
                         };
                         core::mem::size_of::<#repr>() + field_len
                     }
+                    #[inline]
+                    fn tls_serialized_len_checked(&self) -> Option<usize> {
+                        let field_len = match self {
+                            #(#field_arms)*
+                        };
+                        core::mem::size_of::<#repr>().checked_add(field_len)
+                    }
                 }
 
                 impl #impl_generics tls_codec::Size for &#ident #ty_generics #where_clause {
@@ -834,6 +854,10 @@ fn impl_tls_size(parsed_ast: TlsStruct) -> TokenStream2 {
                     fn tls_serialized_len(&self) -> usize {
                         tls_codec::Size::tls_serialized_len(*self)
                     }
+                    #[inline]
+                    fn tls_serialized_len_checked(&self) -> Option<usize> {
+                        tls_codec::Size::tls_serialized_len_checked(*self)
+                    }
                 }
             }
         }
diff --git a/tls_codec/derive/tests/decode.rs b/tls_codec/derive/tests/decode.rs
index 0238cf4a6..a3135ffe6 100644
--- a/tls_codec/derive/tests/decode.rs
+++ b/tls_codec/derive/tests/decode.rs
@@ -273,6 +273,10 @@ mod custom {
         TlsByteSliceU32(v).tls_serialized_len()
     }
 
+    pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {
+        TlsByteSliceU32(v).tls_serialized_len_checked()
+    }
+
     pub fn tls_serialize<W: Write>(v: &[u8], writer: &mut W) -> Result<usize, tls_codec::Error> {
         TlsByteSliceU32(v).tls_serialize(writer)
     }
@@ -297,6 +301,10 @@ mod custom_bytes {
         TlsByteSliceU32(v).tls_serialized_len()
     }
 
+    pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {
+        TlsByteSliceU32(v).tls_serialized_len_checked()
+    }
+
     pub fn tls_serialize<W: Write>(v: &[u8], writer: &mut W) -> Result<usize, tls_codec::Error> {
         TlsByteSliceU32(v).tls_serialize(writer)
     }
diff --git a/tls_codec/derive/tests/decode_bytes.rs b/tls_codec/derive/tests/decode_bytes.rs
index 2c42f0638..e78fe9801 100644
--- a/tls_codec/derive/tests/decode_bytes.rs
+++ b/tls_codec/derive/tests/decode_bytes.rs
@@ -90,6 +90,10 @@ mod custom {
         v.tls_serialized_len()
     }
 
+    pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {
+        v.tls_serialized_len_checked()
+    }
+
     pub fn tls_serialize(v: &[u8]) -> Result<Vec<u8>, tls_codec::Error> {
         v.tls_serialize()
     }
diff --git a/tls_codec/derive/tests/encode.rs b/tls_codec/derive/tests/encode.rs
index 4830e99a9..7cd6f31f2 100644
--- a/tls_codec/derive/tests/encode.rs
+++ b/tls_codec/derive/tests/encode.rs
@@ -131,6 +131,10 @@ mod custom {
         TlsByteSliceU32(v).tls_serialized_len()
     }
 
+    pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {
+        TlsByteSliceU32(v).tls_serialized_len_checked()
+    }
+
     pub fn tls_serialize<W: Write>(v: &[u8], writer: &mut W) -> Result<usize, tls_codec::Error> {
         TlsByteSliceU32(v).tls_serialize(writer)
     }
diff --git a/tls_codec/derive/tests/encode_bytes.rs b/tls_codec/derive/tests/encode_bytes.rs
index 089549f99..4052e249b 100644
--- a/tls_codec/derive/tests/encode_bytes.rs
+++ b/tls_codec/derive/tests/encode_bytes.rs
@@ -107,6 +107,10 @@ mod custom {
         v.tls_serialized_len()
     }
 
+    pub fn tls_serialized_len_checked(v: &[u8]) -> Option<usize> {
+        v.tls_serialized_len_checked()
+    }
+
     pub fn tls_serialize(v: &[u8]) -> Result<Vec<u8>, tls_codec::Error> {
         v.tls_serialize()
     }
diff --git a/tls_codec/src/arrays.rs b/tls_codec/src/arrays.rs
index 3e6200896..b974778c1 100644
--- a/tls_codec/src/arrays.rs
+++ b/tls_codec/src/arrays.rs
@@ -35,12 +35,8 @@ impl<const LEN: usize> Deserialize for [u8; LEN] {
 impl<const LEN: usize> DeserializeBytes for [u8; LEN] {
     #[inline]
     fn tls_deserialize_bytes(bytes: &[u8]) -> Result<(Self, &[u8]), Error> {
-        let out = bytes
-            .get(..LEN)
-            .ok_or(Error::EndOfStream)?
-            .try_into()
-            .map_err(|_| Error::EndOfStream)?;
-        Ok((out, &bytes[LEN..]))
+        let (out, remainder) = bytes.split_at_checked(LEN).ok_or(Error::EndOfStream)?;
+        Ok((out.try_into().map_err(|_| Error::EndOfStream)?, remainder))
     }
 }
 
@@ -55,4 +51,8 @@ impl<const LEN: usize> Size for [u8; LEN] {
     fn tls_serialized_len(&self) -> usize {
         LEN
     }
+    #[inline]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        Some(LEN)
+    }
 }
diff --git a/tls_codec/src/lib.rs b/tls_codec/src/lib.rs
index a6e61e0bc..27bb85679 100644
--- a/tls_codec/src/lib.rs
+++ b/tls_codec/src/lib.rs
@@ -107,7 +107,11 @@ mod serialize_bytes {
     /// efficiently serialized.
     /// This allows to collect the length of a serialized structure before allocating
     /// memory.
+    #[hax_lib::attributes]
     pub trait Size {
+        #[hax_lib::requires(true)]
+        fn tls_serialized_len_checked(&self) -> Option<usize>;
+        #[hax_lib::requires(true)]
         fn tls_serialized_len(&self) -> usize;
     }
 
@@ -115,8 +119,10 @@ mod serialize_bytes {
     ///
     /// The trait provides one function:
     /// * `tls_serialize` that returns a byte vector
+    #[hax_lib::attributes]
     pub trait SerializeBytes: Size {
         /// Serialize `self` and return it as a byte vector.
+        #[hax_lib::requires(true)]
         fn tls_serialize(&self) -> Result<Vec<u8>, Error>;
     }
 }
@@ -146,10 +152,12 @@ impl From<std::io::Error> for Error {
 /// The trait provides two functions:
 /// * `tls_serialize` that takes a buffer to write the serialization to
 /// * `tls_serialize_detached` that returns a byte vector
+#[hax_lib::attributes]
 pub trait Serialize: Size {
     /// Serialize `self` and write it to the `writer`.
     /// The function returns the number of bytes written to `writer`.
     #[cfg(feature = "std")]
+    #[hax_lib::requires(true)]
     fn tls_serialize<W: Write>(&self, writer: &mut W) -> Result<usize, Error>;
 
     /// Serialize `self` and return it as a byte vector.
@@ -164,6 +172,7 @@ pub trait Serialize: Size {
 fn tls_serialize_detached_default<T: ?Sized + Serialize>(s: &T) -> Result<Vec<u8>, Error> {
     let mut buffer = Vec::with_capacity(s.tls_serialized_len());
     let written = s.tls_serialize(&mut buffer)?;
+    #[cfg(not(hax))]
     debug_assert_eq!(
         written,
         buffer.len(),
@@ -184,6 +193,7 @@ fn tls_serialize_detached_default<T: ?Sized + Serialize>(s: &T) -> Result<Vec<u8
 
 /// The `Deserialize` trait defines functions to deserialize a byte slice to a
 /// struct or enum.
+#[hax_lib::attributes]
 pub trait Deserialize: Size {
     /// This function deserializes the `bytes` from the provided a [`std::io::Read`]
     /// and returns the populated struct.
@@ -192,6 +202,7 @@ pub trait Deserialize: Size {
     ///
     /// Returns an error if one occurs during deserialization.
     #[cfg(feature = "std")]
+    #[hax_lib::requires(true)]
     fn tls_deserialize<R: Read>(bytes: &mut R) -> Result<Self, Error>
     where
         Self: Sized;
@@ -226,6 +237,7 @@ fn tls_deserialize_exact_default<T: Deserialize>(bytes: impl AsRef<[u8]>) -> Res
 /// The `DeserializeBytes` trait defines functions to deserialize a byte slice
 /// to a struct or enum. In contrast to [`Deserialize`], this trait operates
 /// directly on byte slices and can return any remaining bytes.
+#[hax_lib::attributes]
 pub trait DeserializeBytes: Size {
     /// This function deserializes the `bytes` from the provided a `&[u8]`
     /// and returns the populated struct, as well as the remaining slice.
@@ -233,6 +245,7 @@ pub trait DeserializeBytes: Size {
     /// In order to get the amount of bytes read, use [`Size::tls_serialized_len`].
     ///
     /// Returns an error if one occurs during deserialization.
+    #[hax_lib::requires(true)]
     fn tls_deserialize_bytes(bytes: &[u8]) -> Result<(Self, &[u8]), Error>
     where
         Self: Sized;
@@ -280,6 +293,7 @@ impl From<U24> for usize {
     fn from(value: U24) -> usize {
         const LEN: usize = core::mem::size_of::<usize>();
         let mut usize_bytes = [0u8; LEN];
+        hax_lib::assume!(usize_bytes.len() == LEN); // https://github.com/cryspen/hax/issues/1702
         usize_bytes[LEN - 3..].copy_from_slice(&value.0);
         usize::from_be_bytes(usize_bytes)
     }
@@ -288,13 +302,14 @@ impl From<U24> for usize {
 impl TryFrom<usize> for U24 {
     type Error = Error;
 
-    fn try_from(value: usize) -> Result<Self, Self::Error> {
+    fn try_from(value: usize) -> Result<Self, Error> {
         const LEN: usize = core::mem::size_of::<usize>();
         // In practice, our usages of this conversion should never be invalid, as the values
         // have to come from `TryFrom<U24> for usize`.
         if value > (1 << 24) - 1 {
             Err(Error::LibraryError)
         } else {
+            hax_lib::assume!(value.to_be_bytes().len() == LEN); // https://github.com/cryspen/hax/issues/1702
             Ok(U24(value.to_be_bytes()[LEN - 3..].try_into()?))
         }
     }
diff --git a/tls_codec/src/primitives.rs b/tls_codec/src/primitives.rs
index 5fac21b1d..17b17e0a3 100644
--- a/tls_codec/src/primitives.rs
+++ b/tls_codec/src/primitives.rs
@@ -12,11 +12,20 @@ use std::io::{Read, Write};
 
 impl<T: Size> Size for Option<T> {
     #[inline]
-    fn tls_serialized_len(&self) -> usize {
-        1 + match self {
-            Some(v) => v.tls_serialized_len(),
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        1usize.checked_add(match self {
+            Some(v) => v.tls_serialized_len_checked()?,
             None => 0,
-        }
+        })
+    }
+    #[inline]
+    fn tls_serialized_len(&self) -> usize {
+        1usize
+            .checked_add(match self {
+                Some(v) => v.tls_serialized_len(),
+                None => 0,
+            })
+            .unwrap_or(0)
     }
 }
 
@@ -25,6 +34,10 @@ impl<T: Size> Size for &Option<T> {
     fn tls_serialized_len(&self) -> usize {
         (*self).tls_serialized_len()
     }
+    #[inline]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        (*self).tls_serialized_len_checked()
+    }
 }
 
 impl<T: Serialize> Serialize for Option<T> {
@@ -33,8 +46,11 @@ impl<T: Serialize> Serialize for Option<T> {
         match self {
             Some(e) => {
                 let written = writer.write(&[1])?;
+                hax_lib::assume!(written == 1);
                 debug_assert_eq!(written, 1);
-                e.tls_serialize(writer).map(|l| l + 1)
+                e.tls_serialize(writer)?
+                    .checked_add(1)
+                    .ok_or(Error::LibraryError)
             }
             None => {
                 writer.write_all(&[0])?;
@@ -49,7 +65,11 @@ impl<T: SerializeBytes> SerializeBytes for Option<T> {
     fn tls_serialize(&self) -> Result<Vec<u8>, Error> {
         match self {
             Some(e) => {
-                let mut out = Vec::with_capacity(e.tls_serialized_len() + 1);
+                let mut out = Vec::with_capacity(
+                    e.tls_serialized_len()
+                        .checked_add(1)
+                        .ok_or(Error::LibraryError)?,
+                );
                 out.push(1);
                 // Not inlining serialized_e is a workaround for
                 // https://github.com/cryspen/hax/issues/1584
@@ -160,6 +180,7 @@ macro_rules! impl_unsigned {
             #[inline]
             fn tls_serialize<W: Write>(&self, writer: &mut W) -> Result<usize, Error> {
                 let written = writer.write(&self.to_be_bytes())?;
+                #[cfg(not(hax))]
                 debug_assert_eq!(written, $bytes);
                 Ok(written)
             }
@@ -178,6 +199,10 @@ macro_rules! impl_unsigned {
             fn tls_serialized_len(&self) -> usize {
                 $bytes
             }
+            #[inline]
+            fn tls_serialized_len_checked(&self) -> Option<usize> {
+                Some($bytes)
+            }
         }
 
         impl Size for &$t {
@@ -185,6 +210,10 @@ macro_rules! impl_unsigned {
             fn tls_serialized_len(&self) -> usize {
                 (*self).tls_serialized_len()
             }
+            #[inline]
+            fn tls_serialized_len_checked(&self) -> Option<usize> {
+                (*self).tls_serialized_len_checked()
+            }
         }
     };
 }
@@ -236,7 +265,10 @@ where
     #[inline(always)]
     fn tls_serialize<W: Write>(&self, writer: &mut W) -> Result<usize, Error> {
         let written = self.0.tls_serialize(writer)?;
-        self.1.tls_serialize(writer).map(|l| l + written)
+        self.1
+            .tls_serialize(writer)?
+            .checked_add(written)
+            .ok_or(Error::LibraryError)
     }
 }
 
@@ -245,9 +277,18 @@ where
     T: Size,
     U: Size,
 {
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        self.0
+            .tls_serialized_len_checked()?
+            .checked_add(self.1.tls_serialized_len_checked()?)
+    }
     #[inline(always)]
     fn tls_serialized_len(&self) -> usize {
-        self.0.tls_serialized_len() + self.1.tls_serialized_len()
+        self.0
+            .tls_serialized_len()
+            .checked_add(self.1.tls_serialized_len())
+            .unwrap_or(0)
     }
 }
 
@@ -292,9 +333,14 @@ where
     #[cfg(feature = "std")]
     #[inline(always)]
     fn tls_serialize<W: Write>(&self, writer: &mut W) -> Result<usize, Error> {
-        let mut written = self.0.tls_serialize(writer)?;
-        written += self.1.tls_serialize(writer)?;
-        self.2.tls_serialize(writer).map(|l| l + written)
+        let written = self.0.tls_serialize(writer)?;
+        let written = written
+            .checked_add(self.1.tls_serialize(writer)?)
+            .ok_or(Error::LibraryError)?;
+        self.2
+            .tls_serialize(writer)?
+            .checked_add(written)
+            .ok_or(Error::LibraryError)
     }
 }
 
@@ -304,9 +350,21 @@ where
     U: Size,
     V: Size,
 {
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        self.0
+            .tls_serialized_len_checked()?
+            .checked_add(self.1.tls_serialized_len_checked()?)?
+            .checked_add(self.2.tls_serialized_len_checked()?)
+    }
     #[inline(always)]
     fn tls_serialized_len(&self) -> usize {
-        self.0.tls_serialized_len() + self.1.tls_serialized_len() + self.2.tls_serialized_len()
+        self.0
+            .tls_serialized_len()
+            .checked_add(self.1.tls_serialized_len())
+            .unwrap_or(0)
+            .checked_add(self.2.tls_serialized_len())
+            .unwrap_or(0)
     }
 }
 
@@ -315,6 +373,10 @@ impl Size for () {
     fn tls_serialized_len(&self) -> usize {
         0
     }
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        Some(0)
+    }
 }
 
 impl Deserialize for () {
@@ -344,6 +406,10 @@ impl<T> Size for PhantomData<T> {
     fn tls_serialized_len(&self) -> usize {
         0
     }
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        Some(0)
+    }
 }
 
 impl<T> Deserialize for PhantomData<T> {
@@ -381,6 +447,10 @@ impl<T: Size> Size for Box<T> {
     fn tls_serialized_len(&self) -> usize {
         self.as_ref().tls_serialized_len()
     }
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        self.as_ref().tls_serialized_len_checked()
+    }
 }
 
 impl<T: Serialize> Serialize for Box<T> {
diff --git a/tls_codec/src/quic_vec.rs b/tls_codec/src/quic_vec.rs
index 194c8ec14..2ede8f221 100644
--- a/tls_codec/src/quic_vec.rs
+++ b/tls_codec/src/quic_vec.rs
@@ -25,6 +25,7 @@ use serde::{Deserialize as SerdeDeserialize, Serialize as SerdeSerialize};
 use crate::{DeserializeBytes, Error, SerializeBytes, Size};
 
 #[cfg(not(feature = "mls"))]
+#[hax_lib::fstar::verification_status(lax)] // Need lemma for (1 << 62) >= 1
 const MAX_LEN: u64 = (1 << 62) - 1;
 #[cfg(not(feature = "mls"))]
 const MAX_LEN_LEN_LOG: usize = 3;
@@ -50,6 +51,7 @@ fn calculate_length(len_len_byte: u8) -> Result<(usize, usize), Error> {
     let length: usize = (len_len_byte & 0x3F).into();
     let len_len_log = (len_len_byte >> 6).into();
     if !cfg!(fuzzing) {
+        #[cfg(not(hax))]
         debug_assert!(len_len_log <= MAX_LEN_LEN_LOG);
     }
     if len_len_log > MAX_LEN_LEN_LOG {
@@ -87,6 +89,7 @@ fn read_variable_length_bytes(bytes: &[u8]) -> Result<((usize, usize), &[u8]), E
 #[inline(always)]
 fn length_encoding_bytes(length: u64) -> Result<usize, Error> {
     if !cfg!(fuzzing) {
+        #[cfg(not(hax))]
         debug_assert!(length <= MAX_LEN);
     }
     if length > MAX_LEN {
@@ -130,6 +133,7 @@ pub fn write_variable_length(content_length: usize) -> Result<Vec<u8>, Error> {
     let mut len = content_length;
     let l = length_bytes.len();
     for i in 0..l {
+        hax_lib::loop_invariant!(|_: usize| length_bytes.len() == l);
         // Not using |= is a workaround for https://github.com/cryspen/hax/issues/1512
         length_bytes[l - i - 1] = length_bytes[l - i - 1] | ((len & 0xFF) as u8);
         len >>= 8;
@@ -143,6 +147,10 @@ impl<T: Size> Size for Vec<T> {
     fn tls_serialized_len(&self) -> usize {
         self.as_slice().tls_serialized_len()
     }
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        self.as_slice().tls_serialized_len_checked()
+    }
 }
 
 impl<T: Size> Size for &Vec<T> {
@@ -150,6 +158,10 @@ impl<T: Size> Size for &Vec<T> {
     fn tls_serialized_len(&self) -> usize {
         (*self).tls_serialized_len()
     }
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        (*self).tls_serialized_len_checked()
+    }
 }
 
 impl<T: DeserializeBytes> DeserializeBytes for Vec<T> {
@@ -165,9 +177,12 @@ impl<T: DeserializeBytes> DeserializeBytes for Vec<T> {
         let mut result = Vec::new();
         let mut read = len_len;
         while (read - len_len) < length {
+            hax_lib::loop_invariant!(read >= len_len);
             let (element, next_remainder) = T::tls_deserialize_bytes(remainder)?;
             remainder = next_remainder;
-            read += element.tls_serialized_len();
+            read = read
+                .checked_add(element.tls_serialized_len())
+                .ok_or(Error::LibraryError)?;
             result.push(element);
         }
         Ok((result, remainder))
@@ -180,6 +195,8 @@ impl<T: SerializeBytes> SerializeBytes for &[T] {
         // We need to pre-compute the length of the content.
         // This requires more computations but the other option would be to buffer
         // the entire content, which can end up requiring a lot of memory.
+
+        hax_lib::fstar!("admit ()"); // https://github.com/cryspen/hax/issues/1700
         let content_length = self.iter().fold(0, |acc, e| acc + e.tls_serialized_len());
         let mut length = write_variable_length(content_length)?;
         let len_len = length.len();
@@ -216,16 +233,24 @@ impl<T: SerializeBytes> SerializeBytes for Vec<T> {
     }
 }
 
+#[allow(clippy::manual_try_fold)]
+fn serialized_len_checked_slice<T: Size>(s: &[T]) -> Option<usize> {
+    hax_lib::fstar!("admit ()"); // https://github.com/cryspen/hax/issues/1700
+    let content_length = s.iter().fold(Some(0usize), |acc, e| {
+        acc?.checked_add(e.tls_serialized_len_checked()?)
+    })?;
+    let len_len = length_encoding_bytes(content_length as u64).ok()?;
+    content_length.checked_add(len_len)
+}
+
 impl<T: Size> Size for &[T] {
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        serialized_len_checked_slice(self)
+    }
     #[inline(always)]
     fn tls_serialized_len(&self) -> usize {
-        let content_length = self.iter().fold(0, |acc, e| acc + e.tls_serialized_len());
-        let len_len = length_encoding_bytes(content_length as u64).unwrap_or({
-            // We can't do anything about the error unless we change the trait.
-            // Let's say there's no content for now.
-            0
-        });
-        content_length + len_len
+        serialized_len_checked_slice(self).unwrap_or(0)
     }
 }
 
@@ -328,18 +353,19 @@ impl From<VLBytes> for Vec<u8> {
 }
 
 #[inline(always)]
-fn tls_serialize_bytes_len(bytes: &[u8]) -> usize {
+fn tls_serialize_bytes_len(bytes: &[u8]) -> Option<usize> {
     let content_length = bytes.len();
-    let len_len = length_encoding_bytes(content_length as u64).unwrap_or({
-        // We can't do anything about the error. Let's say there's no content.
-        0
-    });
-    content_length + len_len
+    let len_len = length_encoding_bytes(content_length as u64).ok()?;
+    content_length.checked_add(len_len)
 }
 
 impl Size for VLBytes {
     #[inline(always)]
     fn tls_serialized_len(&self) -> usize {
+        tls_serialize_bytes_len(self.as_slice()).unwrap_or(0)
+    }
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
         tls_serialize_bytes_len(self.as_slice())
     }
 }
@@ -353,6 +379,7 @@ impl DeserializeBytes for VLBytes {
         }
 
         if !cfg!(fuzzing) {
+            #[cfg(not(hax))]
             debug_assert!(
                 length <= MAX_LEN as usize,
                 "Trying to allocate {length} bytes. Only {MAX_LEN} allowed.",
@@ -363,11 +390,12 @@ impl DeserializeBytes for VLBytes {
                 "Trying to allocate {length} bytes. Only {MAX_LEN} allowed.",
             )));
         }
-        match remainder.get(..length).ok_or(Error::EndOfStream) {
-            Ok(vec) => Ok((Self { vec: vec.to_vec() }, &remainder[length..])),
+        match remainder.split_at_checked(length).ok_or(Error::EndOfStream) {
+            Ok((vec, remainder)) => Ok((Self { vec: vec.to_vec() }, remainder)),
             Err(_e) => {
                 let remaining_len = remainder.len();
                 if !cfg!(fuzzing) {
+                    #[cfg(not(hax))]
                     debug_assert_eq!(
                         remaining_len, length,
                         "Expected to read {length} bytes but {remaining_len} were read.",
@@ -386,6 +414,10 @@ impl Size for &VLBytes {
     fn tls_serialized_len(&self) -> usize {
         (*self).tls_serialized_len()
     }
+    #[inline(always)]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
+        (*self).tls_serialized_len_checked()
+    }
 }
 
 pub struct VLByteSlice<'a>(pub &'a [u8]);
@@ -410,15 +442,23 @@ impl VLByteSlice<'_> {
 impl Size for &VLByteSlice<'_> {
     #[inline]
     fn tls_serialized_len(&self) -> usize {
+        tls_serialize_bytes_len(self.0).unwrap_or(0)
+    }
+    #[inline]
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
         tls_serialize_bytes_len(self.0)
     }
 }
 
 impl Size for VLByteSlice<'_> {
     #[inline]
-    fn tls_serialized_len(&self) -> usize {
+    fn tls_serialized_len_checked(&self) -> Option<usize> {
         tls_serialize_bytes_len(self.0)
     }
+    #[inline]
+    fn tls_serialized_len(&self) -> usize {
+        tls_serialize_bytes_len(self.0).unwrap_or(0)
+    }
 }
 
 #[cfg(feature = "std")]
@@ -470,8 +510,11 @@ pub mod rw {
             let mut result = Vec::new();
             let mut read = len_len;
             while (read - len_len) < length {
+                hax_lib::loop_invariant!(read >= len_len);
                 let element = T::tls_deserialize(bytes)?;
-                read += element.tls_serialized_len();
+                read = read
+                    .checked_add(element.tls_serialized_len())
+                    .ok_or(Error::LibraryError)?;
                 result.push(element);
             }
             Ok(result)
@@ -502,6 +545,7 @@ pub mod rw {
             // We need to pre-compute the length of the content.
             // This requires more computations but the other option would be to buffer
             // the entire content, which can end up requiring a lot of memory.
+            hax_lib::fstar!("admit ()"); // https://github.com/cryspen/hax/issues/1700
             let content_length = self.iter().fold(0, |acc, e| acc + e.tls_serialized_len());
             let len_len = write_length(writer, content_length)?;
 
@@ -543,6 +587,7 @@ mod rw_bytes {
         let content_length = bytes.len();
 
         if !cfg!(fuzzing) {
+            #[cfg(not(hax))]
             debug_assert!(
                 content_length as u64 <= MAX_LEN,
                 "Vector can't be encoded. It's too large. {content_length} >= {MAX_LEN}",
@@ -559,7 +604,9 @@ mod rw_bytes {
         // Now serialize the elements
         writer.write_all(bytes)?;
 
-        Ok(content_length + len_len)
+        content_length
+            .checked_add(len_len)
+            .ok_or(Error::LibraryError)
     }
 
     impl Serialize for VLBytes {
@@ -584,6 +631,7 @@ mod rw_bytes {
             }
 
             if !cfg!(fuzzing) {
+                #[cfg(not(hax))]
                 debug_assert!(
                     length <= MAX_LEN as usize,
                     "Trying to allocate {length} bytes. Only {MAX_LEN} allowed.",
@@ -658,6 +706,9 @@ mod secret_bytes {
         fn tls_serialized_len(&self) -> usize {
             self.0.tls_serialized_len()
         }
+        fn tls_serialized_len_checked(&self) -> Option<usize> {
+            self.0.tls_serialized_len_checked()
+        }
     }
 
     impl DeserializeBytes for SecretVLBytes {
diff --git a/tls_codec/src/tls_vec.rs b/tls_codec/src/tls_vec.rs
index 3b0f9c55d..17a5dd123 100644
--- a/tls_codec/src/tls_vec.rs
+++ b/tls_codec/src/tls_vec.rs
@@ -19,10 +19,11 @@ macro_rules! impl_size {
     ($self:ident, $size:ty, $name:ident, $len_len:literal) => {
         /// The serialized len
         #[inline(always)]
-        fn tls_serialized_length(&$self) -> usize {
+        fn tls_serialized_length(&$self) -> Option<usize> {
+            hax_lib::fstar!("admit ()"); // https://github.com/cryspen/hax/issues/1700
             $self.as_slice()
                 .iter()
-                .fold($len_len, |acc, e| acc + e.tls_serialized_len())
+                .fold(Some($len_len), |acc, e| acc?.checked_add(e.tls_serialized_len_checked()?))
         }
     }
 }
@@ -31,8 +32,8 @@ macro_rules! impl_byte_size {
     ($self:ident, $size:ty, $name:ident, $len_len:literal) => {
         /// The serialized len
         #[inline(always)]
-        fn tls_serialized_byte_length(&$self) -> usize {
-            $self.as_slice().len() + $len_len
+        fn tls_serialized_byte_length(&$self) -> Option<usize> {
+            $self.as_slice().len().checked_add($len_len)
         }
     }
 }
@@ -63,7 +64,7 @@ macro_rules! impl_byte_deserialize {
         #[inline(always)]
         fn deserialize_bytes_bytes(bytes: &[u8]) -> Result<(Self, &[u8]), Error> {
             let (type_len, remainder) = <$size>::tls_deserialize_bytes(bytes)?;
-            let len = type_len.try_into().unwrap();
+            let len: usize = type_len.try_into().unwrap();
             // When fuzzing we limit the maximum size to allocate.
             // XXX: We should think about a configurable limit for the allocation
             //      here.
@@ -74,9 +75,8 @@ macro_rules! impl_byte_deserialize {
                     u16::MAX
                 )));
             }
-            let vec = bytes
-                .get($len_len..len + $len_len)
-                .ok_or(Error::EndOfStream)?;
+            let end = len.checked_add($len_len).ok_or(Error::LibraryError)?;
+            let vec = bytes.get($len_len..end).ok_or(Error::EndOfStream)?;
             let result = Self { vec: vec.to_vec() };
             Ok((result, &remainder.get(len..).ok_or(Error::EndOfStream)?))
         }
@@ -93,8 +93,11 @@ macro_rules! impl_deserialize {
             let mut read = len.tls_serialized_len();
             let len_len = read;
             while (read - len_len) < len.try_into().unwrap() {
+                hax_lib::loop_invariant!(read >= len_len);
                 let element = T::tls_deserialize(bytes)?;
-                read += element.tls_serialized_len();
+                read = read
+                    .checked_add(element.tls_serialized_len())
+                    .ok_or(Error::LibraryError)?;
                 result.push(element);
             }
             Ok(result)
@@ -111,9 +114,12 @@ macro_rules! impl_deserialize_bytes {
             let mut read = len.tls_serialized_len();
             let len_len = read;
             while (read - len_len) < len.try_into().unwrap() {
+                hax_lib::loop_invariant!(read >= len_len);
                 let (element, next_remainder) = T::tls_deserialize_bytes(remainder)?;
                 remainder = next_remainder;
-                read += element.tls_serialized_len();
+                read = read
+                    .checked_add(element.tls_serialized_len())
+                    .ok_or(Error::LibraryError)?;
                 result.push(element);
             }
             Ok((result, remainder))
@@ -130,8 +136,11 @@ macro_rules! impl_serialize {
             // large and write it out.
             let (tls_serialized_len, byte_length) = $self.get_content_lengths()?;
 
+            hax_lib::fstar!("admit ()"); // Need to prove unwrap for usize to U24
             let mut written = <$size as Serialize>::tls_serialize(&<$size>::try_from(byte_length).unwrap(), writer)?;
 
+
+            hax_lib::fstar!("admit ()"); // https://github.com/cryspen/hax/issues/1700
             // Now serialize the elements
             for e in $self.as_slice().iter() {
                 written += e.tls_serialize(writer)?;
@@ -152,10 +161,11 @@ macro_rules! impl_byte_serialize {
             // large and write it out.
             let (tls_serialized_len, byte_length) = $self.get_content_lengths()?;
 
+            hax_lib::fstar!("admit ()"); // Need to prove unwrap for usize to U24
             let mut written = <$size as Serialize>::tls_serialize(&<$size>::try_from(byte_length).unwrap(), writer)?;
 
             // Now serialize the elements
-            written += writer.write($self.as_slice())?;
+            written = written.checked_add(writer.write($self.as_slice())?).ok_or(Error::LibraryError)?;
 
             $self.assert_written_bytes(tls_serialized_len, written)?;
             Ok(written)
@@ -168,9 +178,9 @@ macro_rules! impl_serialize_common {
         $(#[$std_enabled])?
         fn get_content_lengths(&$self) -> Result<(usize, usize), Error> {
             let tls_serialized_len = $self.tls_serialized_len();
-            let byte_length = tls_serialized_len - $len_len;
-
+            let byte_length = tls_serialized_len.checked_sub($len_len).ok_or(Error::InvalidVectorLength)?;
             let max_len = <$size>::MAX.try_into().unwrap();
+            #[cfg(not(hax))]
             debug_assert!(
                 byte_length <= max_len,
                 "Vector length can't be encoded in the vector length a {} >= {}",
@@ -185,6 +195,7 @@ macro_rules! impl_serialize_common {
 
         $(#[$std_enabled])?
         fn assert_written_bytes(&$self, tls_serialized_len: usize, written: usize) -> Result<(), Error> {
+            #[cfg(not(hax))]
             debug_assert_eq!(
                 written, tls_serialized_len,
                 "{} bytes should have been serialized but {} were written",
@@ -207,6 +218,7 @@ macro_rules! impl_serialize_bytes_bytes {
             let (tls_serialized_len, byte_length) = $self.get_content_lengths()?;
 
             let mut vec = Vec::<u8>::with_capacity(tls_serialized_len);
+            hax_lib::fstar!("admit ()"); // Need to prove unwrap for usize to U24
             let length_vec = <$size as SerializeBytes>::tls_serialize(&byte_length.try_into().unwrap())?;
             let mut written = length_vec.len();
             vec.extend_from_slice(&length_vec);
@@ -234,6 +246,10 @@ macro_rules! impl_tls_vec_codec_generic {
         impl<T: $($bounds + )* Size> Size for $name<T> {
             #[inline]
             fn tls_serialized_len(&self) -> usize {
+                self.tls_serialized_length().unwrap_or(0)
+            }
+            #[inline]
+            fn tls_serialized_len_checked(&self) -> Option<usize> {
                 self.tls_serialized_length()
             }
         }
@@ -248,6 +264,10 @@ macro_rules! impl_tls_vec_codec_generic {
         impl<T: $($bounds + )* Size> Size for &$name<T> {
             #[inline]
             fn tls_serialized_len(&self) -> usize {
+                self.tls_serialized_length().unwrap_or(0)
+            }
+            #[inline]
+            fn tls_serialized_len_checked(&self) -> Option<usize> {
                 self.tls_serialized_length()
             }
         }
@@ -278,9 +298,12 @@ macro_rules! impl_tls_vec_codec_bytes {
 
         impl Size for $name {
             #[inline]
-            fn tls_serialized_len(&self) -> usize {
+            fn tls_serialized_len_checked(&self) -> Option<usize> {
                 self.tls_serialized_byte_length()
             }
+            fn tls_serialized_len(&self) -> usize {
+                self.tls_serialized_byte_length().unwrap_or(0)
+            }
         }
 
         impl Serialize for &$name {
@@ -292,9 +315,13 @@ macro_rules! impl_tls_vec_codec_bytes {
 
         impl Size for &$name {
             #[inline]
-            fn tls_serialized_len(&self) -> usize {
+            fn tls_serialized_len_checked(&self) -> Option<usize> {
                 self.tls_serialized_byte_length()
             }
+            #[inline]
+            fn tls_serialized_len(&self) -> usize {
+                self.tls_serialized_byte_length().unwrap_or(0)
+            }
         }
 
         impl Deserialize for $name {
@@ -434,10 +461,12 @@ macro_rules! impl_tls_vec_generic {
             }
         }
 
+        #[hax_lib::attributes]
         impl<T: $($bounds + )*> core::ops::Index<usize> for $name<T> {
             type Output = T;
 
             #[inline]
+            #[hax_lib::requires(i < self.vec.len())]
             fn index(&self, i: usize) -> &T {
                 self.vec.index(i)
             }
@@ -445,6 +474,7 @@ macro_rules! impl_tls_vec_generic {
 
         impl<T: $($bounds + )* core::cmp::PartialEq> core::cmp::PartialEq for $name<T> {
             fn eq(&self, other: &Self) -> bool {
+                hax_lib::fstar!("admit ()"); // https://github.com/cryspen/hax/issues/1704
                 self.vec.eq(&other.vec)
             }
         }
@@ -633,10 +663,12 @@ macro_rules! impl_tls_vec {
             }
         }
 
+        #[hax_lib::attributes]
         impl core::ops::Index<usize> for $name {
             type Output = u8;
 
             #[inline]
+            #[hax_lib::requires(i < self.vec.len())]
             fn index(&self, i: usize) -> &u8 {
                 self.vec.index(i)
             }
@@ -938,16 +970,24 @@ macro_rules! impl_tls_byte_slice {
 
         impl<'a> Size for &$name<'a> {
             #[inline]
-            fn tls_serialized_len(&self) -> usize {
+            fn tls_serialized_len_checked(&self) -> Option<usize> {
                 self.tls_serialized_byte_length()
             }
+            #[inline]
+            fn tls_serialized_len(&self) -> usize {
+                self.tls_serialized_byte_length().unwrap_or(0)
+            }
         }
 
         impl<'a> Size for $name<'a> {
             #[inline]
-            fn tls_serialized_len(&self) -> usize {
+            fn tls_serialized_len_checked(&self) -> Option<usize> {
                 self.tls_serialized_byte_length()
             }
+            #[inline]
+            fn tls_serialized_len(&self) -> usize {
+                self.tls_serialized_byte_length().unwrap_or(0)
+            }
         }
     };
 }
@@ -994,16 +1034,24 @@ macro_rules! impl_tls_slice {
 
         impl<'a, T: Size> Size for &$name<'a, T> {
             #[inline]
-            fn tls_serialized_len(&self) -> usize {
+            fn tls_serialized_len_checked(&self) -> Option<usize> {
                 self.tls_serialized_length()
             }
+            #[inline]
+            fn tls_serialized_len(&self) -> usize {
+                self.tls_serialized_length().unwrap_or(0)
+            }
         }
 
         impl<'a, T: Size> Size for $name<'a, T> {
             #[inline]
-            fn tls_serialized_len(&self) -> usize {
+            fn tls_serialized_len_checked(&self) -> Option<usize> {
                 self.tls_serialized_length()
             }
+            #[inline]
+            fn tls_serialized_len(&self) -> usize {
+                self.tls_serialized_length().unwrap_or(0)
+            }
         }
     };
 }