diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst
index eb79bb57f..1bab0a7b4 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst
@@ -261,8 +261,6 @@ let compress_then_serialize_u
   let hax_temp_output:Prims.unit = result in
   out
 
-#push-options "--admit_smt_queries true"
-
 let deserialize_then_decompress_u
       (v_K v_CIPHERTEXT_SIZE v_U_COMPRESSION_FACTOR: usize)
       (#v_Vector: Type0)
@@ -321,9 +319,9 @@ let deserialize_then_decompress_u
           in
           u_as_ntt)
   in
-  u_as_ntt
-
-#pop-options
+  let result:t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K = u_as_ntt in
+  let _:Prims.unit = admit () (* Panic freedom *) in
+  result
 
 let deserialize_secret_key
       (v_K: usize)
@@ -374,7 +372,7 @@ let deserialize_secret_key
   let _:Prims.unit = admit () (* Panic freedom *) in
   result
 
-#push-options "--admit_smt_queries true"
+#push-options "--z3rlimit 200"
 
 let serialize_secret_key
       (v_K v_OUT_LEN: usize)
@@ -431,7 +429,9 @@ let serialize_secret_key
           <:
           t_Array u8 v_OUT_LEN)
   in
-  out
+  let result:t_Array u8 v_OUT_LEN = out in
+  let _:Prims.unit = admit () (* Panic freedom *) in
+  result
 
 #pop-options
 
@@ -486,8 +486,6 @@ let serialize_public_key
   let _:Prims.unit = admit () (* Panic freedom *) in
   result
 
-#push-options "--admit_smt_queries true"
-
 let decrypt_unpacked
       (v_K v_CIPHERTEXT_SIZE v_VECTOR_U_ENCODED_SIZE v_U_COMPRESSION_FACTOR v_V_COMPRESSION_FACTOR:
           usize)
@@ -519,8 +517,6 @@ let decrypt_unpacked
   in
   Libcrux_ml_kem.Serialize.compress_then_serialize_message #v_Vector message
 
-#pop-options
-
 let decrypt
       (v_K v_CIPHERTEXT_SIZE v_VECTOR_U_ENCODED_SIZE v_U_COMPRESSION_FACTOR v_V_COMPRESSION_FACTOR:
           usize)
@@ -552,7 +548,7 @@ let decrypt
   let _:Prims.unit = admit () (* Panic freedom *) in
   result
 
-#push-options "--admit_smt_queries true"
+#push-options "--z3rlimit 200"
 
 let encrypt_unpacked
       (v_K v_CIPHERTEXT_SIZE v_T_AS_NTT_ENCODED_SIZE v_C1_LEN v_C2_LEN v_U_COMPRESSION_FACTOR v_V_COMPRESSION_FACTOR v_BLOCK_LEN v_ETA1 v_ETA1_RANDOMNESS_SIZE v_ETA2 v_ETA2_RANDOMNESS_SIZE:
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti
index ba4b696bc..08011fe9b 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti
@@ -169,7 +169,8 @@ val decrypt_unpacked
       (requires
         Spec.MLKEM.is_rank v_K /\ v_CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE v_K /\
         v_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR v_K /\
-        v v_VECTOR_U_ENCODED_SIZE <= v v_CIPHERTEXT_SIZE)
+        v_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\
+        v_VECTOR_U_ENCODED_SIZE == Spec.MLKEM.v_C1_SIZE v_K)
       (fun _ -> Prims.l_True)
 
 val decrypt
@@ -241,10 +242,12 @@ val encrypt_unpacked
         v_ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE v_K /\
         v_ETA2 == Spec.MLKEM.v_ETA2 v_K /\
         v_ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE v_K /\
-        v_C1_LEN == Spec.MLKEM.v_C1_SIZE v_K /\
+        v_C1_LEN == Spec.MLKEM.v_C1_SIZE v_K /\ v_C2_LEN == Spec.MLKEM.v_C2_SIZE v_K /\
         v_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR v_K /\
-        v_BLOCK_LEN == Spec.MLKEM.v_C1_BLOCK_SIZE v_K /\ v v_C1_LEN <= v v_CIPHERTEXT_SIZE /\
-        v (Core.Slice.impl__len #u8 randomness) <= 33)
+        v_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\
+        v_BLOCK_LEN == Spec.MLKEM.v_C1_BLOCK_SIZE v_K /\
+        v_CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE v_K /\
+        length randomness == Spec.MLKEM.v_SHARED_SECRET_SIZE)
       (fun _ -> Prims.l_True)
 
 val encrypt
diff --git a/libcrux-ml-kem/src/ind_cpa.rs b/libcrux-ml-kem/src/ind_cpa.rs
index fe0749390..4856be436 100644
--- a/libcrux-ml-kem/src/ind_cpa.rs
+++ b/libcrux-ml-kem/src/ind_cpa.rs
@@ -68,7 +68,8 @@ pub(crate) fn serialize_public_key<
 
 /// Call [`serialize_uncompressed_ring_element`] for each ring element.
 #[inline(always)]
-#[hax_lib::fstar::verification_status(lax)]
+#[hax_lib::fstar::options("--z3rlimit 200")]
+#[hax_lib::fstar::verification_status(panic_free)]
 #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
     $OUT_LEN == Spec.MLKEM.v_CPA_PRIVATE_KEY_SIZE $K"))]
 #[hax_lib::ensures(|res|
@@ -365,17 +366,19 @@ fn compress_then_serialize_u<
 /// The NIST FIPS 203 standard can be found at
 /// <https://csrc.nist.gov/pubs/fips/203/ipd>.
 #[allow(non_snake_case)]
-#[hax_lib::fstar::verification_status(lax)]
-#[hax_lib::requires(fstar!("Spec.MLKEM.is_rank v_K /\\
-      v_ETA1 == Spec.MLKEM.v_ETA1 v_K /\\
-      v_ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE v_K /\\
-      v_ETA2 == Spec.MLKEM.v_ETA2 v_K /\\
-      v_ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE v_K /\\
-      v_C1_LEN == Spec.MLKEM.v_C1_SIZE v_K /\\
-      v_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR v_K /\\
-      v_BLOCK_LEN == Spec.MLKEM.v_C1_BLOCK_SIZE v_K /\\
-      v v_C1_LEN <= v v_CIPHERTEXT_SIZE /\\
-      v (${randomness.len()}) <= 33"))]
+#[hax_lib::fstar::options("--z3rlimit 200")]
+#[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
+      $ETA1 == Spec.MLKEM.v_ETA1 $K /\\
+      $ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\\
+      $ETA2 == Spec.MLKEM.v_ETA2 $K /\\
+      $ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE $K /\\
+      $C1_LEN == Spec.MLKEM.v_C1_SIZE $K /\\
+      $C2_LEN == Spec.MLKEM.v_C2_SIZE $K /\\
+      $U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\\
+      $V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K /\\
+      $BLOCK_LEN == Spec.MLKEM.v_C1_BLOCK_SIZE $K /\\
+      $CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\\
+      length $randomness == Spec.MLKEM.v_SHARED_SECRET_SIZE"))]
 pub(crate) fn encrypt_unpacked<
     const K: usize,
     const CIPHERTEXT_SIZE: usize,
@@ -529,7 +532,7 @@ pub(crate) fn encrypt<
 /// Call [`deserialize_then_decompress_ring_element_u`] on each ring element
 /// in the `ciphertext`.
 #[inline(always)]
-#[hax_lib::fstar::verification_status(lax)]
+#[hax_lib::fstar::verification_status(panic_free)]
 #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
     $CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\\
     $U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K"))]
@@ -603,11 +606,11 @@ fn deserialize_secret_key<const K: usize, Vector: Operations>(
 /// The NIST FIPS 203 standard can be found at
 /// <https://csrc.nist.gov/pubs/fips/203/ipd>.
 #[allow(non_snake_case)]
-#[hax_lib::fstar::verification_status(lax)]
 #[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
     $CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\\
     $U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\\
-    v $VECTOR_U_ENCODED_SIZE <= v $CIPHERTEXT_SIZE"))]
+    $V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K /\\
+    $VECTOR_U_ENCODED_SIZE == Spec.MLKEM.v_C1_SIZE $K"))]
 pub(crate) fn decrypt_unpacked<
     const K: usize,
     const CIPHERTEXT_SIZE: usize,