diff --git a/.envrc b/.envrc
index a3f6be96ea..c263b22455 100644
--- a/.envrc
+++ b/.envrc
@@ -8,3 +8,7 @@ watch_file rust-toolchain.toml
 watch_dir conan
 
 use flake
+
+# Optional, untracked local overrides. To use a different shell, put e.g.
+# `use flake .#formal-verification` in .envrc.local.
+source_env_if_exists .envrc.local
diff --git a/.gitignore b/.gitignore
index 5b21076af3..183fae0004 100644
--- a/.gitignore
+++ b/.gitignore
@@ -92,6 +92,9 @@ target/
 # Direnv's directory
 /.direnv
 
+# Direnv's local, per-developer overrides
+/.envrc.local
+
 # clangd cache
 /.cache
 
diff --git a/bin/check-tools.sh b/bin/check-tools.sh
index ed76861aa4..d04a996c14 100755
--- a/bin/check-tools.sh
+++ b/bin/check-tools.sh
@@ -24,9 +24,13 @@
 # `g++-15`, ...) are probed under both names: a suffixed name can break while
 # the plain one still works (see mkVersionedToolLinks in nix/packages.nix).
 #
+# Tools scoped to a single dev shell rather than to commonPackages are checked
+# only in that shell, keyed off XRPL_DEVSHELL.
+#
 # Environment variables:
 #   CI                      if set, skip the tools above when on macOS.
 #   CHECK_TOOLS_SKIP_CLONE  if set, skip the git-over-HTTPS connectivity check.
+#   XRPL_DEVSHELL           active dev shell; selects shell-specific tools.
 
 set -uo pipefail
 
@@ -163,6 +167,14 @@ if [ "${os}" = "linux" ] || [ "${os}" = "macos" ]; then
     check rustfmt
 fi
 
+# Lean4 is in the formal-verification shell only, not in commonPackages.
+if [ "${XRPL_DEVSHELL:-}" = "formal-verification" ]; then
+    echo
+    echo "Formal verification toolchain:"
+    check lean
+    check lake
+fi
+
 # GCC is the default compiler on Linux. macOS uses the system Apple Clang
 # instead, so GCC/g++/gcov are not expected there.
 if [ "${os}" = "linux" ]; then
diff --git a/nix/check-tools/README.md b/nix/check-tools/README.md
index f23b2dcc21..73fc9765af 100644
--- a/nix/check-tools/README.md
+++ b/nix/check-tools/README.md
@@ -26,6 +26,10 @@ The store paths carry their derivation hash, so they change whenever a tool is
 rebuilt — a `flake.lock` update generally rewrites most of them even when no
 version moves. That is deliberate: it makes tooling changes visible in review.
 
+Tools scoped to a single dev shell rather than to `commonPackages` do not appear
+here: `check-tools.sh` keys those off `XRPL_DEVSHELL`, and none of the three
+environments above is such a shell. Adding to one needs no snapshot update.
+
 ## Regenerating
 
 The two Linux snapshots come from the `nix-ubuntu` image (Docker or a compatible
diff --git a/nix/devshell.nix b/nix/devshell.nix
index 07f7143c5b..99859a8cef 100644
--- a/nix/devshell.nix
+++ b/nix/devshell.nix
@@ -147,6 +147,19 @@ rec {
     versionedTools = clangVersionedTools;
   };
 
+  # The gcc shell plus the Lean4 formal verification toolchain
+  formal-verification = makeShell {
+    shellName = "formal-verification";
+    stdenv = customGccStdenv;
+    compilerName = "gcc";
+    version = gccVersion;
+    versionedTools = gccVersionedTools;
+    extraPackages = [
+      customGccGcov
+      pkgs.lean4
+    ];
+  };
+
   # Nix provides no compiler; use the one from your system (e.g. Apple Clang).
   no-compiler = makeShell {
     shellName = "no-compiler";