diff --git a/.github/workflows/hax.yml b/.github/workflows/hax.yml
index ab4db07d7..df717b56a 100644
--- a/.github/workflows/hax.yml
+++ b/.github/workflows/hax.yml
@@ -42,10 +42,12 @@ jobs:
           curl -L https://github.com/FStarLang/FStar/releases/download/v2023.09.03/fstar_2023.09.03_Linux_x86_64.tar.gz \
             --output Fstar.tar.gz
           tar --extract --file Fstar.tar.gz
-          mv fstar Fstar
-          ls /home/runner/work
-          ls /home/runner/work/libcrux/libcrux/../hax/proof-libs/fstar/../../../
-          false
+
+      - name: ⤵ Clone HACL-star repository
+        uses: actions/checkout@v4
+        with:
+          repository: hacl-star/hacl-star
+          path: hacl-star
 
       - name: ⤵ Clone hax repository
         uses: actions/checkout@v4
@@ -65,7 +67,7 @@ jobs:
           eval $(opam env)
           ./hax-driver.py --kyber-reference
           # Extract the functions in the compress module individually to test
-          # the function-extraction code.
+            # the function-extraction code.
           # Extract functions from the remaining modules to test the
           # module-extraction code.
           ./hax-driver.py --crate-path specs/kyber \
@@ -81,4 +83,11 @@ jobs:
                       sampling \
                       serialize \
             --exclude-modules libcrux::hacl::sha3 libcrux::digest
-           ./hax-driver.py typecheck --admit
+
+      - name: 🏃🏻‍ Lax typecheck the extraction
+        run:
+          env FSTAR_HOME=${{ github.workspace }}/fstar \
+              HACL_HOME=${{ github.workspace }}/hacl-star \
+              HAX_LIBS_HOME=${{ github.workspace }}/hax/proof-libs/fstar \
+              PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
+                ./hax-driver.py typecheck --admit