diff --git a/.github/workflows/rust-cli.yml b/.github/workflows/rust-cli.yml
index 46863943..51e3b5f9 100644
--- a/.github/workflows/rust-cli.yml
+++ b/.github/workflows/rust-cli.yml
@@ -75,7 +75,7 @@ jobs:
           # verify its SHA-256, then execute it — no `curl | sh`.
           curl -sSfL https://raw.githubusercontent.com/leanprover/elan/v3.1.1/elan-init.sh -o elan-init.sh
           echo "f5d473c923c093759ae3839073bec2a58e82cb8bc0e4083930e76090da75b310  elan-init.sh" | sha256sum -c -
-          sh elan-init.sh -y --default-toolchain leanprover/lean4:v4.12.0
+          sh elan-init.sh -y --default-toolchain leanprover/lean4:v4.34.1
           rm -f elan-init.sh
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
diff --git a/proofs/lean4/PathTraversal.lean b/proofs/lean4/PathTraversal.lean
index fcf4122f..25c90a64 100644
--- a/proofs/lean4/PathTraversal.lean
+++ b/proofs/lean4/PathTraversal.lean
@@ -99,7 +99,7 @@ theorem isPrefix_dropLast
       -- (since t :: ts is non-empty), so xs is still a prefix.
       refine ⟨(t :: ts).dropLast, ?_⟩
       subst htail
-      rw [List.dropLast_append_of_ne_nil _ (List.cons_ne_nil t ts)]
+      rw [List.dropLast_append_of_ne_nil (List.cons_ne_nil t ts)]
 
 -- ---------------------------------------------------------------------
 -- Per-step invariant
diff --git a/proofs/lean4/SymlinkOperations.lean b/proofs/lean4/SymlinkOperations.lean
index c42fdd4f..f8635620 100644
--- a/proofs/lean4/SymlinkOperations.lean
+++ b/proofs/lean4/SymlinkOperations.lean
@@ -58,7 +58,7 @@ theorem symlink_unlink_reversible (p : Path) (fs : Filesystem)
       exact ⟨node, hfs⟩
   · simp [h]
 
-/-- Summary:
+/- Summary:
     ✓ Symlink creation and removal operations
     ✓ Preconditions for safe symlink creation
     ✓ Reversibility: unlink(symlink(p, fs)) = fs
diff --git a/proofs/lean4/lakefile.lean b/proofs/lean4/lakefile.lean
index 7aaca912..a6b9b5d7 100644
--- a/proofs/lean4/lakefile.lean
+++ b/proofs/lean4/lakefile.lean
@@ -1,7 +1,13 @@
 -- SPDX-License-Identifier: MPL-2.0
 -- Valence Shell — Lean 4 Proof Package
 --
--- Last verified working: Lean 4 v4.12.0 (2026-03-10)
+-- Last verified working: Lean 4 v4.34.1 (2026-10-02)
+--   Builds clean: FilesystemModel, FileOperations, FilesystemComposition,
+--   FilesystemEquivalence, SymlinkOperations, Extraction, CrashConsistency,
+--   PathTraversal, model_oracle.
+--   Do NOT build (already broken on v4.12.0, not port regressions):
+--   FileContentOperations, RMOOperations, CopyMoveOperations,
+--   PermissionOperations.
 -- Toolchain pinned in: lean-toolchain
 -- CI workflow:          .github/workflows/lean-verification.yml
 --                       .github/workflows/rust-cli.yml (lean4 job)
diff --git a/proofs/lean4/lean-toolchain b/proofs/lean4/lean-toolchain
index 89985206..ba8ebf2d 100644
--- a/proofs/lean4/lean-toolchain
+++ b/proofs/lean4/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.34.1