diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 27d170e..7826320 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -3,13 +3,33 @@ on: push
 jobs:
   build-and-test:
     runs-on: ubuntu-latest
+    timeout-minutes: 600
     steps:
-      - uses: actions/checkout@v2
-      - name: Set up Go
-        uses: actions/setup-go@v2
-        with:
-          go-version: 1.20.3
-      - name: Build
-        run: go build
-      - name: Test
-        run: go test
\ No newline at end of file
+    - name: Checkout repo
+      uses: actions/checkout@v3
+      with:
+        fetch-depth: 0
+    - name: Install Elan
+      run: |
+        curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y -v --default-toolchain leanprover/lean4:nightly-2023-07-12
+        echo "LAKE_VERSION=$(~/.elan/bin/lake --version)" >> $GITHUB_ENV
+    - name: Cache dependencies
+      uses: actions/cache@v3
+      with:
+        path: formal-verification/lake-packages
+        key: "${{ env.LAKE_VERSION }}"
+    - name: Set up Go
+      uses: actions/setup-go@v4
+      with:
+        go-version-file: './go.mod'
+    - name: Build
+      run: go build
+    - name: Test
+      run: go test
+    - name: Export circuit
+      run: ./gnark-mbu extract-circuit --output=formal-verification/FormalVerification.lean
+    - name: Build lean project
+      run: |
+        cd formal-verification
+        ~/.elan/bin/lake exe cache get
+        ~/.elan/bin/lake build
\ No newline at end of file
diff --git a/.gitignore b/.gitignore
index 2da97aa..8f53355 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,10 @@
 .idea
 out
 gnark-mbu
+gnark-mbu.exe
+
+formal-verification/build
+formal-verification/.cache
+formal-verification/lean-packages/*
+formal-verification/lake-packages/*
+!formal-verification/lake-manifest.json
diff --git a/README.md b/README.md
index e0f0edf..c1f4591 100644
--- a/README.md
+++ b/README.md
@@ -54,6 +54,9 @@ This part explains the existing cli commands.
         1. output *file path* - File to be writen 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
 
 ## Benchmarks
 
diff --git a/formal-verification/FormalVerification.lean b/formal-verification/FormalVerification.lean
new file mode 100644
index 0000000..e69de29
diff --git a/formal-verification/Main.lean b/formal-verification/Main.lean
new file mode 100644
index 0000000..f3db683
--- /dev/null
+++ b/formal-verification/Main.lean
@@ -0,0 +1,5 @@
+import ProvenZk.Binary
+import ProvenZk.Hash
+import ProvenZk.Merkle
+
+def main : IO Unit := pure ()
\ No newline at end of file
diff --git a/formal-verification/lake-manifest.json b/formal-verification/lake-manifest.json
new file mode 100644
index 0000000..144219f
--- /dev/null
+++ b/formal-verification/lake-manifest.json
@@ -0,0 +1,45 @@
+{"version": 4,
+ "packagesDir": "lake-packages",
+ "packages":
+ [{"git":
+   {"url": "https://github.com/EdAyers/ProofWidgets4",
+    "subDir?": null,
+    "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8",
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.11"}},
+  {"git":
+   {"url": "https://github.com/mhuisi/lean4-cli.git",
+    "subDir?": null,
+    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
+    "name": "Cli",
+    "inputRev?": "nightly"}},
+  {"git":
+   {"url": "https://github.com/reilabs/proven-zk.git",
+    "subDir?": null,
+    "rev": "08431b93eeef80f6acbf3d6a6401c02d849f6864",
+    "name": "ProvenZK",
+    "inputRev?": "v1.0.0"}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/mathlib4.git",
+    "subDir?": null,
+    "rev": "ea67efc21e4e1496f0a1d954cd0c0a952523133a",
+    "name": "mathlib",
+    "inputRev?": "ea67efc21e4e1496f0a1d954cd0c0a952523133a"}},
+  {"git":
+   {"url": "https://github.com/gebner/quote4",
+    "subDir?": null,
+    "rev": "c0d9516f44d07feee01c1103c8f2f7c24a822b55",
+    "name": "Qq",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/JLimperg/aesop",
+    "subDir?": null,
+    "rev": "f04538ab6ad07642368cf11d2702acc0a9b4bcee",
+    "name": "aesop",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "dff883c55395438ae2a5c65ad5ddba084b600feb",
+    "name": "std",
+    "inputRev?": "main"}}]}
diff --git a/formal-verification/lakefile.lean b/formal-verification/lakefile.lean
new file mode 100644
index 0000000..01a6328
--- /dev/null
+++ b/formal-verification/lakefile.lean
@@ -0,0 +1,22 @@
+import Lake
+open Lake DSL
+
+package «formal-verification» {
+  -- add package configuration options here
+}
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git"@"ea67efc21e4e1496f0a1d954cd0c0a952523133a"
+
+require ProvenZK from git
+  "https://github.com/reilabs/proven-zk.git"@"v1.0.0"
+
+lean_lib FormalVerification {
+  -- add library configuration options here
+}
+
+@[default_target]
+lean_exe «formal-verification» {
+  moreLeanArgs := #["--tstack=1000000"]
+  root := `Main
+}
diff --git a/formal-verification/lean-toolchain b/formal-verification/lean-toolchain
new file mode 100644
index 0000000..6be6051
--- /dev/null
+++ b/formal-verification/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-07-12
diff --git a/main.go b/main.go
index 53624b8..9670744 100644
--- a/main.go
+++ b/main.go
@@ -335,6 +335,32 @@ func main() {
 					return nil
 				},
 			},
+			{
+				Name: "extract-circuit",
+				Flags: []cli.Flag{
+					&cli.StringFlag{Name: "output", Usage: "Output file", Required: true},
+				},
+				Action: func(context *cli.Context) error {
+					path := context.String("output")
+					logging.Logger().Info().Msg("Extracting gnark circuit to Lean")
+					circuit_string, err := prover.ExtractLean()
+					if err != nil {
+						return err
+					}
+					file, err := os.Create(path)
+					defer file.Close()
+					if err != nil {
+						return err
+					}
+					written, err := file.WriteString(circuit_string)
+					if err != nil {
+						return err
+					}
+					logging.Logger().Info().Int("bytesWritten", written).Msg("Lean circuit written to file")
+
+					return nil
+				},
+			},
 		},
 	}
 
diff --git a/prover/insertion_proving_system.go b/prover/insertion_proving_system.go
index 1788531..2fe9631 100644
--- a/prover/insertion_proving_system.go
+++ b/prover/insertion_proving_system.go
@@ -93,6 +93,10 @@ func SetupInsertion(treeDepth uint32, batchSize uint32) (*ProvingSystem, error)
 	return &ProvingSystem{treeDepth, batchSize, pk, vk, ccs}, nil
 }
 
+func ExtractLean() (string, error) {
+	return "", nil
+}
+
 func (ps *ProvingSystem) ProveInsertion(params *InsertionParameters) (*Proof, error) {
 	if err := params.ValidateShape(ps.TreeDepth, ps.BatchSize); err != nil {
 		return nil, err