diff --git a/Benchmarks/Catalog/RelocFixtureA/lean-toolchain b/Benchmarks/Catalog/RelocFixtureA/lean-toolchain
index a8afa7d1b..12359f928 100644
--- a/Benchmarks/Catalog/RelocFixtureA/lean-toolchain
+++ b/Benchmarks/Catalog/RelocFixtureA/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.33.1
+leanprover/lean4:v4.34.0
diff --git a/Benchmarks/Catalog/RelocFixtureB/lean-toolchain b/Benchmarks/Catalog/RelocFixtureB/lean-toolchain
index a8afa7d1b..12359f928 100644
--- a/Benchmarks/Catalog/RelocFixtureB/lean-toolchain
+++ b/Benchmarks/Catalog/RelocFixtureB/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.33.1
+leanprover/lean4:v4.34.0
diff --git a/Benchmarks/Compile/TruthMines/lean-toolchain b/Benchmarks/Compile/TruthMines/lean-toolchain
index a8afa7d1b..12359f928 100644
--- a/Benchmarks/Compile/TruthMines/lean-toolchain
+++ b/Benchmarks/Compile/TruthMines/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.33.1
+leanprover/lean4:v4.34.0
diff --git a/Benchmarks/Compile/lean-toolchain b/Benchmarks/Compile/lean-toolchain
index a8afa7d1b..12359f928 100644
--- a/Benchmarks/Compile/lean-toolchain
+++ b/Benchmarks/Compile/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.33.1
+leanprover/lean4:v4.34.0
diff --git a/Benchmarks/TruthMines/lean-toolchain b/Benchmarks/TruthMines/lean-toolchain
index a8afa7d1b..12359f928 100644
--- a/Benchmarks/TruthMines/lean-toolchain
+++ b/Benchmarks/TruthMines/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.33.1
+leanprover/lean4:v4.34.0
diff --git a/lake-manifest.json b/lake-manifest.json
index 1f571e9bb..8951f4d03 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,20 +15,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
+   "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0",
+   "inputRev": "v4.34.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
+   "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.33.0",
+   "inputRev": "v4.34.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/argumentcomputer/Blake3.lean",
diff --git a/lakefile.lean b/lakefile.lean
index 98fe391ce..d7fce9313 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -18,10 +18,10 @@ require Blake3 from git
   "https://github.com/argumentcomputer/Blake3.lean" @ "78f5bc4b22de1172af8a5d91e7039128084fad3a"
 
 require Cli from git
-  "https://github.com/leanprover/lean4-cli" @ "v4.33.0"
+  "https://github.com/leanprover/lean4-cli" @ "v4.34.0"
 
 require batteries from git
-  "https://github.com/leanprover-community/batteries" @ "v4.33.0"
+  "https://github.com/leanprover-community/batteries" @ "v4.34.0"
 
 /- Reference Lean4-in-Lean4 theory and checker. `IxTcVerify` imports its
 Theory/Verify specification surface, while `bench-lean4lean` and the ignored
diff --git a/lean-toolchain b/lean-toolchain
index a8afa7d1b..12359f928 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.33.1
+leanprover/lean4:v4.34.0