diff --git a/.github/workflows/prover-test.yml b/.github/workflows/prover-test.yml
index 763c92c334..da14e2099d 100644
--- a/.github/workflows/prover-test.yml
+++ b/.github/workflows/prover-test.yml
@@ -74,4 +74,4 @@ jobs:
         run: |
           cd light-prover/formal-verification
           ~/.elan/bin/lake exe cache get
-          ~/.elan/bin/lake build || ~/.elan/bin/lake build
+          ~/.elan/bin/lake build
diff --git a/light-prover/formal-verification/.gitignore b/light-prover/formal-verification/.gitignore
new file mode 100644
index 0000000000..0d3fac651e
--- /dev/null
+++ b/light-prover/formal-verification/.gitignore
@@ -0,0 +1 @@
+lakefile.olean
diff --git a/light-prover/formal-verification/FormalVerification/Lemmas.lean b/light-prover/formal-verification/FormalVerification/Lemmas.lean
index b015f5c01c..40ae628b2d 100644
--- a/light-prover/formal-verification/FormalVerification/Lemmas.lean
+++ b/light-prover/formal-verification/FormalVerification/Lemmas.lean
@@ -1,5 +1,5 @@
 import Mathlib
-import ProvenZK
+import «ProvenZk»
 import FormalVerification.Circuit
 
 open LightProver (F Order)
diff --git a/light-prover/formal-verification/FormalVerification/Merkle.lean b/light-prover/formal-verification/FormalVerification/Merkle.lean
index d753804bbe..6f884fa1de 100644
--- a/light-prover/formal-verification/FormalVerification/Merkle.lean
+++ b/light-prover/formal-verification/FormalVerification/Merkle.lean
@@ -1,4 +1,4 @@
-import ProvenZk
+import «ProvenZk»
 import FormalVerification.Circuit
 import FormalVerification.Lemmas
 import FormalVerification.Rangecheck
diff --git a/light-prover/formal-verification/FormalVerification/Poseidon.lean b/light-prover/formal-verification/FormalVerification/Poseidon.lean
index ce35eb8441..01204db508 100644
--- a/light-prover/formal-verification/FormalVerification/Poseidon.lean
+++ b/light-prover/formal-verification/FormalVerification/Poseidon.lean
@@ -1,7 +1,7 @@
 import FormalVerification.Circuit
 import FormalVerification.Lemmas
 import Mathlib
-import ProvenZk
+import «ProvenZk»
 
 open LightProver (F Order)
 
diff --git a/light-prover/formal-verification/FormalVerification/RangeTree.lean b/light-prover/formal-verification/FormalVerification/RangeTree.lean
index 5a8479f937..3d4019081d 100644
--- a/light-prover/formal-verification/FormalVerification/RangeTree.lean
+++ b/light-prover/formal-verification/FormalVerification/RangeTree.lean
@@ -1,4 +1,4 @@
-import ProvenZK
+import «ProvenZk»
 import FormalVerification.Poseidon
 import FormalVerification.Circuit
 import FormalVerification.Lemmas
diff --git a/light-prover/formal-verification/FormalVerification/Rangecheck.lean b/light-prover/formal-verification/FormalVerification/Rangecheck.lean
index e788fd71b5..dee3ef2729 100644
--- a/light-prover/formal-verification/FormalVerification/Rangecheck.lean
+++ b/light-prover/formal-verification/FormalVerification/Rangecheck.lean
@@ -1,4 +1,4 @@
-import ProvenZk
+import «ProvenZk»
 import FormalVerification.Circuit
 import FormalVerification.Lemmas
 
diff --git a/light-prover/formal-verification/Main.lean b/light-prover/formal-verification/Main.lean
index 099da6fead..a038f61318 100644
--- a/light-prover/formal-verification/Main.lean
+++ b/light-prover/formal-verification/Main.lean
@@ -1,4 +1,4 @@
-import ProvenZK
+import «ProvenZk»
 import FormalVerification.Circuit
 import FormalVerification.Lemmas
 import FormalVerification.Merkle
diff --git a/light-prover/formal-verification/lake-manifest.json b/light-prover/formal-verification/lake-manifest.json
index dc722edddf..6359717fe8 100644
--- a/light-prover/formal-verification/lake-manifest.json
+++ b/light-prover/formal-verification/lake-manifest.json
@@ -14,7 +14,7 @@
     "subDir?": null,
     "rev": "659b51e94d4c5160c5d93b92323f0d0dda05c3ad",
     "opts": {},
-    "name": "ProvenZK",
+    "name": "«proven-zk»",
     "inputRev?": "v1.4.0",
     "inherited": false}},
   {"git":
diff --git a/light-prover/formal-verification/lakefile.lean b/light-prover/formal-verification/lakefile.lean
index 01178a866c..d3877fada7 100644
--- a/light-prover/formal-verification/lakefile.lean
+++ b/light-prover/formal-verification/lakefile.lean
@@ -8,7 +8,7 @@ package «formal-verification» {
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"@"v4.2.0"
 
-require ProvenZK from git
+require «proven-zk» from git
   "https://github.com/reilabs/proven-zk.git"@"v1.4.0"
 
 lean_lib FormalVerification {