diff --git a/formal-verification/lake-manifest.json b/formal-verification/lake-manifest.json
index 5c8316d..e2c9d69 100644
--- a/formal-verification/lake-manifest.json
+++ b/formal-verification/lake-manifest.json
@@ -13,7 +13,12 @@
     "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
     "name": "Cli",
     "inputRev?": "nightly"}},
-  {"path": {"name": "ProvenZK", "dir": "./../../../proven-zk"}},
+  {"git":
+   {"url": "https://github.com/reilabs/proven-zk.git",
+    "subDir?": null,
+    "rev": "ae9327ec14d84b20f1c17f336ed7698e5b0fbae1",
+    "name": "ProvenZK",
+    "inputRev?": "v1.3.0"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
diff --git a/formal-verification/lakefile.lean b/formal-verification/lakefile.lean
index d4ebb7b..f6209ef 100644
--- a/formal-verification/lakefile.lean
+++ b/formal-verification/lakefile.lean
@@ -8,8 +8,8 @@ package «formal-verification» {
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"@"26d0eab43f05db777d1cf31abd31d3a57954b2a9"
 
-require ProvenZK from
-  ".."/".."/".."/"proven-zk"
+require ProvenZK from git
+  "https://github.com/reilabs/proven-zk.git"@"v1.3.0"
 
 lean_lib FormalVerification {
   moreLeanArgs := #["--tstack=65520", "-DmaxRecDepth=10000", "-DmaxHeartbeats=200000000"]