diff --git a/anneal/.gitignore b/anneal/.gitignore
index 7f530424bd..8a2693dfa9 100644
--- a/anneal/.gitignore
+++ b/anneal/.gitignore
@@ -1 +1,3 @@
 .docker-volume-id
+.lake
+.vscode
diff --git a/anneal/lake-manifest.json b/anneal/lake-manifest.json
new file mode 100644
index 0000000000..73cd6b3163
--- /dev/null
+++ b/anneal/lake-manifest.json
@@ -0,0 +1,105 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/AeneasVerif/aeneas",
+   "type": "git",
+   "subDir": "backends/lean",
+   "scope": "",
+   "rev": "d1c3c2677f6a052133a2cf12314cebe6ce9279cc",
+   "name": "aeneas",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5352afccd6866369be9de43f5b7ec47203555f44",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.28.0-rc1",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "7311586e1a56af887b1081d05e80c11b6c41d212",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "875ad9d88ed684e39c16bdea260e6ecfa15afd60",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.86",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "23324752757bf28124a518ec284044c8db79fee5",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "cabbb5a025bfbbc50af9184ed2dfdde6ea4f53a7",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.28.0-rc1",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "anneal",
+ "lakeDir": ".lake"}
diff --git a/anneal/lakefile.toml b/anneal/lakefile.toml
new file mode 100644
index 0000000000..1ef5780a99
--- /dev/null
+++ b/anneal/lakefile.toml
@@ -0,0 +1,13 @@
+name = "anneal"
+version = "0.1.0"
+defaultTargets = ["Anneal"]
+
+[[require]]
+name = "aeneas"
+git = "https://github.com/AeneasVerif/aeneas"
+subDir = "backends/lean"
+rev = "main" # You can replace "main" with a specific commit hash to pin the dependency
+
+[[lean_lib]]
+name = "Anneal"
+srcDir = "src"
diff --git a/anneal/lean-toolchain b/anneal/lean-toolchain
new file mode 100644
index 0000000000..3e9b4e1527
--- /dev/null
+++ b/anneal/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.28.0-rc1
\ No newline at end of file