diff --git a/ImportGraph/Lake.lean b/ImportGraph/Lake.lean
index 22a95ab..b90c612 100644
--- a/ImportGraph/Lake.lean
+++ b/ImportGraph/Lake.lean
@@ -5,149 +5,24 @@ Authors: Thomas R. Murrills
 -/
 module
 
+public import ImportGraph.Util.Modules
 public import Lake.Config.Workspace
 
 import Lake.Load.Workspace
 
-/-
-# Extra `Lake` utilities
-
-This file defines a few convenient lake utilities, notably:
+/-!
+# Lake workspace loading
 
-- `for ... in ... do` instances that allow iterating through lake modules:
-  - Given `dir : System.FilePath`, `for (mod, dirEntry) in dir.modules (root := ...) do` iterates
-    in modules under the directory `dir` (descending into subdirectories)
-  - Given `glob : Lake.Glob`, `for (mod, dirEntry) in glob.modulesIn dir do` iterates through all
-    modules in `dir` matching `glob`.
-- `ImportGraph.IO.getWorkspace : IO Lake.Workspace`: a version of
-  `Lake.loadWorkspace : LoggerIO Lake.Workspace` for use in `IO` which constructs the IO
-  environment variables and finds the lean installation.
+Workspace loading is intended for executables. Library consumers needing only module traversal
+and the associated instances should import `ImportGraph.Util.Modules` instead.
 
-Note that this file should generally not be transitively imported, and is not imported via
-`import ImportGraph`. However, it is a dependency of the `import-graph-workspace-summary` exe,
-which is a default target. As such, it will always get built under `lake build`.
+This file must not be imported by modules reachable from `ImportGraph` or `ImportGraph.Tools`;
+see `ImportGraphTest.NoLakeAxioms`. The workspace-summary executable imports it separately.
 -/
 
 open Lean Lake
 
-public section
-
-namespace ImportGraph
-
-namespace System.FilePath
-
-/-- Allows iteration over the modules (any `*.lean` file) under `dir` via
-`for (mod, dirEntry) in mods do`. Usually invoked via `for (mod, dirEntry) in dir.modules do`; see
-`ImportGraph.System.FilePath.modules` for details. -/
-structure Modules where
-  dir : System.FilePath
-  root : Name := .anonymous
-
-/-- Allows iteration over the modules (any `*.lean` file) under `dir` via
-`for (mod, dirEntry) in dir.modules do`, descending into subdirectories (top-down, left-to-right),
-and constructing the module name according to the directory names and `*.lean` filenames.
-
-For example, if `dir` contains `A/B/C.lean`, this iteration visits `(A.B.C, ⟨"A/B", "C.lean"⟩)`.
-
-If `root` is provided, then `root` is prepended to the module names created from paths in the
-directory, e.g. if `dir` contains `A/B/C.lean` and we iterate through
-``for (mod, dirEntry) in dir.modules (root := `Foo)``, this iteration visits
-`(Foo.A.B.C, ⟨"A/B", "C.lean"⟩)`.
-
-By default, no root is inferred. -/
-@[inline] def modules (dir : System.FilePath) (root := Name.anonymous) : Modules := { dir, root }
-
-@[specialize]
-partial def Modules.forInAux [Monad m] [MonadLiftT IO m] {β}
-    (dir : System.FilePath) (pre : Name) (b : β)
-    (f : Name × IO.FS.DirEntry → β → m (ForInStep β)) : m (ForInStep β) := do
-  let mut b := b
-  for entry in ← dir.readDir do
-    if (← liftM (m := IO) <| entry.path.isDir) then
-      match (← Modules.forInAux entry.path (.str pre entry.fileName) b f) with
-      | ForInStep.yield b' => b := b'
-      | ForInStep.done b'  => return ForInStep.done b'
-    else if entry.path.extension.isEqSome "lean" then
-      let mod := .str pre <| (System.FilePath.withExtension entry.fileName "").toString
-      match (← f (mod, entry) b) with
-      | ForInStep.yield b' => b := b'
-      | ForInStep.done b'  => return ForInStep.done b'
-  return ForInStep.yield b
-
-instance [Monad m] [MonadLiftT IO m] : ForIn m Modules (Name × IO.FS.DirEntry) where
-  forIn spec init f := ForInStep.value <$> Modules.forInAux spec.dir spec.root init f
-
-/--
-Splits `path` into the `DirEntry` for its enclosing directory and file name, as `readDir` would
-report it. `path.parent` (rather than `path.withFileName ""`) is used for `root` so that it carries
-no trailing separator and so that `root / fileName` round-trips back to `path` (matching the entries
-produced when iterating through a directory).
--/
-def toDirEntry (path : System.FilePath) : IO.FS.DirEntry where
-  root := path.parent.getD ""
-  fileName := path.fileName.getD ""
-
-end System.FilePath
-
-open ImportGraph
-
-namespace Lake
-
-/-! ## Missing instances -/
-
-deriving instance Hashable for SemVerCore
-deriving instance Hashable for StdVer
-deriving instance Hashable for LeanVer
-deriving instance Hashable for Date
-deriving instance Hashable for ToolchainVer
-
-deriving instance ToJson, FromJson for Lake.Glob
-
-/-! ## `for ... in` instances -/
-
-/-- Allows iteration over the matched modules via `for (mod, dirEntry) in globMods do`. This is
-typically constructed via `glob.modulesIn dir`. -/
-structure Glob.Modules where
-  glob : Glob
-  dir : System.FilePath
-
-/-- Allows iteration over the modules matched by a `Lake.Glob` in `dir` via
-`for (mod, dirEntry) in glob.modulesIn dir do`. -/
-@[inline] def Glob.modulesIn (dir : System.FilePath) (glob : Glob) : Glob.Modules :=
-  { glob, dir }
-
-/--
-Iterates over the module names selected by `glob`, resolving submodule globs against the `.lean`
-files found under `dir`.
-
-Auxiliary to the `ForIn` instance for `Glob.Modules`.
--/
-@[specialize]
-def Glob.Modules.forIn [Monad m] [MonadLiftT IO m] {β}
-    (spec : Glob.Modules) (init : β)
-    (f : Name × IO.FS.DirEntry → β → m (ForInStep β)) : m β := do
-  match spec.glob with
-  | .one n =>
-    -- Like Lake's `Glob.forEachModuleIn`, which yields `n` unconditionally: we must not require
-    -- `n`'s source file to exist, so build its `DirEntry` without touching the filesystem.
-    let modFile := modToFilePath spec.dir n "lean"
-    return (← f (n, modFile.toDirEntry) init).value
-  | .submodules n =>
-    let modDir := modToFilePath spec.dir n ""
-    -- `ForIn.forIn`, not the `forIn` being defined here (which the local name would shadow).
-    ForIn.forIn (modDir.modules (root := n)) init f
-  | .andSubmodules n =>
-    let modFile := modToFilePath spec.dir n "lean"
-    match ← f (n, modFile.toDirEntry) init with
-    | ForInStep.done b => return b
-    | ForInStep.yield b =>
-      let modDir := modToFilePath spec.dir n ""
-      ForIn.forIn (modDir.modules (root := n)) b f
-
-instance [Monad m] [MonadLiftT IO m] : ForIn m Glob.Modules (Name × IO.FS.DirEntry) where
-  forIn := Glob.Modules.forIn
-
-namespace IO
+namespace ImportGraph.Lake.IO
 
 /-- Loads the lake workspace from the current directory (or, if specified, from `wsDir?`) in `IO`.
 
diff --git a/ImportGraph/Util/Modules.lean b/ImportGraph/Util/Modules.lean
new file mode 100644
index 0000000..6b1d723
--- /dev/null
+++ b/ImportGraph/Util/Modules.lean
@@ -0,0 +1,137 @@
+/-
+Copyright (c) 2026 Thomas R. Murrills. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas R. Murrills
+-/
+module
+
+public import Lake.Config.Glob
+public import Lake.Util.Version
+
+/-!
+# Module traversal utilities
+
+Provides directory and glob iteration, plus the JSON and hashing instances used by workspace
+summaries, without importing Lake workspace configuration or loading.
+-/
+
+open Lean Lake
+
+public section
+
+namespace ImportGraph
+
+namespace System.FilePath
+
+/-- Allows iteration over the modules (any `*.lean` file) under `dir` via
+`for (mod, dirEntry) in mods do`. Usually invoked via `for (mod, dirEntry) in dir.modules do`; see
+`ImportGraph.System.FilePath.modules` for details. -/
+structure Modules where
+  dir : System.FilePath
+  root : Name := .anonymous
+
+/-- Allows iteration over the modules (any `*.lean` file) under `dir` via
+`for (mod, dirEntry) in dir.modules do`, descending into subdirectories (top-down, left-to-right),
+and constructing the module name according to the directory names and `*.lean` filenames.
+
+For example, if `dir` contains `A/B/C.lean`, this iteration visits `(A.B.C, ⟨"A/B", "C.lean"⟩)`.
+
+If `root` is provided, then `root` is prepended to the module names created from paths in the
+directory, e.g. if `dir` contains `A/B/C.lean` and we iterate through
+``for (mod, dirEntry) in dir.modules (root := `Foo)``, this iteration visits
+`(Foo.A.B.C, ⟨"A/B", "C.lean"⟩)`.
+
+By default, no root is inferred. -/
+@[inline] def modules (dir : System.FilePath) (root := Name.anonymous) : Modules := { dir, root }
+
+@[specialize]
+partial def Modules.forInAux [Monad m] [MonadLiftT IO m] {β}
+    (dir : System.FilePath) (pre : Name) (b : β)
+    (f : Name × IO.FS.DirEntry → β → m (ForInStep β)) : m (ForInStep β) := do
+  let mut b := b
+  for entry in ← dir.readDir do
+    if (← liftM (m := IO) <| entry.path.isDir) then
+      match (← Modules.forInAux entry.path (.str pre entry.fileName) b f) with
+      | ForInStep.yield b' => b := b'
+      | ForInStep.done b'  => return ForInStep.done b'
+    else if entry.path.extension.isEqSome "lean" then
+      let mod := .str pre <| (System.FilePath.withExtension entry.fileName "").toString
+      match (← f (mod, entry) b) with
+      | ForInStep.yield b' => b := b'
+      | ForInStep.done b'  => return ForInStep.done b'
+  return ForInStep.yield b
+
+instance [Monad m] [MonadLiftT IO m] : ForIn m Modules (Name × IO.FS.DirEntry) where
+  forIn spec init f := ForInStep.value <$> Modules.forInAux spec.dir spec.root init f
+
+/--
+Splits `path` into the `DirEntry` for its enclosing directory and file name, as `readDir` would
+report it. `path.parent` (rather than `path.withFileName ""`) is used for `root` so that it carries
+no trailing separator and so that `root / fileName` round-trips back to `path` (matching the entries
+produced when iterating through a directory).
+-/
+def toDirEntry (path : System.FilePath) : IO.FS.DirEntry where
+  root := path.parent.getD ""
+  fileName := path.fileName.getD ""
+
+end System.FilePath
+
+open ImportGraph
+
+namespace Lake
+
+/-! ## Missing instances -/
+
+deriving instance Hashable for SemVerCore
+deriving instance Hashable for StdVer
+deriving instance Hashable for LeanVer
+deriving instance Hashable for Date
+deriving instance Hashable for ToolchainVer
+
+deriving instance ToJson, FromJson for Lake.Glob
+
+/-! ## `for ... in` instances -/
+
+/-- Allows iteration over the matched modules via `for (mod, dirEntry) in globMods do`. This is
+typically constructed via `glob.modulesIn dir`. -/
+structure Glob.Modules where
+  glob : Glob
+  dir : System.FilePath
+
+/-- Allows iteration over the modules matched by a `Lake.Glob` in `dir` via
+`for (mod, dirEntry) in glob.modulesIn dir do`. -/
+@[inline] def Glob.modulesIn (dir : System.FilePath) (glob : Glob) : Glob.Modules :=
+  { glob, dir }
+
+/--
+Iterates over the module names selected by `glob`, resolving submodule globs against the `.lean`
+files found under `dir`.
+
+Auxiliary to the `ForIn` instance for `Glob.Modules`.
+-/
+@[specialize]
+def Glob.Modules.forIn [Monad m] [MonadLiftT IO m] {β}
+    (spec : Glob.Modules) (init : β)
+    (f : Name × IO.FS.DirEntry → β → m (ForInStep β)) : m β := do
+  match spec.glob with
+  | .one n =>
+    -- Like Lake's `Glob.forEachModuleIn`, which yields `n` unconditionally: we must not require
+    -- `n`'s source file to exist, so build its `DirEntry` without touching the filesystem.
+    let modFile := modToFilePath spec.dir n "lean"
+    return (← f (n, modFile.toDirEntry) init).value
+  | .submodules n =>
+    let modDir := modToFilePath spec.dir n ""
+    -- `ForIn.forIn`, not the `forIn` being defined here (which the local name would shadow).
+    ForIn.forIn (modDir.modules (root := n)) init f
+  | .andSubmodules n =>
+    let modFile := modToFilePath spec.dir n "lean"
+    match ← f (n, modFile.toDirEntry) init with
+    | ForInStep.done b => return b
+    | ForInStep.yield b =>
+      let modDir := modToFilePath spec.dir n ""
+      ForIn.forIn (modDir.modules (root := n)) b f
+
+instance [Monad m] [MonadLiftT IO m] : ForIn m Glob.Modules (Name × IO.FS.DirEntry) where
+  forIn := Glob.Modules.forIn
+
+end ImportGraph.Lake
diff --git a/ImportGraph/WorkspaceModel/Base.lean b/ImportGraph/WorkspaceModel/Base.lean
index 380317c..7da1b69 100644
--- a/ImportGraph/WorkspaceModel/Base.lean
+++ b/ImportGraph/WorkspaceModel/Base.lean
@@ -8,7 +8,7 @@ module
 public import Lake.Config.Glob
 public import Lake.Util.Version
 
-import ImportGraph.Lake
+import ImportGraph.Util.Modules
 
 /-!
 # Basic Lake workspace data
diff --git a/ImportGraph/WorkspaceModel/Build.lean b/ImportGraph/WorkspaceModel/Build.lean
index 2aca329..cb3b8d3 100644
--- a/ImportGraph/WorkspaceModel/Build.lean
+++ b/ImportGraph/WorkspaceModel/Build.lean
@@ -10,7 +10,7 @@ public import ImportGraph.WorkspaceModel.Summary
 public import ImportGraph.Shake.Algebra
 
 import Lean.Elab.ParseImportsFast
-import ImportGraph.Lake
+import ImportGraph.Util.Modules
 
 /-!
 # Building a `WorkspaceModel`
diff --git a/ImportGraph/WorkspaceModel/Summary.lean b/ImportGraph/WorkspaceModel/Summary.lean
index a7cfd5b..b16f9d2 100644
--- a/ImportGraph/WorkspaceModel/Summary.lean
+++ b/ImportGraph/WorkspaceModel/Summary.lean
@@ -9,14 +9,15 @@ public import ImportGraph.WorkspaceModel.Summary.Core
 public import ImportGraph.WorkspaceModel.Summary.Get
 
 /-!
-Importing this file downstream is "safe", and only transitively introduces the following small Lake
-dependencies:
+Importing this file downstream is "safe", and introduces the following small Lake dependencies
+for its public field types:
 ```
 public import Lake.Config.Glob
 public import Lake.Util.Version
 ```
-Both of these files do not transitively import any further Lake dependencies. They are necessary
-for the types `Glob` and `ToolchainVer` in `WorkspaceSummary` field types.
+These provide `Glob` and `ToolchainVer` in `WorkspaceSummary` field types. Cache validation also
+uses `Lake.Build.Trace` for hashing. None of these imports brings in Lake workspace loading or
+the build type-family axioms.
 
 For Lake interaction with `WorkspaceSummary`, import `ImportGraph.WorkspaceModel.Summary.Lake`.
 -/
diff --git a/ImportGraph/WorkspaceModel/Summary/Cache.lean b/ImportGraph/WorkspaceModel/Summary/Cache.lean
new file mode 100644
index 0000000..37f2e15
--- /dev/null
+++ b/ImportGraph/WorkspaceModel/Summary/Cache.lean
@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2026 Thomas R. Murrills. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas R. Murrills
+-/
+module
+
+public import Lake.Build.Trace
+public import ImportGraph.WorkspaceModel.Summary.Core
+
+import ImportGraph.Util.Modules
+
+/-!
+# Workspace summary cache validation
+
+Computes hashes from the paths stored in a workspace summary. This file does not import Lake
+workspace configuration or loading; extraction from a live workspace belongs in `Summary.Lake`.
+-/
+
+public section
+
+open Lean Lake System
+
+namespace ImportGraph.Lake
+
+/-- Internal helper shared by cache validation and the workspace-summary executable.
+Hashes the toolchain identity and workspace configuration files. -/
+def computeInputHash (leanGitHash : String) (ver : Option ToolchainVer)
+    (manifestFile packageOverridesFile : FilePath)
+    (packageConfigs : Array FilePath) : IO Hash := do
+  let mut hash := Hash.ofHashable ver
+  hash := hash.mix <| Hash.ofText leanGitHash
+  hash := hash.mix <|← Hash.ofText <$> IO.FS.readFile manifestFile
+  if ← packageOverridesFile.pathExists then
+    try
+      hash := hash.mix <|← Hash.ofText <$> IO.FS.readFile packageOverridesFile
+    catch _ => pure () -- ignore it if something went wrong
+  -- Note: `packageConfigs` should (and by default does) include the root package's config as well.
+  for configFile in packageConfigs do
+    hash := hash.mix <|← Hash.ofText <$> IO.FS.readFile configFile
+  return hash
+
+/-- Recomputes the input hash for the `WorkspaceSummary` by re-hashing the files at the given
+paths. Also mixes in the hash for the given lean version. -/
+def WorkspaceSummary.recomputedInputHash (leanGitHash : String) (ws : WorkspaceSummary) :
+    IO Hash := do
+  computeInputHash leanGitHash (← ToolchainVer.ofDir? ws.dir)
+    (manifestFile := ws.manifestFile)
+    (packageOverridesFile := ws.packageOverridesFile)
+    (packageConfigs := ws.packages.map (·.configFile))
+
+/-- Recomputes the hash of the data referred to by the paths in `WorkspaceSummary` and compares it
+to the hash in `WorkspaceSummary`, using the current lean process's git hash.
+
+If `wsDir?` is provided, ensures that the workspace directory provided in the summary is the same
+as the given `wsDir`, else considers it not up-to-date. -/
+def WorkspaceSummary.isUpToDate (ws : WorkspaceSummary) (wsDir? : Option FilePath := none) :
+    IO Bool := do
+  try
+    if let some wsDir := wsDir? then
+      unless (← IO.FS.realPath ws.dir).normalize == (← IO.FS.realPath wsDir).normalize do
+        return false
+    return (← ws.recomputedInputHash Lean.githash).val == ws.inputHash
+  catch _ =>
+    return false
+
+end ImportGraph.Lake
diff --git a/ImportGraph/WorkspaceModel/Summary/Core.lean b/ImportGraph/WorkspaceModel/Summary/Core.lean
index ab7b06d..baf5f03 100644
--- a/ImportGraph/WorkspaceModel/Summary/Core.lean
+++ b/ImportGraph/WorkspaceModel/Summary/Core.lean
@@ -8,7 +8,7 @@ module
 public import Lean.Data.Json
 public import ImportGraph.WorkspaceModel.Base
 
-import ImportGraph.Lake
+import ImportGraph.Util.Modules
 
 /-!
 # Transporting a Lake workspace summary over Json
diff --git a/ImportGraph/WorkspaceModel/Summary/Get.lean b/ImportGraph/WorkspaceModel/Summary/Get.lean
index 0d12058..08d28ed 100644
--- a/ImportGraph/WorkspaceModel/Summary/Get.lean
+++ b/ImportGraph/WorkspaceModel/Summary/Get.lean
@@ -7,7 +7,7 @@ module
 
 public import ImportGraph.WorkspaceModel.Summary.Core
 
-import ImportGraph.WorkspaceModel.Summary.Lake
+import ImportGraph.WorkspaceModel.Summary.Cache
 
 open ImportGraph Lean Lake System
 
diff --git a/ImportGraph/WorkspaceModel/Summary/Lake.lean b/ImportGraph/WorkspaceModel/Summary/Lake.lean
index 94a876e..8d45c73 100644
--- a/ImportGraph/WorkspaceModel/Summary/Lake.lean
+++ b/ImportGraph/WorkspaceModel/Summary/Lake.lean
@@ -6,31 +6,25 @@ Authors: Thomas R. Murrills
 module
 
 public import Lake.Config.Workspace
-public import ImportGraph.WorkspaceModel.Summary.Core
+public import ImportGraph.WorkspaceModel.Summary.Cache
 
 import ImportGraph.Lake
 
+/-!
+# Extraction from a Lake workspace
+
+This file must not be imported by modules reachable from `ImportGraph` or `ImportGraph.Tools`;
+see `ImportGraphTest.NoLakeAxioms`. Library consumers needing cache validation should import
+`ImportGraph.WorkspaceModel.Summary.Cache` instead. The workspace-summary executable uses this
+file to extract a summary from a loaded workspace.
+-/
+
 public section
 
 open ImportGraph Lean Lake System
 
 namespace ImportGraph.Lake
 
-private def computeInputHash (leanGitHash : String) (ver : Option ToolchainVer)
-    (manifestFile packageOverridesFile : FilePath)
-    (packageConfigs : Array FilePath) : IO Hash := do
-  let mut hash := Hash.ofHashable ver
-  hash := hash.mix <| Hash.ofText leanGitHash
-  hash := hash.mix <|← Hash.ofText <$> IO.FS.readFile manifestFile
-  if ← packageOverridesFile.pathExists then
-    try
-      hash := hash.mix <|← Hash.ofText <$> IO.FS.readFile packageOverridesFile
-    catch _ => pure () -- ignore it if something went wrong
-  -- Note: `packageConfigs` should (and by default does) include the root package's config as well.
-  for configFile in packageConfigs do
-    hash := hash.mix <|← Hash.ofText <$> IO.FS.readFile configFile
-  return hash
-
 /-- Computes the hash for the given workspace to persist in the summary. This should agree with the
 recomputed hash from the workspace summary if no changes are made to the package configuration. -/
 nonrec def Workspace.computeInputHash (ws : Lake.Workspace) : IO Hash := do
@@ -41,30 +35,6 @@ nonrec def Workspace.computeInputHash (ws : Lake.Workspace) : IO Hash := do
     (packageOverridesFile := ws.packageOverridesFile)
     (packageConfigs := ws.packages.map (·.configFile))
 
-/-- Recomputes the input hash for the `WorkspaceSummary` by re-hashing the files at the given
-paths. Also mixes in the hash for the given lean version. -/
-def WorkspaceSummary.recomputedInputHash (leanGitHash : String) (ws : WorkspaceSummary) :
-    IO Hash := do
-  computeInputHash leanGitHash (← ToolchainVer.ofDir? ws.dir)
-    (manifestFile := ws.manifestFile)
-    (packageOverridesFile := ws.packageOverridesFile)
-    (packageConfigs := ws.packages.map (·.configFile))
-
-/-- Recomputes the hash of the data referred to by the paths in `WorkspaceSummary` and compares it
-to the hash in `WorkspaceSummary`, using the current lean process's git hash.
-
-If `wsDir?` is provided, ensures that the workspace directory provided in the summary is the same
-as the given `wsDir`, else considers it not up-to-date. -/
-def WorkspaceSummary.isUpToDate (ws : WorkspaceSummary) (wsDir? : Option FilePath := none) :
-    IO Bool := do
-  try
-    if let some wsDir := wsDir? then
-      unless (← IO.FS.realPath ws.dir).normalize == (← IO.FS.realPath wsDir).normalize do
-        return false
-    return (← ws.recomputedInputHash Lean.githash).val == ws.inputHash
-  catch _ =>
-    return false
-
 /-- Summarize a loaded `Lake.Workspace` for transport over Json. -/
 def WorkspaceSummary.ofWorkspace (ws : Lake.Workspace)
     (version : Option ToolchainVer) (inputHash : Hash) : WorkspaceSummary where
diff --git a/ImportGraphTest.lean b/ImportGraphTest.lean
index 8bbe2fc..dde505f 100644
--- a/ImportGraphTest.lean
+++ b/ImportGraphTest.lean
@@ -7,6 +7,7 @@ import ImportGraphTest.Html
 import ImportGraphTest.Imports
 import ImportGraphTest.ImportPretty
 import ImportGraphTest.NormImports
+import ImportGraphTest.NoLakeAxioms
 import ImportGraphTest.Shake.Algebra
 import ImportGraphTest.Shake.Workspace
 import ImportGraphTest.ToTarget
diff --git a/ImportGraphTest/NoLakeAxioms.lean b/ImportGraphTest/NoLakeAxioms.lean
new file mode 100644
index 0000000..293a860
--- /dev/null
+++ b/ImportGraphTest/NoLakeAxioms.lean
@@ -0,0 +1,22 @@
+-- Deliberately omit `module`: ordinary imports load private dependencies too.
+import ImportGraph
+import ImportGraph.Tools
+
+open Lean in
+run_cmd do
+  let env ← getEnv
+  let modules := env.header.moduleNames
+  for moduleName in [`Lake.Config.Workspace, `Lake.Load.Workspace, `Lake.Config.Kinds,
+      `Lake.Build.Data, `Lake.Build.Facets, `Lake.Build.Infos, `Lake.DSL.Targets,
+      `ImportGraph.Lake, `ImportGraph.WorkspaceModel.Summary.Lake,
+      `ImportGraph.WorkspaceModel.Emit] do
+    if modules.contains moduleName then
+      throwError "Unexpected workspace/build import: {moduleName}"
+  unless modules.contains `ImportGraph.WorkspaceModel.Summary.Cache &&
+      (env.find? `ImportGraph.Lake.WorkspaceSummary.isUpToDate).isSome do
+    throwError "Workspace summary cache validation was not imported"
+  for (name, info) in env.constants do
+    if (`Lake).isPrefixOf name && (info matches .axiomInfo _) then
+      throwError "Unexpected Lake axiom after importing import-graph tools: {name}"
+  if (env.find? `ImportGraph.Lake.IO.getWorkspace).isSome then
+    throwError "Lake workspace loader leaked through import-graph tools"
diff --git a/ImportGraphTest/Shake/Workspace.lean b/ImportGraphTest/Shake/Workspace.lean
index 1c55fb6..7feb273 100644
--- a/ImportGraphTest/Shake/Workspace.lean
+++ b/ImportGraphTest/Shake/Workspace.lean
@@ -1,7 +1,8 @@
 module
 
 meta import ImportGraph.WorkspaceModel.Build
-import Lean.Elab.Command
+meta import ImportGraph.WorkspaceModel.Summary.Cache
+meta import Lean.Elab.Command
 
 /-!
 The following tests assume that `ImportGraph.WorkspaceModel.Build` has
@@ -110,6 +111,8 @@ run_cmd
 -- The following test checks that we've found the correct toolchain data.
 run_cmd do
   let s ← getWorkspaceSummary
+  unless ← s.isUpToDate (wsDir? := ← IO.currentDir) do
+    throwError "Workspace summary cache not considered up to date"
   let lakeSrc := s.lakeSrcDir / "Lake.lean"
   unless ← lakeSrc.pathExists do
     throwError "Lake.lean not at {lakeSrc}"