diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 7826320..77aa3ba 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -1,5 +1,6 @@
 name: Test
 on: push
+concurrency: testing_environment
 jobs:
   build-and-test:
     runs-on: ubuntu-latest
@@ -27,7 +28,7 @@ jobs:
     - name: Test
       run: go test
     - name: Export circuit
-      run: ./gnark-mbu extract-circuit --output=formal-verification/FormalVerification.lean
+      run: ./gnark-mbu extract-circuit --output=formal-verification/FormalVerification.lean --tree-depth 30
     - name: Build lean project
       run: |
         cd formal-verification
diff --git a/README.md b/README.md
index c1f4591..2943c5c 100644
--- a/README.md
+++ b/README.md
@@ -51,12 +51,13 @@ This part explains the existing cli commands.
         2. input-hash *hash* - Hash of all public inputs  
 7. r1cs - Builds an r1cs and writes it to a file  
     Flags:  
-        1. output *file path* - File to be writen to  
+        1. output *file path* - File to be written to  
         2. tree-depth *n* - Depth of a tree  
         3. batch-size *n* - Batch size for Merkle tree updates
 8. extract-circuit - Transpiles the circuit from gnark to Lean
     Flags:  
-        1. output *file path* - File to be writen to
+        1. output *file path* - File to be written to
+        2. tree-depth *n* - Merkle tree depth
 
 ## Benchmarks
 
diff --git a/formal-verification/FormalVerification.lean b/formal-verification/FormalVerification.lean
index 70a99d4..b0e890a 100644
--- a/formal-verification/FormalVerification.lean
+++ b/formal-verification/FormalVerification.lean
@@ -1,7 +1,7 @@
 import ProvenZk.Gates
 import ProvenZk.Ext.Vector
 
-namespace Poseidon2
+namespace SemaphoreMTB
 
 def Order : ℕ := 0x30644e72e131a029b85045b68181585d2833e84879b9709143e1f593f0000001
 variable [Fact (Nat.Prime Order)]
@@ -124,4 +124,44 @@ def Poseidon2 (In1: F) (In2: F) (k: F -> Prop): Prop :=
     poseidon_3 vec![0, In1, In2] fun gate_0 =>
     k gate_0[0]
 
-end Poseidon2
\ No newline at end of file
+def ProofRound (Direction: F) (Hash: F) (Sibling: F) (k: F -> Prop): Prop :=
+    Gates.is_bool Direction ∧
+    ∃gate_1, Gates.select Direction Hash Sibling gate_1 ∧
+    ∃gate_2, Gates.select Direction Sibling Hash gate_2 ∧
+    Poseidon2 gate_1 gate_2 fun gate_3 =>
+    k gate_3
+
+def VerifyProof_31_30 (Proof: Vector F 31) (Path: Vector F 30) (k: F -> Prop): Prop :=
+    ProofRound Path[0] Proof[1] Proof[0] fun gate_0 =>
+    ProofRound Path[1] Proof[2] gate_0 fun gate_1 =>
+    ProofRound Path[2] Proof[3] gate_1 fun gate_2 =>
+    ProofRound Path[3] Proof[4] gate_2 fun gate_3 =>
+    ProofRound Path[4] Proof[5] gate_3 fun gate_4 =>
+    ProofRound Path[5] Proof[6] gate_4 fun gate_5 =>
+    ProofRound Path[6] Proof[7] gate_5 fun gate_6 =>
+    ProofRound Path[7] Proof[8] gate_6 fun gate_7 =>
+    ProofRound Path[8] Proof[9] gate_7 fun gate_8 =>
+    ProofRound Path[9] Proof[10] gate_8 fun gate_9 =>
+    ProofRound Path[10] Proof[11] gate_9 fun gate_10 =>
+    ProofRound Path[11] Proof[12] gate_10 fun gate_11 =>
+    ProofRound Path[12] Proof[13] gate_11 fun gate_12 =>
+    ProofRound Path[13] Proof[14] gate_12 fun gate_13 =>
+    ProofRound Path[14] Proof[15] gate_13 fun gate_14 =>
+    ProofRound Path[15] Proof[16] gate_14 fun gate_15 =>
+    ProofRound Path[16] Proof[17] gate_15 fun gate_16 =>
+    ProofRound Path[17] Proof[18] gate_16 fun gate_17 =>
+    ProofRound Path[18] Proof[19] gate_17 fun gate_18 =>
+    ProofRound Path[19] Proof[20] gate_18 fun gate_19 =>
+    ProofRound Path[20] Proof[21] gate_19 fun gate_20 =>
+    ProofRound Path[21] Proof[22] gate_20 fun gate_21 =>
+    ProofRound Path[22] Proof[23] gate_21 fun gate_22 =>
+    ProofRound Path[23] Proof[24] gate_22 fun gate_23 =>
+    ProofRound Path[24] Proof[25] gate_23 fun gate_24 =>
+    ProofRound Path[25] Proof[26] gate_24 fun gate_25 =>
+    ProofRound Path[26] Proof[27] gate_25 fun gate_26 =>
+    ProofRound Path[27] Proof[28] gate_26 fun gate_27 =>
+    ProofRound Path[28] Proof[29] gate_27 fun gate_28 =>
+    ProofRound Path[29] Proof[30] gate_28 fun gate_29 =>
+    k gate_29
+
+end SemaphoreMTB
\ No newline at end of file
diff --git a/formal-verification/FormalVerification/Poseidon/Correctness.lean b/formal-verification/FormalVerification/Poseidon/Correctness.lean
index f8f5687..66d911a 100644
--- a/formal-verification/FormalVerification/Poseidon/Correctness.lean
+++ b/formal-verification/FormalVerification/Poseidon/Correctness.lean
@@ -5,7 +5,7 @@ import Mathlib
 import ProvenZk
 
 open Matrix
-open Poseidon2 (F Order)
+open SemaphoreMTB (F Order)
 
 variable [Fact (Nat.Prime Order)]
 
@@ -64,16 +64,16 @@ def half_rounds_cps
     half_round state (Vector.ofFn fun i => cfg.round_constants[init_const + i]!) fun state' =>
         half_rounds_cps cfg half_round state' (init_const + cfg.t) round_count k
 
-lemma sbox_uncps (A : F) (k : F -> Prop): Poseidon2.sbox A k = k (A ^ 5) := by
-  unfold Poseidon2.sbox
+lemma sbox_uncps (A : F) (k : F -> Prop): SemaphoreMTB.sbox A k = k (A ^ 5) := by
+  unfold SemaphoreMTB.sbox
   simp [Gates.mul]
   apply iff_to_eq
   repeat (rw [pow_succ])
   rw [pow_zero, mul_one, mul_assoc]
 
 lemma mds_3_uncps (S : Vector F 3) (k : Vector F 3 -> Prop):
-  Poseidon2.mds_3 S k = k (mds_matmul Constants.x5_254_3 S) := by
-  simp [Poseidon2.mds_3, Gates.add, Gates.mul]
+  SemaphoreMTB.mds_3 S k = k (mds_matmul Constants.x5_254_3 S) := by
+  simp [SemaphoreMTB.mds_3, Gates.add, Gates.mul]
   apply iff_to_eq
   simp [mds_matmul, Constants.x5_254_3, Constants.x5_254_3_MDS_matrix]
   simp [Vector.to_column, Matrix.to_vector, Vector.ofFn]
@@ -89,8 +89,8 @@ lemma mds_3_uncps (S : Vector F 3) (k : Vector F 3 -> Prop):
   rfl
 
 lemma full_round_3_uncps (S C: Vector F 3) (k : Vector F 3 -> Prop):
-  Poseidon2.fullRound_3_3 S C k = k (full_round Constants.x5_254_3 S C) := by
-  unfold Poseidon2.fullRound_3_3
+  SemaphoreMTB.fullRound_3_3 S C k = k (full_round Constants.x5_254_3 S C) := by
+  unfold SemaphoreMTB.fullRound_3_3
   unfold Gates.add
   simp [Gates.add, sbox_uncps, mds_3_uncps, full_round]
   apply iff_to_eq
@@ -102,8 +102,8 @@ lemma full_round_3_uncps (S C: Vector F 3) (k : Vector F 3 -> Prop):
   conv => rhs ; rw [←Vector.ofFn_get S]
 
 lemma half_round_3_uncps (S C: Vector F 3) (k : Vector F 3 -> Prop):
-  Poseidon2.halfRound_3_3 S C k = k (partial_round Constants.x5_254_3 S C) := by
-  unfold Poseidon2.halfRound_3_3
+  SemaphoreMTB.halfRound_3_3 S C k = k (partial_round Constants.x5_254_3 S C) := by
+  unfold SemaphoreMTB.halfRound_3_3
   unfold Gates.add
   simp [Gates.add, sbox_uncps, mds_3_uncps, partial_round]
   apply iff_to_eq
@@ -151,7 +151,7 @@ lemma partial_rounds_3_uncps
   {S : Vector F 3}
   {start count : Nat}
   {k : Vector F 3 -> Prop}:
-  half_rounds_cps Constants.x5_254_3 Poseidon2.halfRound_3_3 S start count k = k (partial_rounds Constants.x5_254_3 S start count) := by
+  half_rounds_cps Constants.x5_254_3 SemaphoreMTB.halfRound_3_3 S start count k = k (partial_rounds Constants.x5_254_3 S start count) := by
   apply partial_rounds_uncps
   apply half_round_3_uncps
 
@@ -192,7 +192,7 @@ lemma full_rounds_3_uncps
   {S : Vector F 3}
   {start count : Nat}
   {k : Vector F 3 -> Prop}:
-  full_rounds_cps Constants.x5_254_3 Poseidon2.fullRound_3_3 S start count k = k (full_rounds Constants.x5_254_3 S start count) := by
+  full_rounds_cps Constants.x5_254_3 SemaphoreMTB.fullRound_3_3 S start count k = k (full_rounds Constants.x5_254_3 S start count) := by
   apply full_rounds_uncps
   apply full_round_3_uncps
 
@@ -200,9 +200,9 @@ lemma fold_vec_2 {v : Vector F 2}: vec![v[0], v[1]] = v := by
     conv => rhs; rw [←Vector.ofFn_get v]
 
 def looped_poseidon_3 (inp : Vector F 3) (k: Vector F 3 -> Prop): Prop :=
-    full_rounds_cps Constants.x5_254_3 Poseidon2.fullRound_3_3 inp 0 4 fun state =>
-    half_rounds_cps Constants.x5_254_3 Poseidon2.halfRound_3_3 state 12 57  fun state' =>
-    full_rounds_cps Constants.x5_254_3 Poseidon2.fullRound_3_3 state' 183 4 k
+    full_rounds_cps Constants.x5_254_3 SemaphoreMTB.fullRound_3_3 inp 0 4 fun state =>
+    half_rounds_cps Constants.x5_254_3 SemaphoreMTB.halfRound_3_3 state 12 57  fun state' =>
+    full_rounds_cps Constants.x5_254_3 SemaphoreMTB.fullRound_3_3 state' 183 4 k
 
 lemma fold_vec_3 {v : Vector F 3}: vec![v[0], v[1], v[2]] = v := by
     conv => rhs; rw [←Vector.ofFn_get v]
@@ -210,9 +210,9 @@ lemma fold_vec_3 {v : Vector F 3}: vec![v[0], v[1], v[2]] = v := by
 set_option maxRecDepth 2048
 
 theorem looped_poseidon_3_go (inp : Vector F 3) (k : Vector F 3 -> Prop):
-    Poseidon2.poseidon_3 inp k = looped_poseidon_3 inp k := by
+    SemaphoreMTB.poseidon_3 inp k = looped_poseidon_3 inp k := by
     unfold looped_poseidon_3
-    unfold Poseidon2.poseidon_3
+    unfold SemaphoreMTB.poseidon_3
     simp [full_rounds_cps, half_rounds_cps, getElem!, fold_vec_3, Vector.ofFn]
     rfl
 
@@ -295,7 +295,7 @@ theorem perm_folded_go (cfg : Constants) (input_words : Vector cfg.F cfg.t):
   }
 
 theorem poseidon_3_correct (inp : Vector F 3) (k : Vector F 3 -> Prop):
-  Poseidon2.poseidon_3 inp k = k (Poseidon.perm Constants.x5_254_3 inp) := by
+  SemaphoreMTB.poseidon_3 inp k = k (Poseidon.perm Constants.x5_254_3 inp) := by
   simp [
     looped_poseidon_3_go,
     looped_poseidon_3,
@@ -305,4 +305,4 @@ theorem poseidon_3_correct (inp : Vector F 3) (k : Vector F 3 -> Prop):
     perm_folded_go,
     perm_folded
   ]
-  rfl
+  rfl
\ No newline at end of file
diff --git a/formal-verification/FormalVerification/SemanticEquivalence.lean b/formal-verification/FormalVerification/SemanticEquivalence.lean
index 15e0743..cdf88b2 100644
--- a/formal-verification/FormalVerification/SemanticEquivalence.lean
+++ b/formal-verification/FormalVerification/SemanticEquivalence.lean
@@ -6,12 +6,64 @@ import FormalVerification
 import FormalVerification.Poseidon.Spec
 import FormalVerification.Poseidon.Correctness
 
-open Poseidon2 (F Order)
+open SemaphoreMTB (F Order)
 
 variable [Fact (Nat.Prime Order)]
 
+abbrev D := 30
+
 def poseidon₂ : Hash F 2 := fun a => (Poseidon.perm Constants.x5_254_3 vec![0, a.get 0, a.get 1]).get 0
 
-lemma Poseidon2_uncps (a b : F) (k : F -> Prop) : Poseidon2.Poseidon2 a b k ↔ k (poseidon₂ vec![a, b]) := by
-    simp [Poseidon2.Poseidon2, poseidon₂, poseidon_3_correct, getElem]
-    rfl
\ No newline at end of file
+lemma Poseidon2_uncps (a b : F) (k : F -> Prop) : SemaphoreMTB.Poseidon2 a b k ↔ k (poseidon₂ vec![a, b]) := by
+    simp [SemaphoreMTB.Poseidon2, poseidon₂, poseidon_3_correct, getElem]
+    rfl
+
+lemma ProofRound_uncps {direction: F} {hash: F} {sibling: F} {k: F -> Prop} : 
+    SemaphoreMTB.ProofRound direction hash sibling k ↔
+    is_bit direction ∧ k (match Dir.nat_to_dir direction.val with
+    | Dir.left => poseidon₂ vec![sibling, hash]
+    | Dir.right => poseidon₂ vec![hash, sibling]) := by
+    simp [SemaphoreMTB.ProofRound, Gates.is_bool, Gates.select, Gates.is_bool]
+    intro hb
+    cases hb <;> {
+        simp [*]
+        simp [Dir.nat_to_dir, ZMod.val, Order]
+        rw [Poseidon2_uncps]
+    }
+
+def proof_rounds (Siblings : Vector F (n+1)) (PathIndices : Vector F n) (k : F -> Prop) : Prop :=
+  match n with
+  | Nat.zero => k Siblings.head
+  | Nat.succ _ => SemaphoreMTB.ProofRound PathIndices.head Siblings.tail.head Siblings.head fun next =>
+    proof_rounds (next ::ᵥ Siblings.tail.tail) PathIndices.tail k
+
+lemma proof_rounds_uncps
+  {Leaf : F}
+  {Siblings : Vector F n}
+  {PathIndices : Vector F n}
+  {k : F -> Prop}:
+  proof_rounds (Leaf ::ᵥ Siblings) PathIndices k ↔
+  is_vector_binary PathIndices ∧ k (MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec PathIndices) Siblings Leaf) := by
+  induction PathIndices, Siblings using Vector.inductionOn₂ generalizing Leaf with
+  | nil =>
+    simp [is_vector_binary]
+    rfl
+  | @cons n ix sib ixes sibs ih =>
+    simp [MerkleTree.recover_tail_reverse_equals_recover, MerkleTree.recover_tail, proof_rounds]
+    simp [ProofRound_uncps, is_vector_binary_cons, and_assoc, ih]
+    intros
+    rfl
+
+lemma VerifyProof_looped (PathIndices: Vector F D) (Siblings: Vector F (D+1)) (k: F -> Prop):
+    SemaphoreMTB.VerifyProof_31_30 Siblings PathIndices k =
+      proof_rounds Siblings PathIndices k := by
+    unfold SemaphoreMTB.VerifyProof_31_30
+    simp [proof_rounds]
+    rw [←Vector.ofFn_get (v := PathIndices)]
+    rw [←Vector.ofFn_get (v := Siblings)]
+    rfl
+
+lemma VerifyProof_31_30_uncps {PathIndices: Vector F D} {Siblings: Vector F (D+1)} {k : F -> Prop}:
+    SemaphoreMTB.VerifyProof_31_30 (Siblings.head ::ᵥ Siblings.tail) PathIndices k ↔
+    is_vector_binary PathIndices ∧ k (MerkleTree.recover_tail poseidon₂ (Dir.create_dir_vec PathIndices) Siblings.tail Siblings.head) := by
+    simp only [VerifyProof_looped, proof_rounds_uncps]
\ No newline at end of file
diff --git a/go.mod b/go.mod
index f34594e..2868266 100644
--- a/go.mod
+++ b/go.mod
@@ -6,27 +6,24 @@ require (
 	github.com/consensys/gnark v0.8.0
 	github.com/iden3/go-iden3-crypto v0.0.13
 	github.com/prometheus/client_golang v1.14.0
-	github.com/reilabs/gnark-lean-extractor v1.1.0
+	github.com/reilabs/gnark-lean-extractor v1.1.1-0.20230905143002-6e277112c0df
 	github.com/urfave/cli/v2 v2.10.2
 )
 
 require (
 	github.com/beorn7/perks v1.0.1 // indirect
-	github.com/bits-and-blooms/bitset v1.7.0 // indirect
 	github.com/blang/semver/v4 v4.0.0 // indirect
 	github.com/cespare/xxhash/v2 v2.1.2 // indirect
 	github.com/consensys/bavard v0.1.13 // indirect
 	github.com/cpuguy83/go-md2man/v2 v2.0.2 // indirect
 	github.com/golang/protobuf v1.5.2 // indirect
 	github.com/google/pprof v0.0.0-20230309165930-d61513b1440d // indirect
-	github.com/kr/text v0.2.0 // indirect
 	github.com/mattn/go-colorable v0.1.13 // indirect
 	github.com/mattn/go-isatty v0.0.16 // indirect
 	github.com/matttproud/golang_protobuf_extensions v1.0.1 // indirect
 	github.com/prometheus/client_model v0.3.0 // indirect
 	github.com/prometheus/common v0.37.0 // indirect
 	github.com/prometheus/procfs v0.8.0 // indirect
-	github.com/rogpeppe/go-internal v1.10.0 // indirect
 	github.com/russross/blackfriday/v2 v2.1.0 // indirect
 	github.com/xrash/smetrics v0.0.0-20201216005158-039620a65673 // indirect
 	google.golang.org/protobuf v1.28.1 // indirect
diff --git a/go.sum b/go.sum
index 9f8f69c..5b9890b 100644
--- a/go.sum
+++ b/go.sum
@@ -42,8 +42,6 @@ github.com/beorn7/perks v0.0.0-20180321164747-3a771d992973/go.mod h1:Dwedo/Wpr24
 github.com/beorn7/perks v1.0.0/go.mod h1:KWe93zE9D1o94FZ5RNwFwVgaQK1VOXiVxmqh+CedLV8=
 github.com/beorn7/perks v1.0.1 h1:VlbKKnNfV8bJzeqoa4cOKqO6bYr3WgKZxO8Z16+hsOM=
 github.com/beorn7/perks v1.0.1/go.mod h1:G2ZrVWU2WbWT9wwq4/hrbKbnv/1ERSJQ0ibhJ6rlkpw=
-github.com/bits-and-blooms/bitset v1.7.0 h1:YjAGVd3XmtK9ktAbX8Zg2g2PwLIMjGREZJHlV4j7NEo=
-github.com/bits-and-blooms/bitset v1.7.0/go.mod h1:gIdJ4wp64HaoK2YrL1Q5/N7Y16edYb8uY+O0FJTyyDA=
 github.com/blang/semver/v4 v4.0.0 h1:1PFHFE6yCCTv8C1TeyNNarDzntLi7wMI5i/pzqYIsAM=
 github.com/blang/semver/v4 v4.0.0/go.mod h1:IbckMUScFkM3pff0VJDNKRiT6TG/YpiHIM2yvyW5YoQ=
 github.com/census-instrumentation/opencensus-proto v0.2.1/go.mod h1:f6KPmirojxKA12rnyqOA5BBL4O983OfeGPqjHWSTneU=
@@ -61,12 +59,9 @@ github.com/consensys/gnark v0.8.0 h1:0bQ2MyDG4oNjMQpNyL8HjrrUSSL3yYJg0Elzo6LzmcU
 github.com/consensys/gnark v0.8.0/go.mod h1:aKmA7dIiLbTm0OV37xTq0z+Bpe4xER8EhRLi6necrm8=
 github.com/consensys/gnark-crypto v0.9.1 h1:mru55qKdWl3E035hAoh1jj9d7hVnYY5pfb6tmovSmII=
 github.com/consensys/gnark-crypto v0.9.1/go.mod h1:a2DQL4+5ywF6safEeZFEPGRiiGbjzGFRUN2sg06VuU4=
-github.com/consensys/gnark-crypto v0.11.0 h1:QqzHQlwEqlQr5jfWblGDkwlKHpT+4QodYqqExkAtyks=
-github.com/consensys/gnark-crypto v0.11.0/go.mod h1:Iq/P3HHl0ElSjsg2E1gsMwhAyxnxoKK5nVyZKd+/KhU=
 github.com/coreos/go-systemd/v22 v22.3.3-0.20220203105225-a9a7ef127534/go.mod h1:Y58oyj3AT4RCenI/lSvhwexgC+NSVTIJ3seZv2GcEnc=
 github.com/cpuguy83/go-md2man/v2 v2.0.2 h1:p1EgwI/C7NhT0JmVkwCD2ZBK8j4aeHQX2pMHHBfMQ6w=
 github.com/cpuguy83/go-md2man/v2 v2.0.2/go.mod h1:tgQtvFlXSQOSOSIRvRPT7W67SCa46tRHOmNcaadrF8o=
-github.com/creack/pty v1.1.9/go.mod h1:oKZEueFk5CKHvIhNR5MUki03XCEU+Q6VDXinZuGJ33E=
 github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38=
 github.com/davecgh/go-spew v1.1.1 h1:vj9j/u1bqnvCEfJOwUhtlOARqs3+rkHYY13jYWTU97c=
 github.com/davecgh/go-spew v1.1.1/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38=
@@ -170,7 +165,6 @@ github.com/kr/pretty v0.3.1 h1:flRD4NNwYAUpkphVc1HcthR4KEIFJ65n8Mw5qdRn3LE=
 github.com/kr/pty v1.1.1/go.mod h1:pFQYn66WHrOpPYNljwOMqo10TkYh1fy3cYio2l3bCsQ=
 github.com/kr/text v0.1.0/go.mod h1:4Jbv+DJW3UT/LiOwJeYQe1efqtUx/iVham/4vfdArNI=
 github.com/kr/text v0.2.0 h1:5Nx0Ya0ZqY2ygV366QzturHI13Jq95ApcVaJBhpS+AY=
-github.com/kr/text v0.2.0/go.mod h1:eLer722TekiGuMkidMxC/pM04lWEeraHUUmBw8l2grE=
 github.com/leanovate/gopter v0.2.9 h1:fQjYxZaynp97ozCzfOyOuAGOU4aU/z37zf/tOujFk7c=
 github.com/leanovate/gopter v0.2.9/go.mod h1:U2L/78B+KVFIx2VmW6onHJQzXtFb+p5y3y2Sh+Jxxv8=
 github.com/mattn/go-colorable v0.1.12/go.mod h1:u5H1YNBxpqRaxsYJYSkiCWKzEfiAb1Gb520KVy5xxl4=
@@ -222,16 +216,10 @@ github.com/prometheus/procfs v0.6.0/go.mod h1:cz+aTbrPOrUb4q7XlbU9ygM+/jj0fzG6c1
 github.com/prometheus/procfs v0.7.3/go.mod h1:cz+aTbrPOrUb4q7XlbU9ygM+/jj0fzG6c1xBZuNvfVA=
 github.com/prometheus/procfs v0.8.0 h1:ODq8ZFEaYeCaZOJlZZdJA2AbQR98dSHSM1KW/You5mo=
 github.com/prometheus/procfs v0.8.0/go.mod h1:z7EfXMXOkbkqb9IINtpCn86r/to3BnA0uaxHdg830/4=
-github.com/reilabs/gnark-lean-extractor v1.0.0 h1:jLoI4Dh3eAFdhJ3hvUfBmKJgB2NLPGrL7VW+WDRecCQ=
-github.com/reilabs/gnark-lean-extractor v1.0.0/go.mod h1:FuCRQ2kdpdImOzmzFUqMoCMQxn+Nol+AmzPDWlBZLA8=
-github.com/reilabs/gnark-lean-extractor v1.0.1-0.20230831190435-992a084cf5ea h1:5ApM8KKqO+IsluIkGJkcouuZbYf7qC8W98uHOv3asb0=
-github.com/reilabs/gnark-lean-extractor v1.0.1-0.20230831190435-992a084cf5ea/go.mod h1:FuCRQ2kdpdImOzmzFUqMoCMQxn+Nol+AmzPDWlBZLA8=
-github.com/reilabs/gnark-lean-extractor v1.1.0 h1:vxB8Nhzf/TDS4sVM/qvaxJRod+u/mOFdCny/61Z00Bs=
-github.com/reilabs/gnark-lean-extractor v1.1.0/go.mod h1:FuCRQ2kdpdImOzmzFUqMoCMQxn+Nol+AmzPDWlBZLA8=
+github.com/reilabs/gnark-lean-extractor v1.1.1-0.20230905143002-6e277112c0df h1:aCdrzgCm8Xkxz+I35qE0vDU7AtUP9EZkmEKx4eLCuGU=
+github.com/reilabs/gnark-lean-extractor v1.1.1-0.20230905143002-6e277112c0df/go.mod h1:FuCRQ2kdpdImOzmzFUqMoCMQxn+Nol+AmzPDWlBZLA8=
 github.com/rogpeppe/go-internal v1.3.0/go.mod h1:M8bDsm7K2OlrFYOpmOWEs/qY81heoFRclV5y23lUDJ4=
-github.com/rogpeppe/go-internal v1.9.0 h1:73kH8U+JUqXU8lRuOHeVHaa/SZPifC7BkcraZVejAe8=
-github.com/rogpeppe/go-internal v1.9.0/go.mod h1:WtVeX8xhTBvf0smdhujwtBcq4Qrzq/fJaraNFVN+nFs=
-github.com/rogpeppe/go-internal v1.10.0/go.mod h1:UQnix2H7Ngw/k4C5ijL5+65zddjncjaFoBhdsK/akog=
+github.com/rogpeppe/go-internal v1.10.0 h1:TMyTOH3F/DB16zRVcYyreMH6GnZZrwQVAoYjRBZyWFQ=
 github.com/rs/xid v1.4.0/go.mod h1:trrq9SKmegXys3aeAKXMUTdJsYXVwGY3RLcfgqegfbg=
 github.com/rs/zerolog v1.29.0 h1:Zes4hju04hjbvkVkOhdl2HpZa+0PmVwigmo8XoORE5w=
 github.com/rs/zerolog v1.29.0/go.mod h1:NILgTygv/Uej1ra5XxGf82ZFSLk58MFGAUS2o6usyD0=
diff --git a/main.go b/main.go
index 9670744..f17810f 100644
--- a/main.go
+++ b/main.go
@@ -339,11 +339,13 @@ func main() {
 				Name: "extract-circuit",
 				Flags: []cli.Flag{
 					&cli.StringFlag{Name: "output", Usage: "Output file", Required: true},
+					&cli.UintFlag{Name: "tree-depth", Usage: "Merkle tree depth", Required: true},
 				},
 				Action: func(context *cli.Context) error {
 					path := context.String("output")
+					treeDepth := uint32(context.Uint("tree-depth"))
 					logging.Logger().Info().Msg("Extracting gnark circuit to Lean")
-					circuit_string, err := prover.ExtractLean()
+					circuit_string, err := prover.ExtractLean(treeDepth)
 					if err != nil {
 						return err
 					}
diff --git a/prover/circuit_utils.go b/prover/circuit_utils.go
index a5015a6..858aea1 100644
--- a/prover/circuit_utils.go
+++ b/prover/circuit_utils.go
@@ -33,15 +33,31 @@ func (e *bitPatternLengthError) Error() string {
 	return "Bit pattern length was " + strconv.Itoa(e.actualLength) + " not a total number of bytes"
 }
 
-func VerifyProof(api frontend.API, proofSet, helper []frontend.Variable) frontend.Variable {
-	sum := proofSet[0]
-	for i := 1; i < len(proofSet); i++ {
-		api.AssertIsBoolean(helper[i-1])
-		d1 := api.Select(helper[i-1], proofSet[i], sum)
-		d2 := api.Select(helper[i-1], sum, proofSet[i])
-		sum = abstractor.CallGadget(api, poseidon.Poseidon2{In1: d1, In2: d2})[0]
+type ProofRound struct {
+	Direction frontend.Variable
+	Hash      frontend.Variable
+	Sibling   frontend.Variable
+}
+
+func (gadget ProofRound) DefineGadget(api abstractor.API) []frontend.Variable {
+	api.AssertIsBoolean(gadget.Direction)
+	d1 := api.Select(gadget.Direction, gadget.Hash, gadget.Sibling)
+	d2 := api.Select(gadget.Direction, gadget.Sibling, gadget.Hash)
+	sum := api.Call(poseidon.Poseidon2{In1: d1, In2: d2})[0]
+	return []frontend.Variable{sum}
+}
+
+type VerifyProof struct {
+	Proof []frontend.Variable
+	Path  []frontend.Variable
+}
+
+func (gadget VerifyProof) DefineGadget(api abstractor.API) []frontend.Variable {
+	sum := gadget.Proof[0]
+	for i := 1; i < len(gadget.Proof); i++ {
+		sum = api.Call(ProofRound{Direction: gadget.Path[i-1], Hash: gadget.Proof[i], Sibling: sum})[0]
 	}
-	return sum
+	return []frontend.Variable{sum}
 }
 
 // ReducedModRCheck Checks a little-endian array of bits asserting that it represents a number that
diff --git a/prover/deletion_circuit.go b/prover/deletion_circuit.go
index 98b4aa4..8a23741 100644
--- a/prover/deletion_circuit.go
+++ b/prover/deletion_circuit.go
@@ -5,6 +5,7 @@ import (
 	"worldcoin/gnark-mbu/prover/keccak"
 
 	"github.com/consensys/gnark/frontend"
+	"github.com/reilabs/gnark-lean-extractor/abstractor"
 )
 
 type DeletionMbuCircuit struct {
@@ -79,10 +80,10 @@ func (circuit *DeletionMbuCircuit) Define(api frontend.API) error {
 		currentPath = currentPath[:circuit.Depth]
 
 		// Verify proof for idComm.
-		rootPreDeletion := VerifyProof(api, append([]frontend.Variable{circuit.IdComms[i]}, circuit.MerkleProofs[i][:]...), currentPath)
+		rootPreDeletion := abstractor.CallGadget(api, VerifyProof{append([]frontend.Variable{circuit.IdComms[i]}, circuit.MerkleProofs[i][:]...), currentPath})[0]
 
 		// Verify proof for empty leaf.
-		rootPostDeletion := VerifyProof(api, append([]frontend.Variable{emptyLeaf}, circuit.MerkleProofs[i][:]...), currentPath)
+		rootPostDeletion := abstractor.CallGadget(api, VerifyProof{append([]frontend.Variable{emptyLeaf}, circuit.MerkleProofs[i][:]...), currentPath})[0]
 
 		preRootCorrect := api.IsZero(api.Sub(rootPreDeletion, prevRoot))
 		preRootCorrectOrSkip := api.Or(preRootCorrect, skipFlag)
diff --git a/prover/insertion_circuit.go b/prover/insertion_circuit.go
index d0d5129..6ba5874 100644
--- a/prover/insertion_circuit.go
+++ b/prover/insertion_circuit.go
@@ -4,6 +4,7 @@ import (
 	"worldcoin/gnark-mbu/prover/keccak"
 
 	"github.com/consensys/gnark/frontend"
+	"github.com/reilabs/gnark-lean-extractor/abstractor"
 )
 
 type InsertionMbuCircuit struct {
@@ -84,11 +85,11 @@ func (circuit *InsertionMbuCircuit) Define(api frontend.API) error {
 		currentPath := api.ToBinary(currentIndex, circuit.Depth)
 
 		// Verify proof for empty leaf.
-		root = VerifyProof(api, append([]frontend.Variable{emptyLeaf}, circuit.MerkleProofs[i][:]...), currentPath)
+		root = abstractor.CallGadget(api, VerifyProof{append([]frontend.Variable{emptyLeaf}, circuit.MerkleProofs[i][:]...), currentPath})[0]
 		api.AssertIsEqual(root, prevRoot)
 
 		// Verify proof for idComm.
-		root = VerifyProof(api, append([]frontend.Variable{circuit.IdComms[i]}, circuit.MerkleProofs[i][:]...), currentPath)
+		root = abstractor.CallGadget(api, VerifyProof{append([]frontend.Variable{circuit.IdComms[i]}, circuit.MerkleProofs[i][:]...), currentPath})[0]
 
 		// Set root for next iteration.
 		prevRoot = root
diff --git a/prover/insertion_proving_system.go b/prover/insertion_proving_system.go
index 639bc2f..997a78c 100644
--- a/prover/insertion_proving_system.go
+++ b/prover/insertion_proving_system.go
@@ -6,7 +6,6 @@ import (
 	"fmt"
 	"math/big"
 	"worldcoin/gnark-mbu/logging"
-	"worldcoin/gnark-mbu/prover/poseidon"
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/backend/groth16"
@@ -95,9 +94,10 @@ func SetupInsertion(treeDepth uint32, batchSize uint32) (*ProvingSystem, error)
 	return &ProvingSystem{treeDepth, batchSize, pk, vk, ccs}, nil
 }
 
-func ExtractLean() (string, error) {
-	assignment := poseidon.Poseidon2{}
-	return extractor.GadgetToLean(&assignment, ecc.BN254)
+func ExtractLean(treeDepth uint32) (string, error) {
+	// Not checking for treeDepth === 0
+	assignment := VerifyProof{Proof: make([]frontend.Variable, treeDepth+1), Path: make([]frontend.Variable, treeDepth)}
+	return extractor.GadgetToLeanWithName(&assignment, ecc.BN254, "SemaphoreMTB")
 }
 
 func (ps *ProvingSystem) ProveInsertion(params *InsertionParameters) (*Proof, error) {