diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 219163553904..69b9a0d98ecc 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -695,7 +695,7 @@ endif()
 
 set(STDLIBS Init Std Lean Leanc)
 if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  list(APPEND STDLIBS Lake)
+  list(APPEND STDLIBS Lake LeanChecker)
 endif()
 
 add_custom_target(make_stdlib ALL
@@ -758,6 +758,12 @@ if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
     DEPENDS lake_shared
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lake
     VERBATIM)
+
+  add_custom_target(leanchecker ALL
+    WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
+    DEPENDS lake_shared
+    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanchecker
+    VERBATIM)
 endif()
 
 if(PREV_STAGE)
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index e65d855080cc..4b305273a223 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -1502,7 +1502,8 @@ def mkEmptyEnvironment (trustLevel : UInt32 := 0) : IO Environment := do
   return {
     base := .const {
       const2ModIdx    := {}
-      constants       := {}
+      -- Make sure we return a sharing-friendly map set to stage 2, like in `finalizeImport`.
+      constants       := SMap.empty.switch
       header          := { trustLevel }
       extensions      := exts
       irBaseExts      := exts
diff --git a/src/LeanChecker.lean b/src/LeanChecker.lean
new file mode 100644
index 000000000000..f665d6f124ef
--- /dev/null
+++ b/src/LeanChecker.lean
@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2023 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Sebastian Ullrich
+-/
+import Lean.CoreM
+import Lean.Replay
+import LeanChecker.Replay
+import Lake.Load.Manifest
+
+open Lean
+
+unsafe def replayFromImports (module : Name) : IO Unit := do
+  let mFile ← findOLean module
+  unless (← mFile.pathExists) do
+    throw <| IO.userError s!"object file '{mFile}' of module {module} does not exist"
+  -- Load all module data parts (exported, server, private)
+  let mut fnames := #[mFile]
+  let sFile := OLeanLevel.server.adjustFileName mFile
+  if (← sFile.pathExists) then
+    fnames := fnames.push sFile
+    let pFile := OLeanLevel.private.adjustFileName mFile
+    if (← pFile.pathExists) then
+      fnames := fnames.push pFile
+  let parts ← readModuleDataParts fnames
+  if h : parts.size = 0 then throw <| IO.userError "failed to read module data" else
+  let (mod, _) := parts[0]
+  let (_, s) ← importModulesCore mod.imports |>.run
+  let env ← finalizeImport s mod.imports {} 0 false false (isModule := true)
+  let mut newConstants := {}
+  -- Collect constants from last ("most private") part, which subsumes all prior ones
+  for name in parts[parts.size-1].1.constNames, ci in parts[parts.size-1].1.constants do
+    newConstants := newConstants.insert name ci
+  let env' ← env.replay' newConstants
+  env'.freeRegions
+
+unsafe def replayFromFresh (module : Name) : IO Unit := do
+  Lean.withImportModules #[{module}] {} fun env => do
+    discard <| (← mkEmptyEnvironment).replay' env.constants.map₁
+
+/-- Read the name of the main module from the `lake-manifest`. -/
+-- This has been copied from `ImportGraph.getCurrentModule` in the
+-- https://github.com/leanprover-community/import-graph repository.
+def getCurrentModule : IO Name := do
+  match (← Lake.Manifest.load? ⟨"lake-manifest.json"⟩) with
+  | none =>
+    -- TODO: should this be caught?
+    pure .anonymous
+  | some manifest =>
+    -- TODO: This assumes that the `package` and the default `lean_lib`
+    -- have the same name up to capitalisation.
+    -- Would be better to read the `.defaultTargets` from the
+    -- `← getRootPackage` from `Lake`, but I can't make that work with the monads involved.
+    return manifest.name.capitalize
+
+
+/--
+Run as e.g. `leanchecker` to check everything in the current project.
+or e.g. `leanchecker Mathlib.Data.Nat` to check everything with module name
+starting with `Mathlib.Data.Nat`.
+
+This will replay all the new declarations from the target file into the `Environment`
+as it was at the beginning of the file, using the kernel to check them.
+
+You can also use `leanchecker --fresh Mathlib.Data.Nat.Prime.Basic`
+to replay all the constants (both imported and defined in that file) into a fresh environment.
+This can only be used on a single file.
+
+This is not an external verifier, simply a tool to detect "environment hacking".
+-/
+unsafe def main (args : List String) : IO UInt32 := do
+  -- Contributor's note: lean4lean is intended to have a CLI interface matching leanchecker,
+  -- so if you want to make a change here please either make a sibling PR to
+  -- https://github.com/digama0/lean4lean or ping @digama0 (Mario Carneiro) to go fix it.
+  initSearchPath (← findSysroot)
+  let (flags, args) := args.partition fun s => s.startsWith "-"
+  let verbose := "-v" ∈ flags || "--verbose" ∈ flags
+  let fresh := "--fresh" ∈ flags
+  let targets ← do
+    match args with
+    | [] => pure [← getCurrentModule]
+    | args => args.mapM fun arg => do
+      let mod := arg.toName
+      if mod.isAnonymous then
+        throw <| IO.userError s!"Could not resolve module: {arg}"
+      else
+        pure mod
+  let mut targetModules := []
+  let sp ← searchPathRef.get
+  for target in targets do
+    let mut found := false
+    for path in (← SearchPath.findAllWithExt sp "olean") do
+      if let some m := (← searchModuleNameOfFileName path sp) then
+        if !fresh && target.isPrefixOf m || target == m then
+          targetModules := targetModules.insert m
+          found := true
+    if not found then
+      throw <| IO.userError s!"Could not find any oleans for: {target}"
+  if fresh then
+    if targetModules.length != 1 then
+      throw <| IO.userError s!"--fresh flag is only valid when specifying a single module:\n\
+        {targetModules}"
+    for m in targetModules do
+      if verbose then IO.println s!"replaying {m} with --fresh"
+      replayFromFresh m
+  else
+    let mut tasks := #[]
+    for m in targetModules do
+      tasks := tasks.push (m, ← IO.asTask (replayFromImports m))
+    for (m, t) in tasks do
+      if verbose then IO.println s!"replaying {m}"
+      if let .error e := t.get then
+        IO.eprintln s!"leanchecker found a problem in {m}"
+        throw e
+  return 0
diff --git a/src/LeanChecker/Replay.lean b/src/LeanChecker/Replay.lean
new file mode 100644
index 000000000000..683aa50571aa
--- /dev/null
+++ b/src/LeanChecker/Replay.lean
@@ -0,0 +1,191 @@
+/-
+Copyright (c) 2023 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Lean.CoreM
+import Lean.AddDecl
+import Lean.Util.FoldConsts
+
+/-!
+# `Lean.Environment.replay`
+
+`replay env constantMap` will "replay" all the constants in `constantMap : HashMap Name ConstantInfo` into `env`,
+sending each declaration to the kernel for checking.
+
+`replay` does not send constructors or recursors in `constantMap` to the kernel,
+but rather checks that they are identical to constructors or recursors generated in the environment
+after replaying any inductive definitions occurring in `constantMap`.
+
+`replay` can be used either as:
+* a verifier for an `Environment`, by sending everything to the kernel, or
+* a mechanism to safely transfer constants from one `Environment` to another.
+
+## Implementation notes
+
+This is a patched version of `Lean.Environment.Replay`, which is in the `lean4` repository
+up to `v4.18.0`, but will be deprecated in `v4.19.0` and then removed. Once it it removed,
+the prime on the `Replay'` namespace, the prime on `Lean.Environment.replay'`
+should be removed here.
+
+-/
+
+namespace Lean.Environment
+
+namespace Replay'
+
+structure Context where
+  newConstants : Std.HashMap Name ConstantInfo
+
+structure State where
+  env : Kernel.Environment
+  remaining : NameSet := {}
+  pending : NameSet := {}
+  postponedConstructors : NameSet := {}
+  postponedRecursors : NameSet := {}
+
+abbrev M := ReaderT Context <| StateRefT State IO
+
+/-- Check if a `Name` still needs processing. If so, move it from `remaining` to `pending`. -/
+def isTodo (name : Name) : M Bool := do
+  let r := (← get).remaining
+  if r.contains name then
+    modify fun s => { s with remaining := s.remaining.erase name, pending := s.pending.insert name }
+    return true
+  else
+    return false
+
+/-- Use the current `Environment` to throw a `Kernel.Exception`. -/
+def throwKernelException (ex : Kernel.Exception) : M Unit := do
+  throw <| .userError <| (← ex.toMessageData {} |>.toString)
+
+/-- Add a declaration, possibly throwing a `Kernel.Exception`. -/
+def addDecl (d : Declaration) : M Unit := do
+  match (← get).env.addDeclCore 0 d (cancelTk? := none) with
+  | .ok env => modify fun s => { s with env := env }
+  | .error ex => throwKernelException ex
+
+mutual
+/--
+Check if a `Name` still needs to be processed (i.e. is in `remaining`).
+
+If so, recursively replay any constants it refers to,
+to ensure we add declarations in the right order.
+
+The construct the `Declaration` from its stored `ConstantInfo`,
+and add it to the environment.
+-/
+partial def replayConstant (name : Name) : M Unit := do
+  if ← isTodo name then
+    let some ci := (← read).newConstants[name]? | unreachable!
+    replayConstants ci.getUsedConstantsAsSet
+    -- Check that this name is still pending: a mutual block may have taken care of it.
+    if (← get).pending.contains name then
+      match ci with
+      | .defnInfo   info =>
+        addDecl (Declaration.defnDecl   info)
+      | .thmInfo    info =>
+        -- Ignore duplicate theorems. This code is identical to that in `finalizeImport` before it
+        -- added extended duplicates support for the module system, which is not relevant for us
+        -- here as we always load all .olean information. We need this case *because* of the module
+        -- system -- as we have more data loaded than it, we might encounter duplicate private
+        -- theorems where elaboration under the module system would have only one of them in scope.
+        if let some (.thmInfo info') := (← get).env.find? ci.name then
+          if info.name == info'.name &&
+            info.type == info'.type &&
+            info.levelParams == info'.levelParams &&
+            info.all == info'.all
+          then
+            return
+        addDecl (Declaration.thmDecl    info)
+      | .axiomInfo  info =>
+        addDecl (Declaration.axiomDecl  info)
+      | .opaqueInfo info =>
+        addDecl (Declaration.opaqueDecl info)
+      | .inductInfo info =>
+        let lparams := info.levelParams
+        let nparams := info.numParams
+        let all ← info.all.mapM fun n => do pure <| ((← read).newConstants[n]!)
+        for o in all do
+          modify fun s =>
+            { s with remaining := s.remaining.erase o.name, pending := s.pending.erase o.name }
+        let ctorInfo ← all.mapM fun ci => do
+          pure (ci, ← ci.inductiveVal!.ctors.mapM fun n => do
+            pure ((← read).newConstants[n]!))
+        -- Make sure we are really finished with the constructors.
+        for (_, ctors) in ctorInfo do
+          for ctor in ctors do
+            replayConstants ctor.getUsedConstantsAsSet
+        let types : List InductiveType := ctorInfo.map fun ⟨ci, ctors⟩ =>
+          { name := ci.name
+            type := ci.type
+            ctors := ctors.map fun ci => { name := ci.name, type := ci.type } }
+        addDecl (Declaration.inductDecl lparams nparams types false)
+      -- We postpone checking constructors,
+      -- and at the end make sure they are identical
+      -- to the constructors generated when we replay the inductives.
+      | .ctorInfo info =>
+        modify fun s => { s with postponedConstructors := s.postponedConstructors.insert info.name }
+      -- Similarly we postpone checking recursors.
+      | .recInfo info =>
+        modify fun s => { s with postponedRecursors := s.postponedRecursors.insert info.name }
+      | .quotInfo _ =>
+        -- `Quot.lift` and `Quot.ind` have types that reference `Eq`,
+        -- so we need to ensure `Eq` is replayed before adding the quotient declaration.
+        replayConstant `Eq
+        addDecl (Declaration.quotDecl)
+      modify fun s => { s with pending := s.pending.erase name }
+
+/-- Replay a set of constants one at a time. -/
+partial def replayConstants (names : NameSet) : M Unit := do
+  for n in names do replayConstant n
+
+end
+
+/--
+Check that all postponed constructors are identical to those generated
+when we replayed the inductives.
+-/
+def checkPostponedConstructors : M Unit := do
+  for ctor in (← get).postponedConstructors do
+    match (← get).env.find? ctor, (← read).newConstants[ctor]? with
+    | some (.ctorInfo info), some (.ctorInfo info') =>
+      if ! (info == info') then throw <| IO.userError s!"Invalid constructor {ctor}"
+    | _, _ => throw <| IO.userError s!"No such constructor {ctor}"
+
+/--
+Check that all postponed recursors are identical to those generated
+when we replayed the inductives.
+-/
+def checkPostponedRecursors : M Unit := do
+  for ctor in (← get).postponedRecursors do
+    match (← get).env.find? ctor, (← read).newConstants[ctor]? with
+    | some (.recInfo info), some (.recInfo info') =>
+      if ! (info == info') then throw <| IO.userError s!"Invalid recursor {ctor}"
+    | _, _ => throw <| IO.userError s!"No such recursor {ctor}"
+
+end Replay'
+
+open Replay'
+
+/--
+"Replay" some constants into an `Environment`, sending them to the kernel for checking.
+
+Throws a `IO.userError` if the kernel rejects a constant,
+or if there are malformed recursors or constructors for inductive types.
+-/
+def replay' (newConstants : Std.HashMap Name ConstantInfo) (env : Environment) : IO Environment := do
+  let mut remaining : NameSet := ∅
+  for (n, ci) in newConstants.toList do
+    -- We skip unsafe constants, and also partial constants.
+    -- Later we may want to handle partial constants.
+    if !ci.isUnsafe && !ci.isPartial then
+      remaining := remaining.insert n
+  let (_, s) ← StateRefT'.run (s := { env := env.toKernelEnv, remaining }) do
+    ReaderT.run (r := { newConstants }) do
+      for n in remaining do
+        replayConstant n
+      checkPostponedConstructors
+      checkPostponedRecursors
+  return .ofKernelEnv s.env
diff --git a/src/lakefile.toml.in b/src/lakefile.toml.in
index 51f1c94605d6..434ad824b8a3 100644
--- a/src/lakefile.toml.in
+++ b/src/lakefile.toml.in
@@ -8,7 +8,7 @@
 name = "lean4"
 bootstrap = true
 
-defaultTargets = ["Init", "Std", "Lean", "Lake", "LakeMain", "Leanc"]
+defaultTargets = ["Init", "Std", "Lean", "Lake", "LakeMain", "Leanc", "LeanChecker"]
 
 # Have Lake use CMake's build type (e.g., `Release`, `Debug`) where possible
 buildType = "${CMAKE_BUILD_TYPE_TOML}"
@@ -85,3 +85,7 @@ defaultFacets = ["static.export"]
 name = "Leanc"
 srcDir = "${CMAKE_BINARY_DIR}/leanc"
 defaultFacets = ["static"]
+
+[[lean_lib]]
+name = "LeanChecker"
+defaultFacets = ["static"]
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index 6e4d97af09b3..b3365e69307b 100644
--- a/src/stdlib.make.in
+++ b/src/stdlib.make.in
@@ -34,7 +34,7 @@ ifeq "${STAGE}" "0"
 endif
 
 # These can be phony since the inner Makefile/Lake will have the correct dependencies and avoid rebuilds
-.PHONY: Init Std Lean leanshared Lake libLake_shared lake lean
+.PHONY: Init Std Lean leanshared Lake libLake_shared lake lean LeanChecker leanchecker
 
 ifeq "${USE_LAKE}" "ON"
 
@@ -42,7 +42,7 @@ ifeq "${USE_LAKE}" "ON"
 Init:
 	${PREV_STAGE}/bin/lake build -f ${CMAKE_BINARY_DIR}/lakefile.toml $(LAKE_EXTRA_ARGS)
 
-Std Lean Lake Leanc: Init
+Std Lean Lake Leanc LeanChecker: Init
 
 else
 
@@ -68,6 +68,9 @@ Lake: Lean
 # lake is in its own subdirectory, so must adjust relative paths...
 	+"${LEAN_BIN}/leanmake" -C lake lib lib.export ../${LIB}/temp/LakeMain.o.export  PKG=Lake $(LEANMAKE_OPTS) OUT="../${LIB}" LIB_OUT="../${LIB}/lean" TEMP_OUT="../${LIB}/temp" OLEAN_OUT="../${LIB}/lean" EXTRA_SRC_ROOTS=LakeMain.lean
 
+LeanChecker: Lake
+	+"${LEAN_BIN}/leanmake" lib PKG=LeanChecker $(LEANMAKE_OPTS) OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}" LIB_OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}" OLEAN_OUT="${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}"
+
 endif
 
 ${LIB}/temp/empty.c:
@@ -170,3 +173,11 @@ ${CMAKE_BINARY_DIR}/bin/leanc${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_ARCHIVE_OUTPUT_
 	"${CMAKE_BINARY_DIR}/leanc.sh" $< ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@
 
 leanc: ${CMAKE_BINARY_DIR}/bin/leanc${CMAKE_EXECUTABLE_SUFFIX}
+
+${CMAKE_BINARY_DIR}/bin/leanchecker${CMAKE_EXECUTABLE_SUFFIX}: ${CMAKE_ARCHIVE_OUTPUT_DIRECTORY}/libLeanChecker.a ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
+	@echo "[    ] Building $@"
+# on Windows, must remove file before writing a new one (since the old one may be in use)
+	@rm -f $@
+	"${CMAKE_BINARY_DIR}/leanc.sh" $< -lLake_shared ${CMAKE_EXE_LINKER_FLAGS_MAKE} ${LEAN_EXE_LINKER_FLAGS} ${LEANC_OPTS} -o $@
+
+leanchecker: ${CMAKE_BINARY_DIR}/bin/leanchecker${CMAKE_EXECUTABLE_SUFFIX}
diff --git a/tests/common.sh b/tests/common.sh
index a5759abe1441..45e61db1af6d 100644
--- a/tests/common.sh
+++ b/tests/common.sh
@@ -69,14 +69,14 @@ function check_ret {
 function exec_check_raw {
     ret=0
     exec_capture_raw "$@" || ret=$?
-    check_ret
+    check_ret "$@"
 }
 
 # produces filtered output intended for usage with `diff_produced`
 function exec_check {
     ret=0
     exec_capture "$@" || ret=$?
-    check_ret
+    check_ret "$@"
 }
 
 function diff_produced {
diff --git a/tests/pkg/leanchecker/LeanCheckerTests/AddFalse.lean b/tests/pkg/leanchecker/LeanCheckerTests/AddFalse.lean
new file mode 100644
index 000000000000..6092c4eb441d
--- /dev/null
+++ b/tests/pkg/leanchecker/LeanCheckerTests/AddFalse.lean
@@ -0,0 +1,10 @@
+import Lean.Elab.Term
+
+open Lean in
+run_elab
+  modifyEnv fun env => Id.run do
+    let decl := .thmDecl { name := `false, levelParams := [], type := .const ``False [], value := .const ``False [] }
+    let .ok env := env.addDeclCore (doCheck := false) 0 decl none |
+      let _ : Inhabited Environment := ⟨env⟩
+      unreachable!
+    env
diff --git a/tests/pkg/leanchecker/LeanCheckerTests/AddFalse.lean.expected.out b/tests/pkg/leanchecker/LeanCheckerTests/AddFalse.lean.expected.out
new file mode 100644
index 000000000000..b7737dcd7057
--- /dev/null
+++ b/tests/pkg/leanchecker/LeanCheckerTests/AddFalse.lean.expected.out
@@ -0,0 +1,5 @@
+leanchecker found a problem in LeanCheckerTests.AddFalse
+uncaught exception: (kernel) declaration type mismatch, 'false' has type
+  Prop
+but it is expected to have type
+  False
diff --git a/tests/pkg/leanchecker/LeanCheckerTests/AddFalseConstructor.lean b/tests/pkg/leanchecker/LeanCheckerTests/AddFalseConstructor.lean
new file mode 100644
index 000000000000..9de1a0940c49
--- /dev/null
+++ b/tests/pkg/leanchecker/LeanCheckerTests/AddFalseConstructor.lean
@@ -0,0 +1,22 @@
+import LeanCheckerTests.OpenPrivate
+
+set_option Elab.async false
+
+open private Lean.Kernel.Environment.add from Lean.Environment
+open private Lean.Environment.setCheckedSync from Lean.Environment
+
+open Lean in
+run_elab
+  let env ← getEnv
+  let kenv := env.toKernelEnv
+  let kenv := Lean.Kernel.Environment.add kenv <| .ctorInfo {
+    name := `False.intro
+    levelParams := []
+    type := .const ``False []
+    induct := `False
+    cidx := 0
+    numParams := 0
+    numFields := 0
+    isUnsafe := false
+  }
+  setEnv <| Lean.Environment.setCheckedSync env kenv
diff --git a/tests/pkg/leanchecker/LeanCheckerTests/AddFalseConstructor.lean.expected.out b/tests/pkg/leanchecker/LeanCheckerTests/AddFalseConstructor.lean.expected.out
new file mode 100644
index 000000000000..1f52e229a4dd
--- /dev/null
+++ b/tests/pkg/leanchecker/LeanCheckerTests/AddFalseConstructor.lean.expected.out
@@ -0,0 +1,2 @@
+leanchecker found a problem in LeanCheckerTests.AddFalseConstructor
+uncaught exception: No such constructor False.intro
diff --git a/tests/pkg/leanchecker/LeanCheckerTests/NativeDecide.lean b/tests/pkg/leanchecker/LeanCheckerTests/NativeDecide.lean
new file mode 100644
index 000000000000..5aa0b6870ec0
--- /dev/null
+++ b/tests/pkg/leanchecker/LeanCheckerTests/NativeDecide.lean
@@ -0,0 +1,4 @@
+/-! `native_decide` is intentionally not supported at this point. -/
+
+theorem nat_dec : True := by native_decide
+#print axioms nat_dec
diff --git a/tests/pkg/leanchecker/LeanCheckerTests/NativeDecide.lean.expected.out b/tests/pkg/leanchecker/LeanCheckerTests/NativeDecide.lean.expected.out
new file mode 100644
index 000000000000..e8a511c6602f
--- /dev/null
+++ b/tests/pkg/leanchecker/LeanCheckerTests/NativeDecide.lean.expected.out
@@ -0,0 +1,2 @@
+leanchecker found a problem in LeanCheckerTests.NativeDecide
+uncaught exception: (kernel) (interpreter) unknown declaration 'nat_dec._nativeDecide_1_1'
diff --git a/tests/pkg/leanchecker/LeanCheckerTests/OpenPrivate.lean b/tests/pkg/leanchecker/LeanCheckerTests/OpenPrivate.lean
new file mode 100644
index 000000000000..4b5ff13623e0
--- /dev/null
+++ b/tests/pkg/leanchecker/LeanCheckerTests/OpenPrivate.lean
@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Lean.Elab.Command
+import Lean.Util.FoldConsts
+import Lean.Parser.Module
+
+open Lean Parser.Tactic Elab Command
+
+namespace Lean
+
+/-- Collects the names of private declarations referenced in definition `n`. -/
+def Meta.collectPrivateIn [Monad m] [MonadEnv m] [MonadError m]
+  (n : Name) (set := NameSet.empty) : m NameSet := do
+  let c ← getConstInfo n
+  let traverse value := Expr.foldConsts value set fun c a =>
+    if isPrivateName c then a.insert c else a
+  if let some value := c.value? then return traverse value
+  if let some c := (← getEnv).find? (n ++ `_cstage1) then
+    if let some value := c.value? then return traverse value
+  return traverse c.type
+
+/-- Get the module index given a module name. -/
+def Environment.moduleIdxForModule? (env : Environment) (mod : Name) : Option ModuleIdx :=
+  env.allImportedModuleNames.idxOf? mod
+
+instance : DecidableEq ModuleIdx := instDecidableEqNat
+
+/-- Get the list of declarations in a module (referenced by index). -/
+def Environment.declsInModuleIdx (env : Environment) (idx : ModuleIdx) : List Name :=
+  env.const2ModIdx.fold (fun acc n i => if i = idx then n :: acc else acc) []
+
+/-- Add info to the info tree corresponding to a module name. -/
+def Elab.addModuleInfo [Monad m] [MonadInfoTree m] (stx : Ident) : m Unit := do
+  -- HACK: The server looks specifically for ofCommandInfo nodes on `import` syntax
+  -- to do go-to-def for modules, so we have to add something that looks like an import
+  -- to the info tree. (Ideally this would be an `.ofModuleInfo` node instead.)
+  pushInfoLeaf <| .ofCommandInfo {
+    elaborator := `import
+    stx := Unhygienic.run `(Parser.Module.import| import $stx) |>.raw.copyHeadTailInfoFrom stx
+  }
+
+namespace Elab.Command
+
+/-- Core elaborator for `open private` and `export private`. -/
+def elabOpenPrivateLike (ids : Array Ident) (tgts mods : Option (Array Ident))
+  (f : (priv full user : Name) → CommandElabM Name) : CommandElabM Unit := do
+  let mut names := NameSet.empty
+  for tgt in tgts.getD #[] do
+    let n ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo tgt
+    names ← Meta.collectPrivateIn n names
+  for mod in mods.getD #[] do
+    let some modIdx := (← getEnv).moduleIdxForModule? mod.getId
+      | throwError "unknown module {mod}"
+    addModuleInfo mod
+    for declName in (← getEnv).declsInModuleIdx modIdx do
+      if isPrivateName declName then
+        names := names.insert declName
+  let appendNames (msg : String) : String := Id.run do
+    let mut msg := msg
+    for c in names do
+      if let some name := privateToUserName? c then
+        msg := msg ++ s!"{name}\n"
+    msg
+  if ids.isEmpty && !names.isEmpty then
+    logInfo (appendNames "found private declarations:\n")
+  let mut decls := #[]
+  for id in ids do
+    let n := id.getId
+    let mut found := []
+    for c in names do
+      if n.isSuffixOf c then
+        addConstInfo id c
+        found := c::found
+    match found with
+    | [] => throwError appendNames s!"'{n}' not found in the provided declarations:\n"
+    | [c] =>
+      if let some name := privateToUserName? c then
+        let new ← f c name n
+        decls := decls.push (OpenDecl.explicit n new)
+      else unreachable!
+    | _ => throwError s!"provided name is ambiguous: found {found.map privateToUserName?}"
+  modifyScope fun scope => Id.run do
+    let mut openDecls := scope.openDecls
+    for decl in decls do
+      openDecls := decl::openDecls
+    { scope with openDecls := openDecls }
+
+/--
+The command `open private a b c in foo bar` will look for private definitions named `a`, `b`, `c`
+in declarations `foo` and `bar` and open them in the current scope. This does not make the
+definitions public, but rather makes them accessible in the current section by the short name `a`
+instead of the (unnameable) internal name for the private declaration, something like
+`_private.Other.Module.0.Other.Namespace.foo.a`, which cannot be typed directly because of the `0`
+name component.
+
+It is also possible to specify the module instead with
+`open private a b c from Other.Module`.
+-/
+syntax (name := openPrivate) "open" "private" (ppSpace ident)*
+  (" in" (ppSpace ident)*)? (" from" (ppSpace ident)*)? : command
+
+/-- Elaborator for `open private`. -/
+@[command_elab openPrivate] def elabOpenPrivate : CommandElab
+| `(open private $ids* $[in $tgts*]? $[from $mods*]?) =>
+  elabOpenPrivateLike ids tgts mods fun c _ _ => pure c
+| _ => throwUnsupportedSyntax
+
+/--
+The command `export private a b c in foo bar` is similar to `open private`, but instead of opening
+them in the current scope it will create public aliases to the private definition. The definition
+will exist at exactly the original location and name, as if the `private` keyword was not used
+originally.
+
+It will also open the newly created alias definition under the provided short name, like
+`open private`.
+It is also possible to specify the module instead with
+`export private a b c from Other.Module`.
+-/
+syntax (name := exportPrivate) "export" "private" (ppSpace ident)*
+  (" in" (ppSpace ident)*)? (" from" (ppSpace ident)*)? : command
+
+/-- Elaborator for `export private`. -/
+@[command_elab exportPrivate] def elabExportPrivate : CommandElab
+| `(export private $ids* $[in $tgts*]? $[from $mods*]?) =>
+  elabOpenPrivateLike ids tgts mods fun c name _ => liftCoreM do
+    let cinfo ← getConstInfo c
+    if (← getEnv).contains name then
+      throwError s!"'{name}' has already been declared"
+    let decl := Declaration.defnDecl {
+      name := name,
+      levelParams := cinfo.levelParams,
+      type := cinfo.type,
+      value := mkConst c (cinfo.levelParams.map mkLevelParam),
+      hints := ReducibilityHints.abbrev,
+      safety := if cinfo.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe
+    }
+    addDecl decl
+    compileDecl decl
+    pure name
+| _ => throwUnsupportedSyntax
diff --git a/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictA.lean b/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictA.lean
new file mode 100644
index 000000000000..765e44da843c
--- /dev/null
+++ b/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictA.lean
@@ -0,0 +1,8 @@
+module
+
+prelude
+public import Init.Core
+
+public def foo : Nat := 42
+
+public theorem thm1 : True := if foo = 42 then trivial else trivial
diff --git a/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictA2.lean b/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictA2.lean
new file mode 100644
index 000000000000..0658daa8c435
--- /dev/null
+++ b/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictA2.lean
@@ -0,0 +1,7 @@
+module
+
+prelude
+public import Init.Core
+import LeanCheckerTests.PrivateConflictA
+
+public theorem thm1' : True := thm1
diff --git a/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictB.lean b/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictB.lean
new file mode 100644
index 000000000000..c041472abb66
--- /dev/null
+++ b/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictB.lean
@@ -0,0 +1,8 @@
+module
+
+prelude
+public import Init.Core
+
+public def foo : Nat := 23
+
+public theorem thm2 : True := if foo = 23 then trivial else trivial
diff --git a/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictB2.lean b/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictB2.lean
new file mode 100644
index 000000000000..3bcfbddf26bb
--- /dev/null
+++ b/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictB2.lean
@@ -0,0 +1,7 @@
+module
+
+prelude
+public import Init.Core
+import LeanCheckerTests.PrivateConflictB
+
+public theorem thm2' : True := thm2
diff --git a/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictC.lean b/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictC.lean
new file mode 100644
index 000000000000..b530704efebc
--- /dev/null
+++ b/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictC.lean
@@ -0,0 +1,8 @@
+module
+
+prelude
+public import Init.Core
+import LeanCheckerTests.PrivateConflictA2
+import LeanCheckerTests.PrivateConflictB2
+
+public theorem all  : True ∧ True := .intro thm1' thm2'
diff --git a/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictC.lean.fresh.expected.out b/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictC.lean.fresh.expected.out
new file mode 100644
index 000000000000..fff271355cd0
--- /dev/null
+++ b/tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictC.lean.fresh.expected.out
@@ -0,0 +1 @@
+uncaught exception: import LeanCheckerTests.PrivateConflictB failed, environment already contains 'foo' from LeanCheckerTests.PrivateConflictA
diff --git a/tests/pkg/leanchecker/LeanCheckerTests/QuotEq.lean b/tests/pkg/leanchecker/LeanCheckerTests/QuotEq.lean
new file mode 100644
index 000000000000..b7ec3ed52fd3
--- /dev/null
+++ b/tests/pkg/leanchecker/LeanCheckerTests/QuotEq.lean
@@ -0,0 +1,34 @@
+import Lean
+import LeanChecker.Replay
+
+-- Test: Quot/Eq dependency ordering
+--
+-- Test that `replay` correctly handles the dependency of `Quot` on `Eq`.
+-- `Quot.lift` and `Quot.ind` have types that reference `Eq`, so when replaying
+-- a minimal set of constants that includes `Quot` (via `Quot.sound`), we need
+-- to ensure `Eq` is added to the kernel environment before `quotDecl`.
+--
+-- See https://github.com/leanprover/comparator/issues/1
+
+open Lean
+
+-- Test replaying a minimal set of constants including Quot from a fresh environment.
+-- This exercises the fix for the Quot/Eq dependency ordering issue.
+#eval show IO Unit from do
+  -- Get the current environment which has all the constants we need
+  let env ← importModules #[{ module := `Init }] {}
+
+  -- Build a minimal constant map with just Quot.sound, Eq, and their direct requirements
+  let mut constants : Std.HashMap Name ConstantInfo := {}
+  for name in [`Quot.sound, `Eq, `Eq.refl, `Quot] do
+    if let some ci := env.find? name then
+      constants := constants.insert name ci
+
+  IO.println s!"Constants to replay: {constants.size}"
+
+  -- Replay from a fresh environment - this would fail before the fix
+  -- if Quot was processed before Eq
+  let freshEnv ← mkEmptyEnvironment
+  let _ ← freshEnv.replay' constants
+
+  IO.println "Replay succeeded!"
diff --git a/tests/pkg/leanchecker/LeanCheckerTests/ReplaceAxiom.lean b/tests/pkg/leanchecker/LeanCheckerTests/ReplaceAxiom.lean
new file mode 100644
index 000000000000..fa6a24d7dcdf
--- /dev/null
+++ b/tests/pkg/leanchecker/LeanCheckerTests/ReplaceAxiom.lean
@@ -0,0 +1,37 @@
+import LeanCheckerTests.OpenPrivate
+
+open private Lean.Environment.setCheckedSync from Lean.Environment
+open private Lean.Kernel.Environment.mk from Lean.Environment
+open private Lean.Kernel.Environment.extensions from Lean.Environment
+
+/- Redefine `propext : False`. -/
+open Lean Elab Meta in
+#eval modifyEnv (m := MetaM) fun env =>
+  let consts :=
+    { env.constants with
+        map₁ := env.constants.map₁.insert ``propext (.axiomInfo {
+          name := ``propext
+          type := .const ``False []
+          levelParams := []
+          isUnsafe := false
+        })
+    }
+  let kenv := Lean.Kernel.Environment.mk consts
+    env.toKernelEnv.quotInit
+    env.toKernelEnv.diagnostics
+    env.toKernelEnv.const2ModIdx
+    (Lean.Kernel.Environment.extensions env.toKernelEnv)
+    {}
+    env.header
+  Lean.Environment.setCheckedSync env kenv
+
+theorem efsq : ∀ (x y z n : Nat),
+    0 < x → 0 < y → 0 < z → 2 < n →
+    x^n + y^n ≠ z^n := by
+  exfalso
+  exact propext
+
+/-- info: 'efsq' depends on axioms: [propext] -/
+#guard_msgs in
+-- 'efsq' depends on axioms: [propext]
+#print axioms efsq
diff --git a/tests/pkg/leanchecker/LeanCheckerTests/ReplaceAxiom.lean.expected.out b/tests/pkg/leanchecker/LeanCheckerTests/ReplaceAxiom.lean.expected.out
new file mode 100644
index 000000000000..7f28f566dda1
--- /dev/null
+++ b/tests/pkg/leanchecker/LeanCheckerTests/ReplaceAxiom.lean.expected.out
@@ -0,0 +1,12 @@
+leanchecker found a problem in LeanCheckerTests.ReplaceAxiom
+uncaught exception: (kernel) application type mismatch
+  False.elim @propext
+argument has type
+  ∀ {a b : Prop}, Iff a b → Eq a b
+but function has type
+  False →
+    ∀ (x y z n : Nat),
+      instLTNat.lt 0 x →
+        instLTNat.lt 0 y →
+          instLTNat.lt 0 z →
+            instLTNat.lt 2 n → Ne (instHAdd.hAdd (instHPow.hPow x n) (instHPow.hPow y n)) (instHPow.hPow z n)
diff --git a/tests/pkg/leanchecker/lakefile.toml b/tests/pkg/leanchecker/lakefile.toml
new file mode 100644
index 000000000000..6d28ac2a9a25
--- /dev/null
+++ b/tests/pkg/leanchecker/lakefile.toml
@@ -0,0 +1,6 @@
+name = "leanchecker_test"
+defaultTargets = ["LeanCheckerTests"]
+
+[[lean_lib]]
+name = "LeanCheckerTests"
+globs = ["LeanCheckerTests.+"]
diff --git a/tests/pkg/leanchecker/lean-toolchain b/tests/pkg/leanchecker/lean-toolchain
new file mode 100644
index 000000000000..dcca6df980de
--- /dev/null
+++ b/tests/pkg/leanchecker/lean-toolchain
@@ -0,0 +1 @@
+lean4
diff --git a/tests/pkg/leanchecker/test.sh b/tests/pkg/leanchecker/test.sh
new file mode 100755
index 000000000000..0bc0fb0ed47f
--- /dev/null
+++ b/tests/pkg/leanchecker/test.sh
@@ -0,0 +1,35 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+rm -rf .lake/build
+lake build
+
+for f in LeanCheckerTests/*.lean; do
+    # It would be nicer if `common.sh` did not hardcode a single input file
+    set -- "$f"
+    source ../../common.sh
+
+    module="LeanCheckerTests.$(basename "$f" .lean)"
+    # Check for --fresh mode test
+    if [ -f "$f.fresh.expected.out" ]; then
+        # Test --fresh mode (expect failure)
+        expected_ret=1
+        exec_check lake env leanchecker --fresh "$module"
+        # Use fresh expected output for comparison
+        mv "$f.produced.out" "$f.fresh.produced.out"
+        f_save="$f"
+        f="$f.fresh"
+        diff_produced
+        f="$f_save"
+    # Check for normal mode test
+    elif [ -f "$f.expected.out" ]; then
+        # Expect failure with specific output
+        expected_ret=1
+        exec_check lake env leanchecker "$module"
+        diff_produced
+    else
+        # No expected output files - expect success (exit 0)
+        expected_ret=0
+        exec_check_raw lake env leanchecker "$module"
+    fi
+done