diff --git a/src/tests/Tests/LeanCode.lean b/src/tests/Tests/LeanCode.lean
index 45cbb1e1b..e58dd339e 100644
--- a/src/tests/Tests/LeanCode.lean
+++ b/src/tests/Tests/LeanCode.lean
@@ -77,3 +77,34 @@ info: (some (Verso.Genre.Manual.InlineLean.Inline.lean, [{"seq":
     | .other code _ => Option.some (code.name, code.data)
     | _ => .none
   | _ => .none
+
+-- Ensure no spurious unused variable warning for `α`
+#docs (Genre.Manual) mutualInductiveTest "Mutual Inductive Test" :=
+:::::::
+```lean
+mutual
+  inductive TreeA (α : Type) where
+    | leafA : TreeA α
+    | nodeA : α → TreeB α → TreeA α
+
+  inductive TreeB (α : Type) where
+    | leafB : TreeB α
+    | nodeB : α → TreeA α → TreeB α
+end
+```
+:::::::
+
+-- Genuinely unused variable in a code block: the inner linter produces a warning that
+-- appears in the generated highlighted output (via `nonSilentMsgs` in `elabCommands`).
+-- `reportMessages` silences non-error messages, so no build warning is emitted.
+#docs (Genre.Manual) unusedVarTest "Unused Var Test" :=
+:::::::
+```lean (name := unusedVar)
+def unusedArgFn (unused : Nat) : Nat := 0
+```
+```leanOutput unusedVar
+unused variable `unused`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
+```
+:::::::
diff --git a/src/verso-manual/VersoManual/InlineLean.lean b/src/verso-manual/VersoManual/InlineLean.lean
index e8b647468..1395917f4 100644
--- a/src/verso-manual/VersoManual/InlineLean.lean
+++ b/src/verso-manual/VersoManual/InlineLean.lean
@@ -219,6 +219,26 @@ private def toHighlightedLeanInline (shouldShow : Bool) (hls : Highlighted) (str
   ``(Inline.other (Verso.Genre.Manual.InlineLean.Inline.lean $(← quoteHighlightViaSerialization hls)) #[Inline.code $(quote str.getString)])
 
 
+/--
+Sets `linter.unusedVariables` to `false` in all `CommandContextInfo.options` within an info tree.
+
+This prevents the outer unused variable linter from re-processing variables that the inner linter
+(running via `elabCommandTopLevel`) has already correctly handled. This is needed to allow the
+unused variable linter to do the right thing for embedded Lean code. On the one hand, the linter
+needs to run, so that its warnings are accurately recorded. But the linter also may run on the Verso
+document, at which time it can inspect the info trees left behind by the embedded Lean and generate
+spurious warnings. Turning it off before saving info trees works around this issue.
+-/
+private partial def disableUnusedVarLinterInInfoTree : InfoTree → InfoTree
+  | .context (.commandCtx ci) child =>
+    .context (.commandCtx { ci with options := Lean.Linter.linter.unusedVariables.set ci.options false })
+      (disableUnusedVarLinterInInfoTree child)
+  | .context pci child =>
+    .context pci (disableUnusedVarLinterInInfoTree child)
+  | .node info children =>
+    .node info (children.map disableUnusedVarLinterInInfoTree)
+  | .hole id => .hole id
+
 def elabCommands (config : LeanBlockConfig) (str : StrLit)
     (toHighlightedLeanContent : (shouldShow : Bool) → (hls : Highlighted) → (str: StrLit) → DocElabM Term)
     (minCommands : Option Nat := none)
@@ -233,9 +253,11 @@ def elabCommands (config : LeanBlockConfig) (str : StrLit)
 
     let origScopes ← if config.fresh then pure [{header := ""}] else getScopes
 
-    -- Turn off async elaboration so that info trees and messages are available when highlighting syntax
+    -- Turn off async elaboration so that info trees and messages are available when highlighting syntax.
     let origScopes := origScopes.modifyHead fun sc =>
-      { sc with opts := pp.tagAppFns.set (Elab.async.set sc.opts false) true }
+      let opts := Elab.async.set sc.opts false
+      let opts := pp.tagAppFns.set opts true
+      { sc with opts }
 
     let altStr ← parserInputString str
 
@@ -255,8 +277,16 @@ def elabCommands (config : LeanBlockConfig) (str : StrLit)
       cmdState := { cmdState with messages := messages }
 
 
+      -- Use elabCommandTopLevel so that linters run after each command (matching Lean's normal
+      -- behavior). Since it resets messages and infoState, save and restore them to accumulate.
+      let savedMsgs := cmdState.messages
+      let savedTrees := cmdState.infoState.trees
       cmdState ← withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.lean, stx := cmd})) <|
-        runCommand (Command.elabCommand cmd) cmd cctx cmdState
+        runCommand (Command.elabCommandTopLevel cmd) cmd cctx cmdState
+      cmdState := { cmdState with
+        messages := savedMsgs ++ cmdState.messages,
+        infoState := { cmdState.infoState with trees := savedTrees ++ cmdState.infoState.trees }
+      }
 
       if Parser.isTerminalCommand cmd then break
 
@@ -275,8 +305,10 @@ def elabCommands (config : LeanBlockConfig) (str : StrLit)
       setEnv cmdState.env
       setScopes cmdState.scopes
 
+      -- The inner linter has already run correctly via elabCommandTopLevel, so we need to avoid
+      -- re-running it.
       for t in cmdState.infoState.trees do
-        pushInfoTree t
+        pushInfoTree (disableUnusedVarLinterInInfoTree t)
 
 
       let mut hls := Highlighted.empty