diff --git a/.github/workflows/prover-test.yml b/.github/workflows/prover-test.yml
index 1c2cab91a1..3a95f6e0e7 100644
--- a/.github/workflows/prover-test.yml
+++ b/.github/workflows/prover-test.yml
@@ -80,13 +80,13 @@ jobs:
           cd prover/server
           go test -run TestFull -timeout 120m
 
-      # - name: Extract circuit to Lean
-      #   run: |
-      #     cd prover/server
-      #     ./light-prover extract-circuit --output formal-verification/FormalVerification/Circuit.lean --tree-height=26 --compressed-accounts=8
+      - name: Extract circuit to Lean
+        run: |
+          cd prover/server
+          ./light-prover extract-circuit --output formal-verification/FormalVerification/Circuit.lean --address-tree-height 40 --compressed-accounts 8 --state-tree-height 32
 
-      # - name: Build lean project
-      #   run: |
-      #     cd prover/server/formal-verification
-      #     ~/.elan/bin/lake exe cache get
-      #     ~/.elan/bin/lake build
+      - name: Build lean project
+        run: |
+          cd prover/server/formal-verification
+          ~/.elan/bin/lake exe cache get
+          ~/.elan/bin/lake build