feat: add @[trusted_axiom] attribute and linter.untrustedAxioms linter

src/Lean/AddDecl.lean

@@ -192,6 +192,7 @@ where
           -- avoid follow-up errors by (trying to) add broken decl as axiom
           addAsAxiom
           throw ex
+        recordAxioms decl
   addAsAxiom := do
     -- try to add as axiom with given type for def/theorem
     match decl with

src/Lean/Elab/MutualDef.lean

@@ -7,6 +7,7 @@ module
 prelude
 public import Lean.Elab.Deriving.Basic
 public import Lean.Elab.PreDefinition.Main
+import Lean.TrustedAxiomAttr
 import all Lean.Elab.ErrorUtils
 public section
 namespace Lean.Elab
@@ -1441,6 +1442,14 @@ this warning can be disabled with `set_option warn.classDefReducibility false`."
       addPreDefinitions docCtx preDefs
     for view in views, funFVar in funFVars do
       addLocalVarInfo view.declId funFVar
+    if linter.untrustedAxioms.get (← getOptions) then
+      -- lint on the kernel-check chain so that `collectAxioms` does not block elaboration
+      let act ← Core.wrapAsyncAsSnapshot (cancelTk? := none)
+          (desc := s!"linting axioms of {headers.map (·.declName)}") fun _ =>
+        for header in headers do
+          withRef header.declId <| warnIfUsesUntrustedAxioms header.declName
+      let task ← BaseIO.mapTask act (← getEnv).checked
+      Core.logSnapshotTask { stx? := none, reportingRange := .skip, cancelTk? := none, task }
 
   processDeriving (headers : Array DefViewElabHeader) := do
     for header in headers, view in views do

src/Lean/TrustedAxiomAttr.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+module
+
+prelude
+public import Lean.Attributes
+import Lean.Util.CollectAxioms
+import Lean.Util.Sorry
+import Lean.Linter.Init
+import Lean.AddDecl
+
+namespace Lean
+
+/--
+Marks an axiom as "trusted" so that the `linter.untrustedAxioms` linter does not warn about
+declarations depending on axioms tagged with this attribute.
+-/
+@[builtin_doc]
+public builtin_initialize trustedAxiomAttr : TagAttribute ←
+  registerTagAttribute `trusted_axiom "mark an axiom as trusted so that `linter.untrustedAxioms` does not warn about declarations depending on it" fun declName => do
+    unless getOriginalConstKind? (← getEnv) declName matches some .axiom do
+      throwError "Cannot add attribute `@[trusted_axiom]` to non-axiom `{.ofConstName declName}`"
+
+public register_builtin_option linter.untrustedAxioms : Bool := {
+  defValue := false
+  descr    := "Warn when a declaration added to the environment depends on an axiom that is not \
+    tagged with `@[trusted_axiom]`. This should be considered a preliminary elaboration-side \
+    check that does not replace the use of external checker tools such as `comparator` with \
+    their own axiom checks. Unlike other linters, this linter is not enabled by `linter.all` \
+    but only by setting this option explicitly, as it is useful only with a curated set of \
+    `@[trusted_axiom]` declarations."
+}
+
+open Linter in
+public def warnIfUsesUntrustedAxioms (declName : Name) : CoreM Unit := do
+  unless linter.untrustedAxioms.get (← getOptions) do return
+  if (← MonadLog.hasErrors) then return
+  let env ← getEnv
+  let some info := env.find? declName | return
+  if info.isUnsafe then return
+  let axioms ← collectAxioms declName
+  -- Check the axioms first: a syntactic `sorry` always shows up as `sorryAx` in them, so we can
+  -- avoid the `hasSorry` term traversal for sorry-free declarations.
+  if axioms.contains ``sorryAx && warn.sorry.get (← getOptions) &&
+      (info.type.hasSorry || (info.value? (allowOpaque := true)).any (·.hasSorry)) then
+    return
+  let offending := axioms.filter (!trustedAxiomAttr.hasTag env ·)
+  unless offending.isEmpty do
+    let axMsgs := offending.toList.map fun ax => m!"`{MessageData.ofConstName ax}`"
+    logLint linter.untrustedAxioms (← getRef)
+      m!"declaration depends on axioms that are not tagged \
+        `@[trusted_axiom]`: {MessageData.joinSep axMsgs ", "}"
+
+end Lean

src/Lean/Util/CollectAxioms.lean

@@ -13,7 +13,11 @@ namespace Lean
 namespace CollectAxioms
 
 structure State where
-  /-- Cache mapping constants to their (sorted) axiom dependencies. -/
+  /--
+  Cache mapping constants walked by this run to their (sorted) axiom dependencies. Constants
+  answered by `extFind?` are deliberately not copied into this layer, so it contains exactly the
+  constants whose dependencies were not already recorded elsewhere.
+  -/
   seen   : NameMap (Array Name) := {}
   /-- Axioms accumulated for the current constant being processed. -/
   axioms : NameSet := {}
@@ -28,7 +32,8 @@ private def insertArray (s : NameSet) (axs : Array Name) : NameSet :=
 
 /--
 Collect axioms reachable from constant `c`, using `extFind?` to look up pre-computed axioms
-for imported declarations. Results are cached in `State.seen`.
+for imported and already-recorded declarations. Results for walked constants are cached in
+`State.seen`, the second layer of the cache on top of `extFind?`.
 
 When processing a constant not found in `extFind?` or the cache, the function temporarily
 clears the axiom accumulator, recurses into the constant's dependencies, caches the result
@@ -38,9 +43,9 @@ private partial def collect
     (extFind? : Environment → Name → Option (Array Name))
     (c : Name) : M Unit := do
   let env ← read
-  -- Check extension for pre-computed axioms (imported declarations)
+  -- Check extension for pre-computed axioms (imported and already-recorded declarations)
   if let some axs := extFind? env c then
-    modify fun s => { s with axioms := insertArray s.axioms axs, seen := s.seen.insert c axs }
+    modify fun s => { s with axioms := insertArray s.axioms axs }
     return
   -- Check local cache
   let s ← get
@@ -77,6 +82,8 @@ private partial def collect
 private def collectAndGet
     (extFind? : Environment → Name → Option (Array Name))
     (c : Name) : M (Array Name) := do
+  if let some axs := extFind? (← read) c then
+    return axs
   collect extFind? c
   let some axs := (← get).seen.find? c | panic! s!"collectAndGet: '{c}' not in seen after collect"
   return axs
@@ -95,10 +102,12 @@ binary search without requiring the extension object.
 -/
 private structure ExportedAxiomsState where
   importedModuleEntries : Array (Array (Name × Array Name)) := #[]
+  /-- Axiom dependencies of current-module declarations, filled eagerly by `recordAxioms`. -/
+  localEntries : NameMap (Array Name) := {}
 
 instance : Inhabited ExportedAxiomsState := ⟨{}⟩
 
-/-- Look up pre-computed axioms for an imported declaration. -/
+/-- Look up pre-computed axioms for an imported or already-recorded local declaration. -/
 private def ExportedAxiomsState.find? (s : ExportedAxiomsState) (env : Environment)
     (c : Name) : Option (Array Name) :=
   match env.getModuleIdxFor? c with
@@ -108,14 +117,17 @@ private def ExportedAxiomsState.find? (s : ExportedAxiomsState) (env : Environme
       | some entry => some entry.2
       | none       => none
     else none
-  | none => none
+  | none => s.localEntries.find? c
 
 /--
 Environment extension that records axiom dependencies for all declarations in a module.
-Entries are computed once by `beforeExportFn` when the olean is serialized, not during
-elaboration. During elaboration, `collectAxioms` walks bodies directly. Downstream modules
-look up pre-computed entries for imported declarations, so axiom collection never crosses
-module boundaries.
+Entries for the current module are filled eagerly by `recordAxioms` as declarations pass the
+kernel; the `sync` mode makes these writes accumulate along the `checked` environment chain so
+that recording a declaration reuses the entries of all prior declarations. When the olean is
+serialized, `exportEntriesFnEx` exports the entries of all exported declarations, computing any
+entry missing due to e.g. realizations or error recovery. Downstream modules look up
+pre-computed entries for imported declarations, so axiom collection never crosses module
+boundaries.
 -/
 private builtin_initialize exportedAxiomsExt :
     PersistentEnvExtension (Name × Array Name) (Name × Array Name) ExportedAxiomsState ←
@@ -142,14 +154,38 @@ private builtin_initialize exportedAxiomsExt :
       -- Sort by name for binary search at import time.
       let entries := entries.qsort fun a b => Name.quickLt a.1 b.1
       .uniform entries
-    asyncMode     := .mainOnly
+    asyncMode     := .sync
   }
 
+/--
+Computes and records the axiom dependencies of the given just-added declaration into
+`exportedAxiomsExt`. Entries recorded for earlier declarations are reused, so each constant is
+walked only once per module. Skipped in realization contexts, which would require extension
+replay; declarations without an entry are walked on demand by `collectAxioms` instead.
+-/
+public def recordAxioms [Monad m] [MonadEnv m] (decl : Declaration) : m Unit := do
+  let env ← getEnv
+  if env.isRealizing then return
+  let privateEnv := env.setExporting false
+  let s := exportedAxiomsExt.getState env
+  let (_, st) := decl.getTopLevelNames.mapM (CollectAxioms.collectAndGet s.find?)
+    |>.run privateEnv |>.run {}
+  -- `seen` contains exactly the walked constants; skip walked imported constants missing from
+  -- the export table, which `find?` could never answer from `localEntries`.
+  let newEntries := st.seen.foldl (init := #[]) fun acc c axs =>
+    if (env.getModuleIdxFor? c).isNone then
+      acc.push (c, axs)
+    else
+      acc
+  unless newEntries.isEmpty do
+    modifyEnv fun env => exportedAxiomsExt.modifyState env fun s =>
+      { s with localEntries := newEntries.foldl (init := s.localEntries) fun m (c, axs) => m.insert c axs }
+
 /-- Collect all axioms transitively used by a constant. -/
 public def collectAxioms [Monad m] [MonadEnv m] (constName : Name) : m (Array Name) := do
   let env ← getEnv
   let privateEnv := env.setExporting false
-  let s := exportedAxiomsExt.getState (asyncMode := .mainOnly) env
+  let s := exportedAxiomsExt.getState env
   return CollectAxioms.runM privateEnv do
     CollectAxioms.collectAndGet s.find? constName
 

tests/elab/linterUntrustedAxioms.lean

@@ -0,0 +1,153 @@
+/-!
+Tests the `@[trusted_axiom]` attribute and the `linter.untrustedAxioms` linter, which warns when a
+declaration transitively depends on an axiom not tagged `@[trusted_axiom]`.
+-/
+
+axiom untrustedAx : 1 = 2
+
+@[trusted_axiom] axiom trustedAx : 1 = 1
+
+-- The linter is off by default.
+#guard_msgs in
+theorem offByDefault : 1 = 2 := untrustedAx
+
+-- `linter.all` does not enable this linter; it must be enabled explicitly.
+set_option linter.all true in
+#guard_msgs in
+theorem allDoesNotEnable : 1 = 2 := untrustedAx
+
+set_option linter.untrustedAxioms true
+
+/-! Axiom declarations themselves are not linted, only their uses. -/
+
+#guard_msgs in
+axiom anotherUntrustedAx : 2 = 3
+
+#guard_msgs in
+@[trusted_axiom] axiom anotherTrustedAx : 2 = 2
+
+/-! Direct use of an untrusted axiom warns; use of a trusted axiom does not. -/
+
+/--
+warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx`
+
+Note: This linter can be disabled with `set_option linter.untrustedAxioms false`
+-/
+#guard_msgs in
+theorem usesUntrusted : 1 = 2 := untrustedAx
+
+#guard_msgs in
+theorem usesTrusted : 1 = 1 := trustedAx
+
+/-! Transitive dependencies are reported. -/
+
+/--
+warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx`
+
+Note: This linter can be disabled with `set_option linter.untrustedAxioms false`
+-/
+#guard_msgs in
+theorem usesTransitively : 2 = 1 := usesUntrusted.symm
+
+/-! All offending axioms are listed in a single warning. -/
+
+/--
+warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `anotherUntrustedAx`, `untrustedAx`
+
+Note: This linter can be disabled with `set_option linter.untrustedAxioms false`
+-/
+#guard_msgs in
+theorem usesBoth : 1 = 3 := untrustedAx.trans anotherUntrustedAx
+
+/-! Private declarations are linted as well. -/
+
+/--
+warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx`
+
+Note: This linter can be disabled with `set_option linter.untrustedAxioms false`
+-/
+#guard_msgs in
+private theorem privateUses : 1 = 2 := untrustedAx
+
+/-!
+Internal auxiliary declarations (e.g. `match` functions) are not linted separately; their axioms
+are reported once via the surrounding declaration.
+-/
+
+/--
+warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx`
+
+Note: This linter can be disabled with `set_option linter.untrustedAxioms false`
+-/
+#guard_msgs in
+theorem usesViaMatch : (n : Nat) → 1 = 2
+  | 0 => untrustedAx
+  | _+1 => untrustedAx
+
+/-!
+`sorryAx` is not reported for a declaration containing the `sorry` itself, which already produces
+the `warn.sorry` warning.
+-/
+
+/--
+warning: declaration uses `sorry`
+-/
+#guard_msgs in
+theorem usesSorry : 1 = 2 := sorry
+
+/-! Transitive `sorry`s are not covered by `warn.sorry`, so `sorryAx` is reported for them. -/
+
+/--
+warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `sorryAx`
+
+Note: This linter can be disabled with `set_option linter.untrustedAxioms false`
+-/
+#guard_msgs in
+theorem usesSorryTransitively : 2 = 1 := usesSorry.symm
+
+/-! The synchronous elaboration path warns as well. -/
+
+/--
+warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx`
+
+Note: This linter can be disabled with `set_option linter.untrustedAxioms false`
+-/
+#guard_msgs in
+set_option Elab.async false in
+theorem usesUntrustedSync : 1 = 2 := untrustedAx
+
+/-! `example`s are linted. -/
+
+/--
+warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx`
+
+Note: This linter can be disabled with `set_option linter.untrustedAxioms false`
+-/
+#guard_msgs in
+example : 1 = 2 := untrustedAx
+
+/-! Explicitly disabling the linter. -/
+
+set_option linter.untrustedAxioms false in
+#guard_msgs in
+theorem explicitOff : 1 = 2 := untrustedAx
+
+/-! The attribute can only be applied to axioms in the current module. -/
+
+def notAnAxiom : Nat := 1
+
+/-- error: Cannot add attribute `@[trusted_axiom]` to non-axiom `notAnAxiom` -/
+#guard_msgs in
+attribute [trusted_axiom] notAnAxiom
+
+/--
+error: Cannot add attribute `[trusted_axiom]` to declaration `propext` because it is in an imported module
+-/
+#guard_msgs in
+attribute [trusted_axiom] propext
+
+/--
+error: Invalid attribute scope: Attribute `[trusted_axiom]` must be global, not `local`
+-/
+#guard_msgs in
+attribute [local trusted_axiom] anotherUntrustedAx