diff --git a/PurityPlugin.lean b/PurityPlugin.lean
new file mode 100644
index 0000000000..af8caf790b
--- /dev/null
+++ b/PurityPlugin.lean
@@ -0,0 +1,239 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+import Lean
+
+/-! # Purity Plugin
+
+A Lean compiler plugin that ensures impure modules are always re-elaborated.
+
+## How it works
+
+1. **At plugin load** (start of each `lake build`): For every `.lean` source file
+   that does NOT have a `.pure` marker in `.lake/build/lib/lean/`, delete its
+   `.trace` file so Lake rebuilds it.
+
+2. **During elaboration**: A linter runs after each command. It optimistically
+   writes a `.pure` marker. If any impure command is detected, it deletes the
+   marker. At the end of elaboration, only pure modules retain their marker.
+
+Markers live in `.lake/build/lib/lean/` alongside `.olean` files, so they're
+automatically cleaned by `lake clean` and ignored by git.
+
+**Safe by default**: no `.pure` marker = rebuild.
+-/
+
+open Lean
+
+namespace Strata.PurityPlugin
+
+/-- Commands whose elaboration is known to be pure.
+
+## Audit methodology
+
+Each entry was verified by checking the elaborator source in
+`~/.elan/toolchains/leanprover--lean4---v4.29.1/src/lean/Lean/Elab/`.
+A command is pure if its elaborator only modifies the `Environment`
+(adding declarations, setting attributes, modifying scopes) without
+performing `IO` actions that depend on external state.
+
+## Audit results (Lean v4.29.1)
+
+### Declarations — `Lean/Elab/Declaration.lean`, `Lean/Elab/Structure.lean`, etc.
+`declaration` covers `def`, `theorem`, `abbrev`, `opaque`, `instance`,
+`axiom`, `structure`, `class`, `inductive`. These elaborate types and terms,
+add declarations to the environment, and run type-checking. No IO.
+`deriving` generates instances via deriving handlers. Handlers modify the
+environment but don't perform IO.
+`example` elaborates a term and discards it. No persistent effect, no IO.
+
+### Structural — `Lean/Elab/BuiltinCommand.lean`
+`section`, `namespace`, `end`, `variable`, `universe`, `open`, `export`,
+`import`, `mutual`, `in`, `include`, `omit`, `withWeakNamespace`,
+`withExporting`: These modify scopes, namespaces, and open declarations.
+Pure environment operations only.
+
+### Options/attributes — `Lean/Elab/BuiltinCommand.lean`, `Lean/Elab/DeclModifiers.lean`
+`set_option`: Sets an option in the environment. Pure.
+`attribute`: Adds/removes attributes. Pure (attribute handlers may run
+elaboration but not IO).
+
+### Inspection — `Lean/Elab/BuiltinCommand.lean`, `Lean/Elab/Print.lean`
+`check`, `check_failure`, `print`, `printSig`, `printAxioms`, `printEqns`,
+`printTacTags`, `where`, `version`, `synth`: These produce messages but
+don't modify the environment or perform IO beyond message logging (which
+is internal to the elaboration monad, not external IO).
+
+### Assertions — `Lean/Elab/BuiltinCommand.lean`
+`assertNotExists`, `assertNotImported`, `checkAssertions`: Check
+environment properties and produce errors if violated. Pure.
+
+### Documentation — `Lean/Elab/BuiltinCommand.lean`
+`moduleDoc`, `addDocString`: Add documentation to the environment. Pure.
+
+### Syntax/notation — `Lean/Elab/Notation.lean`, `Lean/Elab/Syntax.lean`, etc.
+`syntax`, `syntaxAbbrev`, `syntaxCat`, `notation`, `macro`, `macro_rules`,
+`elab`, `elab_rules`, `scoped`, `local`, `infix`/`infixl`/`infixr`/
+`prefix`/`postfix`, `declare_syntax_cat`, `declare_config_elab`, etc.:
+These register parsers and elaborators in the environment. Pure.
+
+### Simproc — `Lean/Elab/Tactic/Simproc.lean`
+`simproc`, `builtin_simproc`, `dsimproc`, `builtin_dsimproc`: Register
+simplification procedures. Pure.
+
+### Misc — various
+`register_simp_attr`, `register_option`, `register_builtin_option`,
+`register_label_attr`: Register metadata. Pure.
+`register_tactic_tag`, `tactic_extension`, `recommended_spelling`,
+`genInjectiveTheorems`, `registerErrorExplanationStx`: Metadata/codegen. Pure.
+`init_quot`: Initializes quotient type. Pure kernel operation.
+`exit`, `eoi`: Terminate elaboration. Pure.
+`grindPattern`, `binderPredicate`, `mixfix`: Syntax definitions. Pure.
+`Lean.Option.registerOption`, `Lean.Option.registerBuiltinOption`:
+Macros expanding to option registration. Pure.
+
+## NOT on the allowlist (known impure or unknown)
+
+Per the purity definition: a command is impure if its elaboration could read
+state not determined by the module's source and its dependencies' content, or
+mutate state beyond stdout/stderr.
+
+`eval`, `evalBang`: Execute arbitrary code that may perform IO. IMPURE.
+`initialize`: Runs an `IO` action at module load. Even though many only
+  create refs or register extensions, we cannot statically distinguish safe
+  from unsafe. IMPURE.
+`guard`: Evaluates an expression at elaboration time. Could depend on
+  external state via `native_decide` or IO-capable code. IMPURE.
+`run_cmd`, `run_elab`, `run_meta`: Execute monadic code with IO access. IMPURE.
+
+`guard_msgs`: Pure by itself — it wraps another command and checks output
+  against source text. The wrapped command is elaborated separately and
+  checked by the linter independently. (Note: Lean skips linters for
+  `#guard_msgs` but runs them on the inner command.)
+
+Any unknown/unrecognized command: Conservatively treated as IMPURE.
+-/
+private def pureCommandKinds : Std.HashSet SyntaxNodeKind := .ofList [
+  ``Lean.Parser.Command.declaration, ``Lean.Parser.Command.«deriving»,
+  ``Lean.Parser.Command.«section», ``Lean.Parser.Command.«namespace»,
+  ``Lean.Parser.Command.«end», ``Lean.Parser.Command.«variable»,
+  ``Lean.Parser.Command.«universe», ``Lean.Parser.Command.«open»,
+  ``Lean.Parser.Command.«export», ``Lean.Parser.Command.«import»,
+  ``Lean.Parser.Command.«mutual», ``Lean.Parser.Command.«in»,
+  ``Lean.Parser.Command.«include», ``Lean.Parser.Command.«omit»,
+  ``Lean.Parser.Command.withWeakNamespace, ``Lean.Parser.Command.withExporting,
+  ``Lean.Parser.Command.«set_option», ``Lean.Parser.Command.«attribute»,
+  ``Lean.Parser.Command.check, ``Lean.Parser.Command.check_failure,
+  ``Lean.Parser.Command.print, ``Lean.Parser.Command.printSig,
+  ``Lean.Parser.Command.printAxioms, ``Lean.Parser.Command.printEqns,
+  ``Lean.Parser.Command.printTacTags, ``Lean.Parser.Command.«where»,
+  ``Lean.Parser.Command.version, ``Lean.Parser.Command.synth,
+  ``Lean.Parser.Command.assertNotExists, ``Lean.Parser.Command.assertNotImported,
+  ``Lean.Parser.Command.checkAssertions,
+  ``Lean.Parser.Command.moduleDoc, ``Lean.Parser.Command.addDocString,
+  ``Lean.Parser.Command.«register_tactic_tag»,
+  ``Lean.Parser.Command.«tactic_extension»,
+  ``Lean.Parser.Command.«recommended_spelling»,
+  ``Lean.Parser.Command.genInjectiveTheorems,
+  ``Lean.Parser.Command.registerErrorExplanationStx,
+  ``Lean.Parser.Command.«init_quot», ``Lean.Parser.Command.exit,
+  ``Lean.Parser.Command.eoi,
+  `Lean.Option.registerOption, `Lean.Option.registerBuiltinOption,
+  -- Syntax/notation/macro definitions (previously matched by prefix)
+  ``Lean.Parser.Command.syntax, ``Lean.Parser.Command.syntaxAbbrev,
+  ``Lean.Parser.Command.syntaxCat, ``Lean.Parser.Command.notation,
+  ``Lean.Parser.Command.macro, ``Lean.Parser.Command.macro_rules,
+  ``Lean.Parser.Command.elab, ``Lean.Parser.Command.elab_rules,
+  `Lean.Parser.Command.«scoped», `Lean.Parser.Command.«local»,
+  `Lean.Parser.Command.simproc, `Lean.Parser.Command.builtin_simproc,
+  `Lean.Parser.Command.dsimproc, `Lean.Parser.Command.builtin_dsimproc,
+  `Lean.Parser.Command.register_simp_attr,
+  `Lean.Parser.Command.register_option, `Lean.Parser.Command.register_builtin_option,
+  `Lean.Parser.Command.register_label_attr,
+  ``Lean.Parser.Command.«infix», ``Lean.Parser.Command.«infixl»,
+  ``Lean.Parser.Command.«infixr», ``Lean.Parser.Command.«prefix»,
+  ``Lean.Parser.Command.«postfix»,
+  `Lean.Parser.Command.declare_syntax_cat, `Lean.Parser.Command.declare_config_elab,
+  `Lean.Parser.Command.declare_command_config_elab,
+  `Lean.Parser.Command.declare_config_getter,
+  `Lean.Parser.Command.declare_simp_like_tactic,
+  `Lean.Parser.Command.declare_tagged_region,
+  ``Lean.Parser.Command.mixfix, ``Lean.Parser.Command.grindPattern,
+  ``Lean.Parser.Command.binderPredicate
+]
+
+private def isPureCommand (kind : SyntaxNodeKind) : Bool :=
+  pureCommandKinds.contains kind || kind == nullKind
+
+/-- Convert a source path to the build artifact stem.
+`Strata/DDM/Elab/Env.lean` → `.lake/build/lib/lean/Strata/DDM/Elab/Env`
+Handles absolute paths by stripping the CWD prefix. -/
+private def toBuildStem (srcPath : String) : IO String := do
+  let cwd ← IO.currentDir
+  let rel := if srcPath.startsWith cwd.toString
+    then ((srcPath.drop cwd.toString.length).dropWhile (· == '/')).toString
+    else srcPath
+  let stem := if rel.endsWith ".lean" then (rel.dropEnd 5).toString else rel
+  return s!".lake/build/lib/lean/{stem}"
+
+private partial def findLeanFiles (root : System.FilePath) : IO (Array System.FilePath) := do
+  let mut result := #[]
+  if ← root.isDir then
+    for entry in ← root.readDir do
+      result := result ++ (← findLeanFiles entry.path)
+  else if root.extension == some "lean" then
+    result := result.push root
+  return result
+
+/-- At plugin load: delete traces for modules without .pure markers. -/
+private def invalidateImpureTraces : IO Unit := do
+  let lockFile : System.FilePath := ".lake/build/purity_cleanup.lock"
+  if ← lockFile.pathExists then return
+  try IO.FS.writeFile lockFile "" catch _ => return
+  for dir in #["Strata", "StrataTest"] do
+    let path : System.FilePath := dir
+    if ← path.isDir then
+      let files ← findLeanFiles path
+      for file in files do
+        let stem ← toBuildStem file.toString
+        let pureMarker : System.FilePath := stem ++ ".pure"
+        unless ← pureMarker.pathExists do
+          try IO.FS.removeFile (stem ++ ".trace") catch _ => pure ()
+  for extra in #["StrataMain.lean"] do
+    let file : System.FilePath := extra
+    if ← file.pathExists then
+      let stem ← toBuildStem extra
+      let pureMarker : System.FilePath := stem ++ ".pure"
+      unless ← pureMarker.pathExists do
+        try IO.FS.removeFile (stem ++ ".trace") catch _ => pure ()
+  try IO.FS.removeFile lockFile catch _ => pure ()
+
+initialize invalidateImpureTraces
+
+/-- Linter: optimistically write .pure marker on first pure command.
+Delete it if any impure command is seen. -/
+initialize Lean.addLinter {
+  name := `Strata.purityPlugin
+  run := fun stx => do
+    let ctx ← readThe Lean.Elab.Command.Context
+    let fileName := ctx.fileName
+    if fileName.isEmpty then return
+    let stem ← toBuildStem fileName
+    let pureMarker := stem ++ ".pure"
+    let kind := stx.getKind
+    if kind == nullKind then return
+    if !isPureCommand kind then
+      try IO.FS.removeFile pureMarker catch _ => pure ()
+    else
+      let markerExists ← (System.FilePath.mk pureMarker).pathExists
+      unless markerExists do
+        let parent := (System.FilePath.mk pureMarker).parent.getD "."
+        try IO.FS.createDirAll parent catch _ => pure ()
+        IO.FS.writeFile pureMarker ""
+}
+
+end Strata.PurityPlugin
diff --git a/docs/LakeCacheSkimmer.md b/docs/LakeCacheSkimmer.md
new file mode 100644
index 0000000000..3c7686e768
--- /dev/null
+++ b/docs/LakeCacheSkimmer.md
@@ -0,0 +1,161 @@
+# Lake Cache Skimmer: Design Document
+
+## Problem
+
+Lean's `lake build` caches elaboration results in `.olean` files. When a module's
+elaboration depends on external state (file system, SMT solvers, network, etc.),
+the cached result may be stale — but Lake has no way to know this, since it only
+tracks source file changes and dependency graphs.
+See https://github.com/leanprover/lean4/issues/13449.
+
+We need a mechanism that identifies modules whose elaboration *might* depend on
+external state and forces `lake build` to re-elaborate them.
+
+
+## Definition of Purity
+
+A Lean module is **pure** if replaying its build trace produces exactly the same
+observable behavior, given that:
+
+1. The module's source content has not changed, and
+2. The content of all of its transitive dependencies has not changed.
+
+Equivalently, a module is **impure** if its elaboration:
+
+- **Reads** any state not determined by (1) and (2) above — e.g., file system
+  contents outside the dependency graph, environment variables, network state,
+  timestamps, random values, or
+- **Mutates** any state other than stdout and stderr output (which is captured
+  by the build trace).
+
+### Implications
+
+Under this definition:
+
+- **`initialize`** is impure: it runs an arbitrary `IO` action that *could* read
+  external state. We cannot statically distinguish safe from unsafe `initialize`
+  blocks, so all are conservatively impure.
+- **`#eval` / `#eval!`** is impure: executes arbitrary code that could perform IO.
+- **`#guard`** is impure: evaluates an expression at elaboration time.
+- **`run_cmd` / `run_elab` / `run_meta`** are impure: execute monadic code with
+  IO access.
+- **`#guard_msgs`** is pure *by itself*: it wraps another command and checks its
+  output against source text. The wrapped command is checked independently by the
+  linter. (Note: Lean skips linters for `#guard_msgs`, but runs them on the inner
+  command.)
+- **`declaration`** (`def`, `theorem`, etc.) is pure.
+- **Inspection commands** (`#check`, `#print`, etc.) are pure.
+
+## Design Goals
+
+1. **Soundness**: If we identify a module as pure, it must be impossible for its
+   elaboration to have read external state or mutated state beyond stdout/stderr.
+
+2. **Precision**: Minimize false positives (pure modules incorrectly flagged as
+   impure).
+
+3. **Zero workflow change**: Developers should just run `lake build` with no
+   extra steps.
+
+## Solution: Lake Compiler Plugin
+
+The solution is a **Lean compiler plugin** (`PurityPlugin.lean`) that runs
+automatically during every `lake build`. No separate tools or scripts needed.
+
+### How It Works
+
+The plugin uses an **inverted marker** design — safe by default:
+
+1. **At plugin load** (start of each `lake build`): For every `.lean` source file
+   that does NOT have a `.pure` marker in `.lake/build/lib/lean/`, delete its
+   `.trace` file. This causes Lake to rebuild that module.
+
+2. **During elaboration**: A linter (registered via `Lean.addLinter`) runs after
+   each command. It checks the command's syntax kind against a pure allowlist.
+   - If all commands are pure: a `.pure` marker file is written.
+   - If any impure command is detected: the `.pure` marker is deleted.
+
+3. **Result**: After the build, pure modules have `.pure` markers and will be
+   cached on the next build. Impure modules have no markers and will be rebuilt.
+
+### Safety Properties
+
+- **No marker = rebuild**: If the plugin fails to run, a new file is added, or
+  anything unexpected happens, there's no `.pure` marker, so the module gets
+  rebuilt. This is the safe default.
+- **`lake clean` triggers full rebuild**: Cleaning removes all markers, so the
+  next build re-elaborates everything and re-establishes markers.
+- **First build after adding the plugin**: All modules are rebuilt (no markers
+  exist yet). This is expected and correct.
+
+### Configuration
+
+In `lakefile.toml`:
+
+```toml
+[[lean_lib]]
+name = "PurityPlugin"
+defaultFacets = ["shared"]
+
+[[lean_lib]]
+name = "Strata"
+plugins = ["PurityPlugin:shared"]
+```
+
+The plugin is built as a shared library and loaded via `lean --plugin` during
+elaboration of every module in the `Strata` library.
+
+### Pure Command Allowlist
+
+The plugin maintains an allowlist of command syntax kinds known to be pure.
+Any command NOT on the allowlist is conservatively treated as impure.
+
+The allowlist was audited against Lean v4.29.1 source code. See the inline
+documentation in `PurityPlugin.lean` for the full audit.
+
+The allowlist approach is **sound**: unknown commands default to impure (false
+positives, not false negatives). The allowlist should be re-audited when
+upgrading the Lean toolchain.
+
+### Linter API
+
+The plugin uses `Lean.addLinter` to register a callback that runs after every
+top-level command elaboration. Key properties:
+
+- Linters run inside `withoutModifyingEnv`, so they cannot modify the `.olean`.
+  Instead, the plugin writes `.pure` marker files via IO (which IS available
+  in `CommandElabM`).
+- Linters are skipped for `#guard_msgs`, but run on the inner command. This
+  means `#guard_msgs in #eval foo` correctly detects `#eval` as impure.
+- Each module is elaborated in its own Lean process, so the linter state is
+  fresh for each file.
+
+### Marker File Layout
+
+Markers are stored alongside `.olean` files in `.lake/build/lib/lean/`:
+
+```
+.lake/build/lib/lean/Strata/DDM/Elab/Env.olean   # build artifact
+.lake/build/lib/lean/Strata/DDM/Elab/Env.trace    # Lake's build trace
+.lake/build/lib/lean/Strata/DDM/Elab/Env.pure     # purity marker (if pure)
+```
+
+This means:
+- Markers are automatically cleaned by `lake clean`
+- Markers are in `.lake/` which is gitignored
+- No source tree pollution
+
+## Open Questions
+
+1. **Toolchain upgrades**: The pure command allowlist is pinned to a specific
+   Lean version. New impure commands in future Lean versions would not be on
+   the allowlist and would correctly default to impure (safe). However, if a
+   previously-pure command becomes impure, the allowlist would need updating.
+
+2. **Custom `@[command_elab]` elaborators**: The plugin sees the command's
+   syntax kind but can't know whether a custom elaborator performs IO. Unknown
+   command kinds are treated as impure (conservative).
+
+3. **Plugin loading for other libraries**: Currently the plugin is configured
+   only for the `Strata` library. To cover `StrataTest` and other libraries,
+   they would also need `plugins = ["PurityPlugin:shared"]` in their config.
diff --git a/lakefile.toml b/lakefile.toml
index 3010e6ef3a..3e786898c4 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -9,8 +9,13 @@ name = "plausible"
 git = "https://github.com/leanprover-community/plausible.git"
 rev = "bump_to_v4.29.0-rc8"
 
+[[lean_lib]]
+name = "PurityPlugin"
+defaultFacets = ["shared"]
+
 [[lean_lib]]
 name = "Strata"
+plugins = ["PurityPlugin:shared"]
 
 [[lean_exe]]
 name = "strata"