diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean
index 0dc4a0096c05..ae1b5ad83685 100644
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@@ -180,9 +180,11 @@ structure TagAttribute where
 def registerTagAttribute (name : Name) (descr : String)
     (validate : Name → AttrM Unit := fun _ => pure ()) (ref : Name := by exact decl_name%)
     (applicationTime := AttributeApplicationTime.afterTypeChecking)
-    (asyncMode : EnvExtension.AsyncMode := .mainOnly) : IO TagAttribute := do
+    (asyncMode : EnvExtension.AsyncMode := .mainOnly)
+    (declCovered : Bool := false) : IO TagAttribute := do
   let ext : PersistentEnvExtension Name Name NameSet ← registerPersistentEnvExtension {
     name            := ref
+    declCovered    := declCovered
     mkInitial       := pure {}
     addImportedFn   := fun _ _ => pure {}
     addEntryFn      := fun (s : NameSet) n => s.insert n
@@ -210,7 +212,11 @@ def registerTagAttribute (name : Name) (descr : String)
       unless ext.toEnvExtension.asyncMayModify env decl do
         throwAttrNotInAsyncCtx name decl env.asyncPrefix?
       validate decl
-      modifyEnv fun env => ext.addEntry (asyncDecl := decl) env decl
+      modifyEnv fun env =>
+        -- a post-hoc application some recording query could have observed must be recorded for
+        -- covered attributes; see `Environment.declChangeLog`
+        let env := if declCovered then env.logDeclChange decl else env
+        ext.addEntry (asyncDecl := decl) env decl
   }
   registerBuiltinAttribute attrImpl
   return { attr := attrImpl, ext := ext }
@@ -262,10 +268,12 @@ structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where
 
 def registerParametricAttributeExt (ref : Name) (preserveOrder : Bool := false)
     (filterExport : Environment → Name → α → Bool := fun env n _ =>
-      env.contains (skipRealize := false) n) :
+      env.contains (skipRealize := false) n)
+    (declCovered : Bool := false) :
     IO (PersistentEnvExtension (Name × α) (Name × α) (List Name × NameMap α)) :=
   registerPersistentEnvExtension {
     name            := ref
+    declCovered    := declCovered
     mkInitial       := pure ([], {})
     addImportedFn   := fun _ => pure ([], {})
     addEntryFn      := fun (decls, m) (p : Name × α) => (p.1 :: decls, m.insert p.1 p.2)
diff --git a/src/Lean/AuxRecursor.lean b/src/Lean/AuxRecursor.lean
index b906750f4904..e9f4f1b911ec 100644
--- a/src/Lean/AuxRecursor.lean
+++ b/src/Lean/AuxRecursor.lean
@@ -23,7 +23,9 @@ def mkRecOnName (indDeclName : Name) : Name   := Name.mkStr indDeclName recOnSuf
 def mkBRecOnName (indDeclName : Name) : Name  := Name.mkStr indDeclName brecOnSuffix
 def mkBelowName (indDeclName : Name) : Name := Name.mkStr indDeclName belowSuffix
 
-builtin_initialize auxRecExt : TagDeclarationExtension ← mkTagDeclarationExtension (asyncMode := .async .mainEnv)
+builtin_initialize auxRecExt : TagDeclarationExtension ←
+  -- covered: aux-recursor status is an immutable per-declaration fact
+  mkTagDeclarationExtension (asyncMode := .async .mainEnv) (declCovered := true)
 
 def markAuxRecursor (env : Environment) (declName : Name) : Environment :=
   auxRecExt.tag env declName
@@ -50,7 +52,9 @@ def isRecOnRecursor (env : Environment) (declName : Name) : Bool :=
 def isBRecOnRecursor (env : Environment) (declName : Name) : Bool :=
   isAuxRecursorWithSuffix env declName brecOnSuffix
 
-private builtin_initialize sparseCasesOnExt : TagDeclarationExtension ← mkTagDeclarationExtension (asyncMode := .async .mainEnv)
+private builtin_initialize sparseCasesOnExt : TagDeclarationExtension ←
+  -- covered: sparse-`casesOn` status is an immutable per-declaration fact
+  mkTagDeclarationExtension (asyncMode := .async .mainEnv) (declCovered := true)
 
 def markSparseCasesOn (env : Environment) (declName : Name) : Environment :=
   sparseCasesOnExt.tag env declName
@@ -79,7 +83,9 @@ def NoConfusionInfo.arity : NoConfusionInfo → Nat
   | .regular arity _ _ => arity
   | .perCtor arity _   => arity
 
-builtin_initialize noConfusionExt : MapDeclarationExtension NoConfusionInfo ← mkMapDeclarationExtension (asyncMode := .mainOnly)
+builtin_initialize noConfusionExt : MapDeclarationExtension NoConfusionInfo ←
+  -- covered: `noConfusion` facts are immutable per declaration and monotone
+  mkMapDeclarationExtension (asyncMode := .mainOnly) (declCovered := true)
 
 def markNoConfusion (env : Environment) (n : Name) (info : NoConfusionInfo) : Environment :=
   noConfusionExt.insert env n info
diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean
index 79b457a08230..40bedf71dc7f 100644
--- a/src/Lean/Class.lean
+++ b/src/Lean/Class.lean
@@ -69,8 +69,11 @@ Type class environment extension
 -- TODO: add support for scoped instances
 builtin_initialize classExtension : SimplePersistentEnvExtension ClassEntry ClassState ←
   registerSimplePersistentEnvExtension {
+    -- covered: class facts are immutable per declaration and monotone
+    declCovered  := true
     addEntryFn    := ClassState.addEntry
     addImportedFn := fun es => (mkStateFromImportedEntries ClassState.addEntry {} es).switch
+    -- class facts are immutable per declaration and monotone
   }
 
 /-- Return `true` if `n` is the name of type class in the given environment. -/
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 61d372630f94..c52a83be9221 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -200,6 +200,16 @@ structure State where
   traceState      : TraceState     := {}
   /-- Cache for instantiating universe polymorphic declarations. -/
   cache           : Cache          := {}
+  /--
+  Dependencies observed by the computation currently recording, if any
+  (`Core.Context.recordingDeps`); becomes the dependency log of the entry it caches, see
+  `Lean.Meta.SynthInstanceCache` for the only current client. Deliberately *not* backtrackable:
+  `SavedState.restore` does not restore it, so dependencies observed on a path that is later
+  rolled back are kept. Recording more than the surviving path observed is benign
+  over-approximation; losing an observation would not be. For the same reason it does not live
+  in `Meta.Cache`, which `Meta.modifyEnv` clears wholesale.
+  -/
+  recordedDeps    : RecordedDeps   := {}
   /-- Message log. -/
   messages        : MessageLog     := {}
   /-- Info tree. We have the info tree here because we want to update it while adding attributes. -/
@@ -243,6 +253,13 @@ structure Context where
   suppressElabErrors : Bool := false
   /-- Cache of `Lean.inheritedTraceOptions`. -/
   inheritedTraceOptions : Std.HashSet Name := {}
+  /--
+  True while this computation is recording its dependencies into `Core.State.recordedDeps`:
+  by-name option reads are then restricted to the recording accessors, see
+  `Lean.getRecordedOption`. Scoped to the computation rather than carried by the environment,
+  which outlives it in captured display contexts.
+  -/
+  recordingDeps : Bool := false
   deriving Nonempty
 
 /-- CoreM is a monad for manipulating the Lean environment.
@@ -272,11 +289,25 @@ instance : MonadEnv CoreM where
   modifyEnv f := modify fun s => { s with env := f s.env, cache := {} }
 
 instance : MonadOptions CoreM where
-  getOptions := return (← read).options
+  getOptions := do
+    let ctx ← read
+    let options := ctx.options
+    if ctx.recordingDeps then
+      -- The options are returned from the panic so that a violation reports once instead of
+      -- cascading through code that would otherwise see every option unset.
+      have : Inhabited Options := ⟨options⟩
+      return panic! "options acquired inside a computation recording its dependencies; \
+        result-relevant reads must go through `Lean.getRecordedOption`, all others through \
+        `getOptionsUnrestricted`"
+    return options
+  getOptionsUnrestricted := return (← read).options
 
 instance : MonadWithOptions CoreM where
   withOptions f x := do
-    let options := f (← read).options
+    -- unrestricted acquisition: the reads below see either an unchanged value or a write by `f`
+    -- done during recording, and both are part of the resolution cache key
+    -- (`Lean.Meta.SynthInstanceCacheKey.limits`)
+    let options := f (← getOptionsUnrestricted)
     let diag := diagnostics.get options
     if Kernel.isDiagnosticsEnabled (← getEnv) != diag then
       modifyEnv fun env => Kernel.enableDiag env diag
@@ -328,8 +359,12 @@ instance : Elab.MonadInfoTree CoreM where
   modifyInfoState f := modify fun s => { s with infoState := f s.infoState }
 
 @[inline] def modifyCache (f : Cache → Cache) : CoreM Unit :=
-  modify fun ⟨env, next, ngen, auxDeclNGen, trace, cache, messages, infoState, snaps⟩ =>
-   ⟨env, next, ngen, auxDeclNGen, trace, f cache, messages, infoState, snaps⟩
+  modify fun ⟨env, next, ngen, auxDeclNGen, trace, cache, deps, messages, infoState, snaps⟩ =>
+   ⟨env, next, ngen, auxDeclNGen, trace, f cache, deps, messages, infoState, snaps⟩
+
+@[inline] def modifyRecordedDeps (f : RecordedDeps → RecordedDeps) : CoreM Unit :=
+  modify fun ⟨env, next, ngen, auxDeclNGen, trace, cache, deps, messages, infoState, snaps⟩ =>
+   ⟨env, next, ngen, auxDeclNGen, trace, cache, f deps, messages, infoState, snaps⟩
 
 @[inline] def modifyInstLevelTypeCache (f : InstantiateLevelCache → InstantiateLevelCache) : CoreM Unit :=
   modifyCache fun ⟨c₁, c₂⟩ => ⟨f c₁, c₂⟩
@@ -393,6 +428,9 @@ itself after calling `act` as well as by reuse-handling code such as the one sup
 @[specialize] def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState))
     (act : CoreM α) : CoreM (α × SavedState) := do
   if let some (val, state) := reusableResult? then
+    -- Restoring a full state rolls back `State.recordedDeps`, which must not happen while a
+    -- computation is recording; incremental reuse operates between commands.
+    assert! !(← read).recordingDeps
     set state.toState
     IO.addHeartbeats state.passedHeartbeats
     return (val, state)
@@ -477,7 +515,8 @@ register_builtin_option debug.moduleNameAtTimeout : Bool := {
 }
 
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
-  let includeModuleName := debug.moduleNameAtTimeout.get (← getOptions)
+  -- unrestricted acquisition: only reached when the heartbeat limit throws, which is never cached
+  let includeModuleName := debug.moduleNameAtTimeout.get (← getOptionsUnrestricted)
   let atModuleName := if includeModuleName then s!" at `{moduleName}`" else ""
   throw <| Exception.error (← getRef) <| .tagged `runtime.maxHeartbeats m!"\
     (deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\
@@ -566,6 +605,10 @@ def wrapAsync {α : Type} (act : α → CoreM β) (cancelTk? : Option IO.CancelT
   let (childDeclNGen, parentDeclNGen) := (← getDeclNGen).mkChild
   setDeclNGen parentDeclNGen
   let st ← get
+  -- The forked action's final state is discarded below, so anything it records into
+  -- `State.recordedDeps` is lost: a recording computation must not fork. To be revisited when it
+  -- becomes necessary.
+  assert! !(← read).recordingDeps
   let st := { st with auxDeclNGen := childDeclNGen, ngen := childNGen }
   let ctx ← read
   let ctx := { ctx with cancelTk? }
@@ -767,6 +810,48 @@ where doCompile := do
 def compileDecl (decl : Declaration) (logErrors := true) : CoreM Unit := do
   compileDecls (Compiler.getDeclNamesForCodeGen decl) logErrors
 
+/-- Records the lookup `access` in the recording computation's accumulator, if any; see `getRecordedOption`. -/
+private def recordOptionAccess (access : RecordedOptionAccess) : CoreM Unit := do
+  if (← read).recordingDeps then
+    -- Read-before-write: repeated lookups of the same option dominate (e.g. per `isDefEq` step),
+    -- and the membership test avoids the state update for them.
+    let d := (← get).recordedDeps
+    unless d.options.any (·.name == access.name) do
+      Core.modifyRecordedDeps fun ⟨options, extGens, g, p, w⟩ =>
+        ⟨options.push access, extGens, g, p, w⟩
+
+/--
+Records the current generation of the generation-tracked extension with registration index
+`extIdx` in the recording computation's accumulator, if any; the read-side counterpart of the
+`EnvExtension.trackGen` bump. Call sites record the generation through this accessor and then
+read the state itself with `(recorded := true)`.
+-/
+def recordExtGenAccess (extIdx : Nat) : CoreM Unit := do
+  if (← read).recordingDeps then
+    let d := (← get).recordedDeps
+    unless d.extGens.any (·.1 == extIdx) do
+      let gen ← EnvExtension.getRecordedGen (← getEnv) extIdx
+      Core.modifyRecordedDeps fun ⟨options, extGens, g, p, w⟩ =>
+        ⟨options, extGens.push (extIdx, gen), g, p, w⟩
+
+/--
+Reads an option inside a recording computation, recording the lookup as an option dependency
+of the entry being computed (`Core.State.recordedDeps`); see `Lean.Meta.SynthInstanceCache` for
+the only current client. The read bypasses the options restriction, which exists to divert
+result-relevant by-name reads to this function; outside a recording computation it behaves like
+`Lean.Option.get`.
+-/
+def getRecordedOption [KVMap.Value α] (opt : Lean.Option α) : CoreM α := do
+  let raw := (← getOptionsUnrestricted).find? opt.name
+  recordOptionAccess { name := opt.name, value := raw }
+  return (raw.bind KVMap.Value.ofDataValue?).getD opt.defValue
+
+/-- By-name variant of `getRecordedOption`, for options that cannot be referenced directly. -/
+def getRecordedBoolOption (name : Name) (defVal := false) : CoreM Bool := do
+  let raw := (← getOptionsUnrestricted).find? name
+  recordOptionAccess { name, value := raw }
+  return (raw.bind KVMap.Value.ofDataValue?).getD defVal
+
 def getDiag (opts : Options) : Bool :=
   diagnostics.get opts
 
diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean
index 875b0607fba2..bf8b10c0a5ab 100644
--- a/src/Lean/Data/Options.lean
+++ b/src/Lean/Data/Options.lean
@@ -50,7 +50,7 @@ instance : EmptyCollection Options where
 def find := find?
 
 @[inline] def get? {α : Type} [KVMap.Value α] (o : Options) (k : Name) : Option α :=
-  o.map.find? k |>.bind KVMap.Value.ofDataValue?
+  o.find? k |>.bind KVMap.Value.ofDataValue?
 
 @[inline] def get {α : Type} [KVMap.Value α] (o : Options) (k : Name) (defVal : α) : α :=
   o.get? k |>.getD defVal
@@ -147,11 +147,19 @@ def getOptionDescr (name : Name) : IO String := do
 
 class MonadOptions (m : Type → Type) where
   getOptions : m Options
+  /--
+  Acquires the options without the recording check of `getOptions`, for readers whose result
+  provably cannot influence a computation that records its dependencies (trace and profiler
+  collection, message rendering, diagnostics counters, limits whose excess throws and is never
+  cached). Each use carries a one-line argument; see `Lean.getRecordedOption`.
+  -/
+  getOptionsUnrestricted : m Options := getOptions
 
-export MonadOptions (getOptions)
+export MonadOptions (getOptions getOptionsUnrestricted)
 
 instance [MonadLift m n] [MonadOptions m] : MonadOptions n where
   getOptions := liftM (getOptions : m _)
+  getOptionsUnrestricted := liftM (getOptionsUnrestricted : m _)
 
 variable [Monad m] [MonadOptions m]
 
diff --git a/src/Lean/DeclarationRange.lean b/src/Lean/DeclarationRange.lean
index 406579133874..70ba790e01c1 100644
--- a/src/Lean/DeclarationRange.lean
+++ b/src/Lean/DeclarationRange.lean
@@ -29,7 +29,9 @@ def addDeclarationRanges [Monad m] [MonadEnv m] (declName : Name) (declRanges :
   if declName.isAnonymous then
     -- This can happen on elaboration of partial syntax and would panic in `modifyState` otherwise
     return
-  modifyEnv fun env => declRangeExt.insert env declName declRanges
+  -- position metadata, not resolution-relevant: later writes legitimately refine earlier ones
+  -- (e.g. structure elaboration re-reports its generated declarations)
+  modifyEnv fun env => declRangeExt.insert env declName declRanges (allowOverwrite := true)
 
 def findDeclarationRangesCore? [Monad m] [MonadEnv m] (declName : Name) : m (Option DeclarationRanges) :=
   -- In the case of private definitions imported via `import all`, looking in `.olean.server` is not
diff --git a/src/Lean/DocString/Add.lean b/src/Lean/DocString/Add.lean
index 82eb3405a1d5..4dcfd0969bb0 100644
--- a/src/Lean/DocString/Add.lean
+++ b/src/Lean/DocString/Add.lean
@@ -318,7 +318,9 @@ def addMarkdownDocString
     throwError m!"invalid doc string, declaration `{.ofConstName declName}` is in an imported module"
   validateDocComment docComment
   let docString : String ← getDocStringText docComment
-  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
+  -- documentation metadata, not resolution-relevant: later writes legitimately replace
+  -- earlier ones
+  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces (allowOverwrite := true)
 
 /--
 Adds an elaborated Verso docstring to the environment, recording its `deferred` checks under this
@@ -333,7 +335,8 @@ def addVersoDocStringCore [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] [MonadErr
   unless (← getEnv).getModuleIdxFor? declName |>.isNone do
     throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
   modifyEnv fun env =>
-    let env := versoDocStringExt.insert env declName docs
+    -- documentation metadata, as above
+    let env := versoDocStringExt.insert env declName docs (allowOverwrite := true)
     deferred.foldl (init := env) fun env c =>
       Doc.deferredCheckExt.addEntry env { c with site := .decl declName }
 
diff --git a/src/Lean/DocString/Extension.lean b/src/Lean/DocString/Extension.lean
index 8958b216039f..9a50c46b9e08 100644
--- a/src/Lean/DocString/Extension.lean
+++ b/src/Lean/DocString/Extension.lean
@@ -166,7 +166,9 @@ def getBuiltinVersoDocStrings : IO (NameMap VersoDocString) :=
 def addDocStringCore [Monad m] [MonadError m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) (docString : String) : m Unit := do
   unless (← getEnv).getModuleIdxFor? declName |>.isNone do
     throwError m!"invalid doc string, declaration `{.ofConstName declName}` is in an imported module"
-  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces
+  -- documentation metadata, not resolution-relevant: later writes legitimately replace
+  -- earlier ones
+  modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces (allowOverwrite := true)
 
 def removeDocStringCore [Monad m] [MonadError m] [MonadEnv m] [MonadLiftT BaseIO m] (declName : Name) : m Unit := do
   unless (← getEnv).getModuleIdxFor? declName |>.isNone do
diff --git a/src/Lean/Elab/BuiltinEvalCommand.lean b/src/Lean/Elab/BuiltinEvalCommand.lean
index 2ec9947250df..7c66d5f9959d 100644
--- a/src/Lean/Elab/BuiltinEvalCommand.lean
+++ b/src/Lean/Elab/BuiltinEvalCommand.lean
@@ -155,7 +155,6 @@ private def mkFormat (e : Expr) : MetaM Expr := do
         try
           trace[Elab.eval] "Attempting to derive a `Repr` instance for `{.ofConstName name}`"
           liftCommandElabM do applyDerivingHandlers ``Repr #[name]
-          resetSynthInstanceCache
           return ← mkRepr e
         catch ex =>
           trace[Elab.eval] "Failed to use derived `Repr` instance. Exception: {ex.toMessageData}"
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 998561d235aa..017610493754 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -1097,11 +1097,13 @@ such as `open` and `namespace` commands,
 only have an effect for the remainder of the `CommandElabM` computation passed here,
 and do not affect subsequent commands.
 
-*Warning:* when using this from `MetaM` monads, the caches are *not* reset.
-If the command defines new instances for example, you should use `Lean.Meta.resetSynthInstanceCache`
-to reset the instance cache.
+*Warning:* when using this from `MetaM` monads, the `Meta.Cache` caches are *not* reset.
 While the `modifyEnv` function for `MetaM` clears its caches entirely,
 `liftCommandElabM` has no way to reset these caches.
+The type class resolution cache is unaffected by this: its entries record their dependencies
+and self-invalidate when the command changes them (e.g. by adding instances or changing
+reducibility attributes). Other `Meta.Cache` components (e.g. the `whnf` and `isDefEq` caches)
+can however retain results invalidated by the command's environment changes.
 -/
 def liftCommandElabM (cmd : CommandElabM α) (throwOnError : Bool := true) : CoreM α := do
   -- `observing` ensures that if `cmd` throws an exception we still thread state back to `CoreM`.
diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean
index e01bfbfb38c6..ed7726515c03 100644
--- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean
@@ -26,7 +26,9 @@ public structure EqnInfo where
   deriving Inhabited
 
 public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
-  mkMapDeclarationExtension (exportEntriesFn := fun env s =>
+  -- covered: consulted by the reserved-name predicates for fixpoint induction names, so also on
+  -- resolution search paths; populated only when the declaration is created (monotone)
+  mkMapDeclarationExtension (declCovered := true) (exportEntriesFn := fun env s =>
     let all := s.toArray
     -- Do not export for non-exposed defs at exported/server levels
     let exported := s.filter (fun n _ => env.hasExposedBody n) |>.toArray
diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
index bbb0c35cb5e6..6458758e1b04 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
@@ -148,7 +148,8 @@ where
             throwError "no progress at goal\n{MessageData.ofGoal mvarId}"
 
 public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
-  mkMapDeclarationExtension (exportEntriesFn := fun env s =>
+  -- covered: eqn info is registered when the definition is created (monotone, name-keyed)
+  mkMapDeclarationExtension (declCovered := true) (exportEntriesFn := fun env s =>
     let all := s.toArray
     -- Do not export for non-exposed defs at exported/server levels
     let exported := s.filter (fun n _ => env.hasExposedBody n) |>.toArray
diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
index 69a38f359706..3aa557c6ea6b 100644
--- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
@@ -24,7 +24,8 @@ public structure EqnInfo where
   deriving Inhabited
 
 public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
-  mkMapDeclarationExtension (exportEntriesFn := fun env s =>
+  -- covered: eqn info is registered when the definition is created (monotone, name-keyed)
+  mkMapDeclarationExtension (declCovered := true) (exportEntriesFn := fun env s =>
     let all := s.toArray
     -- Do not export for non-exposed defs at exported/server levels
     let exported := s.filter (fun n _ => env.hasExposedBody n) |>.toArray
diff --git a/src/Lean/EnvExtension.lean b/src/Lean/EnvExtension.lean
index 83589454bbd2..3450133f01e7 100644
--- a/src/Lean/EnvExtension.lean
+++ b/src/Lean/EnvExtension.lean
@@ -29,6 +29,9 @@ structure SimplePersistentEnvExtensionDescr (α σ : Type) where
     Option (Environment → σ → List α → OLeanEntries (Array α)) := none
   asyncMode     : EnvExtension.AsyncMode := .mainOnly
   replay?       : Option ((newEntries : List α) → (newState : σ) → σ → List α × σ) := none
+  /-- See `EnvExtension.trackGen`. -/
+  declCovered  : Bool := false
+
 
 /--
 Returns a function suitable for `SimplePersistentEnvExtensionDescr.replay?` that replays all new
@@ -53,6 +56,7 @@ def registerSimplePersistentEnvExtension {α σ : Type} [Inhabited σ] (descr :
       | none    => .uniform (descr.toArrayFn s.1.reverse)
     statsFn := fun s => format "number of local entries: " ++ format s.1.length
     asyncMode := descr.asyncMode
+    declCovered := descr.declCovered
     replay? := descr.replay?.map fun replay oldState newState _ (entries, s) =>
       let newEntries := newState.1.take (newState.1.length - oldState.1.length)
       let (newEntries, s) := replay newEntries newState.2 s
@@ -90,9 +94,11 @@ end SimplePersistentEnvExtension
 @[expose] def TagDeclarationExtension := SimplePersistentEnvExtension Name NameSet
 
 def mkTagDeclarationExtension (name : Name := by exact decl_name%)
-  (asyncMode : EnvExtension.AsyncMode := .mainOnly) : IO TagDeclarationExtension :=
+  (asyncMode : EnvExtension.AsyncMode := .mainOnly)
+  (declCovered : Bool := false) : IO TagDeclarationExtension :=
   registerSimplePersistentEnvExtension {
     name          := name,
+    declCovered  := declCovered,
     addImportedFn := fun _ => {},
     addEntryFn    := fun s n => s.insert n,
     toArrayFn     := fun es => es.toArray.qsort Name.quickLt
@@ -113,7 +119,12 @@ def tag (ext : TagDeclarationExtension) (env : Environment) (declName : Name) :
   else
     have : Inhabited Environment := ⟨env⟩
     assert! env.getModuleIdxFor? declName |>.isNone -- See comment at `TagDeclarationExtension`
-    ext.addEntry (asyncDecl := declName) env declName
+    if ext.getState (asyncMode := ext.toEnvExtension.asyncMode) (asyncDecl := declName) env
+        |>.contains declName then
+      env -- idempotent re-tag: no observable change, nothing to record
+    else
+      let env := if ext.toEnvExtension.declCovered then env.logDeclChange declName else env
+      ext.addEntry (asyncDecl := declName) env declName
 
 def isTagged (ext : TagDeclarationExtension) (env : Environment) (declName : Name)
     (asyncMode := ext.toEnvExtension.asyncMode) : Bool :=
@@ -131,14 +142,17 @@ deriving Inhabited
 
 def mkMapDeclarationExtension (name : Name := by exact decl_name%)
     (asyncMode : EnvExtension.AsyncMode := .async .mainEnv)
+    (declCovered : Bool := false)
     (exportEntriesFn : Environment → NameMap α → OLeanEntries (Array (Name × α)) :=
       -- Do not export info for private defs by default
       fun env s =>
         let all := s.toArray.filter (fun (n, _) => env.contains (skipRealize := false) n)
-        .uniform all) :
+        .uniform all)
+    :
     IO (MapDeclarationExtension α) :=
   .mk <$> registerPersistentEnvExtension {
     name            := name,
+    declCovered    := declCovered,
     mkInitial       := pure {}
     addImportedFn   := fun _ => pure {}
     addEntryFn      := fun s (n, v) => s.insert n v
@@ -153,15 +167,29 @@ def mkMapDeclarationExtension (name : Name := by exact decl_name%)
 
 namespace MapDeclarationExtension
 
-def insert (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (val : α) : Environment :=
+def insert (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (val : α)
+    (allowOverwrite := false) : Environment :=
   have : Inhabited Environment := ⟨env⟩
   if let some modIdx := env.getModuleIdxFor? declName then -- See comment at `MapDeclarationExtension`
     panic! s!"cannot insert `{declName}` into `{ext.name}`, it is not defined in the current module but in `{env.allImportedModuleNames[modIdx]!}`"
+  -- Write-once guard: dependency-recording coverage claims for declaration-keyed
+  -- extensions rest on entries being immutable once written (`EnvExtension.trackGen`). Sites
+  -- that legitimately update an entry must say so (`allowOverwrite`), with a justification.
+  else if !allowOverwrite &&
+      (ext.toPersistentEnvExtension.getState (asyncDecl := declName) env
+        |>.contains declName) then
+    panic! s!"cannot insert `{declName}` into `{ext.name}`, it is already present; \
+      declaration-keyed extension entries are immutable once written (pass \
+      `allowOverwrite := true` with a justification if this update is intended)"
   else
+    -- only covered extensions participate in resolution-cache validation; see
+    -- `Environment.declChangeLog`
+    let env := if ext.toEnvExtension.declCovered then env.logDeclChange declName else env
     ext.addEntry (asyncDecl := declName) env (declName, val)
 
 def find? [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name)
-    (asyncMode := ext.toEnvExtension.asyncMode) (level := OLeanLevel.exported) : Option α :=
+    (asyncMode := ext.toEnvExtension.asyncMode) (level := OLeanLevel.exported)
+    : Option α :=
   match env.getModuleIdxFor? declName with
   | some modIdx =>
     match (ext.getModuleEntries (level := level) env modIdx).binSearch (declName, default) (fun a b => Name.quickLt a.1 b.1) with
@@ -169,7 +197,8 @@ def find? [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment)
     | none   => none
   | none => (ext.getState (asyncMode := asyncMode) (asyncDecl := declName) env).find? declName
 
-def contains [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) : Bool :=
+def contains [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name)
+    : Bool :=
   match env.getModuleIdxFor? declName with
   | some modIdx => (ext.getModuleEntries env modIdx).binSearchContains (declName, default) (fun a b => Name.quickLt a.1 b.1)
   | none        => (ext.getState (asyncDecl := declName) env).contains declName
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 33928512dadc..bd25222439d1 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -540,6 +540,53 @@ private structure RealizationContext where
   -/
   realizeMapRef : IO.Ref (NameMap NonScalar /- PHashMap α (Task Dynamic) -/)
 
+/--
+One option lookup observed by a recording computation: the raw `Options.find?` result, so that
+validation is default-independent and covers set↔unset transitions exactly. See
+`Lean.getRecordedOption`.
+-/
+structure RecordedOptionAccess where
+  name  : Name
+  value : Option DataValue
+  deriving BEq
+
+/--
+What a recording computation observed about its environment and options, accumulated in
+`Lean.Core.State.recordedDeps` while it runs; replaying the observations decides whether a
+result cached by that computation is still valid. Type class resolution is currently the only
+client, see `Lean.Meta.SynthInstance`.
+-/
+structure RecordedDeps where
+  /--
+  The option lookups performed, deduplicated by name; a cached result may only be reused when
+  these lookups give the same answers in the current context.
+  -/
+  options : Array RecordedOptionAccess := #[]
+  /--
+  Per accessed generation-tracked extension (see `EnvExtension.trackGen`), the state generation
+  that was observed: `(extension index, generation)`. The dependency is stale once the
+  extension's generation moves.
+  -/
+  extGens : Array (Nat × Nat) := #[]
+  /--
+  Value of `Environment.recordGen` when recording started. While it is unchanged, none of the
+  recorded environment dependencies can have changed and validation skips their checks.
+  -/
+  recordGen : Nat := 0
+  /--
+  Length of the declaration change log (`Environment.declChangeLog`) when recording started.
+  Changes appended since whose target was born after `constBirthW` are skipped during
+  validation (the computation cannot have observed a declaration that did not exist yet); any other
+  change conservatively invalidates the entry.
+  -/
+  changeLogPos : Nat := 0
+  /--
+  Value of `Environment.constBirthGen` when recording started: the birth watermark for
+  `changeLogPos`.
+  -/
+  constBirthW : Nat := 0
+  deriving Inhabited
+
 /--
 Elaboration-specific extension of `Kernel.Environment` that adds tracking of asynchronously
 elaborated declarations.
@@ -612,6 +659,55 @@ structure Environment where
   `elabMutualDef` may switch from public to private when e.g. entering the proof of a theorem.
   -/
   isExporting : Bool := false
+  /--
+  True while a computation is recording its dependencies on this environment branch
+  (`Lean.Core.State.recordedDeps`): its by-name option reads are restricted to
+  `Lean.getRecordedOption`, generation-tracked extensions must be read through the recording
+  accessors (`EnvExtension.trackGen`), and every other extension read must be of a covered
+  extension (`EnvExtension.declCovered`).
+  -/
+  isRecordingDeps : Bool := false
+  /--
+  Log of declaration-keyed state changes some recording computation could have observed: a write
+  about a declaration is appended when the declaration was born before the latest arming
+  (`recordArmBirthGen`); writes about younger declarations cannot falsify any recorded entry and
+  stay silent. Cache entries are validated against the log by birth arithmetic
+  (`Environment.checkDeclChangeLog`); reducibility status changes are the most common source.
+  -/
+  declChangeLog : Array Name := #[]
+  /--
+  Value of `Environment.constBirthGen` at the most recent arming of a recording computation on this
+  lineage; see `declChangeLog`.
+  -/
+  recordArmBirthGen : Nat := 0
+  /--
+  Persistent tier of the type class resolution cache, `none` for empty. The value is a
+  `Lean.Meta.SynthInstanceCache` (not nameable in this module; accessed with confined casts in
+  `Lean.Meta.Instances`). It lives in a plain field rather than an environment extension so that
+  a cache fill costs one structure copy instead of copying the extension state array, while
+  keeping the same branch-local value semantics: fills roll back with the environment, and
+  parallel elaboration branches never observe each other's fills.
+  -/
+  synthCacheRaw? : Option NonScalar := none
+  /--
+  Counter bumped by every modification a recorded dependency could refer to: any
+  state change of a generation-tracked extension and every post-hoc reducibility change. Cache
+  entries are stamped with it (`RecordedDeps.recordGen`); while it is unchanged, validation skips
+  all per-dependency environment checks. It deliberately does not cover option values, which are
+  context rather than environment state.
+  -/
+  recordGen : Nat := 0
+  /--
+  Birth indices of the constants added on this environment lineage, assigned when a constant
+  becomes observable here (synchronous `addDecl`, asynchronous registration); imported constants
+  and constants with unknown provenance (e.g. realized constants, currently) are absent and
+  treated as index 0, older than any watermark, which is the conservative direction. Consumers
+  capture a watermark (`constBirthGen`) and test `constBirthIdx n > watermark` to prove that a
+  recording taken at the watermark cannot have observed `n`; see `Environment.declChangeLog`.
+  -/
+  constBirths : PHashMap Name Nat := {}
+  /-- Watermark counter for `constBirths`. -/
+  constBirthGen : Nat := 0
 deriving Nonempty
 
 @[inline] private def VisibilityMap.get (m : VisibilityMap α) (env : Environment) : α :=
@@ -656,6 +752,56 @@ def setExporting (env : Environment) (isExporting : Bool) : Environment :=
   else
     { env with isExporting }
 
+/-- Bumps `env.recordGen`; see there. Called where recorded dependencies change outside `EnvExtension.modifyState`. -/
+def bumpRecordGen (env : Environment) : Environment :=
+  { env with recordGen := env.recordGen + 1 }
+
+/-- Registers `n` as born now on this environment lineage; see `Environment.constBirths`. -/
+def registerConstBirth (env : Environment) (n : Name) : Environment :=
+  { env with constBirths := env.constBirths.insert n (env.constBirthGen + 1)
+             constBirthGen := env.constBirthGen + 1 }
+
+/--
+Birth index of `n` on this lineage; 0 (older than any watermark) for imported constants and
+constants of unknown provenance. See `Environment.constBirths`.
+-/
+def constBirthIdx (env : Environment) (n : Name) : Nat :=
+  env.constBirths.find? n |>.getD 0
+
+/--
+Records a state change about `declName` in `Environment.declChangeLog` if some recording
+computation could have observed the pre-change state, i.e. if the declaration was born before
+the latest arming; see there. Callers invoke this only for writes that actually change
+observable state (idempotent re-registrations stay silent).
+-/
+def logDeclChange (env : Environment) (declName : Name) : Environment :=
+  if env.constBirthIdx declName ≤ env.recordArmBirthGen then
+    -- the log check sits behind the `recordGen` short-circuit, so appends must bump it
+    { env with declChangeLog := env.declChangeLog.push declName }.bumpRecordGen
+  else
+    env
+
+/--
+Validates the declaration-change dependencies of an entry recorded at log position `fromPos`
+with birth watermark `birthW`: every change appended since must
+target a declaration born after the watermark; see `Environment.declChangeLog`.
+-/
+def checkDeclChangeLog (env : Environment) (fromPos birthW : Nat) : Bool :=
+  fromPos ≤ env.declChangeLog.size &&
+    env.declChangeLog.all (fun d => env.constBirthIdx d > birthW) (start := fromPos)
+
+/-- Updates `env.synthCacheRaw?`; see there. -/
+def setSynthCacheRaw? (env : Environment) (v? : Option NonScalar) : Environment :=
+  { env with synthCacheRaw? := v? }
+
+/-- Updates `env.isRecordingDeps`; arming also stamps `Environment.recordArmBirthGen`. -/
+def setRecordingDeps (env : Environment) (recording : Bool) : Environment :=
+  if recording then
+    { env with isRecordingDeps := true, recordArmBirthGen := env.constBirthGen }
+  else if env.isRecordingDeps then
+    { env with isRecordingDeps := false }
+  else env
+
 /-- Consistently updates synchronous and (private) asynchronous parts of the environment without blocking. -/
 private def modifyCheckedAsync (env : Environment) (f : Kernel.Environment → Kernel.Environment) : Environment :=
   { env with checked := env.checked.map (sync := true) f, base.private := f env.base.private }
@@ -714,6 +860,7 @@ def addDeclCore (env : Environment) (maxHeartbeats : USize) (maxRecDepth : USize
   -- visibility scopes but the caller can still customize the public one on the main elaboration
   -- branch by use of `addConstAsync` as is the case for `Lean.addDecl`.
   for n in decl.getNames do
+    env := env.registerConstBirth n
     let some info := env.checked.get.find? n | unreachable!
     env := { env with asyncConstsMap.private := env.asyncConstsMap.private.add {
       constInfo := .ofConstantInfo info
@@ -1053,6 +1200,7 @@ def addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind)
       | some v => .mk v.nestedConsts.public
       | none   => .mk (α := AsyncConsts) default
   }
+  let env := env.registerConstBirth constName
   return {
     constName, kind, exportedKind?
     mainEnv := { env with
@@ -1322,6 +1470,38 @@ structure EnvExtension (σ : Type) where private mk ::
   present.
   -/
   replay?   : Option (ReplayFn σ)
+  /-- Name for diagnostics; set automatically for persistent extensions. -/
+  name      : Name
+  /--
+  Whether the extension state is stored together with a generation counter that every
+  modification bumps. Type class resolution cache entries depend on extension state in one of
+  two regimes:
+
+  * *Generation-tracked* (`trackGen`): reads by a recording computation go through the recording
+    accessors, which record the observed generation as a dependency of the cache entry being
+    computed, so a state change invalidates exactly the entries that consulted this extension;
+    see `Lean.Meta.SynthInstance`. A *pure* read while recording panics. For
+    extensions answering *shape* queries (candidate sets such as instances), where a new
+    declaration changes answers about pre-existing queries.
+  * *Covered* (`declCovered`): declaration-keyed content whose observable changes are
+    enforced by the write machinery rather than trusted: entries are write-stability-guarded
+    (`MapDeclarationExtension.insert`), and a write some recording computation could have observed
+    is appended to the declaration change log and validated by birth arithmetic
+    (`Environment.declChangeLog`, `Environment.constBirths`). Reads are then free everywhere.
+    The registration site states the extension's coverage argument in one line; the residual
+    assumption, uniform across covered extensions, is that reads are keyed by declarations
+    reachable from the computation.
+
+  A read of an unclassified extension while recording panics: a recording computation is a
+  closed system, so every extension it consults is classifiable at
+  registration. `tests/elab/tc_cache_covered_claims.lean` locks the audit.
+
+  Must use `AsyncMode.local` or `.mainOnly`: generations are branch-local, matching the
+  visibility of the resolution cache.
+  -/
+  trackGen : Bool
+  /-- Whether reads of this extension are covered; see `trackGen` for the classification. -/
+  declCovered : Bool
   deriving Inhabited
 
 namespace EnvExtension
@@ -1335,13 +1515,23 @@ private builtin_initialize envExtensionsRef : IO.Ref (Array (EnvExtension EnvExt
   user-defined environment extensions. When this happens, we must adjust the size of the `env.extensions`.
   This method is invoked when processing `import`s.
 -/
+private unsafe def mkInitialEntryUnsafe (ext : EnvExtension EnvExtensionState) : IO EnvExtensionState := do
+  let s ← ext.mkInitial
+  if ext.trackGen then
+    return unsafeCast ((0, s) : Nat × EnvExtensionState)
+  return s
+
+/-- Creates the state array entry for `ext`; see `modifyStateImpl` for the `.recorded` pairing. -/
+@[implemented_by mkInitialEntryUnsafe]
+private opaque mkInitialEntry (ext : EnvExtension EnvExtensionState) : IO EnvExtensionState
+
 partial def ensureExtensionsArraySize (exts : Array EnvExtensionState) : IO (Array EnvExtensionState) := do
   loop exts.size exts
 where
   loop (i : Nat) (exts : Array EnvExtensionState) : IO (Array EnvExtensionState) := do
     let envExtensions ← envExtensionsRef.get
     if h : i < envExtensions.size then
-      let s ← envExtensions[i].mkInitial
+      let s ← mkInitialEntry envExtensions[i]
       let exts := exts.push s
       loop (i + 1) exts
     else
@@ -1349,34 +1539,48 @@ where
 
 private def invalidExtMsg := "invalid environment extension has been accessed"
 
-private unsafe def setStateImpl {σ} (ext : EnvExtension σ) (exts : Array EnvExtensionState) (s : σ) : Array EnvExtensionState :=
-  if h : ext.idx < exts.size then
-    exts.set ext.idx (unsafeCast s)
-  else
-    -- do not return an empty array on panic, avoiding follow-up out-of-bounds accesses
-    have : Inhabited (Array EnvExtensionState) := ⟨exts⟩
-    panic! invalidExtMsg
+/-
+For `.recorded` extensions the entry stored in the state array is the state paired with its
+generation counter (as `Nat × σ`); all other extensions store the state directly. The pairing is
+confined to `modifyStateImpl`/`getStateImpl` and `mkInitialEntry`, which are the only functions
+creating or reading entries.
+-/
 
-private unsafe def modifyStateImpl {σ : Type} (ext : EnvExtension σ) (exts : Array EnvExtensionState) (f : σ → σ) : Array EnvExtensionState :=
+private unsafe def modifyStateImpl {σ : Type} (ext : EnvExtension σ) (exts : Array EnvExtensionState) (f : σ → σ)
+    (keepRecordGen := false) : Array EnvExtensionState :=
   if ext.idx < exts.size then
     exts.modify ext.idx fun s =>
-      let s : σ := unsafeCast s
-      let s : σ := f s
-      unsafeCast s
+      if ext.trackGen then
+        let (gen, s) : Nat × σ := unsafeCast s
+        unsafeCast ((if keepRecordGen then gen else gen + 1, f s) : Nat × σ)
+      else
+        let s : σ := unsafeCast s
+        let s : σ := f s
+        unsafeCast s
   else
     -- do not return an empty array on panic, avoiding follow-up out-of-bounds accesses
     have : Inhabited (Array EnvExtensionState) := ⟨exts⟩
     panic! invalidExtMsg
 
-private unsafe def getStateImpl {σ} [Inhabited σ] (ext : EnvExtension σ) (exts : Array EnvExtensionState) : σ :=
+private unsafe def getStateImpl {σ} [Inhabited σ] (ext : EnvExtension σ) (exts : Array EnvExtensionState)
+    (tripwire : Bool := false) : σ :=
   if h : ext.idx < exts.size then
-    unsafeCast exts[ext.idx]
+    if tripwire then
+      -- an unclaimed read while recording: no recorded dependency validates it
+      panic! s!"unclassified environment extension read while recording dependencies: \
+        `{ext.name}` (index {ext.idx}); the extension should either be registered as covered \
+        (`declCovered`, with a justification) or generation-tracked and read through the \
+        recording accessors (see `EnvExtension.trackGen`)"
+    else if ext.trackGen then
+      (unsafeCast exts[ext.idx] : Nat × σ).2
+    else
+      unsafeCast exts[ext.idx]
   else
     panic! invalidExtMsg
 
 def mkInitialExtStates : IO (Array EnvExtensionState) := do
   let exts ← envExtensionsRef.get
-  exts.mapM fun ext => ext.mkInitial
+  exts.mapM mkInitialEntry
 
 /--
 Checks whether `modifyState (asyncDecl := declName)` may be called on an async environment
@@ -1400,21 +1604,35 @@ def asyncMayModify (ext : EnvExtension σ) (env : Environment) (asyncDecl : Name
 Applies the given function to the extension state. See `AsyncMode` for details on how modifications
 from different environment branches are reconciled.
 
+For generation-tracked extensions the modification bumps the state's generation counter,
+invalidating recorded entries that depend on it, unless `keepRecordGen` is set;
+see `EnvExtension.trackGen`.
+
 Note that in modes `sync` and `async`, `f` will be called twice, on the local and on the `checked`
 state.
 -/
 def modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ)
-    (asyncMode := ext.asyncMode) (asyncDecl : Name := .anonymous) : Environment := Id.run do
+    (asyncMode := ext.asyncMode) (asyncDecl : Name := .anonymous)
+    (keepRecordGen := false) : Environment := Id.run do
   -- for panics
   let _ : Inhabited Environment := ⟨env⟩
   -- safety: `ext`'s constructor is private, so we can assume the entry at `ext.idx` is of type `σ`
+  -- Only generation-tracked modifications advance an invalidation counter; untracked extension
+  -- state is validated purely through the read-side covered claims (`EnvExtension.trackGen`).
+  let bumped (env : Environment) : Environment :=
+    if ext.trackGen && !keepRecordGen then
+      env.bumpRecordGen
+    else
+      env
   match asyncMode with
   | .mainOnly =>
     if let some asyncCtx := env.asyncCtx? then
       return panic! s!"environment extension is marked as `mainOnly` but used in {asyncCtx.descr}"
-    return { env with base.private.extensions := unsafe ext.modifyStateImpl env.base.private.extensions f }
+    let env := bumped env
+    return { env with base.private.extensions := unsafe ext.modifyStateImpl env.base.private.extensions f keepRecordGen }
   | .local =>
-    return { env with base.private.extensions := unsafe ext.modifyStateImpl env.base.private.extensions f }
+    let env := bumped env
+    return { env with base.private.extensions := unsafe ext.modifyStateImpl env.base.private.extensions f keepRecordGen }
   | _ =>
     if asyncMode matches .async _ then
       if asyncDecl.isAnonymous then
@@ -1428,8 +1646,9 @@ def modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ
       if let some (n :: _) := env.asyncCtx?.map (·.realizingStack) then
         return panic! s!"environment extension must set `replay?` field to be \
           used in realization context '{n}'"
-    env.modifyCheckedAsync fun env =>
-      { env with extensions := unsafe ext.modifyStateImpl env.extensions f }
+    -- `trackGen` extensions cannot use these modes (see `registerEnvExtension`)
+    (bumped env).modifyCheckedAsync fun env =>
+      { env with extensions := unsafe ext.modifyStateImpl env.extensions f keepRecordGen }
 
 /--
 Sets the extension state to the given value. See `AsyncMode` for details on how modifications from
@@ -1440,10 +1659,17 @@ def setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) (a
 
 -- `unsafe` fails to infer `Nonempty` here
 private unsafe def getStateUnsafe {σ : Type} [Inhabited σ] (ext : EnvExtension σ)
-    (env : Environment) (asyncMode := ext.asyncMode) (asyncDecl : Name := .anonymous) : σ := Id.run do
+    (env : Environment) (asyncMode := ext.asyncMode) (asyncDecl : Name := .anonymous)
+    (recorded := false) : σ := Id.run do
+  -- Reads of unclassified extensions and pure reads of generation-tracked extensions panic
+  -- while recording; see `getStateImpl` and `EnvExtension.trackGen`. `recorded` is
+  -- internal plumbing for the recording accessors: the caller asserts it has recorded this
+  -- tracked extension's generation for the current query.
+  let tripwire := env.isRecordingDeps &&
+    (if ext.trackGen then !recorded else !ext.declCovered)
   -- safety: `ext`'s constructor is private, so we can assume the entry at `ext.idx` is of type `σ`
   match asyncMode with
-  | .sync => ext.getStateImpl env.checked.get.extensions
+  | .sync => ext.getStateImpl env.checked.get.extensions tripwire
   | .async branch =>
     if asyncDecl.isAnonymous then
       panic! "called on `async` extension, must set `asyncDecl` \
@@ -1452,22 +1678,22 @@ private unsafe def getStateUnsafe {σ : Type} [Inhabited σ] (ext : EnvExtension
     -- analogous structure to `findAsync?`; see there
     -- safety: `ext`'s constructor is private, so we can assume the entry at `ext.idx` is of type `σ`
     if env.base.get env |>.constants.contains asyncDecl then
-      return ext.getStateImpl env.base.private.extensions
+      return ext.getStateImpl env.base.private.extensions tripwire
 
     -- specialization of the following branch, nested async decls are rare
     if let some c := env.asyncConsts.find? asyncDecl then
       match branch with
       | .asyncEnv =>
         if let some exts := c.exts? then
-          return ext.getStateImpl exts.get
+          return ext.getStateImpl exts.get tripwire
         else
-          return ext.getStateImpl env.base.private.extensions
+          return ext.getStateImpl env.base.private.extensions tripwire
       | .mainEnv =>
         if c.isRealized then
           if let some exts := c.exts? then
-            return ext.getStateImpl exts.get
+            return ext.getStateImpl exts.get tripwire
         else
-          return ext.getStateImpl env.base.private.extensions
+          return ext.getStateImpl env.base.private.extensions tripwire
 
     if let some (c, parent?) := env.asyncConsts.findRecAndParent? asyncDecl then
       -- If `parent?` is `none`, the current branch is the parent
@@ -1481,17 +1707,17 @@ private unsafe def getStateUnsafe {σ : Type} [Inhabited σ] (ext : EnvExtension
           -- this specific case, accessing the latter will in particular not block longer than the
           -- former.
           | .mainEnv => if c.isRealized then c.exts? else parentExts?) then
-        return ext.getStateImpl exts.get
+        return ext.getStateImpl exts.get tripwire
       -- NOTE: if `exts?` is `none`, we should *not* try the following, more expensive branches that
       -- will just come to the same conclusion
     else if let some c := env.allRealizations.get.find? asyncDecl then
       if let some exts := c.exts? then
-        return ext.getStateImpl exts.get
+        return ext.getStateImpl exts.get tripwire
     -- fallback; we could enforce that `asyncDecl` and its extension state always exist but the
     -- upside of doing is unclear and it is not true in e.g. the compiler. One alternative would be
     -- to add a `getState?` that does not panic in such cases.
-    ext.getStateImpl env.base.private.extensions
-  | _         => ext.getStateImpl env.base.private.extensions
+    ext.getStateImpl env.base.private.extensions tripwire
+  | _         => ext.getStateImpl env.base.private.extensions tripwire
 
 /--
 Returns the current extension state. See `AsyncMode` for details on how modifications from
@@ -1502,7 +1728,31 @@ only for important optimizations.
 -/
 @[implemented_by getStateUnsafe]
 opaque getState {σ : Type} [Inhabited σ] (ext : EnvExtension σ) (env : Environment)
-  (asyncMode := ext.asyncMode) (asyncDecl : Name := .anonymous) : σ
+  (asyncMode := ext.asyncMode) (asyncDecl : Name := .anonymous) (recorded := false) : σ
+
+private unsafe def getGenUnsafe (ext : EnvExtension EnvExtensionState) (env : Environment) : Nat :=
+  -- `.recorded` extensions are restricted to `.local`/`.mainOnly`, whose state lives in the
+  -- current branch's array.
+  let exts := env.base.private.extensions
+  if h : ext.idx < exts.size then
+    (unsafeCast exts[ext.idx] : Nat × EnvExtensionState).1
+  else 0
+
+@[implemented_by getGenUnsafe]
+private opaque getGen (ext : EnvExtension EnvExtensionState) (env : Environment) : Nat
+
+/--
+Current generation of the `.recorded` extension with registration index `idx` on the current
+branch of `env`, or 0 if `idx` does not denote a `.recorded` extension. Used to validate the
+`RecordedDeps.extGens` dependencies of a recorded entry.
+-/
+def getRecordedGen (env : Environment) (idx : Nat) : BaseIO Nat := do
+  let exts ← envExtensionsRef.get
+  if h : idx < exts.size then
+    let ext := exts[idx]
+    if ext.trackGen then
+      return getGen ext env
+  return 0
 
 end EnvExtension
 
@@ -1515,12 +1765,19 @@ end EnvExtension
    For that, you need to register a persistent environment extension. -/
 def registerEnvExtension {σ : Type} (mkInitial : IO σ)
     (replay? : Option (ReplayFn σ) := none)
-    (asyncMode : EnvExtension.AsyncMode := .mainOnly) : IO (EnvExtension σ) := do
+    (asyncMode : EnvExtension.AsyncMode := .mainOnly)
+    (name : Name := .anonymous)
+    (trackGen : Bool := false)
+    (declCovered : Bool := false) : IO (EnvExtension σ) := do
   unless (← initializing) do
     throw (IO.userError "failed to register environment, extensions can only be registered during initialization")
+  if trackGen then
+    unless asyncMode matches .local | .mainOnly do
+      throw (IO.userError "generation-tracked environment extensions must use `AsyncMode.local` or \
+        `.mainOnly`; generations are branch-local (see `EnvExtension.trackGen`)")
   let exts ← EnvExtension.envExtensionsRef.get
   let idx := exts.size
-  let ext : EnvExtension σ := { idx, mkInitial, asyncMode, replay? }
+  let ext : EnvExtension σ := { idx, mkInitial, asyncMode, replay?, name, trackGen, declCovered }
   -- safety: `EnvExtensionState` is opaque, so we can upcast to it
   EnvExtension.envExtensionsRef.modify fun exts => exts.push (unsafe unsafeCast ext)
   pure ext
@@ -1669,12 +1926,13 @@ but is limited to the maximum level actually imported: `exported` on the cmdline
 language server. Higher levels will return the data of the maximum imported level.
 -/
 def getModuleEntries {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ)
-    (env : Environment) (m : ModuleIdx) (level := OLeanLevel.exported) : Array α :=
+    (env : Environment) (m : ModuleIdx) (level := OLeanLevel.exported) : Array α := Id.run do
+  -- imported entries are immutable within a module, so reads record no resolution dependency
   let exts := match level with
     | .exported => env.base.private.extensions
     | _         => env.serverBaseExts
   -- safety: as in `getStateUnsafe`
-  unsafe (ext.toEnvExtension.getStateImpl exts).importedEntries[m]!
+  return unsafe (ext.toEnvExtension.getStateImpl exts).importedEntries[m]!
 
 /-- Retrieves additional IR extension state for the interpreter. -/
 def getModuleIREntries {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ)
@@ -1690,8 +1948,10 @@ def addEntry {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : En
 
 /-- Get the current state of the given extension in the given environment. -/
 def getState {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ) (env : Environment)
-    (asyncMode := ext.toEnvExtension.asyncMode) (asyncDecl : Name := .anonymous) : σ :=
-  (ext.toEnvExtension.getState (asyncMode := asyncMode) (asyncDecl := asyncDecl) env).state
+    (asyncMode := ext.toEnvExtension.asyncMode) (asyncDecl : Name := .anonymous)
+    (recorded := false) : σ :=
+  (ext.toEnvExtension.getState (asyncMode := asyncMode) (asyncDecl := asyncDecl)
+    (recorded := recorded) env).state
 
 /-- Set the current state of the given extension in the given environment. -/
 def setState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (s : σ) : Environment :=
@@ -1699,8 +1959,10 @@ def setState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : En
 
 /-- Modify the state of the given extension in the given environment by applying the given function. -/
 def modifyState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (f : σ → σ)
-    (asyncMode := ext.toEnvExtension.asyncMode) (asyncDecl : Name := Name.anonymous) : Environment :=
-  ext.toEnvExtension.modifyState (asyncMode := asyncMode) (asyncDecl := asyncDecl) env fun ps => { ps with state := f (ps.state) }
+    (asyncMode := ext.toEnvExtension.asyncMode) (asyncDecl : Name := Name.anonymous)
+    (keepRecordGen := false) : Environment :=
+  ext.toEnvExtension.modifyState (asyncMode := asyncMode) (asyncDecl := asyncDecl)
+    (keepRecordGen := keepRecordGen) env fun ps => { ps with state := f (ps.state) }
 
 end PersistentEnvExtension
 
@@ -1716,6 +1978,10 @@ structure PersistentEnvExtensionDescrCore (α β σ : Type) where
   statsFn           : σ → Format := fun _ => Format.nil
   asyncMode         : EnvExtension.AsyncMode := .mainOnly
   replay?           : Option (ReplayFn σ) := none
+  /-- See `EnvExtension.trackGen`. -/
+  trackGen : Bool := false
+  /-- See `EnvExtension.trackGen`. -/
+  declCovered : Bool := false
 
 attribute [inherit_doc PersistentEnvExtension.exportEntriesFn]
   PersistentEnvExtensionDescrCore.exportEntriesFnEx
@@ -1742,7 +2008,8 @@ unsafe def registerPersistentEnvExtensionUnsafe {α β σ : Type} [Inhabited σ]
   if pExts.any (fun ext => ext.name == descr.name) then throw (IO.userError s!"invalid environment extension, '{descr.name}' has already been used")
   let replay? := descr.replay?.map fun replay =>
     fun oldState newState newConsts s => { s with state := replay oldState.state newState.state newConsts s.state }
-  let ext ← registerEnvExtension (asyncMode := descr.asyncMode) (replay? := replay?) do
+  let ext ← registerEnvExtension (asyncMode := descr.asyncMode) (replay? := replay?)
+      (name := descr.name) (trackGen := descr.trackGen) (declCovered := descr.declCovered) do
     let initial ← descr.mkInitial
     let s : PersistentEnvExtensionState α σ := {
       importedEntries := #[],
@@ -2756,6 +3023,14 @@ def realizeConst (env : Environment) (forConst : Name) (constName : Name)
     pure (.mk res)
   let some res := res.get? RealizeConstResult | unreachable!
   let exPromise ← IO.Promise.new
+  -- The realized constants and their extension-state snapshots become observable on this
+  -- lineage with this merge, so this is where their birth indices are assigned; see
+  -- `Environment.constBirths`.
+  let env := res.newConsts.private.foldl (init := env) fun env c =>
+    if env.asyncConstsMap.private.find? c.constInfo.name |>.isSome then
+      env
+    else
+      env.registerConstBirth c.constInfo.name
   let env := { env with
     asyncConstsMap := {
       «private» := res.newConsts.private.foldl (init := env.asyncConstsMap.private) fun consts c =>
@@ -2881,11 +3156,21 @@ This is consulted for all definitions regardless of their reducibility hints. Cu
 structural recursion to ensure that parent definitions get the correct height even though the
 `_f` helper definitions are marked as `.abbrev` (which `getMaxHeight` would otherwise ignore). -/
 builtin_initialize defHeightOverrideExt : EnvExtension (NameMap UInt32) ←
-  registerEnvExtension (pure {}) (asyncMode := .local)
+  -- covered: overrides are declaration-keyed, write-stability-guarded, and logged
+  registerEnvExtension (pure {}) (asyncMode := .local) (declCovered := true)
 
 /-- Register a height override for a definition so that `getMaxHeight` uses it. -/
 def setDefHeightOverride (env : Environment) (declName : Name) (height : UInt32) : Environment :=
-  defHeightOverrideExt.modifyState env fun m => m.insert declName height
+  let env := env.logDeclChange declName
+  defHeightOverrideExt.modifyState env fun m =>
+    -- write-stability guard; see `MapDeclarationExtension.insert`
+    match m.find? declName with
+    | some prev =>
+      if prev != height then
+        panic! s!"definition height override for `{declName}` is already set"
+      else
+        m
+    | none => m.insert declName height
 
 def getMaxHeight (env : Environment) (e : Expr) : UInt32 :=
   let overrides := defHeightOverrideExt.getState env
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 5e2281389fe2..e52da5269017 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -811,15 +811,18 @@ instance (m n) [MonadLift m n] [AddMessageContext m] : AddMessageContext n where
   addMessageContext := fun msg => liftM (addMessageContext msg : m _)
 
 def addMessageContextPartial {m} [Monad m] [MonadEnv m] [MonadOptions m] (msgData : MessageData) : m MessageData := do
-  let env ← getEnv
-  let opts ← getOptions
+  -- unrestricted acquisition: a message context is a display context, whose later reads cannot
+  -- influence a cached resolution result; the environment's recording marker is dropped so that
+  -- later extension reads by message consumers do not trip it
+  let env := (← getEnv).setRecordingDeps false
+  let opts ← getOptionsUnrestricted
   return MessageData.withContext { env := env, mctx := {}, lctx := {}, opts := opts } msgData
 
 def addMessageContextFull {m} [Monad m] [MonadEnv m] [MonadMCtx m] [MonadLCtx m] [MonadOptions m] (msgData : MessageData) : m MessageData := do
-  let env ← getEnv
+  let env := (← getEnv).setRecordingDeps false
   let mctx ← getMCtx
   let lctx ← getLCtx
-  let opts ← getOptions
+  let opts ← getOptionsUnrestricted
   return MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msgData
 
 class ToMessageData (α : Type) where
@@ -862,7 +865,8 @@ def toMessageList (msgs : Array MessageData) : MessageData :=
 namespace Kernel.Exception
 
 private def mkCtx (env : Environment) (lctx : LocalContext) (opts : Options) (msg : MessageData) : MessageData :=
-  MessageData.withContext { env := .ofKernelEnv env, mctx := {}, lctx := lctx, opts := opts } msg
+  MessageData.withContext
+    { env := .ofKernelEnv env, mctx := {}, lctx := lctx, opts } msg
 
 def toMessageData (e : Kernel.Exception) (opts : Options) : MessageData :=
   match e with
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index e207f8f137bd..ca3bd5766856 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -350,15 +350,112 @@ structure InfoCacheKey where
 instance : Hashable InfoCacheKey where
   hash := private fun { configKey, expr, nargs? } => mixHash (hash configKey) <| mixHash (hash expr) (hash nargs?)
 
+/--
+The option lookups a type class resolution cache entry was computed under, deduplicated by name;
+a lookup may only use an entry whose recorded accesses give the same answers in the current
+context. See `SynthInstanceCache`.
+-/
+abbrev SynthOptionAccessLog := Array RecordedOptionAccess
+
+/--
+Resource limits a type class resolution query runs under; part of the cache key, see
+`SynthInstanceCacheKey.limits`.
+-/
+structure SynthLimits where
+  maxHeartbeats           : Nat
+  synthInstanceHeartbeats : Nat
+  maxRecDepth             : Nat
+  exponentiationThreshold : Nat
+  deriving Hashable, BEq, Inhabited
+
+/--
+The definitional-equality and unfolding compatibility flags, resolved and recorded once per type
+class resolution query (`synthInstanceCore?`) so that their per-step reads inside the search
+avoid the recording accessors; see `getSynthDefEqFlag`. Being resolved up front, they are part
+of the cache key (`SynthInstanceCacheKey.defEqFlags`) rather than recorded dependencies: every
+query partitions on all of them, whether its search reaches the corresponding reads or not.
+They are global compatibility settings, so the sharing lost to this over-approximation is
+negligible.
+-/
+structure SynthDefEqFlags where
+  respectTransparency      : Bool
+  respectTransparencyTypes : Bool
+  implicitBump             : Bool
+  reducibleClassField      : Bool
+  lazyProjDelta            : Bool
+  lazyWhnfCore             : Bool
+  smartUnfolding           : Bool
+  deriving Inhabited, BEq, Hashable
+
 -- Remark: we don't need to store `Config.toKey` because typeclass resolution uses a fixed configuration.
 structure SynthInstanceCacheKey where
   localInsts        : LocalInstances
   type              : Expr
   /--
+  For a normalized (`.noMVars`, fvar-typed) query, the canonical types of the free variables
+  referenced by `type`/`localInsts`, indexed by their canonical position (see the fvar
+  normalization in `SynthInstance.lean`). Free variables in `type` and `localInsts` are renamed
+  to positional canonical identifiers, so structurally identical queries in different local
+  contexts share a cache entry. Empty for non-normalized (raw) keys.
+  -/
+  normFVarTypes     : Array Expr := #[]
+  /--
+  For each closure position, the canonical value of that free variable if it is let-bound, and
+  `none` otherwise. A let-bound variable's value is visible to definitional unfolding, so contexts
+  that agree on the types but not the values are not interchangeable. Empty for raw keys.
+  -/
+  normFVarValues    : Array (Option Expr) := #[]
+  /--
   Value of `synthPendingDepth` when instance was synthesized or failed to be synthesized.
   See issue #2522.
   -/
   synthPendingDepth : Nat
+  /--
+  Namespaces with scoped instances that are currently activated (e.g. via `open`), in canonical
+  order. Keying the cache by this set keeps entries from outside a scope valid after the scope
+  ends, e.g. for the `open Classical in` expansion of `by_cases`.
+  -/
+  activeScopedInsts : Array Name
+  /--
+  Instances currently added with the `local` attribute kind (`Instances.localInstanceNames`).
+  Like `activeScopedInsts`, keying the cache by this set keeps entries from outside a scope
+  containing `attribute [local instance]` valid after the scope ends, and prevents entries
+  computed with the local instance from leaking out of the scope.
+  -/
+  localAttrInsts    : Array Name
+  /--
+  Instances currently erased via `attribute [-instance]` (`Instances.erased`), in canonical
+  order. Erasure is delimited by its surrounding scope like local instances, and entries are
+  keyed by it for the same reason: an entry (in particular a cached failure) computed under an
+  erasure must not be served once the surrounding scope ends and restores the instance.
+  -/
+  erasedInsts       : Array Name
+  /--
+  Effective maximum result size (`synthInstance.maxSize` unless overridden by the caller).
+  The cache persists across commands, so results (in particular failures) obtained under a
+  different size limit must not be reused.
+  -/
+  maxResultSize     : Nat
+  /--
+  The definitional-equality flags the query runs under, resolved up front; see
+  `SynthDefEqFlags`. Options read lazily during the search are recorded per entry instead
+  (`SynthOptionAccessLog`).
+  -/
+  defEqFlags        : SynthDefEqFlags
+  /--
+  Value of `Environment.isExporting`: in the exporting state, fewer definitions can be unfolded,
+  which can change the result of typeclass resolution.
+  -/
+  isExporting       : Bool
+  /--
+  The resource limits in effect for the query (`maxHeartbeats`, `synthInstance.maxHeartbeats`,
+  `maxRecDepth`, `exponentiation.threshold`). Exceeding a limit throws, and results are only
+  cached on the success path, so a limit cannot influence a stored result; keying by them
+  nevertheless makes that a structural property rather than an argument about exception paths,
+  and lets their (frequent, mostly out-of-query) reads be plain unrestricted reads. Limits are
+  effectively constant per module, so this does not partition the cache in practice.
+  -/
+  limits            : SynthLimits
   deriving Hashable, BEq
 
 /-- Resulting type for `abstractMVars` -/
@@ -371,7 +468,20 @@ structure AbstractMVarsResult where
 def AbstractMVarsResult.numMVars (r : AbstractMVarsResult) : Nat :=
   r.mvars.size
 
-abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey (Option AbstractMVarsResult)
+/--
+Type class resolution cache. Each key holds one entry per observed combination of dependencies:
+the search records every result-relevant option lookup (`getRecordedOption`) and every observed
+environment dependency (accessed `.recorded` extensions and reducibility statuses; see
+`Lean.EnvExtension.TCResolutionAccess`) into the entry's `SynthDepLog`, and a lookup may only
+use an entry whose recorded dependencies give the same answers in the current context.
+Dependencies the search never observed do not partition the cache. The search observes no other
+options or extensions, as it runs with `Core.Context.recordingDeps` set, which diverts option
+acquisitions to the recording
+`Core.Context.recordingDeps` set, which divert by-name option reads to the recording
+accessors and panic on `.deny` extension accesses.
+-/
+abbrev SynthInstanceCache :=
+  PersistentHashMap SynthInstanceCacheKey (List (RecordedDeps × Option AbstractMVarsResult))
 
 -- Key for `InferType` and `WHNF` caches
 structure ExprConfigCacheKey where
@@ -409,8 +519,46 @@ We should also investigate the impact on memory consumption.
 -/
 abbrev DefEqCache := PersistentHashMap DefEqCacheKey Bool
 
+/--
+The free-variable normalization of a local instance context: the canonical position of every free
+variable reachable from the local instances (transitively via their types), that variable's
+recursively normalized type, and the local instances themselves over the canonical variables. See
+the normalization in `SynthInstance.lean`.
+-/
+structure SynthNormClosure where
+  fmap            : PersistentHashMap FVarId Nat
+  order           : Array FVarId
+  types           : Array Expr
+  /-- The canonical value of each let-bound closure variable; `none` for the others. -/
+  values          : Array (Option Expr)
+  canonLocalInsts : LocalInstances
+
+/--
+`SynthNormClosure` memoized for the local instances it was computed from. The closure does not
+depend on the query, so every type class query made under the same local instances shares it;
+recomputing it per query dominates the cost of building a cache key.
+-/
+structure SynthNormClosureMemo where
+  /-- The local instances the closure was computed for. -/
+  localInsts : LocalInstances
+  /--
+  The closure variables whose raw `LocalDecl` type or let-value mentions a metavariable, with the
+  instantiation the closure was built from (`true` = the value, `false` = the type). A `LocalDecl`
+  is immutable, so only these can change: a metavariable may be assigned, or an assignment reverted
+  by backtracking.
+  -/
+  mvarTyped : Array (FVarId × Bool × Expr)
+  /-- `none` if the local instance context cannot be soundly normalized. -/
+  closure? : Option SynthNormClosure
+
 /--
 Cache datastructures for type inference, type class resolution, whnf, and definitional equality.
+
+The `synthInstance` field is the *transient* tier of the type class resolution cache: it has
+the lifetime of the current `Meta.State` and holds all entries, including context-sensitive ones
+(keys containing metavariables, or results with abstracted metavariables) whose validity is tied
+to the current elaboration context. Context-free entries are additionally stored in an
+environment extension so that they persist across commands (see `synthInstanceCacheExt`).
 -/
 structure Cache where
   inferType      : InferTypeCache := {}
@@ -419,6 +567,12 @@ structure Cache where
   whnf           : WhnfCache := {}
   defEqTrans     : DefEqCache := {} -- transient cache for terms containing mvars or using nonstandard configuration options, it is frequently reset.
   defEqPerm      : DefEqCache := {} -- permanent cache for terms not containing mvars and using standard configuration options
+  /--
+  One-slot memo for the free-variable normalization of the local instance context; see
+  `SynthNormClosureMemo`. One slot suffices because the local instances change rarely relative to
+  the number of type class queries made under them.
+  -/
+  synthNormClosure : Option SynthNormClosureMemo := none
   deriving Inhabited
 
 /--
@@ -526,6 +680,8 @@ structure Context where
   Remark: `synthPending` fails if `synthPendingDepth > maxSynthPendingDepth`.
   -/
   synthPendingDepth : Nat                  := 0
+  /-- Set per type class resolution query; see `SynthDefEqFlags`. -/
+  synthDefEqFlags?  : Option SynthDefEqFlags := none
   /--
   A predicate to control whether a constant can be unfolded or not at `whnf`.
   If set, overrides `Config.canUnfoldPredicateConfig`.
@@ -683,13 +839,13 @@ def resetCache : MetaM Unit :=
   modifyCache fun _ => {}
 
 @[inline] def modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
-  modifyCache fun ⟨ic, c1, c2, c3, c4, c5⟩ => ⟨f ic, c1, c2, c3, c4, c5⟩
+  modifyCache fun ⟨ic, c1, c2, c3, c4, c5, c6⟩ => ⟨f ic, c1, c2, c3, c4, c5, c6⟩
 
 @[inline] def modifyDefEqTransientCache (f : DefEqCache → DefEqCache) : MetaM Unit :=
-  modifyCache fun ⟨c1, c2, c3, c4, defeqTrans, c5⟩ => ⟨c1, c2, c3, c4, f defeqTrans, c5⟩
+  modifyCache fun ⟨c1, c2, c3, c4, defeqTrans, c5, c6⟩ => ⟨c1, c2, c3, c4, f defeqTrans, c5, c6⟩
 
 @[inline] def modifyDefEqPermCache (f : DefEqCache → DefEqCache) : MetaM Unit :=
-  modifyCache fun ⟨c1, c2, c3, c4, c5, defeqPerm⟩ => ⟨c1, c2, c3, c4, c5, f defeqPerm⟩
+  modifyCache fun ⟨c1, c2, c3, c4, c5, defeqPerm, c6⟩ => ⟨c1, c2, c3, c4, c5, f defeqPerm, c6⟩
 
 def mkExprConfigCacheKey (expr : Expr) : MetaM ExprConfigCacheKey :=
   return { expr, configKey := (← read).configKey }
@@ -707,9 +863,6 @@ def mkInfoCacheKey (expr : Expr) (nargs? : Option Nat) : MetaM InfoCacheKey :=
 @[inline] def resetDefEqPermCaches : MetaM Unit :=
   modifyDefEqPermCache fun _ => {}
 
-@[inline] def resetSynthInstanceCache : MetaM Unit :=
-  modifyCache fun c => {c with synthInstance := {}}
-
 @[inline] def modifyDiag (f : Diagnostics → Diagnostics) : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
     modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache, zetaDeltaFVarIds, postponed, diag := f diag }
@@ -1212,6 +1365,19 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) :
 @[inline] def withIncSynthPending : n α → n α :=
   mapMetaM <| withReader (fun ctx => { ctx with synthPendingDepth := ctx.synthPendingDepth + 1 })
 
+/--
+Reads a definitional-equality compatibility flag: from the per-query resolved flags inside a
+type class resolution query, and via `fallback` from the ambient options otherwise. Inside a
+query the flags are always armed and already recorded (`SynthDefEqFlags`), so the read costs a
+context projection; per-step read sites in `isDefEq`/`whnf` use this instead of the recording
+accessors.
+-/
+@[inline] def getSynthDefEqFlag (proj : SynthDefEqFlags → Bool) (fallback : Options → Bool) :
+    MetaM Bool := do
+  match (← read).synthDefEqFlags? with
+  | some flags => return proj flags
+  | none       => return fallback (← getOptions)
+
 @[inline] def withInTypeClassResolution : n α → n α :=
   mapMetaM <| withReader (fun ctx => { ctx with inTypeClassResolution := true })
 
@@ -2270,7 +2436,8 @@ def instantiateLambdaWithParamInfos (e : Expr) (args : Array Expr) (cleanupAnnot
   return (res, e)
 
 def getPPContext : MetaM PPContext := do
-  return { env := (← getEnv), mctx := (← getMCtx), lctx := (← getLCtx), opts := (← getOptions),
+  -- unrestricted acquisition: a message context is a display context, see `addMessageContextFull`
+  return { env := (← getEnv), mctx := (← getMCtx), lctx := (← getLCtx), opts := (← getOptionsUnrestricted),
            currNamespace := (← getCurrNamespace), openDecls := (← getOpenDecls) }
 
 /-- Pretty-print the given expression. -/
@@ -2591,7 +2758,8 @@ def instantiateMVarsIfMVarApp (e : Expr) : MetaM Expr := do
     return e
 
 def instantiateMVarsProfiling (e : Expr) : MetaM Expr := do
-  profileitM Exception s!"instantiate metavars" (← getOptions) do
+  -- unrestricted acquisition: profiler collection cannot influence a cached resolution result
+  profileitM Exception s!"instantiate metavars" (← getOptionsUnrestricted) do
   withTraceNode `Meta.instantiateMVars (fun _ => pure e) do
     instantiateMVars e
 
@@ -2745,7 +2913,8 @@ def realizeConst (forConst : Name) (constName : Name) (realize : MetaM Unit) :
     let exAct ← Core.wrapAsyncAsSnapshot (cancelTk? := none) fun
       | none => return
       | some ex => do
-        logError <| ex.toMessageData (← getOptions)
+        -- unrestricted acquisition: rendering an exception, which is never cached
+        logError <| ex.toMessageData (← getOptionsUnrestricted)
     Core.logSnapshotTask {
       stx? := none
       task := (← BaseIO.mapTask (t := exTask) exAct)
diff --git a/src/Lean/Meta/Constructions/SparseCasesOn.lean b/src/Lean/Meta/Constructions/SparseCasesOn.lean
index f184572b0c27..146a1406b892 100644
--- a/src/Lean/Meta/Constructions/SparseCasesOn.lean
+++ b/src/Lean/Meta/Constructions/SparseCasesOn.lean
@@ -24,7 +24,10 @@ structure SparseCasesOnKey where
 deriving BEq, Hashable
 
 builtin_initialize sparseCasesOnCacheExt : EnvExtension (PHashMap SparseCasesOnKey Name) ←
-  registerEnvExtension (pure {}) (asyncMode := .local)  -- mere cache, keep it local
+  -- mere cache, keep it local; may be consulted on resolution search paths via the reserved-name
+  -- covered: realization cache, populated on demand; reads never observe result-relevant
+  -- absence, and entries are write-stability-guarded
+  registerEnvExtension (pure {}) (asyncMode := .local) (declCovered := true)
 
 /-- Information necessary to recognize and split on sparse casesOn (in particular in MatchEqs) -/
 public structure SparseCasesOnInfo where
@@ -35,6 +38,8 @@ public structure SparseCasesOnInfo where
 deriving Inhabited
 
 builtin_initialize sparseCasesOnInfoExt : MapDeclarationExtension SparseCasesOnInfo ←
+  -- consulted by the reserved-name predicate for `else_eq` names, so also on resolution search
+  -- paths; populated only when the declaration is created (monotone)
   mkMapDeclarationExtension (exportEntriesFn := fun env s =>
     let all := s.toArray
     -- Do not export for non-exposed defs at exported/server levels
@@ -133,7 +138,15 @@ public def mkSparseCasesOn (indName : Name) (ctors : Array Name) : MetaM Name :=
     (value       := value)
     (hints       := ReducibilityHints.abbrev)
   addDecl (.defnDecl decl)
-  modifyEnv fun env => sparseCasesOnCacheExt.modifyState env fun s => s.insert key declName
+  modifyEnv fun env => sparseCasesOnCacheExt.modifyState env fun s =>
+    -- write-stability guard; see `MapDeclarationExtension.insert`
+    match s.find? key with
+    | some prev =>
+      if prev != declName then
+        panic! s!"sparse `casesOn` for `{declName}` is already registered as `{prev}`"
+      else
+        s
+    | none => s.insert key declName
   setReducibleAttribute declName
   modifyEnv fun env => markSparseCasesOn env declName
   modifyEnv fun env => sparseCasesOnInfoExt.insert env declName {
diff --git a/src/Lean/Meta/Diagnostics.lean b/src/Lean/Meta/Diagnostics.lean
index d1b9c832edb7..0d3e3ae57110 100644
--- a/src/Lean/Meta/Diagnostics.lean
+++ b/src/Lean/Meta/Diagnostics.lean
@@ -39,7 +39,8 @@ def DiagSummary.isEmpty (s : DiagSummary) : Bool :=
   s.data.isEmpty
 
 def mkDiagSummary (cls : Name) (counters : PHashMap Name Nat) (p : Name → Bool := fun _ => true) : MetaM DiagSummary := do
-  let threshold := diagnostics.threshold.get (← getOptions)
+  -- unrestricted acquisition: diagnostics counters cannot influence a cached resolution result
+  let threshold := diagnostics.threshold.get (← getOptionsUnrestricted)
   let entries := collectAboveThreshold counters threshold p Name.lt
   if entries.isEmpty then
     return {}
@@ -103,7 +104,7 @@ def reportDiag : MetaM Unit := do
     let m := appendSection m `reduction "unfolded reducible declarations" unfoldReducible
     let m := appendSection m `type_class "used instances" inst
     let m := appendSection m `type_class
-              s!"max synth pending failures (maxSynthPendingDepth: {maxSynthPendingDepth.get (← getOptions)}), use `set_option maxSynthPendingDepth <limit>`"
+              s!"max synth pending failures (maxSynthPendingDepth: {maxSynthPendingDepth.get (← getOptionsUnrestricted)}), use `set_option maxSynthPendingDepth <limit>`"
               synthPending (resultSummary := false)
     let m := appendSection m `def_eq "heuristic for solving `f a =?= f b`" heu
     let m := appendSection m `reduction "Axioms (possibly imported non-exposed defs) that were tried to be unfolded" unfoldAxiom
diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean
index c20d482ac376..b323c2b24bbd 100644
--- a/src/Lean/Meta/Eqns.lean
+++ b/src/Lean/Meta/Eqns.lean
@@ -47,6 +47,8 @@ def eqnAffectingOptions : Array (Lean.Option Bool) :=
 keyed by declaration name. Only populated when at least one option has a non-default value.
 Stores an association list of (option name, value) pairs for options that differ from defaults. -/
 builtin_initialize eqnOptionsExt : MapDeclarationExtension (Array (Name × DataValue)) ←
+  -- consulted during equation realization, which can happen inside a resolution search;
+  -- populated only when the declaration is created (monotone)
   mkMapDeclarationExtension (asyncMode := .local)
 
 def eqnThmSuffixBase := "eq"
@@ -157,7 +159,10 @@ structure EqnsExtState where
 
 /-- A mapping from equational theorem to the declaration it was derived from.  -/
 builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
-  registerEnvExtension (pure {}) (asyncMode := .local)
+  -- consulted during equation realization, which can happen inside a resolution search;
+  -- covered: realized on demand, so reads never observe result-relevant absence, and
+  -- registered equations are write-stability-guarded
+  registerEnvExtension (pure {}) (asyncMode := .local) (declCovered := true)
 
 /--
 Runs `act` with the equation-affecting options restored to the values stored for `declName`
@@ -216,7 +221,16 @@ Stores in the `eqnsExt` environment extension that `eqThms` are the equational t
 -/
 private def registerEqnThms (declName : Name) (eqThms : Array Name) : CoreM Unit := do
   modifyEnv fun env => eqnsExt.modifyState env fun s => { s with
-    mapInv := eqThms.foldl (init := s.mapInv) fun mapInv eqThm => mapInv.insert eqThm declName
+    mapInv := eqThms.foldl (init := s.mapInv) fun mapInv eqThm =>
+      -- write-stability guard; see `MapDeclarationExtension.insert`. Re-registration with the
+      -- same parent is idempotent (e.g. `alreadyGenerated?` re-registers realized equations).
+      match mapInv.find? eqThm with
+      | some prev =>
+        if prev != declName then
+          panic! s!"equation theorem `{eqThm}` is already registered for `{prev}`"
+        else
+          mapInv
+      | none => mapInv.insert eqThm declName
   }
 
 /--
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index c5cc39145b4c..e2e7eb706693 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -376,8 +376,8 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta
   for i in finfo.paramInfo.size...args₁.size do
     unless (← Meta.isExprDefEqAux args₁[i]! args₂[i]!) do
       return false
-  let respectTransparency := backward.isDefEq.respectTransparency.get (← getOptions)
-  let implicitBump := backward.isDefEq.implicitBump.get (← getOptions)
+  let respectTransparency ← getSynthDefEqFlag (·.respectTransparency) (backward.isDefEq.respectTransparency.get ·)
+  let implicitBump ← getSynthDefEqFlag (·.implicitBump) (backward.isDefEq.implicitBump.get ·)
   for i in postponedImplicit do
     /- Second pass: unify implicit arguments.
        When `respectTransparency` is `false` (old behavior), we bump to `.default` so that
@@ -485,9 +485,9 @@ and is used to enable the transparency bump when checking metavariable assignmen
 If `backward.isDefEq.respectTransparency` is `false`, then we automatically disable
 `backward.isDefEq.respectTransparency.types` too.
 -/
-abbrev respectTransparencyAtTypes : CoreM Bool := do
-  let opts ← getOptions
-  return backward.isDefEq.respectTransparency.types.get opts && backward.isDefEq.respectTransparency.get opts
+abbrev respectTransparencyAtTypes : MetaM Bool := do
+  return (← getSynthDefEqFlag (·.respectTransparencyTypes) (backward.isDefEq.respectTransparency.types.get ·))
+    && (← getSynthDefEqFlag (·.respectTransparency) (backward.isDefEq.respectTransparency.get ·))
 
 private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
   withTraceNodeBefore `Meta.isDefEq.assign.checkTypes (fun _ => return m!"({mvar} : {← inferType mvar}) := ({v} : {← inferType v})") do
@@ -1445,7 +1445,7 @@ private def isNonTrivialRegular (info : DefinitionVal) : MetaM Bool := do
          only applies there. At higher transparency levels, the normal unfolding behavior is
          sufficient, and running the heuristic adds overhead without benefit.
          See https://github.com/leanprover/lean4/pull/12650 -/
-      return projInfo.fromClass && backward.whnf.reducibleClassField.get (← getOptions) && (← getTransparency) == .reducible
+      return projInfo.fromClass && (← getSynthDefEqFlag (·.reducibleClassField) (backward.whnf.reducibleClassField.get ·)) && (← getTransparency) == .reducible
     return false
   | .opaque => return false
 where
@@ -1758,7 +1758,7 @@ private def etaEq (t s : Expr) : Bool :=
   performance foot-gun. Users can use the backward compatibility flag to restore the old behavior.
 -/
 private def withProofIrrelTransparency (k : MetaM α) : MetaM α := do
-  if backward.isDefEq.respectTransparency.get (← getOptions) then
+  if (← getSynthDefEqFlag (·.respectTransparency) (backward.isDefEq.respectTransparency.get ·)) then
     k
   else
     withInferTypeConfig k
@@ -2112,7 +2112,7 @@ private def isDefEqProj : Expr → Expr → MetaM Bool
     if (← read).inTypeClassResolution then
       -- See comment at `inTypeClassResolution`
       pure (i == j && m == n) <&&> isDefEqStructArgs (Meta.isExprDefEqAux t s)
-    else if !backward.isDefEq.lazyProjDelta.get (← getOptions) then
+    else if !(← getSynthDefEqFlag (·.lazyProjDelta) (backward.isDefEq.lazyProjDelta.get ·)) then
       pure (i == j && m == n) <&&> isDefEqStructArgs (Meta.isExprDefEqAux t s)
     else if i == j && m == n then
       isDefEqStructArgs (isDefEqProjDelta t s i)
@@ -2275,7 +2275,7 @@ private def cacheResult (keyInfo : DefEqCacheKeyInfo) (result : Bool) : MetaM Un
     modifyDefEqTransientCache fun c => c.insert key result
 
 private def whnfCoreAtDefEq (e : Expr) : MetaM Expr := do
-  if backward.isDefEq.lazyWhnfCore.get (← getOptions) then
+  if (← getSynthDefEqFlag (·.lazyWhnfCore) (backward.isDefEq.lazyWhnfCore.get ·)) then
     withConfig (fun ctx => { ctx with proj := .yesWithDeltaI }) <| whnfCore e
   else
     whnfCore e
@@ -2284,7 +2284,8 @@ set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_is_expr_def_eq]
 partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecDepth do
   withTraceNodeBefore `Meta.isDefEq (fun _ => do
-    if trace.Meta.isDefEq.printTransparency.get (← getOptions) then
+    -- unrestricted read: trace collection cannot influence a cached resolution result
+    if trace.Meta.isDefEq.printTransparency.get (← getOptionsUnrestricted) then
       return m!"[{toString (← getTransparency)}] {t} =?= {s}"
     else
       return m!"{t} =?= {s}") do
diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean
index 98ed55bb22bb..dea8b0a16a17 100644
--- a/src/Lean/Meta/Instances.lean
+++ b/src/Lean/Meta/Instances.lean
@@ -77,15 +77,28 @@ structure Instances where
   discrTree     : InstanceTree := DiscrTree.empty
   instanceNames : PHashMap Name InstanceEntry := {}
   erased        : PHashSet Name := {}
+  /--
+  Names of instances added with the `local` attribute kind into this state, in insertion order.
+  Local instances are delimited by their surrounding scope, which restores the previous
+  `Instances` state (and thereby the previous value of this field) when it is closed. The field
+  is part of the type class resolution cache key (`SynthInstanceCacheKey.localAttrInsts`), so
+  cache entries never leak into or out of scopes with local instances.
+  -/
+  localInstanceNames : Array Name := #[]
   deriving Inhabited
 
 def addInstanceEntry (d : Instances) (e : InstanceEntry) : Instances :=
+  let d := if e.attrKind matches .local then
+    { d with localInstanceNames := d.localInstanceNames.push (e.globalName?.getD .anonymous) }
+  else
+    d
   match e.globalName? with
   | some n => { d with discrTree := d.discrTree.insertKeyValue e.keys e, instanceNames := d.instanceNames.insert n e, erased := d.erased.erase n }
   | none   => { d with discrTree := d.discrTree.insertKeyValue e.keys e }
 
 def Instances.eraseCore (d : Instances) (declName : Name) : Instances :=
-  { d with erased := d.erased.insert declName, instanceNames := d.instanceNames.erase declName }
+  { d with erased := d.erased.insert declName, instanceNames := d.instanceNames.erase declName,
+           localInstanceNames := d.localInstanceNames.filter (· != declName) }
 
 def Instances.erase [Monad m] [MonadError m] (d : Instances) (declName : Name) : m Instances := do
   unless d.instanceNames.contains declName do
@@ -99,8 +112,69 @@ builtin_initialize instanceExtension : SimpleScopedEnvExtension InstanceEntry In
     exportEntry? := fun _ e =>
       if e.globalName?.any (!isPrivateName ·) then .uniform (some e)
       else ⟨none, none, some e⟩
+    -- adding or erasing an instance bumps the generation, invalidating resolution cache
+    -- entries that consulted the instance table; scope activation is covered by the cache key
+    -- (`SynthInstanceCacheKey.activeScopedInsts`/`localAttrInsts`) instead
+    trackGen := true
   }
 
+private unsafe def getSynthCacheUnsafe (env : Environment) : SynthInstanceCache :=
+  match env.synthCacheRaw? with
+  | some v => unsafeCast v
+  | none   => {}
+
+/--
+Persistent tier of the `synthInstance` result cache, stored in `Environment.synthCacheRaw?`;
+see there and `Lean.Meta.SynthInstance`. It persists across commands and is not stored in
+`.olean` files.
+
+Only *context-free* entries are stored here: keys without metavariables and closed results.
+Context-sensitive entries (whose validity depends on the ambient metavariable context) live in
+the transient `Meta.Cache.synthInstance` tier instead.
+
+Both fills and invalidation are plain (branch-local) environment modifications: an entry is
+only ever observable in environments derived from the one it was filled in, so rolling back the
+environment (e.g. discarding a speculatively added instance) also rolls back the entries that
+were computed with it, and parallel elaboration branches never observe each other's fills.
+Entries persisted within a rolled-back region are lost with it; within a single command the
+transient tier compensates, as `Meta.Cache` is deliberately not restored by
+`Meta.SavedState.restore` (see `Lean.Meta.SynthInstance.insertCachedResult`).
+-/
+@[implemented_by getSynthCacheUnsafe]
+opaque _root_.Lean.Environment.synthCache (env : Environment) : SynthInstanceCache
+
+private unsafe def setSynthCacheUnsafe (env : Environment) (c : SynthInstanceCache) : Environment :=
+  env.setSynthCacheRaw? (some (unsafeCast c))
+
+/-- Replaces the persistent tier of the `synthInstance` result cache; see `Environment.synthCache`. -/
+@[implemented_by setSynthCacheUnsafe]
+opaque _root_.Lean.Environment.setSynthCache (env : Environment) (c : SynthInstanceCache) : Environment
+
+/--
+Resets the persistent tier of the type class resolution cache. Use `resetSynthInstanceCache`
+instead from `MetaM`, which also clears the transient `Meta.Cache.synthInstance` tier;
+context-free entries are written to both tiers (see `Lean.Meta.SynthInstance.insertCachedResult`).
+-/
+def resetSynthInstanceCacheCore : CoreM Unit :=
+  modify fun s => { s with env := s.env.setSynthCacheRaw? none }
+
+/--
+Resets the type class resolution cache (both the persistent tier and the transient
+`Meta.Cache.synthInstance` tier).
+
+Calling this function is normally unnecessary: cache entries record the dependencies of their
+search (relevant options, instances, unification hints, reducibility statuses; see
+`Lean.Meta.SynthInstance`) and are automatically invalidated when a dependency changes,
+including through environment modifications the current `Meta.State` cannot observe (e.g.
+running a command via `liftCommandElabM`). Known remaining gaps that do require an explicit
+reset: deactivation of *scoped* unification hints (ending the surrounding scope or section),
+and dropping *local* unification hints at the end of a section, neither of which is covered by
+the cache key or the recorded dependencies.
+-/
+def resetSynthInstanceCache : MetaM Unit := do
+  resetSynthInstanceCacheCore
+  modifyCache fun c => { c with synthInstance := {} }
+
 private def mkInstanceKey (e : Expr) : MetaM (Array InstanceKey) := do
   let type ← inferType e
   withNewMCtxDepth do
@@ -353,24 +427,28 @@ builtin_initialize
       modifyEnv fun env => instanceExtension.modifyState env fun _ => s
   }
 
+-- `recorded := true` below: every resolution query records the instance-table generation once
+-- when it starts (`Lean.recordExtGenAccess` in `synthInstanceCore?`), which covers every
+-- read of the table during the query.
+
 def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry) :=
-  return Meta.instanceExtension.getState (← getEnv) |>.discrTree
+  return Meta.instanceExtension.getState (recorded := true) (← getEnv) |>.discrTree
 
 def getErasedInstances : CoreM (PHashSet Name) :=
-  return Meta.instanceExtension.getState (← getEnv) |>.erased
+  return Meta.instanceExtension.getState (recorded := true) (← getEnv) |>.erased
 
 def isInstanceCore (env : Environment) (declName : Name) : Bool :=
-  Meta.instanceExtension.getState env |>.instanceNames.contains declName
+  Meta.instanceExtension.getState (recorded := true) env |>.instanceNames.contains declName
 
 def isInstance (declName : Name) : CoreM Bool :=
   return isInstanceCore (← getEnv) declName
 
 def getInstancePriority? (declName : Name) : CoreM (Option Nat) := do
-  let some entry := Meta.instanceExtension.getState (← getEnv) |>.instanceNames.find? declName | return none
+  let some entry := Meta.instanceExtension.getState (recorded := true) (← getEnv) |>.instanceNames.find? declName | return none
   return entry.priority
 
 def getInstanceAttrKind? (declName : Name) : CoreM (Option AttributeKind) := do
-  let some entry := Meta.instanceExtension.getState (← getEnv) |>.instanceNames.find? declName | return none
+  let some entry := Meta.instanceExtension.getState (recorded := true) (← getEnv) |>.instanceNames.find? declName | return none
   return entry.attrKind
 
 /-! # Default instance support -/
diff --git a/src/Lean/Meta/Match/MatchEqsExt.lean b/src/Lean/Meta/Match/MatchEqsExt.lean
index 07d1f07a1611..9212ebec0028 100644
--- a/src/Lean/Meta/Match/MatchEqsExt.lean
+++ b/src/Lean/Meta/Match/MatchEqsExt.lean
@@ -30,15 +30,27 @@ structure MatchEqnsExtState where
 
 /- We generate the equations and splitter on demand, and do not save them on .olean files. -/
 builtin_initialize matchEqnsExt : EnvExtension MatchEqnsExtState ←
+  -- consulted during match-equation realization, which can happen inside a resolution search;
+  -- a mere name mapping for realized equation theorems (monotone)
   -- Using `local` allows us to use the extension in `realizeConst` without specifying `replay?`.
   -- The resulting state can still be accessed on the generated declarations using `.asyncEnv`;
-  -- see below
-  registerEnvExtension (pure {}) (asyncMode := .local)
+  -- see below. Covered: realized on demand, so reads never observe result-relevant absence,
+  -- and registered equations are write-stability-guarded.
+  registerEnvExtension (pure {}) (asyncMode := .local) (declCovered := true)
 
 def registerMatchEqns (matchDeclName : Name) (matchEqns : MatchEqns) : CoreM Unit := do
   modifyEnv fun env => matchEqnsExt.modifyState env fun { map, eqns } => {
     eqns := matchEqns.eqnNames.foldl (init := eqns) fun eqns eqn => eqns.insert eqn
-    map := map.insert matchDeclName matchEqns
+    -- write-stability guard; see `MapDeclarationExtension.insert`. Re-registration with the
+    -- same equations is idempotent.
+    map :=
+      match map.find? matchDeclName with
+      | some prev =>
+        if prev.eqnNames != matchEqns.eqnNames then
+          panic! s!"match equations for `{matchDeclName}` are already registered"
+        else
+          map
+      | none => map.insert matchDeclName matchEqns
   }
 
 /-
diff --git a/src/Lean/Meta/Match/MatchPatternAttr.lean b/src/Lean/Meta/Match/MatchPatternAttr.lean
index d7e0883c6a4a..e9d12ce671e1 100644
--- a/src/Lean/Meta/Match/MatchPatternAttr.lean
+++ b/src/Lean/Meta/Match/MatchPatternAttr.lean
@@ -32,7 +32,10 @@ def isYellow (color : String) : Bool :=
 -/
 @[builtin_doc]
 builtin_initialize matchPatternAttr : TagAttribute ←
-  registerTagAttribute `match_pattern "mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)"
+  -- consulted during resolution `isDefEq`; post-hoc tagging is treated as decl-time (the tag is
+  -- effectively part of the definition)
+  -- covered: declaration-keyed; post-hoc applications are recorded in the declaration change log
+  registerTagAttribute (declCovered := true) `match_pattern "mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)"
     (validate := fun declName => do
       withExporting (isExporting := !isPrivateName declName) do
         if !(← getConstInfo declName).isDefinition then
diff --git a/src/Lean/Meta/Match/MatcherInfo.lean b/src/Lean/Meta/Match/MatcherInfo.lean
index b1f76d269f21..be4268b16270 100644
--- a/src/Lean/Meta/Match/MatcherInfo.lean
+++ b/src/Lean/Meta/Match/MatcherInfo.lean
@@ -127,6 +127,8 @@ builtin_initialize extension : SimplePersistentEnvExtension Entry State ←
     addEntryFn    := State.addEntry
     addImportedFn := fun es => (mkStateFromImportedEntries State.addEntry {} es).switch
     asyncMode     := .async .mainEnv
+    -- covered: matcher facts are immutable per declaration and monotone
+    declCovered  := true
     exportEntriesFnEx? := some fun env _ entries =>
       let all := entries.toArray
       -- Do not export info for private defs at exported/server levels
diff --git a/src/Lean/Meta/MethodSpecs.lean b/src/Lean/Meta/MethodSpecs.lean
index b5a044e7073f..6702ea683237 100644
--- a/src/Lean/Meta/MethodSpecs.lean
+++ b/src/Lean/Meta/MethodSpecs.lean
@@ -112,12 +112,20 @@ overloaded `Cls.op` operation, and similarly `instClsT.op_spec_<n>` based on the
 `opImpl.eq_<n>`.
 -/
 @[builtin_doc]
-builtin_initialize methodSpecsAttr : ParametricAttribute MethodSpecsAttrData ←
-  registerParametricAttribute {
+builtin_initialize methodSpecsAttr : ParametricAttribute MethodSpecsAttrData ← do
+  let impl : ParametricAttributeImpl MethodSpecsAttrData := {
     name := `method_specs
     descr := "generate method specification theorems"
     getParam
   }
+  -- consulted (via the reserved-name machinery) when specification theorems are realized, which
+  -- can happen inside a resolution search; the attribute is applied when the method
+  -- implementation is declared (monotone)
+  -- covered: declaration-keyed, applied when the method implementation is declared
+  let ext ← registerParametricAttributeExt (α := MethodSpecsAttrData) impl.ref impl.preserveOrder
+    (declCovered := true)
+    impl.filterExport
+  registerParametricAttributeForExt impl ext
 
 builtin_initialize methodSpecsSimpExtension : SimpExtension ←
   registerSimpAttr `method_specs_simp
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 450d8edb60c6..041006db03c5 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -32,6 +32,11 @@ register_builtin_option backward.synthInstance.canonInstances : Bool := {
   descr := "use optimization that relies on 'morally canonical' instances during type class resolution"
 }
 
+register_builtin_option debug.synthInstance.checkCacheHits : Bool := {
+  defValue := false
+  descr := "differentially validate type class resolution cache hits: re-run every served query from scratch and panic if the recomputed result differs from the cached one, which means a dependency of the entry was not recorded (development soak check; roughly doubles resolution cost)"
+}
+
 namespace SynthInstance
 
 def getMaxHeartbeats (opts : Options) : Nat :=
@@ -598,7 +603,7 @@ def generate : SynthM Unit := do
     let mctx := gNode.mctx
     let mvar := gNode.mvar
     /- See comment at `typeHasMVars` -/
-    if backward.synthInstance.canonInstances.get (← getOptions) then
+    if (← getRecordedOption backward.synthInstance.canonInstances) then
       unless gNode.typeHasMVars do
         if let some entry := (← get).tableEntries[key]? then
           if entry.answers.any fun answer => answer.result.numMVars == 0 then
@@ -680,7 +685,9 @@ def main (type : Expr) (maxResultSize : Nat) : MetaM (Option AbstractMVarsResult
        newSubgoal (← getMCtx) key mvar Waiter.root
        synth
      tryCatchRuntimeEx
-       (action.run { maxResultSize := maxResultSize, maxHeartbeats := getMaxHeartbeats (← getOptions) } |>.run' {})
+       -- unrestricted acquisition: the limit is part of the resolution cache key
+       -- (`SynthInstanceCacheKey.limits`)
+       (action.run { maxResultSize, maxHeartbeats := getMaxHeartbeats (← getOptionsUnrestricted) } |>.run' {})
        fun ex =>
          if ex.isRuntime then
            throwError "failed to synthesize{indentExpr type}\n{ex.toMessageData}{useDiagnosticMsg}"
@@ -921,6 +928,118 @@ private def applyAbstractResult? (type : Expr) (abstResult? : Option AbstractMVa
   check result
   return some result
 
+/-- Returns whether every recorded lookup in `log` gives the same answer in `opts`. -/
+private def validOptionAccesses (opts : Options) (log : SynthOptionAccessLog) : Bool :=
+  log.all fun a => opts.find? a.name == a.value
+
+/--
+Merges the environment dependencies observed by a nested query (or served from a used cache
+entry) into the enclosing query's accumulator. The enclosing query keeps its own
+`changeLogPos` and `recordGen`: they were captured when that query started, and the merged
+dependencies are validated against them like the query's own observations.
+-/
+private def _root_.Lean.RecordedDeps.mergeInto (child parent : RecordedDeps) : RecordedDeps :=
+  let options := child.options.foldl (init := parent.options) fun l a =>
+    if l.any (·.name == a.name) then l else l.push a
+  let extGens := child.extGens.foldl (init := parent.extGens) fun l d =>
+    if l.any (·.1 == d.1) then l else l.push d
+  { parent with options, extGens }
+
+/--
+Identity of two dependency logs for entry replacement in `insertCachedResult`: same option
+answers and same dependency *shape* (same extensions and reducibility declarations observed).
+The observed generations and statuses are deliberately not part of the identity: a fresh
+observation with the same shape supersedes the old entry, whose generations can never recur.
+-/
+private def sameDepIdentity (a b : RecordedDeps) : Bool :=
+  a.options == b.options
+  && a.extGens.size == b.extGens.size
+  && a.extGens.all (fun d => b.extGens.any (·.1 == d.1))
+
+/--
+Inserts a result into the type class resolution cache: always into the transient
+`Meta.Cache.synthInstance` tier, which has the lifetime of the current `Meta.State`, and
+additionally into the persistent tier if `persist` is true.
+
+Only context-free entries may be persisted: the key must not contain metavariables and the result
+must be closed. Results with abstracted metavariables are only valid relative to the elaboration
+context that created them: their degrees of freedom (e.g. universe metavariables not determined
+by the key, cf. `Small`) are resolved by ambient constraints, so reusing them in a different
+context can produce incorrectly instantiated terms.
+
+A persistent insertion is rolled back together with the environment (see
+`Environment.synthCache`); the transient copy then still serves the entry for the rest of the
+command, as `Meta.SavedState.restore` deliberately does not restore `Meta.Cache`. Without it,
+backtracking-heavy elaboration (e.g. tactics trying alternatives) would re-run every failed
+attempt's typeclass queries from scratch.
+-/
+private def insertCachedResult (key : SynthInstanceCacheKey) (log : RecordedDeps)
+    (result? : Option AbstractMVarsResult) (persist : Bool) : MetaM Unit := do
+  -- One entry per observed dependency combination; replace an entry with the same identity.
+  let upsert (c : SynthInstanceCache) : SynthInstanceCache :=
+    c.insert key <| (log, result?) :: (c.find? key |>.getD [] |>.filter fun e => !sameDepIdentity e.1 log)
+  if persist then
+    -- Modify the environment directly instead of via `Meta.modifyEnv`, which would reset the
+    -- `Meta.Cache` caches.
+    modifyThe Core.State fun s =>
+      { s with env := s.env.setSynthCache (upsert s.env.synthCache) }
+  modifyCache fun c => { c with synthInstance := upsert c.synthInstance }
+
+/--
+Validates a cache entry's recorded dependencies against the current context. Returns `none` if
+any recorded answer has changed; otherwise the entry may be used, and the returned Boolean
+indicates the log was *re-stamped*: `Environment.recordGen` had moved, all recorded
+dependencies re-answered identically, and the log now carries the current stamps (including
+the reducibility log position and birth watermark, so each log segment is scanned at most once
+per entry). The caller re-inserts a re-stamped entry.
+
+The status re-asks may record into the armed query's accumulator, which is benign: it
+over-approximates the current query's dependencies.
+-/
+private def validateDeps? (opts : Options) (env : Environment)
+    (log : RecordedDeps) : BaseIO (Option (RecordedDeps × Bool)) := do
+  unless validOptionAccesses opts log.options do return none
+  -- Global short-circuit: while `Environment.recordGen` is unchanged, no recorded environment
+  -- dependency can have changed and the per-dependency checks are skipped.
+  if log.recordGen == env.recordGen then
+    return some (log, false)
+  for (idx, gen) in log.extGens do
+    unless (← EnvExtension.getRecordedGen env idx) == gen do return none
+  unless env.checkDeclChangeLog log.changeLogPos log.constBirthW do return none
+  return some ({ log with
+    recordGen := env.recordGen
+    changeLogPos := env.declChangeLog.size
+    constBirthW := env.constBirthGen }, true)
+
+/--
+Returns the type class resolution cache entry for `key` from the transient
+(`Meta.Cache.synthInstance`) or persistent (`Environment.synthCache`) tier, together with its
+recorded dependencies. Only entries whose recorded dependencies give the same answers in the
+current context are considered (`validateDeps?`); a re-stamped entry is re-inserted into its
+tier. See `SynthInstanceCache`.
+-/
+private def findCachedResult? (key : SynthInstanceCacheKey) :
+    MetaM (Option (RecordedDeps × Option AbstractMVarsResult)) := do
+  -- unrestricted acquisition: only compared against recorded lookups (`validOptionAccesses`)
+  let opts ← getOptionsUnrestricted
+  let env ← getEnv
+  let findIn (c : SynthInstanceCache) :
+      BaseIO (Option (RecordedDeps × Option AbstractMVarsResult × Bool)) := do
+    let some entries := c.find? key | return none
+    for (log, val?) in entries do
+      if let some (log, restamped) ← validateDeps? opts env log then
+        return some (log, val?, restamped)
+    return none
+  if let some (log, val?, restamped) ← findIn (← get).cache.synthInstance then
+    if restamped then
+      insertCachedResult key log val? (persist := false)
+    return some (log, val?)
+  if let some (log, val?, restamped) ← findIn env.synthCache then
+    if restamped then
+      insertCachedResult key log val? (persist := true)
+    return some (log, val?)
+  return none
+
 /--
 Auxiliary function for converting a cached `AbstractMVarsResult` returned by `SynthInstance.main` into an `Expr`.
 This function tries to avoid the potentially expensive `check` at `applyCachedAbstractResult?`.
@@ -940,42 +1059,348 @@ private def applyCachedAbstractResult? (type : Expr) (abstResult? : Option Abstr
     applyAbstractResult? type abstResult?
 
 /-- Helper function for caching synthesized type class instances. -/
-private def cacheResult (cacheKey : SynthInstanceCacheKey) (kind : PreprocessKind) (abstResult? : Option AbstractMVarsResult) (result? : Option Expr) : MetaM Unit := do
-  -- **TODO**: simplify this function.
-  match abstResult? with
-  | none => modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey none }
-  | some abstResult =>
-    if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty && kind matches .noMVars | .mvarsNoOutputParams then
-      match result? with
-      | none => modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey none }
-      | some result =>
-        -- See `applyCachedAbstractResult?` If new metavariables have **not** been introduced,
-        -- we don't need to perform extra checks again when reusing result.
-        modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some { expr := result, paramNames := #[], mvars := #[] }) }
-    else
-      modify fun s => { s with cache.synthInstance := s.cache.synthInstance.insert cacheKey (some abstResult) }
+private def cacheResult (cacheKey : SynthInstanceCacheKey) (log : RecordedDeps) (kind : PreprocessKind) (normalized : Bool) (abstResult? : Option AbstractMVarsResult) (result? : Option Expr) : MetaM Unit := do
+  -- The stored value: for a closed result we store the concrete `result` expr with an empty
+  -- `AbstractMVarsResult` so that `applyCachedAbstractResult?` can skip re-`check`ing it.
+  let value? :=
+    match abstResult? with
+    | none => none
+    | some abstResult =>
+      if abstResult.numMVars == 0 && abstResult.paramNames.isEmpty && kind matches .noMVars | .mvarsNoOutputParams then
+        result?.map fun result => { expr := result, paramNames := #[], mvars := #[] }
+      else
+        some abstResult
+  -- Only context-free entries may be persisted: a key without metavariables, a key that does not
+  -- depend on the identity of any free variable, and a closed value (no abstracted metavariables,
+  -- no free variables); see `insertCachedResult`.
+  --
+  -- The key is tested for metavariables directly rather than through `.noMVars`. An
+  -- `.mvarsOutputParams` query has its output parameters replaced by a wildcard in the key, so the
+  -- key is metavariable-free whenever every metavariable sits in an output parameter, even though
+  -- the query itself is not. Such an entry is as context-free as a `.noMVars` one: the wildcard
+  -- stands for a value the input parameters determine, and a hit re-derives it by unifying the
+  -- cached result against the query (`assignOutParams`).
+  --
+  -- A `normalized` key names its free variables by canonical position and records their types in
+  -- `normFVarTypes`, so it is context-free even though it mentions free variables. A raw key is
+  -- context-free only if it mentions none: an `FVarId` identifies a variable only within the
+  -- `NameGenerator` that created it, and the cache outlives any of them.
+  let persist := !cacheKey.type.hasMVar &&
+    (normalized || (cacheKey.localInsts.isEmpty && !cacheKey.type.hasFVar)) &&
+    (value?.all fun r => r.numMVars == 0 && r.paramNames.isEmpty && !r.expr.hasFVar)
+  insertCachedResult cacheKey log value? (persist := persist)
+
+/-!
+Free-variable normalization of the cache key and result. Two `.noMVars` queries that are
+structurally identical up to the identities of their free variables (e.g. `Foo α` under `[Foo α]`
+vs. `Foo β` under `[Foo β]`) are made to share a single cache entry: every free variable reachable
+from the query type and the local instances is renamed to a canonical positional identifier, and
+the result is stored over the same canonical variables and re-instantiated with the current
+context's free variables on a hit.
+
+This is sound because a hit means the normalized key components are `BEq`-equal, i.e. the two
+contexts are identical up to free-variable renaming, and the synthesized result only mentions free
+variables in that closure (the query's variables and the local instances). Queries that cannot be
+soundly normalized fall back to the raw (unnormalized) key: see `normalizeContext?`.
+-/
+namespace SynthNorm
+
+/-- Canonical positional free-variable identifier used in the normalized cache key. -/
+private def canonFVarId (i : Nat) : FVarId := ⟨.mkNum `_snf i⟩
+
+private structure State where
+  /-- Assigns each source free variable its canonical position. Persistent, so that a memoized
+  closure seeds a query's state in constant time. -/
+  fmap  : PersistentHashMap FVarId Nat := {}
+  /-- Canonical position to source free variable (inverse of `fmap`), for re-instantiation. -/
+  order : Array FVarId := #[]
+  /-- Canonical position to the (recursively normalized) type of that free variable. -/
+  types : Array Expr := #[]
+  /-- Canonical position to the normalized value of that free variable, if it is let-bound. -/
+  values : Array (Option Expr) := #[]
+  /-- Set when the closure cannot be soundly normalized (let-bound or mvar-typed variable). -/
+  bail  : Bool := false
+  /-- Closure variables whose raw `LocalDecl` type or let-value mentions a metavariable, with the
+  instantiation used; see `SynthNormClosureMemo.mvarTyped`. -/
+  mvarTyped : Array (FVarId × Bool × Expr) := #[]
+  /--
+  Memoizes `normExpr` on visited subterms so that terms with DAG sharing are traversed in DAG
+  size, not tree size. Sound because positions are assigned by first occurrence and never change:
+  revisiting a subterm yields the same normalization. Keyed structurally (`ExprStructEq` hashes
+  are cached and its equality short-circuits on pointer identity).
+  -/
+  cache : Std.HashMap ExprStructEq Expr := {}
+
+private abbrev M := ReaderT LocalContext (StateT State MetaM)
+
+/--
+Renames every free variable to a canonical positional identifier by first-occurrence order,
+recording and recursively normalizing each one's type, and its value if it is let-bound. Sets
+`bail` on a variable whose type or value contains an unassigned metavariable, which is not
+context-free and so cannot be soundly normalized.
+-/
+private partial def normExpr (e : Expr) : M Expr := do
+  if (← get).bail then return e
+  unless e.hasFVar do return e
+  match e with
+  | .fvar id =>
+    if let some i := (← get).fmap.find? id then
+      return .fvar (canonFVarId i)
+    -- `preprocess` puts this marker in output-parameter positions; it is a constant, not a
+    -- variable of the local context, and must not be renamed (nor bail the normalization).
+    if id.name == `__wild__ then return e
+    match (← read).find? id with
+    | none =>
+      modify fun s => { s with bail := true }
+      return e
+    | some decl =>
+      -- `Expr.hasMVar` is a syntactic flag: it stays set for metavariables that are already
+      -- assigned, whose values are context-free. Instantiate before deciding to bail. The result is
+      -- recorded even when we bail below: assigning the metavariable that made us bail must
+      -- invalidate the memoized closure.
+      let inst (isValue : Bool) (e : Expr) : M Expr := do
+        unless e.hasMVar do return e
+        let e ← instantiateMVars e
+        modify fun s => { s with mvarTyped := s.mvarTyped.push (id, isValue, e) }
+        return e
+      let type ← inst false decl.type
+      -- A nondependent `ldecl` (`have`) hides its value from definitional unfolding, so
+      -- `LocalDecl.value?` reports none and the value stays out of the key.
+      let value? ← match decl.value? with
+        | none   => pure none
+        | some v => do
+          let v ← inst true v
+          pure (some v)
+      if type.hasMVar || (match value? with | some v => v.hasMVar | none => false) then
+        modify fun s => { s with bail := true }
+        return e
+      let i := (← get).order.size
+      modify fun s =>
+        { s with fmap := s.fmap.insert id i, order := s.order.push id,
+                 types := s.types.push default, values := s.values.push none }
+      let nty ← normExpr type
+      let nval? ← match value? with
+        | none   => pure none
+        | some v => do
+          let v ← normExpr v
+          pure (some v)
+      modify fun s => { s with types := s.types.set! i nty, values := s.values.set! i nval? }
+      return .fvar (canonFVarId i)
+  | _ =>
+    if let some r := (← get).cache[(e : ExprStructEq)]? then
+      return r
+    let r ← match e with
+      | .app f a          => pure <| .app (← normExpr f) (← normExpr a)
+      | .lam n d b bi     => pure <| .lam n (← normExpr d) (← normExpr b) bi
+      | .forallE n d b bi => pure <| .forallE n (← normExpr d) (← normExpr b) bi
+      | .letE n t v b nd  => pure <| .letE n (← normExpr t) (← normExpr v) (← normExpr b) nd
+      | .mdata m b        => pure <| .mdata m (← normExpr b)
+      | .proj s i b       => pure <| .proj s i (← normExpr b)
+      | e                 => pure e
+    modify fun s => { s with cache := s.cache.insert e r }
+    return r
+
+/-- The free-variable-normalized cache context for a query; see `normalizeContext?`. -/
+structure Context where
+  normType        : Expr
+  canonLocalInsts : LocalInstances
+  fvarTypes       : Array Expr
+  fvarValues      : Array (Option Expr)
+  fmap            : PersistentHashMap FVarId Nat
+  order           : Array FVarId
+
+/--
+Whether a memoized closure is still valid: every closure variable whose type mentions a
+metavariable must still instantiate to what the closure was built from. The other closure
+variables have immutable types, and the local instances are compared by the caller.
+-/
+private def isValidMemo (lctx : LocalContext) (memo : SynthNormClosureMemo) : MetaM Bool := do
+  for (id, isValue, e) in memo.mvarTyped do
+    let some decl := lctx.find? id | return false
+    let some raw := (if isValue then decl.value? else some decl.type) | return false
+    unless (← instantiateMVars raw) == e do return false
+  return true
+
+/--
+The free-variable-normalized closure of the local instances, or `none` if it cannot be soundly
+normalized. Memoized in `Meta.Cache.synthNormClosure`: the closure is the same for every query made
+under the same local instances, and normalizing it per query dominates the cost of a cache key.
+-/
+private def getClosure? (localInsts : LocalInstances) : MetaM (Option SynthNormClosure) := do
+  let lctx ← getLCtx
+  let cache := (← get).cache
+  if let some memo := cache.synthNormClosure then
+    if memo.localInsts == localInsts && (← isValidMemo lctx memo) then
+      return memo.closure?
+  let go : M LocalInstances :=
+    localInsts.mapM fun li => return { li with fvar := ← normExpr li.fvar }
+  let (canonLocalInsts, st) ← go.run lctx |>.run {}
+  let closure? :=
+    if st.bail then none
+    else some { fmap := st.fmap, order := st.order, types := st.types, values := st.values,
+                canonLocalInsts }
+  modifyCache fun c =>
+    { c with synthNormClosure := some { localInsts, mvarTyped := st.mvarTyped, closure? } }
+  return closure?
+
+/--
+Computes the free-variable-normalized cache context for a `.noMVars` query, or `none` if it cannot
+be soundly normalized (some free variable in the closure has an unassigned metavariable in its type
+or value). The closure comprises the free variables of the local instances and of `cacheKeyType`,
+together with their types, transitively. The local instances are normalized first, so that their
+part of the closure does not depend on the query and can be memoized; see `getClosure?`.
+-/
+def normalizeContext? (cacheKeyType : Expr) (localInsts : LocalInstances) :
+    MetaM (Option Context) := do
+  let some closure ← getClosure? localInsts | return none
+  let lctx ← getLCtx
+  -- Seed from the memoized closure; the query type may extend it with further free variables.
+  let st0 : State := { fmap := closure.fmap, order := closure.order, types := closure.types,
+                       values := closure.values }
+  let (normType, st) ← (normExpr cacheKeyType).run lctx |>.run st0
+  if st.bail then return none
+  return some { normType, canonLocalInsts := closure.canonLocalInsts, fvarTypes := st.types,
+                fvarValues := st.values, fmap := st.fmap, order := st.order }
+
+/--
+Abstracts the closure free variables of `e` into loose bound variables (positional, by the closure
+`order`), or `none` if `e` mentions a free variable outside the closure (in which case the value is
+context-dependent beyond its key and must not be reused).
+
+The abstracted value contains no context-specific free variables, so it is safe to store in the
+shared cache and re-instantiate in a different context (cf. `reopen`), analogously to how
+`abstractMVars` produces a closed schema. `.noMVars` results have no abstracted metavariables, so
+`e` never wraps the value in metavariable binders and this abstraction composes with the universe
+handling in `openAbstractMVarsResult`.
+-/
+def abstractOverClosure? (ctx : Context) (e : Expr) : Option Expr :=
+  -- Abstract first, then check the (cached) `hasFVar` flag of the result: any remaining free
+  -- variable is outside the closure. Unlike `hasAnyFVar`, this is linear in the DAG size of `e`.
+  let e := e.abstract (ctx.order.map Expr.fvar)
+  if e.hasFVar then none else some e
+
+/-- Abstracts the free variables of a cache value, or `none` if the result escapes the closure. -/
+def abstractValue? (ctx : Context) (abstResult? : Option AbstractMVarsResult) (result? : Option Expr) :
+    Option (Option AbstractMVarsResult × Option Expr) := do
+  let abstResult? ← match abstResult? with
+    | none   => some none
+    | some a => (abstractOverClosure? ctx a.expr).map fun e => some { a with expr := e }
+  let result? ← match result? with
+    | none   => some none
+    | some r => (abstractOverClosure? ctx r).map some
+  some (abstResult?, result?)
+
+/--
+Re-instantiates a closure-abstracted value (see `abstractOverClosure?`) with the current context's
+closure free variables `order`.
+-/
+def reopen (order : Array FVarId) (e : Expr) : Expr :=
+  e.instantiateRev (order.map Expr.fvar)
+
+end SynthNorm
+
+/--
+The `Meta.Config` used for all type class resolution. The ambient configuration is replaced
+wholesale rather than adjusted: resolution results are cached across contexts and commands with no
+configuration component in the cache key, so any ambient configuration that influenced the search
+(e.g. `canUnfoldPredicateConfig` set by `simp`) would leak between contexts through the cache.
+Search-relevant state that must flow in from the caller is context, not configuration, and is part
+of the cache key (e.g. `synthPendingDepth`, the relevant options).
+-/
+private def synthInstanceConfig : Config :=
+  { isDefEqStuckEx := true, transparency := .instances,
+    foApprox := true, ctxApprox := true, constApprox := false, univApprox := false }
+
+/--
+Marks the query as recording on the environment (`Environment.isRecordingDeps`) without
+resetting `Meta.Cache` (which `Meta.modifyEnv` would).
+-/
+private def setRecordingDeps (recording : Bool) : MetaM Unit :=
+  modifyThe Core.State fun s => { s with env := s.env.setRecordingDeps recording }
 
 def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do
-  let opts ← getOptions
-  let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
+  -- For a nested query this read happens under the enclosing query's restriction and is recorded
+  -- as its dependency: the value determines the nested query's cache key.
+  let maxResultSize ← match maxResultSize? with
+    | some n => pure n
+    | none   => getRecordedOption synthInstance.maxSize
+  -- The query's dependencies: result-relevant option lookups on the search path go through the
+  -- recording accessors (`getRecordedOption`), and observed environment dependencies are
+  -- recorded directly; both flow into the accumulator `Core.State.recordedDeps`, which becomes
+  -- the cache entry's dependency log, see `SynthInstanceCache`. The enclosing query's
+  -- accumulator (if any) is saved here and the nested query's effective dependencies are
+  -- merged into it on exit (`finally` below): the enclosing query observed the result.
+  let parentDeps := (← getThe Core.State).recordedDeps
+  let parentRecording := (← readThe Core.Context).recordingDeps
+  let fresh : RecordedDeps :=
+    { recordGen := (← getEnv).recordGen
+      changeLogPos := (← getEnv).declChangeLog.size
+      constBirthW := (← getEnv).constBirthGen }
+  modifyThe Core.State fun s => { s with recordedDeps := fresh }
+  -- Both halves of the recording marker are armed here and must stay in lockstep: pure
+  -- extension reads can only see the one on the environment (`EnvExtension.trackGen`), while
+  -- everything reading through `CoreM` sees the scoped one, which needs no restoring.
+  setRecordingDeps true
+  try
+  withTheReader Core.Context (fun ctx => { ctx with recordingDeps := true }) do
+  -- Resolve the per-step definitional-equality flags once; they are part of the cache key
+  -- rather than recorded dependencies, so the raw reads are not logged. See `SynthDefEqFlags`.
+  -- Unrestricted acquisition: everything read below is part of the key.
+  let opts ← getOptionsUnrestricted
+  let getB (n : Name) (d : Bool) : Bool :=
+    ((opts.find? n).bind KVMap.Value.ofDataValue?).getD d
+  let flags : SynthDefEqFlags := {
+    respectTransparency      := getB `backward.isDefEq.respectTransparency true
+    respectTransparencyTypes := getB `backward.isDefEq.respectTransparency.types true
+    implicitBump             := getB `backward.isDefEq.implicitBump true
+    reducibleClassField      := getB `backward.whnf.reducibleClassField true
+    lazyProjDelta            := getB `backward.isDefEq.lazyProjDelta true
+    lazyWhnfCore             := getB `backward.isDefEq.lazyWhnfCore true
+    smartUnfolding           := getB `smartUnfolding true
+  }
+  -- Resource limits are part of the cache key (`SynthInstanceCacheKey.limits`): exceeding one
+  -- throws and results are only stored on the success path, so a limit cannot influence a
+  -- stored result, and keying by them makes that structural. Read by name because their
+  -- accessors live in modules this one does not import.
+  let getN (n : Name) (d : Nat) : Nat :=
+    ((opts.find? n).bind KVMap.Value.ofDataValue?).getD d
+  let limits : SynthLimits := {
+    maxHeartbeats           := getN `maxHeartbeats 200000
+    synthInstanceHeartbeats := getN `synthInstance.maxHeartbeats 20000
+    maxRecDepth             := getN `maxRecDepth 512
+    exponentiationThreshold := getN `exponentiation.threshold 256
+  }
+  withReader (fun ctx => { ctx with synthDefEqFlags? := some flags }) do
   withTraceNode `Meta.synthInstance
     (fun _ => return m!"{← instantiateMVars type}") do
-  withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
-                                          foApprox := true, ctxApprox := true, constApprox := false, univApprox := false }) do
+  withConfig (fun _ => synthInstanceConfig) do
   withInTypeClassResolution do
     let localInsts ← getLocalInstances
     let type ← instantiateMVars type
     let { type, cacheKeyType, kind } ← preprocess type
-    let cacheKey := { localInsts, type := cacheKeyType, synthPendingDepth := (← read).synthPendingDepth }
-    match (← get).cache.synthInstance.find? cacheKey with
-    | some abstResult? =>
-      trace[Meta.synthInstance.cache] "cached: {type}"
-      let result? ← applyCachedAbstractResult? type abstResult?
-      trace[Meta.synthInstance] "result {result?} (cached)"
-      return result?
-    | none =>
-      trace[Meta.synthInstance.cache] "new: {type}"
-      let abstResult? ← withNewMCtxDepth (allowLevelAssignments := true) do
+    -- Normalize the free variables of the key and result so that structurally identical queries in
+    -- different local contexts share a cache entry. Metavariables are left exactly as they are, so
+    -- this applies to metavariable-laden queries as well: their keys are otherwise context-specific
+    -- and can never be shared. `.mvarsOutputParams` keys have their output parameters replaced by a
+    -- wildcard already, so they are usually metavariable-free apart from it.
+    let normCtx? ← SynthNorm.normalizeContext? cacheKeyType localInsts
+    -- The instance-table generation is recorded once per query here, covering every read of
+    -- the table on the search path.
+    recordExtGenAccess instanceExtension.ext.toEnvExtension.idx
+    let insts := instanceExtension.getState (recorded := true) (← getEnv)
+    let cacheKey := { localInsts, type := cacheKeyType, synthPendingDepth := (← read).synthPendingDepth,
+                      activeScopedInsts := instanceExtension.getActiveScopesWithEntries (recorded := true) (← getEnv),
+                      localAttrInsts := insts.localInstanceNames,
+                      erasedInsts := if insts.erased.isEmpty then #[]
+                        else insts.erased.fold (init := #[]) (·.push ·) |>.qsort Name.quickLt,
+                      maxResultSize, defEqFlags := flags, limits,
+                      isExporting := (← getEnv).isExporting }
+    let rawKey := cacheKey
+    let cacheKey := match normCtx? with
+      | some c => { cacheKey with localInsts := c.canonLocalInsts, type := c.normType, normFVarTypes := c.fvarTypes, normFVarValues := c.fvarValues }
+      | none   => cacheKey
+    let runSearch : MetaM (Option AbstractMVarsResult) :=
+      withNewMCtxDepth (allowLevelAssignments := true) do
         match kind with
         | .noMVars =>
           /-
@@ -1000,12 +1425,108 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met
           SynthInstance.main (← preprocessOutParam type) maxResultSize
         | .mvarsNoOutputParams => SynthInstance.main type maxResultSize
         | .mvarsOutputParams => SynthInstance.main (← preprocessOutParam type) maxResultSize
+    -- Differential validation of a served hit (`debug.synthInstance.checkCacheHits`): recompute
+    -- the query from scratch and compare against the served result. The recompute bypasses the
+    -- entry under test by construction (the search body performs no cache lookup), and its
+    -- recorded dependencies flow into the current accumulator, which only strengthens the
+    -- entry's log. Raw `toString` is used for reporting: the pretty printer acquires the options,
+    -- which the recording marker diverts.
+    let checkHit (served? : Option AbstractMVarsResult) : MetaM Unit := do
+      -- deliberately unrestricted acquisition: purely diagnostic, cannot influence a cached result
+      unless debug.synthInstance.checkCacheHits.get (← getOptionsUnrestricted) do return
+      -- Fresh heartbeat budget: the recompute must not consume the query's own allowance. The
+      -- check is observation-only, so recompute exceptions are reported instead of propagated:
+      -- a search that throws where the cache had an answer is itself a divergence.
+      let fresh?? : Except String (Option AbstractMVarsResult) ←
+        try
+          .ok <$> withCurrHeartbeats runSearch
+        catch ex => do
+          let msg ← ex.toMessageData.toString
+          pure <| .error s!"exception: {msg}"
+      let pp : Option AbstractMVarsResult → String
+        | none => "none"
+        | some r => toString r.expr
+      let mismatch? : Option String := match fresh?? with
+        | .error e => some e
+        | .ok fresh? =>
+          let same := match served?, fresh? with
+            | none, none => true
+            | some a, some b => a.numMVars == b.numMVars && a.paramNames == b.paramNames && a.expr == b.expr
+            | _, _ => false
+          if same then none else some (pp fresh?)
+      if let some fresh := mismatch? then
+        -- the panic is the branch result: an unused pure binding would be dead-code-eliminated
+        panic! s!"type class resolution cache hit differs from recomputation for\n  \
+          {toString type}\ncached: {pp served?}\nrecomputed: {fresh}\n\
+          an environment dependency of the served entry was not recorded; see \
+          `Lean.EnvExtension.trackGen`"
+    -- Raw-key front-cache: repeated queries in one context must return the *same* result object.
+    -- A normalized hit re-instantiates the stored schema (`SynthNorm.reopen`), which allocates a
+    -- fresh copy per hit; consumers that rely on pointer identity for sharing (e.g. `grind`'s
+    -- alpha-sharing) would pay deep structural work for every copy. The transient tier therefore
+    -- additionally memoizes the reopened result under the unnormalized key, with the query's
+    -- effective option dependencies.
+    let insertRawKey (abstResult? : Option AbstractMVarsResult) : MetaM Unit := do
+      let log : RecordedDeps := (← getThe Core.State).recordedDeps
+      modifyCache fun c => { c with synthInstance := c.synthInstance.insert rawKey <|
+        (log, abstResult?) :: (c.synthInstance.find? rawKey |>.getD [] |>.filter fun e => !sameDepIdentity e.1 log) }
+    if normCtx?.isSome then
+      if let some entries := (← get).cache.synthInstance.find? rawKey then
+        let env ← getEnv
+        for (entryLog, abstResult?) in entries do
+          -- Front-cache entries are transient (per command), so serving skips the re-stamp.
+          if let some (entryLog, _) ← validateDeps? opts env entryLog then
+            trace[Meta.synthInstance.cache] "cached: {type}"
+            -- The used entry's dependencies become dependencies of this query.
+            Core.modifyRecordedDeps entryLog.mergeInto
+            checkHit abstResult?
+            let result? ← applyCachedAbstractResult? type abstResult?
+            trace[Meta.synthInstance] "result {result?} (cached)"
+            return result?
+    match ← findCachedResult? cacheKey with
+    | some (entryLog, abstResult?) =>
+      trace[Meta.synthInstance.cache] "cached: {type}"
+      -- The used entry's dependencies become dependencies of this query.
+      Core.modifyRecordedDeps entryLog.mergeInto
+      -- Re-instantiate the closure-abstracted result with the current context's free variables.
+      let abstResult? := match normCtx? with
+        | some c => abstResult?.map fun a => { a with expr := SynthNorm.reopen c.order a.expr }
+        | none   => abstResult?
+      if normCtx?.isSome then
+        insertRawKey abstResult?
+      checkHit abstResult?
+      let result? ← applyCachedAbstractResult? type abstResult?
+      trace[Meta.synthInstance] "result {result?} (cached)"
+      return result?
+    | none =>
+      trace[Meta.synthInstance.cache] "new: {type}"
+      let abstResult? ← runSearch
       let result? ← applyAbstractResult? type abstResult?
       trace[Meta.synthInstance] "result {result?}"
-      cacheResult cacheKey kind abstResult? result?
+      let log : RecordedDeps := (← getThe Core.State).recordedDeps
+      match normCtx? with
+      | none   => cacheResult cacheKey log kind (normalized := false) abstResult? result?
+      | some c =>
+        -- The context-level result goes under the raw key (see the front-cache above), including
+        -- when the abstraction below fails: an escaping result is still valid in this context.
+        insertRawKey abstResult?
+        -- Store the result over the canonical closure variables; skip caching (this query only) if
+        -- the result escapes the closure and so is not context-free.
+        match SynthNorm.abstractValue? c abstResult? result? with
+        | some (nAbstResult?, nResult?) => cacheResult cacheKey log kind (normalized := true) nAbstResult? nResult?
+        | none => pure ()
       return result?
-
-def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) (decl := type.getAppFn.constName?.getD .anonymous) do
+  finally
+    -- Restore the enclosing accumulator, merging this query's effective dependencies into it.
+    -- The environment half of the marker is state, so unlike the scoped half it is restored here.
+    let childDeps := (← getThe Core.State).recordedDeps
+    setRecordingDeps parentRecording
+    modifyThe Core.State fun s => { s with recordedDeps :=
+      if parentRecording then childDeps.mergeInto parentDeps else parentDeps }
+
+def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do
+  -- unrestricted acquisition: profiler collection cannot influence a cached resolution result
+  profileitM Exception "typeclass inference" (← getOptionsUnrestricted) (decl := type.getAppFn.constName?.getD .anonymous) do
   synthInstanceCore? type maxResultSize?
 
 /--
@@ -1041,7 +1562,7 @@ private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <|
     | none   =>
       return false
     | some _ =>
-      let max := maxSynthPendingDepth.get (← getOptions)
+      let max ← getRecordedOption maxSynthPendingDepth
       if (← read).synthPendingDepth > max then
         trace[Meta.synthPending] "too many nested synthPending invocations"
         recordSynthPendingFailure mvarDecl.type
diff --git a/src/Lean/Meta/UnificationHint.lean b/src/Lean/Meta/UnificationHint.lean
index b4a6bbf8add0..f0150ac4e4b7 100644
--- a/src/Lean/Meta/UnificationHint.lean
+++ b/src/Lean/Meta/UnificationHint.lean
@@ -38,6 +38,10 @@ builtin_initialize unificationHintExtension : SimpleScopedEnvExtension Unificati
   registerSimpleScopedEnvExtension {
     addEntry := UnificationHints.add
     initial  := {}
+    -- adding a hint bumps the generation, invalidating resolution cache entries that consulted
+    -- the hints; unlike reducibility there is no declaration-time exemption, as a new hint
+    -- applies to pre-existing terms
+    trackGen := true
   }
 
 structure UnificationConstraint where
@@ -102,7 +106,8 @@ def tryUnificationHints (t s : Expr) : MetaM Bool := do
     return false
   if t.isMVar then
     return false
-  let hints := unificationHintExtension.getState (← getEnv)
+  recordExtGenAccess unificationHintExtension.ext.toEnvExtension.idx
+  let hints := unificationHintExtension.getState (recorded := true) (← getEnv)
   let candidates ← withConfigWithKey config <| hints.discrTree.getMatch t
   for candidate in candidates do
     if (← tryCandidate candidate) then
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 059e41e77244..bd4c88d82703 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -822,7 +822,7 @@ private def unfoldDefault (fInfo : ConstantInfo) (us : List Level) (e : Expr) :
   if fInfo.hasValue then
     recordUnfold fInfo.name
     deltaBetaDefinition fInfo us e.getAppRevArgs (fun _ => pure none) fun e => do
-      if !backward.whnf.reducibleClassField.get (← getOptions) then
+      if !(← getSynthDefEqFlag (·.reducibleClassField) (backward.whnf.reducibleClassField.get ·)) then
         return some e
       else if !(← getTransparency) matches .reducible then
         return some e
@@ -850,7 +850,7 @@ mutual
         else
           let unfoldDefault (_ : Unit) : MetaM (Option Expr) :=
             unfoldDefault fInfo fLvls e
-          if smartUnfolding.get (← getOptions) then
+          if (← getSynthDefEqFlag (·.smartUnfolding) (smartUnfolding.get ·)) then
             match ((← getEnv).find? (skipRealize := true) (mkSmartUnfoldingNameFor fInfo.name)) with
             | some fAuxInfo@(.defnInfo _) =>
               -- We use `preserveMData := true` to make sure the smart unfolding annotation are not erased in an over-application.
@@ -915,7 +915,7 @@ mutual
       let some cinfo ← getConstInfoNoEx? declName ignoreTransparency | pure none
       -- check smart unfolding only after `getUnfoldableConstNoEx?` because smart unfoldings have a
       -- significant chance of not existing and `Environment.contains` misses are more costly
-      if smartUnfolding.get (← getOptions) && (← getEnv).contains (mkSmartUnfoldingNameFor declName) then
+      if (← getSynthDefEqFlag (·.smartUnfolding) (smartUnfolding.get ·)) && (← getEnv).contains (mkSmartUnfoldingNameFor declName) then
         return none
       else
         unless cinfo.hasValue do
diff --git a/src/Lean/ProjFns.lean b/src/Lean/ProjFns.lean
index f58c99d0dec0..39d7b7895bbb 100644
--- a/src/Lean/ProjFns.lean
+++ b/src/Lean/ProjFns.lean
@@ -27,7 +27,9 @@ structure ProjectionFunctionInfo where
   fromClass : Bool
   deriving Inhabited, Repr
 
-builtin_initialize projectionFnInfoExt : MapDeclarationExtension ProjectionFunctionInfo ← mkMapDeclarationExtension
+builtin_initialize projectionFnInfoExt : MapDeclarationExtension ProjectionFunctionInfo ←
+  -- covered: projection facts are immutable per declaration and monotone
+  mkMapDeclarationExtension (declCovered := true)
 
 def addProjectionFnInfo (env : Environment) (projName : Name) (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : Environment :=
   projectionFnInfoExt.insert env projName { ctorName, numParams, i, fromClass }
@@ -70,7 +72,9 @@ structure AuxParentProjectionInfo where
   fromClass : Bool
   deriving Inhabited, Repr
 
-builtin_initialize auxParentProjInfoExt : MapDeclarationExtension AuxParentProjectionInfo ← mkMapDeclarationExtension
+builtin_initialize auxParentProjInfoExt : MapDeclarationExtension AuxParentProjectionInfo ←
+  -- covered: parent-projection facts are immutable per declaration and monotone
+  mkMapDeclarationExtension (declCovered := true)
 
 def addAuxParentProjectionInfo (env : Environment) (projName : Name) (numParams : Nat) (fromClass : Bool) : Environment :=
   auxParentProjInfoExt.insert env projName { numParams, fromClass }
diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean
index d32f8582486f..73e5839d6b9e 100644
--- a/src/Lean/ReducibilityAttrs.lean
+++ b/src/Lean/ReducibilityAttrs.lean
@@ -51,6 +51,9 @@ def ReducibilityStatus.toAttrString : ReducibilityStatus → String
 builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × ReducibilityStatus) (Name × ReducibilityStatus) (NameMap ReducibilityStatus) ←
   registerPersistentEnvExtension {
     name            := `reducibilityCore
+    -- covered: status changes about observable declarations are recorded in the declaration
+    -- change log and validated by birth arithmetic (see `Environment.declChangeLog`)
+    declCovered    := true
     mkInitial       := pure {}
     addImportedFn   := fun _ _ => pure {}
     addEntryFn      := fun (s : NameMap ReducibilityStatus) (p : Name × ReducibilityStatus) => s.insert p.1 p.2
@@ -71,6 +74,8 @@ builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × Reducib
 builtin_initialize reducibilityExtraExt : SimpleScopedEnvExtension (Name × ReducibilityStatus) (SMap Name ReducibilityStatus) ←
   registerSimpleScopedEnvExtension {
     name := `reducibilityExtra
+    -- covered: as for `reducibilityCoreExt` above
+    declCovered := true
     initial := {}
     addEntry := fun d (declName, status) => d.insert declName status
     finalizeImport := fun d => d.switch
@@ -101,22 +106,14 @@ private def setReducibilityStatusCore (env : Environment) (declName : Name) (sta
     reducibilityExtraExt.addCore env (declName, status) attrKind currNamespace
 
 /-
-TODO: it would be great if we could distinguish between the following two situations
-
-1-
-```
-@[reducible] def foo := ...
-```
-
-2-
-```
-def foo := ...
-...
-attribute [reducible] foo
-```
-
-Reason: the second one is problematic if user has add simp theorems or TC instances that include `foo`.
-Recall that the discrimination trees unfold `[reducible]` declarations while indexing new entries.
+The type class resolution cache distinguishes the following two situations by birth arithmetic
+(`Environment.declChangeLog`): an attribute that is part of `foo`'s own elaboration
+(`@[reducible] def foo := ...`) is skipped during validation, while a post-hoc
+`attribute [reducible] foo` invalidates the entries that could have observed the old status.
+
+TODO: the distinction is not yet surfaced to other consumers: discrimination trees unfold
+`[reducible]` declarations while indexing new entries, so a post-hoc change can invalidate
+already-indexed simp theorems or TC instances mentioning `foo`; see `validate` below.
 -/
 
 register_builtin_option allowUnsafeReducibility : Bool := {
@@ -182,6 +179,9 @@ private def addAttr (status : ReducibilityStatus) (declName : Name) (stx : Synta
   validate declName status attrKind
   let ns ← getCurrNamespace
   modifyEnv fun env => setReducibilityStatusCore env declName status attrKind ns
+  -- Reducibility determines what `isDefEq` may unfold, so a status change some recording
+  -- query could have observed must be recorded; see `Environment.declChangeLog`.
+  modifyEnv fun env => env.logDeclChange declName
 
 builtin_initialize
   registerBuiltinAttribute {
@@ -256,7 +256,13 @@ builtin_initialize
 def getReducibilityStatus [Monad m] [MonadEnv m] (declName : Name) : m ReducibilityStatus := do
   return getReducibilityStatusCore (← getEnv) declName
 
-/-- Set the reducibility attribute for the given declaration. -/
+/--
+Set the reducibility attribute for the given declaration.
+
+Note: does not bump the reducibility change counter (`reducibilityChangedExt`). Use only for
+declarations created by the caller itself (before other code can have cached results about
+them); status changes to pre-existing declarations must go through the reducibility attributes.
+-/
 def setReducibilityStatus [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit :=
   modifyEnv fun env => setReducibilityStatusCore env declName s .global .anonymous
 
diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index b687cc6b3cb7..d101461cd986 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -43,7 +43,9 @@ def registerReservedNamePredicate (p : Environment → Name → Bool) : IO Unit
   reservedNamePredicatesRef.modify fun ps => ps.push p
 
 builtin_initialize reservedNamePredicatesExt : EnvExtension (Array (Environment → Name → Bool)) ←
-  registerEnvExtension reservedNamePredicatesRef.get
+  -- covered: consulted by `Environment.find?` (via `isReservedName`), so also on resolution
+  -- search paths; the predicate set is fixed at initialization
+  registerEnvExtension reservedNamePredicatesRef.get (declCovered := true)
 
 /--
 Returns `true` if `name` is a reserved name.
diff --git a/src/Lean/ScopedEnvExtension.lean b/src/Lean/ScopedEnvExtension.lean
index 69a91dfc305b..0704b401aa94 100644
--- a/src/Lean/ScopedEnvExtension.lean
+++ b/src/Lean/ScopedEnvExtension.lean
@@ -40,6 +40,10 @@ structure Descr (α : Type) (β : Type) (σ : Type) where
   addEntry       : σ → β → σ
   finalizeImport : σ → σ := id
   exportEntry?   : Environment → α → OLeanEntries (Option α) := fun _ a => .uniform (some a)
+  /-- See `EnvExtension.trackGen`. -/
+  trackGen : Bool := false
+  /-- See `EnvExtension.trackGen`. -/
+  declCovered : Bool := false
 
 instance [Inhabited α] : Inhabited (Descr α β σ) where
   default := {
@@ -135,6 +139,8 @@ unsafe def registerScopedEnvExtensionUnsafe (descr : Descr α β σ) : IO (Scope
     -- `AsyncMode.local` below). Allowing the latter is important for tactics such as -- `classical`
     -- or `open in`.
     asyncMode       := .mainOnly
+    trackGen := descr.trackGen
+    declCovered := descr.declCovered
   }
   let ext := { descr := descr, ext := ext : ScopedEnvExtension α β σ }
   scopedEnvExtensionsRef.modify fun exts => exts.push (unsafeCast ext)
@@ -143,14 +149,22 @@ unsafe def registerScopedEnvExtensionUnsafe (descr : Descr α β σ) : IO (Scope
 @[implemented_by registerScopedEnvExtensionUnsafe]
 opaque registerScopedEnvExtension (descr : Descr α β σ) : IO (ScopedEnvExtension α β σ)
 
+/-
+The scope-stack operations (`pushScope`/`popScope`/`setDelimitsLocal`/`activateScoped`) preserve
+the generation of `.recorded` extensions (`keepRecordGen`): for the type class resolution cache,
+scope activation state is part of the cache key (`SynthInstanceCacheKey.activeScopedInsts`),
+and entries computed with local entries in scope are keyed or documented as requiring an
+explicit reset (see `Lean.Meta.resetSynthInstanceCache`). Content changes (`addEntry` and
+friends) bump the generation as usual.
+-/
 def ScopedEnvExtension.pushScope (ext : ScopedEnvExtension α β σ) (env : Environment) : Environment :=
-  ext.ext.modifyState (asyncMode := .local) env fun s =>
+  ext.ext.modifyState (asyncMode := .local) (keepRecordGen := true) env fun s =>
     match s.stateStack with
     | [] => s
     | state :: stack => { s with stateStack := { state with delimitsLocal := true } :: state :: stack }
 
 def ScopedEnvExtension.popScope (ext : ScopedEnvExtension α β σ) (env : Environment) : Environment :=
-  ext.ext.modifyState (asyncMode := .local) env fun s =>
+  ext.ext.modifyState (asyncMode := .local) (keepRecordGen := true) env fun s =>
     match s.stateStack with
     | _      :: state₂ :: stack => { s with stateStack := state₂ :: stack }
     | _ => s
@@ -160,7 +174,7 @@ to turn off delimiting of local entries across multiple implicit scope levels
 (e.g. those introduced by compound `namespace A.B.C` expansions).
 -/
 def ScopedEnvExtension.setDelimitsLocal (ext : ScopedEnvExtension α β σ) (env : Environment) (depth : Nat) : Environment :=
-  ext.ext.modifyState (asyncMode := .local) env fun s =>
+  ext.ext.modifyState (asyncMode := .local) (keepRecordGen := true) env fun s =>
     {s with stateStack := go depth s.stateStack}
 where
   go : Nat → List (State σ) → List (State σ)
@@ -203,13 +217,28 @@ def ScopedEnvExtension.add [Monad m] [MonadResolveName m] [MonadEnv m] (ext : Sc
   modifyEnv (ext.addCore · b kind ns)
 
 def ScopedEnvExtension.getState [Inhabited σ] (ext : ScopedEnvExtension α β σ)
-    (env : Environment) (asyncMode := ext.ext.toEnvExtension.asyncMode) : σ :=
-  match ext.ext.getState (asyncMode := asyncMode) env |>.stateStack with
+    (env : Environment) (asyncMode := ext.ext.toEnvExtension.asyncMode)
+    (recorded := false) : σ :=
+  match ext.ext.getState (asyncMode := asyncMode) (recorded := recorded) env |>.stateStack with
   | top :: _ => top.state
   | _        => unreachable!
 
+/--
+Returns the active scopes of `ext` that have scoped entries, in a canonical order. Activated
+namespaces without scoped entries for this extension are omitted, so the result only changes when
+the set of activated scoped entries may have changed.
+-/
+def ScopedEnvExtension.getActiveScopesWithEntries (ext : ScopedEnvExtension α β σ)
+    (env : Environment) (asyncMode := ext.ext.toEnvExtension.asyncMode)
+    (recorded := false) : Array Name :=
+  let s := ext.ext.getState (asyncMode := asyncMode) (recorded := recorded) env
+  match s.stateStack with
+  | top :: _ => top.activeScopes.foldl (init := #[]) fun acc ns =>
+      if s.scopedEntries.map.contains ns then acc.push ns else acc
+  | _ => #[]
+
 def ScopedEnvExtension.activateScoped (ext : ScopedEnvExtension α β σ) (env : Environment) (namespaceName : Name) : Environment :=
-  ext.ext.modifyState (asyncMode := .local) env fun s =>
+  ext.ext.modifyState (asyncMode := .local) (keepRecordGen := true) env fun s =>
     match s.stateStack with
     | top :: stack =>
       if top.activeScopes.contains namespaceName then
@@ -261,6 +290,10 @@ structure SimpleScopedEnvExtension.Descr (α : Type) (σ : Type) where
   initial        : σ
   finalizeImport : σ → σ := id
   exportEntry?   : Environment → α → OLeanEntries (Option α) := fun _ a => .uniform (some a)
+  /-- See `EnvExtension.trackGen`. -/
+  trackGen : Bool := false
+  /-- See `EnvExtension.trackGen`. -/
+  declCovered : Bool := false
 
 def registerSimpleScopedEnvExtension (descr : SimpleScopedEnvExtension.Descr α σ) : IO (SimpleScopedEnvExtension α σ) := do
   registerScopedEnvExtension {
@@ -271,6 +304,8 @@ def registerSimpleScopedEnvExtension (descr : SimpleScopedEnvExtension.Descr α
     ofOLeanEntry   := fun _ a => return a
     finalizeImport := descr.finalizeImport
     exportEntry?   := descr.exportEntry?
+    trackGen := descr.trackGen
+    declCovered := descr.declCovered
   }
 
 end Lean
diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean
index 77e580c4e57b..066d85c80660 100644
--- a/src/Lean/Structure.lean
+++ b/src/Lean/Structure.lean
@@ -85,6 +85,9 @@ private structure StructureState where
   deriving Inhabited
 
 private builtin_initialize structureExt : PersistentEnvExtension StructureInfo StructureInfo (Unit × StructureState) ← registerPersistentEnvExtension {
+  -- covered: structure facts are immutable per declaration (the sanctioned `parentInfo` update
+  -- in `setStructureParents` is recorded in the declaration change log)
+  declCovered    := true
   mkInitial       := pure ((), {})
   addImportedFn   := fun _ => pure ((), {})
   addEntryFn      := fun (_, s) e => ((), { s with map := s.map.insert e.structName e })
@@ -107,11 +110,17 @@ Every structure created by `structure` or `class` has such an entry.
 This should be followed up with `setStructureParents` and `setStructureResolutionOrder`.
 -/
 def registerStructure (env : Environment) (e : StructureDescr) : Environment :=
-  structureExt.addEntry env {
-    structName := e.structName
-    fieldNames := e.fields.map fun e => e.fieldName
-    fieldInfo  := e.fields.qsort StructureFieldInfo.lt
-  }
+  have : Inhabited Environment := ⟨env⟩
+  -- Write-once guard; see `MapDeclarationExtension.insert`. The one sanctioned update is
+  -- `setStructureParents` below.
+  if structureExt.getState env |>.snd.map.contains e.structName then
+    panic! s!"structure `{e.structName}` is already registered"
+  else
+    structureExt.addEntry env {
+      structName := e.structName
+      fieldNames := e.fields.map fun e => e.fieldName
+      fieldInfo  := e.fields.qsort StructureFieldInfo.lt
+    }
 
 /--
 Sets parent projection info for a structure defined in the current module.
@@ -120,7 +129,11 @@ Throws an error if the structure has not already been registered with `Lean.regi
 def setStructureParents [Monad m] [MonadEnv m] [MonadError m] (structName : Name) (parentInfo : Array StructureParentInfo) : m Unit := do
   let some info := structureExt.getState (← getEnv) |>.snd.map.find? structName
     | throwError "cannot set structure parents for `{structName}`, structure not defined in current module"
-  modifyEnv fun env => structureExt.addEntry env { info with parentInfo }
+  -- Sanctioned second write to the structure's entry: `parentInfo` is filled in after
+  -- `registerStructure`, once the parent projections exist. The change is recorded in the
+  -- declaration change log, so entries armed in between (e.g. from default-value elaboration)
+  -- are invalidated by birth arithmetic; see `Environment.declChangeLog`.
+  modifyEnv fun env => structureExt.addEntry (env.logDeclChange structName) { info with parentInfo }
 
 /-- Gets the `StructureInfo` if `structName` has been declared as a structure to the elaborator. -/
 def getStructureInfo? (env : Environment) (structName : Name) : Option StructureInfo :=
@@ -419,7 +432,8 @@ We use an environment extension to cache resolution orders.
 These are not expensive to compute, but worth caching, and we save olean storage space.
 -/
 builtin_initialize structureResolutionExt : EnvExtension StructureResolutionState ←
-  registerEnvExtension (pure {}) (asyncMode := .local)  -- mere cache
+  -- covered: mere cache of a pure computation over covered inputs
+  registerEnvExtension (pure {}) (asyncMode := .local) (declCovered := true)
 
 /-- Gets the resolution order if it has already been cached. -/
 private def getStructureResolutionOrder? (env : Environment) (structName : Name) : Option (Array Name) :=
diff --git a/src/Lean/Util/PPExt.lean b/src/Lean/Util/PPExt.lean
index 51fe5793e2c1..50cf529ac06b 100644
--- a/src/Lean/Util/PPExt.lean
+++ b/src/Lean/Util/PPExt.lean
@@ -64,9 +64,19 @@ builtin_initialize ppFnsRef : IO.Ref PPFns ←
   }
 
 builtin_initialize ppExt : EnvExtension PPFns ←
-  registerEnvExtension ppFnsRef.get
+  registerEnvExtension ppFnsRef.get (name := `pp)
+
+/--
+Pretty printing is a legitimate consumer of arbitrary extension state even when its context was
+captured inside a region with restricted extension access (e.g. a trace message constructed
+during type class resolution): rendering happens outside the restricted computation and cannot
+contaminate its caches. Lift the restriction from the captured environment.
+-/
+private def PPContext.unrestricted (ctx : PPContext) : PPContext :=
+  { ctx with env := ctx.env.setRecordingDeps false }
 
 def ppExprWithInfos (ctx : PPContext) (e : Expr) : BaseIO FormatWithInfos := do
+  let ctx := ctx.unrestricted
   if pp.raw.get ctx.opts then
     let e := instantiateMVarsCore ctx.mctx e |>.1
     return format (toString e)
@@ -80,6 +90,7 @@ def ppExprWithInfos (ctx : PPContext) (e : Expr) : BaseIO FormatWithInfos := do
         pure f!"failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)"
 
 def ppConstNameWithInfos (ctx : PPContext) (n : Name) : BaseIO FormatWithInfos := do
+  let ctx := ctx.unrestricted
   match (← ppExt.getState ctx.env |>.ppConstNameWithInfos ctx n |>.toBaseIO) with
   | .ok fmt => return fmt
   | .error ex =>
@@ -89,6 +100,7 @@ def ppConstNameWithInfos (ctx : PPContext) (n : Name) : BaseIO FormatWithInfos :
       pure f!"failed to pretty print constant (use 'set_option pp.rawOnError true' for raw representation)"
 
 def ppTerm (ctx : PPContext) (stx : Term) : BaseIO Format := do
+  let ctx := ctx.unrestricted
   if pp.raw.get ctx.opts then
     return formatRawTerm ctx stx
   else
@@ -101,6 +113,7 @@ def ppTerm (ctx : PPContext) (stx : Term) : BaseIO Format := do
         pure f!"failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)"
 
 def ppLevel (ctx : PPContext) (l : Level) : BaseIO Format := do
+  let ctx := ctx.unrestricted
   match (← ppExt.getState ctx.env |>.ppLevel ctx l |>.toBaseIO) with
   | .ok fmt => return fmt
   | .error ex =>
@@ -110,6 +123,7 @@ def ppLevel (ctx : PPContext) (l : Level) : BaseIO Format := do
       pure f!"failed to pretty print level (use 'set_option pp.rawOnError true' for raw representation)"
 
 def ppGoal (ctx : PPContext) (mvarId : MVarId) : BaseIO Format := do
+  let ctx := ctx.unrestricted
   match (← ppExt.getState ctx.env |>.ppGoal ctx mvarId |>.toBaseIO) with
   | .ok fmt => return fmt
   | .error ex =>
diff --git a/src/Lean/Util/SafeExponentiation.lean b/src/Lean/Util/SafeExponentiation.lean
index 476983a5900b..fa5bdc21b747 100644
--- a/src/Lean/Util/SafeExponentiation.lean
+++ b/src/Lean/Util/SafeExponentiation.lean
@@ -27,7 +27,9 @@ reports a warning and returns `false`.
 This method ensures there is at most one warning message of this kind in the message log.
 -/
 def checkExponent (n : Nat) (warning := true) : CoreM Bool := do
-  let threshold := exponentiation.threshold.get (← getOptions)
+  -- unrestricted acquisition: the threshold is part of the resolution cache key
+  -- (`Lean.Meta.SynthInstanceCacheKey.limits`)
+  let threshold := exponentiation.threshold.get (← getOptionsUnrestricted)
   if n > threshold then
     if (← pure warning <&&> logMessageKind `unsafe.exponentiation) then
       logWarning s!"exponent {n} exceeds the threshold {threshold}, exponentiation operation was not evaluated, use `set_option {exponentiation.threshold.name} <num>` to set a new threshold"
diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean
index 4d441f69db37..837bad02ca76 100644
--- a/src/Lean/Util/Trace.lean
+++ b/src/Lean/Util/Trace.lean
@@ -106,7 +106,7 @@ def resetTraceState : m Unit :=
   opts.hasTrace && go (`trace ++ cls)
 where
   go (opt : Name) : Bool :=
-    if let some enabled := opts.get? opt then
+    if let some enabled := (opts.find? opt).bind KVMap.Value.ofDataValue? then
       enabled
     else if let .str parent _ := opt then
       inherited.contains opt && go parent
@@ -116,7 +116,8 @@ where
 /-- Determine if tracing is available for a given class, checking ancestor classes if appropriate. -/
 @[inline]
 def isTracingEnabledFor (cls : Name) : m Bool := do
-  return checkTraceOption (← MonadTrace.getInheritedTraceOptions) (← getOptions) cls
+  -- unrestricted acquisition: trace collection cannot influence a cached resolution result
+  return checkTraceOption (← MonadTrace.getInheritedTraceOptions) (← getOptionsUnrestricted) cls
 
 @[export lean_is_trace_class_enabled]
 private def isTracingEnabledForExport (opts : Options) (cls : Name) : BaseIO Bool := do
@@ -211,7 +212,7 @@ True if the `trace.profiler` data should be retained for export - either to a fi
 that would otherwise consume the trace state as messages must leave it intact.
 -/
 @[inline] def trace.profiler.isExporting (opts : Options) : Bool :=
-  (trace.profiler.output.get? opts).isSome || trace.profiler.serve.get opts
+  (opts.find? trace.profiler.output.name).isSome || trace.profiler.serve.get opts
 
 register_builtin_option trace.profiler.output.pp : Bool := {
   defValue := false
@@ -332,7 +333,9 @@ The `cls`, `collapsed`, and `tag` arguments are forwarded to the constructor of
 def withTraceNode [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m]
     [ExceptToTraceResult ε α] (cls : Name)
     (msg : Except ε α → m MessageData) (k : m α) (collapsed := true) (tag := "") : m α := do
-  let opts ← getOptions
+  -- unrestricted acquisition here and in `postCallback`: trace and profiler collection cannot
+  -- influence a cached resolution result
+  let opts ← getOptionsUnrestricted
   if !opts.hasTrace then
     return (← k)
   let clsEnabled ← isTracingEnabledFor cls
@@ -415,7 +418,9 @@ TODO: find better name for this function.
 def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m]
     [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] [ExceptToTraceResult ε α] (cls : Name)
     (msg : Unit → m MessageData) (k : m α) (collapsed := true) (tag := "") : m α := do
-  let opts ← getOptions
+  -- unrestricted acquisition here and in `postCallback`: trace and profiler collection cannot
+  -- influence a cached resolution result
+  let opts ← getOptionsUnrestricted
   if !opts.hasTrace then
     return (← k)
   let clsEnabled ← isTracingEnabledFor cls
@@ -445,7 +450,8 @@ where
     MonadExcept.ofExcept res
 
 def addTraceAsMessages [Monad m] [MonadRef m] [MonadLog m] [MonadTrace m] : m Unit := do
-  if trace.profiler.isExporting (← getOptions) then
+  -- unrestricted acquisition: profiler collection cannot influence a cached resolution result
+  if trace.profiler.isExporting (← getOptionsUnrestricted) then
     -- do not add trace messages if the profile is being exported (`trace.profiler.output` or
     -- `trace.profiler.serve`) as it would be redundant, pretty printing the trace messages is
     -- expensive, and `getResetTraces` would consume the data we want to export
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 3baec9ac0fdd..bfd7e2768544 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -16,14 +16,14 @@ options get_option_overrides() {
 
     // uncomment for ABI-breaking changes affecting meta code;
     // see also next option!
-    //opts = opts.update({"interpreter", "prefer_native"}, true);
+    opts = opts.update({"interpreter", "prefer_native"}, true);
 
     // comment out when enabling `prefer_native` should also affect use
     // of built-in parsers in quotations; this should usually be done, but setting
     // both to `true` may be necessary for handling non-builtin parsers with
     // builtin elaborators
     // TODO: make consistent across stages
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
+    //opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
 
     // changes to builtin parsers may also require uncommenting the following option if macros/syntax
     // with custom precheck hooks were affected
diff --git a/tests/elab/tc_cache_check_hits.lean b/tests/elab/tc_cache_check_hits.lean
new file mode 100644
index 000000000000..5d1b4c861263
--- /dev/null
+++ b/tests/elab/tc_cache_check_hits.lean
@@ -0,0 +1,34 @@
+/-!
+Runs representative elaboration with `debug.synthInstance.checkCacheHits`, the differential
+validation of type class resolution cache hits: every served entry is recomputed from scratch
+and compared. A panic here means a served result diverged from recomputation, i.e. some
+dependency of the entry was not recorded.
+-/
+
+set_option debug.synthInstance.checkCacheHits true
+
+class R (α : Type) where
+  val : Nat
+
+instance : R Nat := ⟨1⟩
+instance : R (List α) := ⟨2⟩
+instance [R α] [R β] : R (α × β) := ⟨3⟩
+
+def f (n : Nat) : Nat := R.val Nat + n
+
+example : R.val (List Nat) = 2 := rfl
+example : R.val (List Nat) = 2 := rfl
+example : R.val (Nat × List Nat) = 3 := rfl
+example : R.val (Nat × List Nat) = 3 := rfl
+
+def sumIt (l : List Nat) : Nat := l.foldl (· + ·) 0
+
+example : sumIt [1, 2, 3] = 6 := by simp [sumIt]
+example : sumIt [1, 2, 3] = 6 := by simp [sumIt]
+
+structure Wrap where
+  out : Nat
+
+instance : R Wrap := ⟨4⟩
+
+example (w : Wrap) : R.val Wrap + w.out = 4 + w.out := rfl
diff --git a/tests/elab/tc_cache_covered_claims.lean b/tests/elab/tc_cache_covered_claims.lean
new file mode 100644
index 000000000000..2434a9acbafc
--- /dev/null
+++ b/tests/elab/tc_cache_covered_claims.lean
@@ -0,0 +1,76 @@
+/-!
+Locks the extension-classification audit of the type class resolution dependency tracking: any
+resolution-path read of an unclassified environment extension panics unconditionally (see
+`Lean.EnvExtension.trackGen`). The file elaborates representative content whose searches
+traverse the covered extensions: structures and classes (structure info, class table,
+projection functions), instances with out-params, matchers and equation realization (matcher
+info, eqns, match eqns), reducibility reads and post-hoc changes (declaration change log), and
+auxiliary recursors. A panic here means the search path reached an extension that should
+either be registered as covered (`declCovered`, with a justification) or generation-tracked
+and read through the recording accessors.
+-/
+
+structure Pt where
+  x : Nat
+  y : Nat
+
+class Dist (α : Type) where
+  dist : α → α → Nat
+
+instance : Dist Pt := ⟨fun a b => (a.x - b.x) + (a.y - b.y) + (b.x - a.x) + (b.y - a.y)⟩
+
+structure Pt3 extends Pt where
+  z : Nat
+
+instance : Dist Pt3 := ⟨fun a b => Dist.dist a.toPt b.toPt + (a.z - b.z) + (b.z - a.z)⟩
+
+def d3 (a b : Pt3) : Nat := Dist.dist a b
+
+class Sz (α : Type) (β : outParam Type) where
+  sz : α → β
+
+instance : Sz (List α) Nat := ⟨List.length⟩
+
+example (l : List Nat) : Nat := Sz.sz l + d3 ⟨⟨1, 2⟩, 3⟩ ⟨⟨4, 5⟩, 6⟩
+
+-- Matcher creation and equation realization inside proofs.
+def classify : List Nat → Nat
+  | [] => 0
+  | [x] => x
+  | _ :: _ :: _ => 2
+
+example : classify [] = 0 := by simp [classify]
+example : classify [7] = 7 := by simp [classify]
+example (x y : Nat) (l : List Nat) : classify (x :: y :: l) = 2 := by simp [classify]
+
+-- Structural recursion (def height overrides) and generated equations.
+def sumUp : Nat → Nat
+  | 0 => 0
+  | n + 1 => n + 1 + sumUp n
+
+example : sumUp 3 = 6 := by simp [sumUp]
+
+-- Reducibility: a definition guarding an instance, then a post-hoc change observed by a query.
+def Wrapped := Nat
+
+example : (inferInstance : Dist Pt).dist ⟨0, 0⟩ ⟨1, 1⟩ = 2 := rfl
+
+attribute [reducible] Wrapped
+
+instance : Dist Wrapped := ⟨fun a b => (a : Nat) + (b : Nat)⟩
+
+example : Dist.dist (2 : Wrapped) (3 : Wrapped) = 5 := rfl
+
+-- Auxiliary recursors and noConfusion on an inductive family.
+inductive Tree (α : Type) where
+  | leaf : Tree α
+  | node : Tree α → α → Tree α → Tree α
+
+def Tree.size : Tree α → Nat
+  | .leaf => 0
+  | .node l _ r => l.size + 1 + r.size
+
+instance : Dist (Tree Nat) := ⟨fun a b => a.size + b.size⟩
+
+example (t : Tree Nat) : Dist.dist t t = 2 * t.size := by
+  simp [Dist.dist, Nat.two_mul]
diff --git a/tests/elab/tc_cache_fvar_norm.lean b/tests/elab/tc_cache_fvar_norm.lean
new file mode 100644
index 000000000000..27facf90fe81
--- /dev/null
+++ b/tests/elab/tc_cache_fvar_norm.lean
@@ -0,0 +1,43 @@
+/-!
+Tests that the type class resolution cache normalizes free variables, so that structurally
+identical instance queries in different local contexts (differing only in fvar identities) share a
+single persistent cache entry and hit each other.
+-/
+
+set_option trace.Meta.synthInstance.cache true
+
+class Foo (α : Type) where
+
+-- A query that resolves to a local instance, in a context with local fvars `α` and `[Foo α]`.
+/-- trace: [Meta.synthInstance.cache] new: Foo α -/
+#guard_msgs in
+@[reducible] def f1 (α : Type) [Foo α] : Foo α := inferInstance
+
+-- The same query in a fresh context (`β`): the normalized key matches `f1`, so this hits.
+/-- trace: [Meta.synthInstance.cache] cached: Foo β -/
+#guard_msgs in
+@[reducible] def f2 (β : Type) [Foo β] : Foo β := inferInstance
+
+-- Even reusing the original variable name `α` is a fresh fvar; still a hit.
+/-- trace: [Meta.synthInstance.cache] cached: Foo α -/
+#guard_msgs in
+@[reducible] def f3 (α : Type) [Foo α] : Foo α := inferInstance
+
+-- A different query shape (`Foo (List α)` is not derivable from `[Foo α]`) must NOT hit the above.
+/--
+error: failed to synthesize instance of type class
+  Foo (List α)
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+trace: [Meta.synthInstance.cache] new: Foo (List α)
+-/
+#guard_msgs in
+@[reducible] def g1 (α : Type) [Foo α] : Foo (List α) := inferInstance
+
+-- Distinct local-instance context (`[Foo (List α)]`) partitions the key: the normalized types of
+-- the local instances differ, so this `Foo (List α)` query is a fresh entry that succeeds, rather
+-- than a hit of the failure above.
+/-- trace: [Meta.synthInstance.cache] new: Foo (List α) -/
+#guard_msgs in
+@[reducible] def g2 (α : Type) [Foo (List α)] : Foo (List α) := inferInstance
diff --git a/tests/elab/tc_cache_fvar_norm_dag.lean b/tests/elab/tc_cache_fvar_norm_dag.lean
new file mode 100644
index 000000000000..6fd459aafc04
--- /dev/null
+++ b/tests/elab/tc_cache_fvar_norm_dag.lean
@@ -0,0 +1,22 @@
+import Lean
+
+/-!
+Tests that the free-variable normalization of the type class resolution cache traverses
+DAG-shared query types in DAG size, not tree size. `grind` builds heavily shared terms by
+substitution (e.g. deeply nested `if`-terms whose tree size is exponential in their DAG size);
+an unmemoized traversal exhausts the heartbeat budget or hangs. Synthesizing `Foo t` for a
+`Prod` tower `t` of depth 64 (tree size `2^64`, DAG size 65) must complete instantly.
+-/
+
+class Foo (α : Type) : Prop where
+
+instance instFoo (α : Type) : Foo α := ⟨⟩
+
+open Lean Meta
+
+run_meta do
+  withLocalDeclD `α (mkSort .one) fun α => do
+    let mut t := α
+    for _ in [0:64] do
+      t := mkApp2 (mkConst ``Prod [.zero, .zero]) t t
+    discard <| synthInstance (mkApp (mkConst ``Foo) t)
diff --git a/tests/elab/tc_cache_fvar_norm_let.lean b/tests/elab/tc_cache_fvar_norm_let.lean
new file mode 100644
index 000000000000..0e0cf03aac87
--- /dev/null
+++ b/tests/elab/tc_cache_fvar_norm_let.lean
@@ -0,0 +1,52 @@
+/-!
+Tests that the value of a let-bound free variable is part of the normalized type class cache key.
+Definitional unfolding can see a let value, so two contexts agreeing on the types of their free
+variables but not on a let value are not interchangeable, while two contexts agreeing on both are.
+-/
+
+class Bar (n : Nat) where
+
+instance : Bar 1 := ⟨⟩
+
+set_option trace.Meta.synthInstance.cache true
+
+/--
+trace: [Meta.synthInstance.cache] new: OfNat Nat 1
+---
+trace: [Meta.synthInstance.cache] new: Bar n
+-/
+#guard_msgs in
+example : True := by
+  let n : Nat := 1
+  have : Bar n := inferInstance
+  trivial
+
+-- The same context up to the identity of `n`: the normalized keys agree, so both queries hit.
+/--
+trace: [Meta.synthInstance.cache] new: OfNat Nat 1
+---
+trace: [Meta.synthInstance.cache] new: Bar n
+-/
+#guard_msgs in
+example : True := by
+  let n : Nat := 1
+  have : Bar n := inferInstance
+  trivial
+
+-- A different let value: the types still agree, so omitting the value from the key would reuse the
+-- success above and synthesize `Bar 2`.
+/--
+error: failed to synthesize instance of type class
+  Bar n
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+trace: [Meta.synthInstance.cache] new: OfNat Nat 2
+---
+trace: [Meta.synthInstance.cache] new: Bar n
+-/
+#guard_msgs in
+example : True := by
+  let n : Nat := 2
+  have : Bar n := inferInstance
+  trivial
diff --git a/tests/elab/tc_cache_fvar_norm_mvar_type.lean b/tests/elab/tc_cache_fvar_norm_mvar_type.lean
new file mode 100644
index 000000000000..cfbb1c82c0d2
--- /dev/null
+++ b/tests/elab/tc_cache_fvar_norm_mvar_type.lean
@@ -0,0 +1,38 @@
+/-!
+Tests that the type class resolution cache normalizes free variables even when a variable in the
+normalization closure has an assigned metavariable in its type. `Expr.hasMVar` stays set for
+assigned metavariables, so a naive check gives up on such contexts and falls back to a raw,
+context-specific cache key.
+-/
+
+class Foo (α : Type) where
+class Bar (α : Type) where
+instance : Foo Nat := ⟨⟩
+instance [Foo α] : Bar α := ⟨⟩
+
+set_option trace.Meta.synthInstance.cache true
+
+-- `inst : Foo ?m` with `?m := Nat` assigned by the ascription. It is a local instance, hence part
+-- of the closure normalized for the `Bar Nat` key.
+/--
+trace: [Meta.synthInstance.cache] new: Foo Nat
+---
+trace: [Meta.synthInstance.cache] new: Bar Nat
+-/
+#guard_msgs in
+example : True := by
+  have inst : Foo _ := (inferInstance : Foo Nat)
+  have : Bar Nat := inferInstance
+  trivial
+
+-- The same query under a fresh `inst`: the normalized keys agree, so both queries hit.
+/--
+trace: [Meta.synthInstance.cache] new: Foo Nat
+---
+trace: [Meta.synthInstance.cache] new: Bar Nat
+-/
+#guard_msgs in
+example : True := by
+  have inst : Foo _ := (inferInstance : Foo Nat)
+  have : Bar Nat := inferInstance
+  trivial
diff --git a/tests/elab/tc_cache_invalidation.lean b/tests/elab/tc_cache_invalidation.lean
new file mode 100644
index 000000000000..9390730c290c
--- /dev/null
+++ b/tests/elab/tc_cache_invalidation.lean
@@ -0,0 +1,141 @@
+/-!
+Tests that the persistent type class resolution cache is invalidated by post-hoc environment
+changes that affect definitional equality during resolution: reducibility attribute changes and
+new unification hints. A reducibility attribute applied as part of a declaration's own
+elaboration does not invalidate the cache, since no cached entry can mention the new declaration.
+-/
+
+set_option trace.Meta.synthInstance.cache true
+
+class R (α : Type) where
+
+instance : R Nat := ⟨⟩
+
+def MyNat := Nat
+
+-- `MyNat` is semireducible, so resolution cannot unfold it: the failure is cached.
+/--
+error: failed to synthesize instance of type class
+  R MyNat
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+trace: [Meta.synthInstance.cache] new: R MyNat
+-/
+#guard_msgs in
+def r1 : Unit := let _ : R MyNat := inferInstance; ()
+
+/--
+error: failed to synthesize instance of type class
+  R MyNat
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+trace: [Meta.synthInstance.cache] cached: R MyNat
+-/
+#guard_msgs in
+def r2 : Unit := let _ : R MyNat := inferInstance; ()
+
+-- A reducibility attribute that is part of a declaration's own elaboration does not reset the
+-- cache: the entry above is still served.
+@[reducible] def OtherNat := Nat
+
+/--
+error: failed to synthesize instance of type class
+  R MyNat
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+trace: [Meta.synthInstance.cache] cached: R MyNat
+-/
+#guard_msgs in
+def r3 : Unit := let _ : R MyNat := inferInstance; ()
+
+-- A post-hoc reducibility change resets the cache; `MyNat` now unfolds during resolution and the
+-- query succeeds.
+attribute [reducible] MyNat
+
+/-- trace: [Meta.synthInstance.cache] new: R MyNat -/
+#guard_msgs in
+def r4 : Unit := let _ : R MyNat := inferInstance; ()
+
+/-- trace: [Meta.synthInstance.cache] cached: R MyNat -/
+#guard_msgs in
+def r5 : Unit := let _ : R MyNat := inferInstance; ()
+
+-- All declarations happen up front so that no instance addition (which invalidates every entry
+-- that consulted the instance table) interferes with the queries below.
+class OP (α : Type) (β : outParam Type) where
+
+instance : OP Nat Bool := ⟨⟩
+
+def NotBool := List Nat
+
+def YetAnotherNat := Nat
+
+-- The `R Nat` search succeeds without any failing unification, so it never consults the
+-- unification hints and records no dependency on them: adding a hint below must not invalidate
+-- this entry.
+/-- trace: [Meta.synthInstance.cache] new: R Nat -/
+#guard_msgs in
+def q1 : Unit := let _ : R Nat := inferInstance; ()
+
+/-- trace: [Meta.synthInstance.cache] cached: R Nat -/
+#guard_msgs in
+def q2 : Unit := let _ : R Nat := inferInstance; ()
+
+-- A query whose output parameter fails to unify does consult the hints on the failure path and
+-- records the dependency; the failure is cached with it.
+/--
+error: failed to synthesize instance of type class
+  OP Nat NotBool
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+trace: [Meta.synthInstance.cache] new: OP Nat NotBool
+-/
+#guard_msgs in
+def q3 : Unit := let _ : OP Nat NotBool := inferInstance; ()
+
+/--
+error: failed to synthesize instance of type class
+  OP Nat NotBool
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+trace: [Meta.synthInstance.cache] cached: OP Nat NotBool
+-/
+#guard_msgs in
+def q4 : Unit := let _ : OP Nat NotBool := inferInstance; ()
+
+-- The hint is irrelevant to both cached queries, but only the `OP` search consulted the hint
+-- table: adding the hint invalidates exactly that entry.
+@[unification_hint] def yetAnotherHint : Prop := YetAnotherNat = Nat
+
+/--
+error: failed to synthesize instance of type class
+  OP Nat NotBool
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+trace: [Meta.synthInstance.cache] new: OP Nat NotBool
+-/
+#guard_msgs in
+def q5 : Unit := let _ : OP Nat NotBool := inferInstance; ()
+
+/-- trace: [Meta.synthInstance.cache] cached: R Nat -/
+#guard_msgs in
+def q6 : Unit := let _ : R Nat := inferInstance; ()
+
+-- A post-hoc reducibility change (here: overriding an imported declaration) bumps the change
+-- counter and conservatively invalidates every earlier entry, including entries whose search
+-- never consulted the declaration.
+attribute [local implicit_reducible] Function.const
+
+/-- trace: [Meta.synthInstance.cache] new: R Nat -/
+#guard_msgs in
+def q7 : Unit := let _ : R Nat := inferInstance; ()
+
+/-- trace: [Meta.synthInstance.cache] cached: R Nat -/
+#guard_msgs in
+def q8 : Unit := let _ : R Nat := inferInstance; ()
diff --git a/tests/elab/tc_cache_options.lean b/tests/elab/tc_cache_options.lean
new file mode 100644
index 000000000000..63295d051feb
--- /dev/null
+++ b/tests/elab/tc_cache_options.lean
@@ -0,0 +1,33 @@
+import Lean.Elab.Command
+
+/-!
+Tests that the type class resolution cache tracks options by *recorded accesses*: a query
+records every result-relevant option lookup it performs (`Lean.getRecordedOption`), and an
+entry is served only while those lookups give the same answers. Options the search never read
+do not partition the cache; options it did read do.
+-/
+
+open Lean Meta Elab Command
+
+class Boo (α : Type) where
+
+instance : Boo Nat := ⟨⟩
+
+/--
+trace: [Meta.synthInstance.cache] new: Boo Nat
+[Meta.synthInstance.cache] cached: Boo Nat
+[Meta.synthInstance.cache] cached: Boo Nat
+[Meta.synthInstance.cache] new: Boo Nat
+-/
+#guard_msgs in
+run_cmd liftTermElabM do
+  let ty := mkApp (mkConst ``Boo) (mkConst ``Nat)
+  let query : TermElabM Unit :=
+    withOptions (·.setBool `trace.Meta.synthInstance.cache true) do
+      discard <| synthInstance? ty
+  query
+  query
+  -- A result-irrelevant option the search never reads does not partition the cache.
+  withOptions (·.setBool `pp.universes true) do query
+  -- `backward.synthInstance.canonInstances` is read by the search, so it does.
+  withOptions (·.setBool `backward.synthInstance.canonInstances false) do query
diff --git a/tests/elab/tc_cache_options_key.lean b/tests/elab/tc_cache_options_key.lean
new file mode 100644
index 000000000000..f2dcb1144c99
--- /dev/null
+++ b/tests/elab/tc_cache_options_key.lean
@@ -0,0 +1,52 @@
+/-!
+Tests that the type class resolution cache tracks options by *recorded accesses*: every
+result-relevant option lookup on the search path is recorded as a dependency of the cache entry
+(`Lean.getRecordedOption`), and an entry is reused exactly when its recorded lookups give the
+same answers. Options the search never read do not partition the cache, result-irrelevant
+options (e.g. pretty printing) are never recorded, and plainly acquiring the options on the
+search path panics (`Core.Context.recordingDeps`), so no access can go untracked; the frameworks
+whose reads cannot influence results (trace collection, limits) acquire them via
+`getOptionsUnrestricted` at their accessors.
+-/
+
+set_option trace.Meta.synthInstance.cache true
+
+class Boo (α : Type) where
+
+instance : Boo Nat := ⟨⟩
+
+/-- trace: [Meta.synthInstance.cache] new: Boo Nat -/
+#guard_msgs in
+def b1 : Unit := let _ : Boo Nat := inferInstance; ()
+
+-- Result-irrelevant options do not partition the cache.
+set_option pp.universes true in
+/-- trace: [Meta.synthInstance.cache] cached: Boo Nat -/
+#guard_msgs in
+def b2 : Unit := let _ : Boo Nat := inferInstance; ()
+
+-- A result-relevant option the search never read does not partition the cache either: this
+-- search never invokes `synthPending`, so `maxSynthPendingDepth` is not among its recorded
+-- dependencies.
+set_option maxSynthPendingDepth 2 in
+/-- trace: [Meta.synthInstance.cache] cached: Boo Nat -/
+#guard_msgs in
+def b3 : Unit := let _ : Boo Nat := inferInstance; ()
+
+-- An option the search did read invalidates: every search consults
+-- `backward.synthInstance.canonInstances`, so changing it forces a fresh entry.
+set_option backward.synthInstance.canonInstances false in
+/-- trace: [Meta.synthInstance.cache] new: Boo Nat -/
+#guard_msgs in
+def b4 : Unit := let _ : Boo Nat := inferInstance; ()
+
+-- Entries for both observed values coexist: back at the default, `b1`'s entry is reused …
+/-- trace: [Meta.synthInstance.cache] cached: Boo Nat -/
+#guard_msgs in
+def b5 : Unit := let _ : Boo Nat := inferInstance; ()
+
+-- … and the entry recorded under the changed value remains valid in its setting.
+set_option backward.synthInstance.canonInstances false in
+/-- trace: [Meta.synthInstance.cache] cached: Boo Nat -/
+#guard_msgs in
+def b6 : Unit := let _ : Boo Nat := inferInstance; ()
diff --git a/tests/elab/tc_cache_persist.lean b/tests/elab/tc_cache_persist.lean
new file mode 100644
index 000000000000..10dfd2b365c7
--- /dev/null
+++ b/tests/elab/tc_cache_persist.lean
@@ -0,0 +1,185 @@
+/-!
+Tests that the type class resolution cache persists across commands, is reset when instances are
+added or erased, and keys entries by the set of activated scoped instances and of local
+instances.
+
+Persistent cache fills are environment modifications, so they are rolled back together with the
+environment; in particular `example`s (which are elaborated inside `withoutModifyingEnv`) can
+read the cache but do not contribute new entries to it.
+-/
+
+set_option trace.Meta.synthInstance.cache true
+
+class Boo (α : Type) where
+
+instance booNat : Boo Nat := ⟨⟩
+
+/-- trace: [Meta.synthInstance.cache] new: Boo Nat -/
+#guard_msgs in
+def b1 : Unit := let _ : Boo Nat := inferInstance; ()
+
+-- The result is cached across commands.
+/-- trace: [Meta.synthInstance.cache] cached: Boo Nat -/
+#guard_msgs in
+def b2 : Unit := let _ : Boo Nat := inferInstance; ()
+
+class Coo (α : Type) where
+
+-- Failures are cached as well, including across commands.
+/--
+error: failed to synthesize instance of type class
+  Coo Nat
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+trace: [Meta.synthInstance.cache] new: Coo Nat
+-/
+#guard_msgs in
+def c1 : Unit := let _ : Coo Nat := inferInstance; ()
+
+/--
+error: failed to synthesize instance of type class
+  Coo Nat
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+trace: [Meta.synthInstance.cache] cached: Coo Nat
+-/
+#guard_msgs in
+def c2 : Unit := let _ : Coo Nat := inferInstance; ()
+
+-- Adding an instance resets the cache, so the cached failure above is discarded.
+instance : Coo Nat := ⟨⟩
+
+/-- trace: [Meta.synthInstance.cache] new: Coo Nat -/
+#guard_msgs in
+def c3 : Unit := let _ : Coo Nat := inferInstance; ()
+
+-- The reset clears the whole cache, including unrelated entries.
+/-- trace: [Meta.synthInstance.cache] new: Boo Nat -/
+#guard_msgs in
+def b3 : Unit := let _ : Boo Nat := inferInstance; ()
+
+/-- trace: [Meta.synthInstance.cache] cached: Boo Nat -/
+#guard_msgs in
+def b4 : Unit := let _ : Boo Nat := inferInstance; ()
+
+-- Erasing an instance resets the cache.
+attribute [-instance] booNat
+
+/--
+error: failed to synthesize instance of type class
+  Boo Nat
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+trace: [Meta.synthInstance.cache] new: Boo Nat
+-/
+#guard_msgs in
+def b5 : Unit := let _ : Boo Nat := inferInstance; ()
+
+class Doo (α : Type) where
+
+namespace N
+scoped instance dooNat : Doo Nat := ⟨⟩
+end N
+
+/--
+error: failed to synthesize instance of type class
+  Doo Nat
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+trace: [Meta.synthInstance.cache] new: Doo Nat
+-/
+#guard_msgs in
+def d1 : Unit := let _ : Doo Nat := inferInstance; ()
+
+-- Activating a scoped instance via `open` switches to a different cache key partition, so the
+-- cached failure above is not consulted and synthesis succeeds.
+open N in
+/-- trace: [Meta.synthInstance.cache] new: Doo Nat -/
+#guard_msgs in
+def d2 : Unit := let _ : Doo Nat := inferInstance; ()
+
+-- After the scope ends, the entries from before the `open` are valid again.
+/--
+error: failed to synthesize instance of type class
+  Doo Nat
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+trace: [Meta.synthInstance.cache] cached: Doo Nat
+-/
+#guard_msgs in
+def d3 : Unit := let _ : Doo Nat := inferInstance; ()
+
+-- Re-activating the scope makes the entries cached inside the previous `open` valid again.
+open N
+
+/-- trace: [Meta.synthInstance.cache] cached: Doo Nat -/
+#guard_msgs in
+def d4 : Unit := let _ : Doo Nat := inferInstance; ()
+
+-- Local instances are part of the cache key as well, so entries computed with a local instance
+-- do not leak out of its scope.
+class Eoo (α : Type) where
+
+@[instance_reducible] def eooNat : Eoo Nat := ⟨⟩
+
+section
+attribute [local instance] eooNat
+
+/-- trace: [Meta.synthInstance.cache] new: Eoo Nat -/
+#guard_msgs in
+def e1 : Unit := let _ : Eoo Nat := inferInstance; ()
+
+/-- trace: [Meta.synthInstance.cache] cached: Eoo Nat -/
+#guard_msgs in
+def e2 : Unit := let _ : Eoo Nat := inferInstance; ()
+
+end
+
+/--
+error: failed to synthesize instance of type class
+  Eoo Nat
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+---
+trace: [Meta.synthInstance.cache] new: Eoo Nat
+-/
+#guard_msgs in
+def e3 : Unit := let _ : Eoo Nat := inferInstance; ()
+
+-- `example`s do not contribute cache entries: their environment changes, including cache fills,
+-- are reverted.
+class Foo (α : Type) where
+
+instance : Foo Nat := ⟨⟩
+
+/-- trace: [Meta.synthInstance.cache] new: Foo Nat -/
+#guard_msgs in
+example : Foo Nat := inferInstance
+
+/-- trace: [Meta.synthInstance.cache] new: Foo Nat -/
+#guard_msgs in
+def f1 : Unit := let _ : Foo Nat := inferInstance; ()
+
+/-- trace: [Meta.synthInstance.cache] cached: Foo Nat -/
+#guard_msgs in
+def f2 : Unit := let _ : Foo Nat := inferInstance; ()
+
+-- `synthInstance.maxSize` is part of the cache key, so cached results (in particular failures)
+-- obtained under a different size limit are not reused.
+/-- trace: [Meta.synthInstance.cache] new: Coo Nat -/
+#guard_msgs in
+def c4 : Unit := let _ : Coo Nat := inferInstance; ()
+
+/-- trace: [Meta.synthInstance.cache] cached: Coo Nat -/
+#guard_msgs in
+def c5 : Unit := let _ : Coo Nat := inferInstance; ()
+
+set_option synthInstance.maxSize 100 in
+/-- trace: [Meta.synthInstance.cache] new: Coo Nat -/
+#guard_msgs in
+def c6 : Unit := let _ : Coo Nat := inferInstance; ()
diff --git a/tests/elab/tc_cache_persist_fvar.lean b/tests/elab/tc_cache_persist_fvar.lean
new file mode 100644
index 000000000000..933e9a068925
--- /dev/null
+++ b/tests/elab/tc_cache_persist_fvar.lean
@@ -0,0 +1,44 @@
+import Lean
+
+/-!
+Tests that free-variable-dependent type class resolution cache entries are not persisted across
+commands.
+
+A `FVarId` identifies a variable only within the `NameGenerator` that created it. The pretty
+printer runs with a fresh one (`PPContext.runCoreM`), so a delaborator that synthesizes an instance
+under a binder sees the same `FVarId`s in every command. Persisting an entry keyed by such a
+variable makes the next command's unrelated query hit it. Reduced from Mathlib's `max`/`⊔`
+delaborator, which decides on notation by testing for a `LinearOrder` instance.
+-/
+
+open Lean
+
+class Foo (α : Type) where
+class Bar (α : Type) where
+
+def wrap {α : Type} (a : α) : α := a
+
+open Lean Meta PrettyPrinter Delaborator SubExpr in
+@[delab app.wrap]
+def delabWrap : Delab := do
+  let e ← getExpr
+  guard (e.getAppNumArgs == 2)
+  let α := e.appFn!.appArg!
+  -- The pretty printer clears the local instances, so re-add them, as Mathlib's delaborator does.
+  let decls := (← getLCtx).decls.toList.filterMap id
+  let r? ← withLocalInstances decls do
+    synthInstance? (mkApp (mkConst ``Foo) α)
+  let a ← withAppArg delab
+  let tag := mkIdent (if r?.isSome then `FOO else `NOFOO)
+  `($tag $a)
+
+-- Delaborating this fails to synthesize `Foo _pp_uniq.1`.
+/-- info: fun α [Bar α] a => NOFOO a : (α : Type) → [Bar α] → α → α -/
+#guard_msgs in
+#check fun (α : Type) [Bar α] (a : α) => wrap a
+
+-- The binder is a different variable that merely reuses the `FVarId`, and `Foo` is synthesizable
+-- from it, so the failure above must not be reused.
+/-- info: fun α [Foo α] a => FOO a : (α : Type) → [Foo α] → α → α -/
+#guard_msgs in
+#check fun (α : Type) [Foo α] (a : α) => wrap a
diff --git a/tests/elab/tc_cache_persist_transparency.lean b/tests/elab/tc_cache_persist_transparency.lean
new file mode 100644
index 000000000000..97ea5ed4cf91
--- /dev/null
+++ b/tests/elab/tc_cache_persist_transparency.lean
@@ -0,0 +1,40 @@
+/-!
+Tests option-dependency recording on the `backward.isDefEq.respectTransparency` options, which
+decide whether `isDefEq` bumps the transparency when assigning a metavariable. They belong to the
+per-query resolved flags (`Lean.Meta.SynthDefEqFlags`): every query records them up front, so
+toggling them partitions the cache regardless of whether the search reached the corresponding
+reads. See `tc_cache_options_key.lean` for a lazily recorded option that only partitions the
+queries that read it.
+-/
+
+set_option trace.Meta.synthInstance.cache true
+
+class Foo (α : Type) where
+
+instance fooNat : Foo Nat := ⟨⟩
+
+/-- trace: [Meta.synthInstance.cache] new: Foo Nat -/
+#guard_msgs in
+def a1 : Unit := let _ : Foo Nat := inferInstance; ()
+
+-- A different `backward.isDefEq.respectTransparency` partitions the cache.
+set_option backward.isDefEq.respectTransparency false in
+/-- trace: [Meta.synthInstance.cache] new: Foo Nat -/
+#guard_msgs in
+def a2 : Unit := let _ : Foo Nat := inferInstance; ()
+
+-- Likewise for `backward.isDefEq.respectTransparency.types`.
+set_option backward.isDefEq.respectTransparency.types false in
+/-- trace: [Meta.synthInstance.cache] new: Foo Nat -/
+#guard_msgs in
+def a3 : Unit := let _ : Foo Nat := inferInstance; ()
+
+-- The entries of all partitions remain valid.
+/-- trace: [Meta.synthInstance.cache] cached: Foo Nat -/
+#guard_msgs in
+def a4 : Unit := let _ : Foo Nat := inferInstance; ()
+
+set_option backward.isDefEq.respectTransparency false in
+/-- trace: [Meta.synthInstance.cache] cached: Foo Nat -/
+#guard_msgs in
+def a5 : Unit := let _ : Foo Nat := inferInstance; ()
diff --git a/tests/elab/tc_cache_reducibility_birth.lean b/tests/elab/tc_cache_reducibility_birth.lean
new file mode 100644
index 000000000000..b636f218a8e8
--- /dev/null
+++ b/tests/elab/tc_cache_reducibility_birth.lean
@@ -0,0 +1,45 @@
+import Lean.Elab.Command
+
+/-!
+Tests that reducibility changes invalidate the type class resolution cache within a command by
+birth arithmetic: a change whose target was born after a cached entry's query is skipped during
+validation (the query cannot have observed it), while a change to a pre-existing declaration
+invalidates the entry. See `Lean.Environment.declChangeLog`.
+-/
+
+open Lean Meta Elab Command
+
+class R (α : Type) where
+
+instance : R Nat := ⟨⟩
+
+def MyNat := Nat
+
+-- `MyNat` is semireducible, so resolution cannot unfold it and the failure is cached (`new:`
+-- then `cached:`). Marking a *freshly created* constant `[reducible]` leaves the entry alive:
+-- the constant was born after the entry's watermark, so the change is skipped (`cached:`).
+-- Marking pre-existing `MyNat` `[reducible]` invalidates the entry; `MyNat` now unfolds and the
+-- query succeeds (`new:` then `cached:`).
+/--
+trace: [Meta.synthInstance.cache] new: R MyNat
+[Meta.synthInstance.cache] cached: R MyNat
+[Meta.synthInstance.cache] cached: R MyNat
+[Meta.synthInstance.cache] new: R MyNat
+[Meta.synthInstance.cache] cached: R MyNat
+-/
+#guard_msgs in
+run_cmd liftTermElabM do
+  let ty := mkApp (mkConst ``R) (mkConst ``MyNat)
+  let query : TermElabM Unit :=
+    withOptions (·.setBool `trace.Meta.synthInstance.cache true) do
+      discard <| synthInstance? ty
+  query
+  query
+  addDecl <| .defnDecl {
+    name := `freshHelper, levelParams := [], type := mkConst ``Nat,
+    value := mkNatLit 1, hints := .abbrev, safety := .safe }
+  Attribute.add `freshHelper `reducible .missing
+  query
+  Attribute.add ``MyNat `reducible .missing
+  query
+  query
diff --git a/tests/elab_fail/eraseInsts.lean b/tests/elab_fail/eraseInsts.lean
index f53ecb9c413c..e04811694d90 100644
--- a/tests/elab_fail/eraseInsts.lean
+++ b/tests/elab_fail/eraseInsts.lean
@@ -13,3 +13,13 @@ def f2 (a b : Foo) := a + b -- Error
 end
 
 def f3 (a b : Foo) := a + b
+
+-- Same, with an explicit result type so that the failed query is metavariable-free and its
+-- cached failure reaches the persistent (cross-command) cache tier.
+section
+attribute [-instance] fooAdd
+
+def g2 (a b : Foo) : Foo := a + b -- Error
+end
+
+def g3 (a b : Foo) : Foo := a + b
diff --git a/tests/elab_fail/eraseInsts.lean.out.expected b/tests/elab_fail/eraseInsts.lean.out.expected
index 7c9b54ffd094..6f424e83fe9b 100644
--- a/tests/elab_fail/eraseInsts.lean.out.expected
+++ b/tests/elab_fail/eraseInsts.lean.out.expected
@@ -2,3 +2,7 @@ eraseInsts.lean:12:22-12:27: error(lean.synthInstanceFailed): failed to synthesi
   HAdd Foo Foo ?m
 
 Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+eraseInsts.lean:22:28-22:33: error(lean.synthInstanceFailed): failed to synthesize instance of type class
+  HAdd Foo Foo ?m
+
+Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
diff --git a/tests/lake/tests/kinds/produced.out b/tests/lake/tests/kinds/produced.out
index e69de29bb2d1..280bc4e62bfa 100644
--- a/tests/lake/tests/kinds/produced.out
+++ b/tests/lake/tests/kinds/produced.out
@@ -0,0 +1 @@
+dynlib