diff --git a/.github/workflows/hax.yml b/.github/workflows/hax.yml
index 2b578e8b..e385b948 100644
--- a/.github/workflows/hax.yml
+++ b/.github/workflows/hax.yml
@@ -68,7 +68,7 @@ jobs:
 
       - name: 🏃 Extract ML-DSA crate
         working-directory: libcrux-ml-dsa
-        run: cargo hax into fstar
+        run: ./hax.py extract
 
       - name: 🏃 Lax ML-DSA crate
         working-directory: libcrux-ml-dsa
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti
index 0359b18d..3ff04ac4 100644
--- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti
+++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti
@@ -170,7 +170,7 @@ let impl_1: Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 t_Shake256x4 =
     f_init_absorb_x4
     =
     (fun (input0: t_Slice u8) (input1: t_Slice u8) (input2: t_Slice u8) (input3: t_Slice u8) ->
-        init_absorb_x4 input0 input2 input2 input3);
+        init_absorb_x4 input0 input1 input2 input3);
     f_squeeze_first_block_x4_pre = (fun (self: t_Shake256x4) -> true);
     f_squeeze_first_block_x4_post
     =