diff --git a/src/Lean/Linter.lean b/src/Lean/Linter.lean
index 5933f053f300..7f0dcc64176b 100644
--- a/src/Lean/Linter.lean
+++ b/src/Lean/Linter.lean
@@ -19,3 +19,4 @@ public import Lean.Linter.Sets
 public import Lean.Linter.UnusedSimpArgs
 public import Lean.Linter.Coe
 public import Lean.Linter.GlobalAttributeIn
+public import Lean.Linter.EnvLinter
diff --git a/src/Lean/Linter/EnvLinter.lean b/src/Lean/Linter/EnvLinter.lean
new file mode 100644
index 000000000000..959cbc78b780
--- /dev/null
+++ b/src/Lean/Linter/EnvLinter.lean
@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public import Lean.Linter.EnvLinter.Basic
+public import Lean.Linter.EnvLinter.Frontend
diff --git a/src/Lean/Linter/EnvLinter/Basic.lean b/src/Lean/Linter/EnvLinter/Basic.lean
new file mode 100644
index 000000000000..520fb8a0f895
--- /dev/null
+++ b/src/Lean/Linter/EnvLinter/Basic.lean
@@ -0,0 +1,163 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
+-/
+module
+
+prelude
+public import Lean.Structure
+public import Lean.Elab.InfoTree.Main
+import Lean.ExtraModUses
+
+public section
+
+open Lean Meta
+
+namespace Lean.Linter.EnvLinter
+
+/-!
+# Basic environment linter types and attributes
+
+This file defines the basic types and attributes used by the environment
+linting framework. An environment linter consists of a function
+`(declaration : Name) → MetaM (Option MessageData)`, this function together with some
+metadata is stored in the `EnvLinter` structure. We define two attributes:
+
+ * `@[builtin_env_linter]` applies to a declaration of type `EnvLinter`
+   and adds it to the default linter set.
+
+ * `@[builtin_nolint linterName]` omits the tagged declaration from being checked by
+   the linter with name `linterName`.
+-/
+
+/--
+Returns true if `decl` is an automatically generated declaration.
+
+Also returns true if `decl` is an internal name or created during macro
+expansion.
+-/
+def isAutoDecl (decl : Name) : CoreM Bool := do
+  if decl.hasMacroScopes then return true
+  if decl.isInternal then return true
+  let env ← getEnv
+  if isReservedName env decl then return true
+  if let Name.str n s := decl then
+    if (← isAutoDecl n) then return true
+    if s.startsWith "proof_"
+        || s.startsWith "match_"
+        || s.startsWith "unsafe_"
+        || s.startsWith "grind_"
+    then return true
+    if env.isConstructor n && s ∈ ["injEq", "inj", "sizeOf_spec", "elim", "noConfusion"] then
+      return true
+    if let ConstantInfo.inductInfo _ := env.find? n then
+      if s.startsWith "brecOn_" || s.startsWith "below_" then return true
+      if s ∈ [casesOnSuffix, recOnSuffix, brecOnSuffix, belowSuffix,
+          "ndrec", "ndrecOn", "noConfusionType", "noConfusion", "ofNat", "toCtorIdx", "ctorIdx",
+          "ctorElim", "ctorElimType"] then
+        return true
+      if let some _ := isSubobjectField? env n (.mkSimple s) then
+        return true
+    -- Coinductive/inductive lattice-theoretic predicates:
+    if let ConstantInfo.inductInfo _ := env.find? (Name.str n "_functor") then
+      if s == "functor_unfold" || s == casesOnSuffix || s == "mutual" then return true
+      if env.isConstructor (Name.str (Name.str n "_functor") s) then return true
+  pure false
+
+/-- An environment linting test for the `lake builtin-lint` command. -/
+structure EnvLinter where
+  /-- `test` defines a test to perform on every declaration. It should never fail. Returning `none`
+  signifies a passing test. Returning `some msg` reports a failing test with error `msg`. -/
+  test : Name → MetaM (Option MessageData)
+  /-- `noErrorsFound` is the message printed when all tests are negative -/
+  noErrorsFound : MessageData
+  /-- `errorsFound` is printed when at least one test is positive -/
+  errorsFound : MessageData
+  /-- If `isDefault` is false, this linter is only run when `--clippy` is passed. -/
+  isDefault := true
+
+/-- A `NamedEnvLinter` is an environment linter associated to a particular declaration. -/
+structure NamedEnvLinter extends EnvLinter where
+  /-- The name of the named linter. This is just the declaration name without the namespace. -/
+  name : Name
+  /-- The linter declaration name -/
+  declName : Name
+
+/-- Gets an environment linter by declaration name. -/
+def getEnvLinter (name declName : Name) : CoreM NamedEnvLinter := unsafe
+  return { ← evalConstCheck EnvLinter ``EnvLinter declName with name, declName }
+
+/-- Defines the `envLinterExt` extension for adding an environment linter to the default set. -/
+builtin_initialize envLinterExt :
+    SimplePersistentEnvExtension (Name × Bool) (NameMap (Name × Bool)) ←
+  let addEntryFn := fun m (n, b) => m.insert (n.updatePrefix .anonymous) (n, b)
+  registerSimplePersistentEnvExtension {
+    addImportedFn := fun nss =>
+      nss.foldl (init := {}) fun m ns => ns.foldl (init := m) addEntryFn
+    addEntryFn
+  }
+
+/--
+Defines the `@[builtin_env_linter]` attribute for adding a linter to the default set.
+The form `@[builtin_env_linter clippy]` will not add the linter to the default set,
+but it can be selected by `lake builtin-lint --clippy`.
+
+Linters are named using their declaration names, without the namespace. These must be distinct.
+-/
+syntax (name := builtin_env_linter) "builtin_env_linter" &" clippy"? : attr
+
+builtin_initialize registerBuiltinAttribute {
+  name := `builtin_env_linter
+  descr := "Use this declaration as a linting test in `lake builtin-lint`"
+  add   := fun decl stx kind => do
+    let dflt := stx[1].isNone
+    unless kind == .global do throwError "invalid attribute `builtin_env_linter`, must be global"
+    let shortName := decl.updatePrefix .anonymous
+    if let some (declName, _) := (envLinterExt.getState (← getEnv)).find? shortName then
+      Elab.addConstInfo stx declName
+      throwError
+        "invalid attribute `builtin_env_linter`, linter `{shortName}` has already been declared"
+    let isPublic := !isPrivateName decl; let isMeta := isMarkedMeta (← getEnv) decl
+    unless isPublic && isMeta do
+      throwError "invalid attribute `builtin_env_linter`, \
+        declaration `{.ofConstName decl}` must be marked as `public` and `meta`\
+        {if isPublic then " but is only marked `public`" else ""}\
+        {if isMeta then " but is only marked `meta`" else ""}"
+    let constInfo ← getConstInfo decl
+    unless ← (isDefEq constInfo.type (mkConst ``EnvLinter)).run' do
+      throwError "`{.ofConstName decl}` must have type `{.ofConstName ``EnvLinter}`, got \
+        `{constInfo.type}`"
+    modifyEnv fun env => envLinterExt.addEntry env (decl, dflt)
+}
+
+/-- `@[builtin_nolint linterName]` omits the tagged declaration from being checked by
+the linter with name `linterName`. -/
+syntax (name := builtin_nolint) "builtin_nolint" (ppSpace ident)+ : attr
+
+/-- Defines the user attribute `builtin_nolint` for skipping environment linters. -/
+builtin_initialize builtinNolintAttr : ParametricAttribute (Array Name) ←
+  registerParametricAttribute {
+    name := `builtin_nolint
+    descr := "Do not report this declaration in any of the tests of `lake builtin-lint`"
+    getParam := fun _ => fun
+      | `(attr| builtin_nolint $[$ids]*) => ids.mapM fun id => withRef id <| do
+        let shortName := id.getId.eraseMacroScopes
+        let some (declName, _) := (envLinterExt.getState (← getEnv)).find? shortName
+          | throwError "linter '{shortName}' not found"
+        Elab.addConstInfo id declName
+        recordExtraModUseFromDecl (isMeta := false) declName
+        pure shortName
+      | _ => Elab.throwUnsupportedSyntax
+  }
+
+/-- Returns true if `decl` should be checked
+using `linter`, i.e., if there is no `builtin_nolint` attribute. -/
+def shouldBeLinted [Monad m] [MonadEnv m] (linter : Name) (decl : Name) : m Bool :=
+  return !((builtinNolintAttr.getParam? (← getEnv) decl).getD #[]).contains linter
+
+end Lean.Linter.EnvLinter
diff --git a/src/Lean/Linter/EnvLinter/Frontend.lean b/src/Lean/Linter/EnvLinter/Frontend.lean
new file mode 100644
index 000000000000..61586960ba0f
--- /dev/null
+++ b/src/Lean/Linter/EnvLinter/Frontend.lean
@@ -0,0 +1,180 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Robert Y. Lewis, Gabriel Ebner
+-/
+module
+
+prelude
+public import Lean.Linter.EnvLinter.Basic
+import Lean.DeclarationRange
+import Lean.Util.Path
+import Lean.CoreM
+import Lean.Elab.Command
+
+public section
+
+open Lean Meta
+
+namespace Lean.Linter.EnvLinter
+
+/-- Verbosity for the linter output. -/
+inductive LintVerbosity
+  /-- `low`: only print failing checks, print nothing on success. -/
+  | low
+  /-- `medium`: only print failing checks, print confirmation on success. -/
+  | medium
+  /-- `high`: print output of every check. -/
+  | high
+  deriving Inhabited, DecidableEq, Repr
+
+/-- `getChecks clippy runOnly` produces a list of linters.
+`runOnly` is an optional list of names that should resolve to declarations with type
+`NamedEnvLinter`. If populated, only these linters are run (regardless of the default
+configuration). Otherwise, it uses all enabled linters in the environment tagged with
+`@[builtin_env_linter]`. If `clippy` is false, it only uses linters with `isDefault = true`. -/
+def getChecks (clippy : Bool) (runOnly : Option (List Name)) :
+    CoreM (Array NamedEnvLinter) := do
+  let mut result := #[]
+  for (name, declName, isDefault) in envLinterExt.getState (← getEnv) do
+    let shouldRun := match runOnly with
+      | some only => only.contains name
+      | none => clippy || isDefault
+    if shouldRun then
+      let linter ← getEnvLinter name declName
+      result := result.binInsert (·.name.lt ·.name) linter
+  pure result
+
+
+/--
+Runs all the specified linters on all the specified declarations in parallel,
+producing a list of results.
+-/
+def lintCore (decls : Array Name) (linters : Array NamedEnvLinter) :
+    CoreM (Array (NamedEnvLinter × Std.HashMap Name MessageData)) := do
+  let tasks : Array (NamedEnvLinter × Array (Name × Task (Except Exception <| Option MessageData))) ←
+    linters.mapM fun linter => do
+      let decls ← decls.filterM (shouldBeLinted linter.name)
+      (linter, ·) <$> decls.mapM fun decl => (decl, ·) <$> do
+        let act : MetaM (Option MessageData) := do
+          linter.test decl
+        EIO.asTask <| (← Core.wrapAsync (fun _ =>
+          act |>.run' Elab.Command.mkMetaContext
+        ) (cancelTk? := none)) ()
+
+  let result ← tasks.mapM fun (linter, decls) => do
+    let mut msgs : Std.HashMap Name MessageData := {}
+    for (declName, msgTask) in decls do
+      let msg? ← match msgTask.get with
+      | Except.ok msg? => pure msg?
+      | Except.error err => pure m!"LINTER FAILED:\n{err.toMessageData}"
+      if let .some msg := msg? then
+        msgs := msgs.insert declName msg
+    pure (linter, msgs)
+  return result
+
+/-- Sorts a map with declaration keys as names by line number. -/
+def sortResults (results : Std.HashMap Name α) : CoreM <| Array (Name × α) := do
+  let mut key : Std.HashMap Name Nat := {}
+  for (n, _) in results.toArray do
+    if let some range ← findDeclarationRanges? n then
+      key := key.insert n <| range.range.pos.line
+  pure $ results.toArray.qsort fun (a, _) (b, _) => key.getD a 0 < key.getD b 0
+
+/-- Formats a linter warning as `#check` command with comment. -/
+def printWarning (declName : Name) (warning : MessageData) (useErrorFormat : Bool := false)
+  (filePath : System.FilePath := default) : CoreM MessageData := do
+  if useErrorFormat then
+    if let some range ← findDeclarationRanges? declName then
+      let msg ← addMessageContextPartial
+        m!"{filePath}:{range.range.pos.line}:{range.range.pos.column + 1}: error: {
+          ← mkConstWithLevelParams declName} {warning}"
+      return msg
+  addMessageContextPartial m!"#check {← mkConstWithLevelParams declName} /- {warning} -/"
+
+/-- Formats a map of linter warnings using `printWarning`, sorted by line number. -/
+def printWarnings (results : Std.HashMap Name MessageData) (filePath : System.FilePath := default)
+    (useErrorFormat : Bool := false) : CoreM MessageData := do
+  (MessageData.joinSep ·.toList Format.line) <$>
+    (← sortResults results).mapM fun (declName, warning) =>
+      printWarning declName warning (useErrorFormat := useErrorFormat) (filePath := filePath)
+
+/--
+Formats a map of linter warnings grouped by filename with `-- filename` comments.
+-/
+def groupedByFilename (results : Std.HashMap Name MessageData) (useErrorFormat : Bool := false) :
+    CoreM MessageData := do
+  let sp ← if useErrorFormat then getSrcSearchPath else pure {}
+  let grouped : Std.HashMap Name (System.FilePath × Std.HashMap Name MessageData) ←
+    results.foldM (init := {}) fun grouped declName msg => do
+      let mod ← findModuleOf? declName
+      let mod := mod.getD (← getEnv).mainModule
+      grouped.insert mod <$>
+        match grouped[mod]? with
+        | some (fp, msgs) => pure (fp, msgs.insert declName msg)
+        | none => do
+          let fp ← if useErrorFormat then
+            pure <| (← sp.findWithExt "lean" mod).getD (modToFilePath "." mod "lean")
+          else pure default
+          pure (fp, .insert {} declName msg)
+  let grouped' := grouped.toArray.qsort fun (a, _) (b, _) => toString a < toString b
+  (MessageData.joinSep · (Format.line ++ Format.line)) <$>
+    grouped'.toList.mapM fun (mod, fp, msgs) => do
+      pure m!"-- {mod}\n{← printWarnings msgs (filePath := fp) (useErrorFormat := useErrorFormat)}"
+
+/--
+Formats the linter results as Lean code with comments and `#check` commands.
+-/
+def formatLinterResults
+    (results : Array (NamedEnvLinter × Std.HashMap Name MessageData))
+    (decls : Array Name)
+    (groupByFilename : Bool)
+    (whereDesc : String) (runClippyLinters : Bool)
+    (verbose : LintVerbosity) (numLinters : Nat) (useErrorFormat : Bool := false) :
+    CoreM MessageData := do
+  let formattedResults ← results.filterMapM fun (linter, results) => do
+    if !results.isEmpty then
+      let warnings ←
+        if groupByFilename || useErrorFormat then
+          groupedByFilename results (useErrorFormat := useErrorFormat)
+        else
+          printWarnings results
+      pure $ some m!"/- The `{linter.name}` linter reports:\n{linter.errorsFound} -/\n{warnings}\n"
+    else if verbose = LintVerbosity.high then
+      pure $ some m!"/- OK: {linter.noErrorsFound} -/"
+    else
+      pure none
+  let mut s := MessageData.joinSep formattedResults.toList Format.line
+  let numAutoDecls := (← decls.filterM isAutoDecl).size
+  let failed := results.map (·.2.size) |>.foldl (·+·) 0
+  unless verbose matches LintVerbosity.low do
+    s := m!"-- Found {failed} error{if failed == 1 then "" else "s"
+      } in {decls.size - numAutoDecls} declarations (plus {
+      numAutoDecls} automatically generated ones) {whereDesc
+      } with {numLinters} linters\n\n{s}"
+  unless runClippyLinters do s := m!"{s}-- (non-clippy linters skipped)\n"
+  pure s
+
+/-- Get the list of declarations in the current module. -/
+def getDeclsInCurrModule : CoreM (Array Name) := do
+  pure $ (← getEnv).constants.map₂.foldl (init := #[]) fun r k _ => r.push k
+
+/-- Get the list of all declarations in the environment. -/
+def getAllDecls : CoreM (Array Name) := do
+  pure $ (← getEnv).constants.map₁.fold (init := ← getDeclsInCurrModule) fun r k _ => r.push k
+
+/-- Get the list of all declarations in the specified package. -/
+def getDeclsInPackage (pkg : Name) : CoreM (Array Name) := do
+  let env ← getEnv
+  let mut decls ← getDeclsInCurrModule
+  let modules := env.header.moduleNames.map (pkg.isPrefixOf ·)
+  return env.constants.map₁.fold (init := decls) fun decls declName _ =>
+    if modules[env.const2ModIdx[declName]?.get!]! then
+      decls.push declName
+    else decls
+
+end Lean.Linter.EnvLinter
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index e44444704908..a3147b4d3f63 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,5 @@
 #include "util/options.h"
-
+// Please update stage0
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/elab/env_linter.lean b/tests/elab/env_linter.lean
new file mode 100644
index 000000000000..13d2e20bce3c
--- /dev/null
+++ b/tests/elab/env_linter.lean
@@ -0,0 +1,226 @@
+import Lean
+
+open Lean Linter EnvLinter Meta
+
+/-! ## Dummy env linter for testing -/
+
+/-- A dummy linter that flags any declaration whose last name component starts with "bad". -/
+@[builtin_env_linter]
+public meta def dummyBadName : EnvLinter where
+  test declName := do
+    if let .str _ s := declName then
+      if s.startsWith "bad" then
+        return some m!"declaration name starts with 'bad'"
+    return none
+  noErrorsFound := "no bad names found"
+  errorsFound := "found bad names"
+
+/-! ## Test: extension registration -/
+
+def testExtContains (name : Name) : CoreM Bool := do
+  let ext := envLinterExt.getState (← getEnv)
+  return ext.contains name
+
+/-- info: true -/
+#guard_msgs in
+#eval testExtContains `dummyBadName
+
+/-- info: false -/
+#guard_msgs in
+#eval testExtContains `nonexistentLinter
+
+/-! ## Test: getEnvLinter resolves the linter -/
+
+def testResolveLinter : CoreM String := do
+  let some (declName, _) := (envLinterExt.getState (← getEnv)).find? `dummyBadName
+    | throwError "not found"
+  let linter ← getEnvLinter `dummyBadName declName
+  return toString linter.name
+
+/-- info: "dummyBadName" -/
+#guard_msgs in
+#eval testResolveLinter
+
+/-! ## Test: dummy linter detects bad names -/
+
+def badDef : Nat := 42
+def goodDef : Nat := 42
+
+def testLinterDetects (declName : Name) : MetaM Bool := do
+  let some (linterDeclName, _) := (envLinterExt.getState (← getEnv)).find? `dummyBadName
+    | throwError "not found"
+  let linter ← getEnvLinter `dummyBadName linterDeclName
+  return (← linter.test declName).isSome
+
+/-- info: true -/
+#guard_msgs in
+#eval testLinterDetects `badDef
+
+/-- info: false -/
+#guard_msgs in
+#eval testLinterDetects `goodDef
+
+/-! ## Test: builtin_nolint -/
+
+@[builtin_nolint dummyBadName]
+def badButNolinted : Nat := 99
+
+def testShouldBeLinted (linter decl : Name) : CoreM Bool := do
+  shouldBeLinted linter decl
+
+/-- info: false -/
+#guard_msgs in
+#eval testShouldBeLinted `dummyBadName `badButNolinted
+
+/-- info: true -/
+#guard_msgs in
+#eval testShouldBeLinted `dummyBadName `badDef
+
+/-! ## Test: builtin_env_linter clippy -/
+
+@[builtin_env_linter clippy]
+public meta def dummyClippyLinter : EnvLinter where
+  test _ := return none
+  noErrorsFound := "ok"
+  errorsFound := "err"
+
+-- The extension stores (declName, isDefault). Clippy-only means isDefault = false.
+
+def testIsDefault (name : Name) : CoreM (Option Bool) := do
+  let ext := envLinterExt.getState (← getEnv)
+  match ext.find? name with
+  | some (_, isDefault) => return some isDefault
+  | none => return none
+
+/-- info: some false -/
+#guard_msgs in
+#eval testIsDefault `dummyClippyLinter
+
+/-- info: some true -/
+#guard_msgs in
+#eval testIsDefault `dummyBadName
+
+/-! ## Test: duplicate linter name is rejected -/
+
+/--
+error: invalid attribute `builtin_env_linter`, linter `dummyBadName` has already been declared
+-/
+#guard_msgs in
+@[builtin_env_linter] public meta def Other.dummyBadName : EnvLinter :=
+  { test := fun _ => return none, noErrorsFound := "", errorsFound := "" }
+
+/-! ## Test: isAutoDecl -/
+
+/-- info: true -/
+#guard_msgs in
+#eval isAutoDecl `Nat.casesOn
+
+/-- info: true -/
+#guard_msgs in
+#eval isAutoDecl `Nat.recOn
+
+/-- info: false -/
+#guard_msgs in
+#eval isAutoDecl `Nat.add
+
+/-! ## Test: getChecks -/
+
+-- Default mode: only isDefault=true linters
+def testGetChecksDefault : CoreM (Array Name) := do
+  let checks ← getChecks (clippy := false) (runOnly := none)
+  return checks.map (·.name)
+
+-- dummyBadName is default, dummyClippyLinter is not
+/-- info: #[`dummyBadName] -/
+#guard_msgs in
+#eval testGetChecksDefault
+
+-- Clippy mode: all linters
+def testGetChecksClippy : CoreM (Array Name) := do
+  let checks ← getChecks (clippy := true) (runOnly := none)
+  return checks.map (·.name)
+
+/-- info: #[`dummyBadName, `dummyClippyLinter] -/
+#guard_msgs in
+#eval testGetChecksClippy
+
+-- runOnly: only specified linters
+def testGetChecksRunOnly : CoreM (Array Name) := do
+  let checks ← getChecks (clippy := false) (runOnly := some [`dummyClippyLinter])
+  return checks.map (·.name)
+
+/-- info: #[`dummyClippyLinter] -/
+#guard_msgs in
+#eval testGetChecksRunOnly
+
+/-! ## Test: getDeclsInCurrModule -/
+
+def testDeclsInCurrModule : CoreM Bool := do
+  let decls ← getDeclsInCurrModule
+  -- Our test declarations should be in the current module
+  return decls.contains `badDef && decls.contains `goodDef && decls.contains `badButNolinted
+
+/-- info: true -/
+#guard_msgs in
+#eval testDeclsInCurrModule
+
+/-! ## Test: lintCore -/
+
+-- lintCore should find badDef but not goodDef or badButNolinted
+def testLintCore : CoreM (Array (Name × Nat)) := do
+  let linters ← getChecks (clippy := false) (runOnly := none)
+  let results ← lintCore #[`badDef, `goodDef, `badButNolinted] linters
+  return results.map fun (linter, msgs) => (linter.name, msgs.size)
+
+/-- info: #[(`dummyBadName, 1)] -/
+#guard_msgs in
+#eval testLintCore
+
+-- Verify which declaration was flagged
+def testLintCoreDetail : CoreM (Array Name) := do
+  let linters ← getChecks (clippy := false) (runOnly := none)
+  let results ← lintCore #[`badDef, `goodDef, `badButNolinted] linters
+  let mut flagged := #[]
+  for (_, msgs) in results do
+    for (name, _) in msgs.toArray do
+      flagged := flagged.push name
+  return flagged
+
+/-- info: #[`badDef] -/
+#guard_msgs in
+#eval testLintCoreDetail
+
+/-! ## Test: formatLinterResults -/
+
+def testFormatResults : CoreM Format := do
+  let linters ← getChecks (clippy := false) (runOnly := none)
+  let results ← lintCore #[`badDef, `goodDef] linters
+  let msg ← formatLinterResults results #[`badDef, `goodDef]
+    (groupByFilename := false) (whereDesc := "in test") (runClippyLinters := true)
+    (verbose := .medium) (numLinters := linters.size)
+  return (← msg.format)
+
+/--
+info: -- Found 1 error in 2 declarations (plus 0 automatically generated ones) in test with 1 linters
+
+/- The `dummyBadName` linter reports:
+found bad names -/
+#check badDef /- declaration name starts with 'bad' -/
+-/
+#guard_msgs in
+#eval testFormatResults
+
+-- No errors case
+def testFormatResultsClean : CoreM Format := do
+  let linters ← getChecks (clippy := false) (runOnly := none)
+  let results ← lintCore #[`goodDef] linters
+  let msg ← formatLinterResults results #[`goodDef]
+    (groupByFilename := false) (whereDesc := "in test") (runClippyLinters := true)
+    (verbose := .medium) (numLinters := linters.size)
+  return (← msg.format)
+
+/--
+info: -- Found 0 errors in 1 declarations (plus 0 automatically generated ones) in test with 1 linters
+-/
+#guard_msgs in
+#eval testFormatResultsClean