diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index bc6a40bde0..2930abd117 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -2302,6 +2302,10 @@ theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
 macro (name := mvcgenMacro) (priority:=low) "mvcgen" : tactic =>
   Macro.throwError "to use `mvcgen`, please include `import Std.Tactic.Do`"
 
+/-- Experimental Sym-based drop-in for `mvcgen`; see `mvcgen` for documentation. -/
+macro (name := mvcgen'Macro) (priority:=low) "mvcgen'" : tactic =>
+  Macro.throwError "to use `mvcgen'`, please include `import Std.Tactic.Do`"
+
 /--
 `cbv` performs simplification that closely mimics call-by-value evaluation.
 It reduces terms by unfolding definitions using their defining equations and
diff --git a/src/Lean/Elab/Tactic/Do.lean b/src/Lean/Elab/Tactic/Do.lean
index 47359990ff..e5976f0efb 100644
--- a/src/Lean/Elab/Tactic/Do.lean
+++ b/src/Lean/Elab/Tactic/Do.lean
@@ -12,3 +12,4 @@ public import Lean.Elab.Tactic.Do.Attr
 public import Lean.Elab.Tactic.Do.LetElim
 public import Lean.Elab.Tactic.Do.Spec
 public import Lean.Elab.Tactic.Do.VCGen
+public import Lean.Elab.Tactic.Do.Internal
diff --git a/src/Lean/Elab/Tactic/Do/Internal.lean b/src/Lean/Elab/Tactic/Do/Internal.lean
new file mode 100644
index 0000000000..719de42217
--- /dev/null
+++ b/src/Lean/Elab/Tactic/Do/Internal.lean
@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Lean.Elab.Tactic.Do.Internal.VCGen
diff --git a/tests/bench/mvcgen/sym/lib/VCGen.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen.lean
similarity index 62%
rename from tests/bench/mvcgen/sym/lib/VCGen.lean
rename to src/Lean/Elab/Tactic/Do/Internal/VCGen.lean
index 9cc8f0509e..1599820a64 100644
--- a/tests/bench/mvcgen/sym/lib/VCGen.lean
+++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen.lean
@@ -4,16 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Graf
 -/
 module
-public meta import VCGen.Reduce
-public meta import VCGen.SpecDB
-public meta import VCGen.RuleConstruction
-public meta import VCGen.Context
-public meta import VCGen.Util
-public meta import VCGen.RuleCache
-public meta import VCGen.Entails
-public meta import VCGen.Solve
-public meta import VCGen.Driver
-public meta import VCGen.Frontend
+
+prelude
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Reduce
+public import Lean.Elab.Tactic.Do.Internal.VCGen.SpecDB
+public import Lean.Elab.Tactic.Do.Internal.VCGen.RuleConstruction
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Context
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Util
+public import Lean.Elab.Tactic.Do.Internal.VCGen.RuleCache
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Entails
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Solve
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Driver
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Frontend
 
 /-!
 The `mvcgen'` tactic, split across the modules above.
diff --git a/tests/bench/mvcgen/sym/lib/VCGen/Context.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean
similarity index 92%
rename from tests/bench/mvcgen/sym/lib/VCGen/Context.lean
rename to src/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean
index 739d9ecb45..13ce4f25d4 100644
--- a/tests/bench/mvcgen/sym/lib/VCGen/Context.lean
+++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean
@@ -4,20 +4,20 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Graf
 -/
 module
-public import Lean.Elab
-public import Lean.Meta
-public meta import Lean.Elab
-public meta import Lean.Meta
-meta import Lean.Meta.Sym.Pattern
-meta import Lean.Meta.Sym.Simp.DiscrTree
-public meta import Lean.Meta.Tactic.Grind.Main
-public meta import Lean.Elab.Tactic.Do.VCGen.Basic
-public meta import VCGen.SpecDB
+
+prelude
+public import Lean.Elab.Tactic.Do.VCGen.Basic
+public import Lean.Elab.Tactic.Do.Internal.VCGen.SpecDB
+public import Lean.Meta.Sym.Apply
+public import Lean.Meta.Sym.Simp.SimpM
+public import Lean.Meta.Tactic.Grind.Types
 
 open Lean Meta Elab Tactic Sym
 open Lean.Elab.Tactic.Do Lean.Elab.Tactic.Do.SpecAttr
 open Std.Do
 
+namespace Lean.Elab.Tactic.Do.Internal
+
 /-!
 The `VCGenM` monad: its read-only `Context` (spec database + a fixed bundle of
 pre-built `BackwardRule`s + user-customisable simp methods + pre-tactic) and
@@ -33,7 +33,7 @@ public inductive VCGen.PreTac where
   /-- Use a user-provided tactic syntax. -/
   | tactic (tac : Syntax)
 
-public meta def VCGen.PreTac.isGrind : VCGen.PreTac → Bool
+public def VCGen.PreTac.isGrind : VCGen.PreTac → Bool
   | .grind .. => true
   | _ => false
 
@@ -160,21 +160,23 @@ namespace VCGen
 
 /-- Register a join-point `JumpSiteInfo` for the given fvar. Called when a
 `let __do_jp := …` is detected as a shared continuation. -/
-public meta def registerJP (fv : FVarId) (info : JumpSiteInfo) : _root_.VCGenM Unit :=
+public def registerJP (fv : FVarId) (info : JumpSiteInfo) : VCGenM Unit :=
   modify fun s => { s with jps := s.jps.insert fv info }
 
 /-- Look up a previously-registered join point by fvar id. -/
-public meta def knownJP? (fv : FVarId) : _root_.VCGenM (Option JumpSiteInfo) :=
+public def knownJP? (fv : FVarId) : VCGenM (Option JumpSiteInfo) :=
   return (← get).jps.get? fv
 
 /-- True iff fuel has been exhausted (`Fuel.limited 0`). -/
-public meta def outOfFuel : _root_.VCGenM Bool :=
+public def outOfFuel : VCGenM Bool :=
   return match (← get).fuel with | .limited 0 => true | _ => false
 
 /-- Decrement remaining fuel by one. No-op when fuel is `.unlimited` or already at zero. -/
-public meta def burnOne : _root_.VCGenM Unit :=
+public def burnOne : VCGenM Unit :=
   modify fun s => { s with fuel := match s.fuel with
     | .limited (n+1) => .limited n
     | other => other }
 
 end VCGen
+
+end Lean.Elab.Tactic.Do.Internal
diff --git a/tests/bench/mvcgen/sym/lib/VCGen/Driver.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.lean
similarity index 90%
rename from tests/bench/mvcgen/sym/lib/VCGen/Driver.lean
rename to src/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.lean
index ceec32f61a..1f11003a5e 100644
--- a/tests/bench/mvcgen/sym/lib/VCGen/Driver.lean
+++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Driver.lean
@@ -4,20 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Graf
 -/
 module
-public import Lean.Elab
-public import Lean.Meta
-public meta import Lean.Elab
-public meta import Lean.Meta
-public meta import Lean.Meta.Tactic.Grind.Main
-public meta import Lean.Meta.Tactic.Grind.Solve
-public meta import VCGen.Context
-public meta import VCGen.Util
-public meta import VCGen.Solve
+
+prelude
+public import Lean.Elab.Tactic.Meta
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Context
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Solve
+public import Lean.Meta.Sym.Grind
 
 open Lean Meta Elab Tactic Sym
 open Lean.Elab.Tactic.Do.SpecAttr
 open Std.Do
 
+namespace Lean.Elab.Tactic.Do.Internal
+
 /-!
 Worklist driver for `mvcgen'`. Wraps `solve` with a queue of pending goals,
 emits VCs (or invariant holes) for those `solve` cannot decompose further,
@@ -33,7 +32,7 @@ Runs the `preTac` on the VC:
 - `.tactic`: runs the user-provided tactic on the VC, potentially emitting multiple subgoals.
 - `.none`: returns the VC as-is.
 -/
-public meta def PreTac.run : PreTac →  Grind.Goal → VCGenM (List MVarId)
+public def PreTac.run : PreTac →  Grind.Goal → VCGenM (List MVarId)
   | .none, goal => return [goal.mvarId]
   | .grind silent, goal => do
     let savedMCtx ← getMCtx
@@ -59,7 +58,7 @@ succeeded. Numbering is 1-based; out-of-order labelled forms (e.g. `| inv2 => 
 before `| inv1 => …`) are supported because the map is keyed by parsed number,
 not position.
 -/
-private meta def tryInlineInvariant (n : Nat) (mv : MVarId) : VCGenM Bool := do
+private def tryInlineInvariant (n : Nat) (mv : MVarId) : VCGenM Bool := do
   let some alt := (← read).invariantAlts[n]? | return false
   try
     let tac ← match alt with
@@ -87,7 +86,7 @@ each in `State.invariants` (1-based stable index) and try to inline-elaborate
 its matching user alt. Returns the remaining non-invariant subgoals for `work`
 to enqueue. Eager handling here ensures dependent VCs see `?inv` assigned by
 the time they reach `emitVC`/`preTac`. -/
-private meta def handleInvariantSubgoals (subgoals : List MVarId) : VCGenM (Array MVarId) := do
+private def handleInvariantSubgoals (subgoals : List MVarId) : VCGenM (Array MVarId) := do
   let env ← getEnv
   let mut others : Array MVarId := #[]
   for sg in subgoals do
@@ -107,7 +106,7 @@ Called when decomposing the goal further did not succeed; in this case we emit a
 Invariant subgoals are handled separately by `handleInvariantSubgoals` directly inside `work`,
 so they never reach this path.
 -/
-public meta def emitVC (goal : Grind.Goal) : VCGenM Unit := do
+public def emitVC (goal : Grind.Goal) : VCGenM Unit := do
   let goal ← (← read).preTac.processHypotheses goal
   let mut vcs := #[]
   -- `trivial`: when false, skip `repeatAndRfl` (which collapses And-chains via rfl);
@@ -124,7 +123,7 @@ public meta def emitVC (goal : Grind.Goal) : VCGenM Unit := do
     vcs := vcs.push mvarId
   modify fun s => { s with vcs := s.vcs ++ vcs }
 
-public meta def work (goal : Grind.Goal) : VCGenM Unit := do
+public def work (goal : Grind.Goal) : VCGenM Unit := do
   let mvarId ← preprocessMVar goal.mvarId
   let goal := { goal with mvarId }
   let mut worklist := #[goal] -- worklist is LIFO (popped from the back)
@@ -183,7 +182,7 @@ Return the VCs and invariant goals.
 
 `stepLimit?`, when `some n`, seeds the fuel counter to `n`; when `none`, fuel is unlimited.
 -/
-public meta partial def main (goal : MVarId) (ctx : Context) (stepLimit? : Option Nat := none) :
+public partial def main (goal : MVarId) (ctx : Context) (stepLimit? : Option Nat := none) :
     Grind.GrindM Result := do
   let grindGoal ← Grind.mkGoalCore goal
   let initState : State := { fuel := match stepLimit? with | some n => .limited n | none => .unlimited }
@@ -200,3 +199,5 @@ public meta partial def main (goal : MVarId) (ctx : Context) (stepLimit? : Optio
     preTacFailed := state.preTacFailed }
 
 end VCGen
+
+end Lean.Elab.Tactic.Do.Internal
diff --git a/tests/bench/mvcgen/sym/lib/VCGen/Entails.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Entails.lean
similarity index 90%
rename from tests/bench/mvcgen/sym/lib/VCGen/Entails.lean
rename to src/Lean/Elab/Tactic/Do/Internal/VCGen/Entails.lean
index 811ff7a605..b5fe5438db 100644
--- a/tests/bench/mvcgen/sym/lib/VCGen/Entails.lean
+++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Entails.lean
@@ -4,17 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Graf
 -/
 module
-public import Lean.Elab
-public import Lean.Meta
-public meta import Lean.Elab
-public meta import Lean.Meta
-public meta import Lean.Elab.Tactic.Do.VCGen.Split
-public meta import VCGen.Context
-public meta import VCGen.Reduce
-public meta import VCGen.Util
+
+prelude
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Context
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Util
+public import Lean.Meta.Sym.Util
 
 open Lean Meta Elab Tactic Sym Sym.Internal
 open Lean.Elab.Tactic.Do.SpecAttr
+open Lean.Elab.Tactic.Do.Internal
 open Std.Do
 
 /-!
@@ -23,13 +21,15 @@ Entailment-shaped goal decomposition: unfolding `Triple.of_entails_wp`, splittin
 that drives `H ⊢ₛ T` to either a closed goal or a residual.
 -/
 
+namespace Lean.Elab.Tactic.Do.Internal
+
 namespace VCGen
 
 /--
 Unfold `⦃P⦄ x ⦃Q⦄` into `P ⊢ₛ wp⟦x⟧ Q` by applying `Tiple.of_wp`, ensuring that `PostShape.args ps`
 is reduced.
 -/
-public meta def tripleOfWP (goal : MVarId) : _root_.VCGenM MVarId := goal.withContext do
+public def tripleOfWP (goal : MVarId) : VCGenM MVarId := goal.withContext do
   let .goals [goal] ← (← read).tripleOfEntailsWPRule.applyChecked goal
     | throwError "Applying {.ofConstName ``Triple.of_entails_wp} to {goal} failed"
   goal.withContext do
@@ -39,7 +39,7 @@ public meta def tripleOfWP (goal : MVarId) : _root_.VCGenM MVarId := goal.withCo
     goal.replaceTargetDefEq (← Sym.Internal.mkAppS₃ ent σs P Q)
 
 open Lean.Elab.Tactic.Do in
-public meta def solveExceptCondsEntails (goal : MVarId) : _root_.VCGenM (Option MVarId) := goal.withContext do
+public def solveExceptCondsEntails (goal : MVarId) : VCGenM (Option MVarId) := goal.withContext do
   let target ← goal.getType
   let_expr ent@ExceptConds.entails ps P Q := target | return none
   let P ← reduceHead P
@@ -56,7 +56,7 @@ public meta def solveExceptCondsEntails (goal : MVarId) : _root_.VCGenM (Option
   return some goal
 
 open Lean.Elab.Tactic.Do in
-public meta def solvePostCondEntails (goal : MVarId) : _root_.VCGenM (Option (List MVarId)) := goal.withContext do
+public def solvePostCondEntails (goal : MVarId) : VCGenM (Option (List MVarId)) := goal.withContext do
   let target ← goal.getType
   let_expr PostCond.entails _α _ps _P _Q := target | return none
   -- Try closing the whole entailment by reflexivity first.
@@ -88,7 +88,7 @@ then peel a leading `SPred.pure (σ::σs) φ s` from each side of `⊢ₛ` via
 Performs the pure-cons cleanup at the exact iteration the state variable is introduced,
 so the goal stays in canonical form throughout the eta-expansion loop.
 -/
-public meta def consIntroAndSimpStep (goal : MVarId) : VCGenM (Option MVarId) := do
+public def consIntroAndSimpStep (goal : MVarId) : VCGenM (Option MVarId) := do
   let ctx ← read
   let .goals [g'] ← ctx.entailsConsIntroRule.applyChecked goal | return none
   let mut goal ← introsSimp g' m!"after applying {.ofConstName ``SPred.entails_cons_intro}"
@@ -98,7 +98,7 @@ public meta def consIntroAndSimpStep (goal : MVarId) : VCGenM (Option MVarId) :=
     goal := g''
   return some goal
 
-public meta def neededStateIntro (thm : SpecTheoremNew) (goal : MVarId) (excessArgs : Array Expr) : VCGenM (Option MVarId) := do
+public def neededStateIntro (thm : SpecTheoremNew) (goal : MVarId) (excessArgs : Array Expr) : VCGenM (Option MVarId) := do
   let .triple potential := thm.kind | return none
   let mut n := potential - excessArgs.size
   if n = 0 then return none
@@ -121,7 +121,7 @@ Break down `H ⊢ₛ T` as far as possible, reporting `none` when no progress wa
 5. If either `T` was pure `⌜φ₂⌝` (and `H` was not), we turn `T.down` into `φ₂`.
    (NB: If `H` was pure, then we have already lifted `φ₁` to the local context.)
 -/
-public meta def solveSPredEntails (goal : MVarId) : VCGenM (Option MVarId) := goal.withContext do
+public def solveSPredEntails (goal : MVarId) : VCGenM (Option MVarId) := goal.withContext do
   let_expr SPred.entails _σs H T := (← goal.getType) | return none
   let mut progress := false
   let mut goal := goal
@@ -189,3 +189,5 @@ public meta def solveSPredEntails (goal : MVarId) : VCGenM (Option MVarId) := go
     return none
 
 end VCGen
+
+end Lean.Elab.Tactic.Do.Internal
diff --git a/tests/bench/mvcgen/sym/lib/VCGen/Frontend.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.lean
similarity index 90%
rename from tests/bench/mvcgen/sym/lib/VCGen/Frontend.lean
rename to src/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.lean
index 0fad2ab120..af095e7781 100644
--- a/tests/bench/mvcgen/sym/lib/VCGen/Frontend.lean
+++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Frontend.lean
@@ -4,25 +4,26 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Graf
 -/
 module
-public import Lean.Elab
-public import Lean.Meta
-public import Lean.Parser
-public meta import Lean.Elab
-public meta import Lean.Meta
-public meta import Lean.Meta.Tactic.Grind.Main
-public meta import Lean.Meta.Tactic.Grind.Solve
-public meta import Lean.Elab.Tactic.Do.VCGen.Basic
-public meta import Lean.Elab.Tactic.Do.LetElim
-public meta import Lean.Elab.Tactic.Do.VCGen.SuggestInvariant
-public meta import Lean.Elab.Tactic.Do.VCGen
-meta import Lean.Elab.Tactic.Grind
-public meta import VCGen.Context
-public meta import VCGen.Driver
+
+prelude
+public import Lean.Elab.Tactic.Do.VCGen.SuggestInvariant
+public import Lean.Elab.Tactic.Do.VCGen
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Context
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Driver
+public import Lean.Meta.Sym.Simp.Attr
+public import Lean.Meta.Sym.Simp.ControlFlow
+public import Lean.Meta.Sym.Simp.EvalGround
+public import Lean.Meta.Sym.Simp.Forall
+public import Lean.Meta.Sym.Simp.Rewrite
+public import Lean.Meta.Sym.Simp.Simproc
+import Lean.Elab.Tactic.Grind.Main
 
 open Lean Parser Meta Elab Tactic Sym
 open Lean.Elab.Tactic.Do Lean.Elab.Tactic.Do.SpecAttr
 open Std.Do
 
+namespace Lean.Elab.Tactic.Do.Internal
+
 /-!
 `mvcgen'` tactic frontend: parse the user-facing argument syntax into a
 `VCGen.Context`, run `VCGen.main`, and replace the main goal with the
@@ -37,7 +38,7 @@ spec theorems and simp lemmas. Follows the same approach as
 `Lean.Elab.Tactic.Do.VCGen.mkSpecContext`: each entry is first tried as a spec theorem,
 and on failure falls back to a simp/unfold lemma processed via `mkSimpContext`.
 -/
-public meta def mkSpecContext (lemmas : Syntax) (ignoreStarArg := false) : TacticM VCGen.Context := do
+public def mkSpecContext (lemmas : Syntax) (ignoreStarArg := false) : TacticM VCGen.Context := do
   let mut specThms ← getSpecTheorems
   let mut simpStuff := #[]
   let mut starArg := false
@@ -139,24 +140,18 @@ public meta def mkSpecContext (lemmas : Syntax) (ignoreStarArg := false) : Tacti
 
 end VCGen
 
-syntax (name := mvcgen') "mvcgen'" optConfig
-  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")?
-  (invariantAlts)?
-  (&" simplifying_assumptions" (ppSpace colGt ident)? (" [" ident,* "]")?)?
-  (&" with " tactic)? : tactic
-
 /-- Warn about `mvcgen'` config options that are accepted by the parser but currently
 ignored at runtime. As more options gain implementation support, drop their checks
 here. Options with implemented semantics (`trivial`, `elimLets`, `stepLimit`,
 `invariants?`) are silently accepted. -/
-private meta def warnIgnoredConfig (config : VCGen.Config) : TacticM Unit := do
+private def warnIgnoredConfig (config : VCGen.Config) : TacticM Unit := do
   let default : VCGen.Config := {}
   if config.leave != default.leave then
     logWarning "mvcgen': the `leave` config option is currently ignored."
 
 /-- Parse grind configuration from the `with grind ...` clause and build `Grind.Params`.
 Overrides the internal simp step limit to accommodate large unrolled goals. -/
-private meta def elabGrindParams (grindStx : Syntax) (goal : MVarId) : TacticM Grind.Params := do
+private def elabGrindParams (grindStx : Syntax) (goal : MVarId) : TacticM Grind.Params := do
   let `(tactic| grind $config:optConfig $[only%$only]? $[ [$grindParams:grindParam,*] ]? $[=> $_:grindSeq]?) := grindStx
     | throwUnsupportedSyntax
   let grindConfig ← elabGrindConfig config
@@ -167,7 +162,7 @@ Build `Sym.Simp.Methods` from a variant name and extra theorems.
 Supports the anonymous (default) variant. Named variants require a public
 `elabSimpMethods` API in `Lean.Elab.Tactic.Grind.Sym` (see TODO below).
 -/
-private meta def elabSymSimpParts
+private def elabSymSimpParts
     (variantId? : Option (TSyntax `ident))
     (extraIds? : Option (Array (TSyntax `ident)))
     : TacticM Sym.Simp.Methods := do
@@ -201,14 +196,14 @@ private meta def elabSymSimpParts
     post := post >> thms.rewrite
   return { pre, post }
 
-private meta def elabSimplifyingAssumptions (simpClause : Syntax) : TacticM (Option Sym.Simp.Methods) := do
+private def elabSimplifyingAssumptions (simpClause : Syntax) : TacticM (Option Sym.Simp.Methods) := do
   if simpClause.getNumArgs == 0 then return none
   let variantId? := if simpClause[1].getNumArgs != 0 then some ⟨simpClause[1][0]⟩ else none
   let extraIds? := if simpClause[2].getNumArgs != 0
     then some (simpClause[2][1].getSepArgs.map (⟨·⟩)) else none
   pure (some (← elabSymSimpParts variantId? extraIds?))
 
-private meta def elabPreTac (goal : MVarId) (withPreTac : Syntax) : TacticM (VCGen.PreTac × Grind.Params) := do
+private def elabPreTac (goal : MVarId) (withPreTac : Syntax) : TacticM (VCGen.PreTac × Grind.Params) := do
   let mut params ← Grind.mkDefaultParams {}
   if withPreTac.getNumArgs == 0 then return (.none, params)
   let preTac := withPreTac[1]
@@ -235,7 +230,7 @@ and `none` when no `invariants` clause is provided. Errors on mixed bullet/label
 forms (one or the other is enforced by the `dotOrCase` flag in the upstream
 elaborator; we replicate that check here).
 -/
-private meta def parseInvariantMap (stx : Syntax) :
+private def parseInvariantMap (stx : Syntax) :
     TacticM (Option (Std.HashMap Nat Syntax)) := do
   let some altsStx := stx.getOptional? | return none
   -- The `invariants?` (suggest) form is handled separately by upstream's `elabInvariants`.
@@ -279,7 +274,7 @@ position (which equals the `inv<n>` tag the entry carries — `Driver.main` assi
 tags consecutively), and elaborate the matching alt. Invariants that were already
 elaborated inline by `Driver.emitVC` (tracked in `inlineHandled`) are skipped, so
 we don't warn about alts that were already consumed there. -/
-private meta def elabRemainingInvariants (alts : Std.HashMap Nat Syntax)
+private def elabRemainingInvariants (alts : Std.HashMap Nat Syntax)
     (invariants : Array MVarId) (inlineHandled : Std.HashSet Nat) : TacticM Unit := do
   let mut handled := inlineHandled
   for h : i in 0...invariants.size do
@@ -297,8 +292,11 @@ private meta def elabRemainingInvariants (alts : Std.HashMap Nat Syntax)
     unless handled.contains n do
       logWarningAt alt s!"Invariant alternative `inv{n}` does not match any invariant goal."
 
-@[tactic mvcgen']
-public meta def elabMVCGen' : Tactic := fun stx => withMainContext do
+@[builtin_tactic Lean.Parser.Tactic.mvcgen']
+public def elabMVCGen' : Tactic := fun stx => withMainContext do
+  if mvcgen.warning.get (← getOptions) then
+    logWarningAt stx "The `mvcgen'` tactic is an experimental drop-in replacement for `mvcgen` \
+      that will eventually replace it. Avoid using it in production projects."
   let config ← elabConfig stx[1]
   warnIgnoredConfig config
   let goal ← getMainGoal
@@ -329,3 +327,5 @@ public meta def elabMVCGen' : Tactic := fun stx => withMainContext do
   replaceMainGoal (invariants ++ result.vcs).toList
   if result.preTacFailed then
     throwError "pre-tactic failed on at least one VC; see errors above"
+
+end Lean.Elab.Tactic.Do.Internal
diff --git a/tests/bench/mvcgen/sym/lib/VCGen/Reduce.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Reduce.lean
similarity index 88%
rename from tests/bench/mvcgen/sym/lib/VCGen/Reduce.lean
rename to src/Lean/Elab/Tactic/Do/Internal/VCGen/Reduce.lean
index c96930bdb9..5e304973f3 100644
--- a/tests/bench/mvcgen/sym/lib/VCGen/Reduce.lean
+++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Reduce.lean
@@ -4,12 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Graf
 -/
 module
-public import Lean.Meta
-public meta import Lean.Meta
-meta import Lean.Meta.Sym.Pattern
+
+prelude
+public import Lean.Meta.Sym.SymM
+public import Lean.Meta.WHNF
 
 open Lean Meta Sym
 
+namespace Lean.Elab.Tactic.Do.Internal
+
+namespace VCGen
+
 /-!
 SymM-level head-redex reducer used throughout VCGen.
 -/
@@ -27,7 +32,7 @@ no further progress is made:
 
 Returns `none` when no reduction was possible. Maintains maximal sharing via `shareCommonInc`.
 -/
-public meta partial def reduceHead? (e : Expr) : SymM (Option Expr) :=
+public partial def reduceHead? (e : Expr) : SymM (Option Expr) :=
   withReducible <| go none e.getAppFn e.getAppRevArgs
   where
     go lastReduction f rargs := do
@@ -59,5 +64,8 @@ public meta partial def reduceHead? (e : Expr) : SymM (Option Expr) :=
         | none    => pure lastReduction
       | _ => pure lastReduction
 
-public meta def reduceHead (e : Expr) : SymM Expr :=
+public def reduceHead (e : Expr) : SymM Expr :=
   return (← reduceHead? e).getD e
+
+end VCGen
+end Lean.Elab.Tactic.Do.Internal
diff --git a/tests/bench/mvcgen/sym/lib/VCGen/RuleCache.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/RuleCache.lean
similarity index 71%
rename from tests/bench/mvcgen/sym/lib/VCGen/RuleCache.lean
rename to src/Lean/Elab/Tactic/Do/Internal/VCGen/RuleCache.lean
index e2d89b12cc..54b6850881 100644
--- a/tests/bench/mvcgen/sym/lib/VCGen/RuleCache.lean
+++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/RuleCache.lean
@@ -4,18 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Graf
 -/
 module
-public import Lean.Elab
-public import Lean.Meta
-public meta import Lean.Elab
-public meta import Lean.Meta
-public meta import Lean.Elab.Tactic.Do.VCGen.Split
-public meta import VCGen.Context
-public meta import VCGen.RuleConstruction
-public meta import VCGen.Util
+
+prelude
+public import Lean.Elab.Tactic.Do.VCGen.Split
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Context
+public import Lean.Elab.Tactic.Do.Internal.VCGen.RuleConstruction
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Util
 
 open Lean Meta Elab Tactic Sym
 open Lean.Elab.Tactic.Do.SpecAttr
-open VCGen
+open Lean.Elab.Tactic.Do.Internal
 open Std.Do
 
 /-!
@@ -23,21 +21,23 @@ open Std.Do
 `VCGen.RuleConstruction`. The cache key is `(declName, m, excessArgs.size)`.
 -/
 
-namespace VCGen
+namespace Lean.Elab.Tactic.Do.Internal
 
 @[inline]
-public meta def Std.HashMap.getDM [Monad m] [BEq α] [Hashable α]
+def Std.HashMap.getDM [Monad m] [BEq α] [Hashable α]
     (cache : Std.HashMap α β) (key : α) (fallback : m β) : m (β × Std.HashMap α β) := do
   if let some b := cache.get? key then
     return (b, cache)
   let b ← fallback
   return (b, cache.insert key b)
 
-public meta def SpecTheoremNew.global? (specThm : SpecTheoremNew) : Option Name :=
+namespace VCGen
+
+public def SpecTheoremNew.global? (specThm : SpecTheoremNew) : Option Name :=
   match specThm.proof with | .global decl => some decl | _ => none
 
 /-- See the documentation for `mkBackwardRuleFromSpec` and `mkBackwardRuleFromSimpSpec`. -/
-public meta def mkBackwardRuleFromSpecCached (specThm : SpecTheoremNew) (m σs ps instWP : Expr)
+public def mkBackwardRuleFromSpecCached (specThm : SpecTheoremNew) (m σs ps instWP : Expr)
     (excessArgs : Array Expr) : VCGenM BackwardRule := do
   let mkRuleSlow := match specThm.kind with
     | .triple _ => mkBackwardRuleFromSpec     specThm m σs ps instWP excessArgs
@@ -50,7 +50,7 @@ public meta def mkBackwardRuleFromSpecCached (specThm : SpecTheoremNew) (m σs p
 
 open Lean.Elab.Tactic.Do in
 /-- Creates and caches a backward rule for splitting `ite`, `dite`, or matchers. -/
-public meta def mkBackwardRuleFromSplitInfoCached (splitInfo : SplitInfo) (m σs ps instWP : Expr) (excessArgs : Array Expr) : _root_.VCGenM BackwardRule := do
+public def mkBackwardRuleFromSplitInfoCached (splitInfo : SplitInfo) (m σs ps instWP : Expr) (excessArgs : Array Expr) : VCGenM BackwardRule := do
   let cacheKey := match splitInfo with
     | .ite .. => ``ite
     | .dite .. => ``dite
@@ -62,3 +62,5 @@ public meta def mkBackwardRuleFromSplitInfoCached (splitInfo : SplitInfo) (m σs
   return res
 
 end VCGen
+
+end Lean.Elab.Tactic.Do.Internal
diff --git a/tests/bench/mvcgen/sym/lib/VCGen/RuleConstruction.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.lean
similarity index 94%
rename from tests/bench/mvcgen/sym/lib/VCGen/RuleConstruction.lean
rename to src/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.lean
index 7c37daf815..84365a9f6d 100644
--- a/tests/bench/mvcgen/sym/lib/VCGen/RuleConstruction.lean
+++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.lean
@@ -4,21 +4,24 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Graf
 -/
 module
-public import Lean.Elab
-public import Lean.Meta
-public import Lean.Expr
-public meta import Lean.Elab
-public meta import Lean.Meta
-public meta import Lean.Meta.Match.Rewrite
-public meta import Lean.Elab.Tactic.Do.VCGen.Split
-meta import Lean.Meta.Sym.Pattern
-public meta import VCGen.Reduce
-public meta import VCGen.SpecDB
+
+prelude
+public import Lean.Elab.Tactic.Do.VCGen.Split
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Reduce
+public import Lean.Elab.Tactic.Do.Internal.VCGen.SpecDB
+public import Lean.Meta.Sym.AlphaShareBuilder
+public import Lean.Meta.Sym.Apply
+public import Lean.Meta.Sym.InstantiateMVarsS
+public import Lean.Meta.Sym.Util
 
 open Lean Meta Elab Tactic Sym
 open Lean.Elab.Tactic.Do.SpecAttr
 open Std.Do
 
+namespace Lean.Elab.Tactic.Do.Internal
+
+namespace VCGen
+
 /-!
 Construction of `BackwardRule`s from `SpecTheoremNew`s and split info. Pure
 `SymM` — no knowledge of `VCGenM`. The `VCGenM` cache wrappers live in
@@ -26,13 +29,13 @@ Construction of `BackwardRule`s from `SpecTheoremNew`s and split info. Pure
 -/
 
 /-- Build goal: `P ⊢ₛ wp⟦prog⟧ Q ss...`. Meant to be partially applied for convenience. -/
-private meta def mkGoal (u v : Level) (m σs ps instWP α : Expr) (ss : Array Expr) (P Q : Expr) (prog : Expr) : Expr :=
+private def mkGoal (u v : Level) (m σs ps instWP α : Expr) (ss : Array Expr) (P Q : Expr) (prog : Expr) : Expr :=
   mkApp3 (mkConst ``SPred.entails [u]) σs P
     (mkAppN (mkApp4 (mkConst ``PredTrans.apply [u]) ps α
       (mkApp5 (mkConst ``WP.wp [u, v]) m ps instWP α prog) Q) ss)
 
 /-- Extract the program from a goal built by `mkGoal`. -/
-private meta def extractProgFromGoal (goal : Expr) : Expr :=
+private def extractProgFromGoal (goal : Expr) : Expr :=
   goal.getArg! 2 |>.getArg! 2 |>.getArg! 4
 
 /--
@@ -121,7 +124,7 @@ prf : ∀ (α : Type) (x : StateT Nat Id α) (β : Type) (f : α → StateT Nat
 We are still investigating how to get rid of more kernel unfolding overhead, such as for `wp` and
 `List.rec`.
 -/
-public meta def mkBackwardRuleFromSpec (specThm : SpecTheoremNew) (m σs ps instWP : Expr) (excessArgs : Array Expr) : SymM BackwardRule := do
+public def mkBackwardRuleFromSpec (specThm : SpecTheoremNew) (m σs ps instWP : Expr) (excessArgs : Array Expr) : SymM BackwardRule := do
   let preprocessExpr : Expr → SymM Expr := shareCommon <=< liftMetaM ∘ unfoldReducible
   -- Create a backward rule for the spec we look up in the database.
   -- In order for the backward rule to apply, we need to instantiate both `m` and `ps` with the ones
@@ -236,7 +239,7 @@ For example, `MonadState.get.eq_1 : get = self.1` with `m = StateT σ m'` yields
 that rewrites `wp⟦get⟧` to `wp⟦MonadStateOf.get⟧` (after instance synthesis + projection
 reduction + unfoldReducible).
 -/
-public meta def mkBackwardRuleFromSimpSpec (specThm : SpecTheoremNew) (m σs ps instWP : Expr)
+public def mkBackwardRuleFromSimpSpec (specThm : SpecTheoremNew) (m σs ps instWP : Expr)
     (excessArgs : Array Expr) : SymM BackwardRule := do
   let preprocessExpr : Expr → SymM Expr := shareCommon <=< liftMetaM ∘ unfoldReducible
   let wpType ← liftMetaM <| Meta.inferType instWP
@@ -303,7 +306,7 @@ Uses `SplitInfo.withAbstract` to open fvars for the split, then `SplitInfo.split
 to build the splitting proof. Hypothesis types are discovered via `rwIfOrMatcher` inside
 the splitter telescope.
 -/
-public meta def mkBackwardRuleForSplit (splitInfo : SplitInfo) (m σs ps instWP : Expr) (excessArgs : Array Expr) : SymM BackwardRule := do
+public def mkBackwardRuleForSplit (splitInfo : SplitInfo) (m σs ps instWP : Expr) (excessArgs : Array Expr) : SymM BackwardRule := do
   let preprocessExpr : Expr → SymM Expr := shareCommon <=< liftMetaM ∘ unfoldReducible
   let wpType ← liftMetaM <| Meta.inferType instWP
   let us := wpType.getAppFn.constLevels!
@@ -349,3 +352,6 @@ public meta def mkBackwardRuleForSplit (splitInfo : SplitInfo) (m σs ps instWP
   let prf ← instantiateMVars prf
   let res ← abstractMVars prf
   mkBackwardRuleFromExpr res.expr res.paramNames.toList
+
+end VCGen
+end Lean.Elab.Tactic.Do.Internal
diff --git a/tests/bench/mvcgen/sym/lib/VCGen/Solve.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.lean
similarity index 90%
rename from tests/bench/mvcgen/sym/lib/VCGen/Solve.lean
rename to src/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.lean
index faf64e3f0f..32ad5fbe2c 100644
--- a/tests/bench/mvcgen/sym/lib/VCGen/Solve.lean
+++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.lean
@@ -4,22 +4,20 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Graf
 -/
 module
-public import Lean.Elab
-public import Lean.Meta
-public meta import Lean.Elab
-public meta import Lean.Meta
-public meta import Lean.Meta.Match.Rewrite
-public meta import Lean.Elab.Tactic.Do.VCGen.Split
-public meta import VCGen.Context
-public meta import VCGen.Reduce
-public meta import VCGen.Util
-public meta import VCGen.RuleCache
-public meta import VCGen.Entails
+
+prelude
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Context
+public import Lean.Elab.Tactic.Do.Internal.VCGen.RuleCache
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Entails
+public import Lean.Meta.Sym.InstantiateS
 
 open Lean Meta Elab Tactic Sym Sym.Internal
 open Lean.Elab.Tactic.Do.SpecAttr
+open Lean.Elab.Tactic.Do.Internal
 open Std.Do
 
+namespace Lean.Elab.Tactic.Do.Internal
+
 
 /-!
 The main `solve` step. Runs once per worklist iteration and either fully
@@ -44,14 +42,14 @@ public inductive SolveResult where
   /-- Successfully decomposed the goal. These are the subgoals. -/
   | goals (subgoals : List MVarId)
 
-private meta def isDuplicable (e : Expr) : Bool := match e with
+private def isDuplicable (e : Expr) : Bool := match e with
   | .bvar .. | .mvar .. | .fvar .. | .const .. | .lit .. | .sort .. => true
   | .mdata _ e | .proj _ _ e => isDuplicable e
   | .lam .. | .forallE .. | .letE .. => false
   | .app .. => e.isAppOf ``OfNat.ofNat
 
 /-- Strategy 1: introduce binders if the target is a `∀`. -/
-private meta def tryForallIntro (goal : MVarId) (target : Expr) :
+private def tryForallIntro (goal : MVarId) (target : Expr) :
     VCGenM (Option SolveResult) := do
   unless target.isForall do return none
   return some <| .goals [← introsSimp goal m!"foralls in `solve`"]
@@ -65,7 +63,7 @@ at the point where the upstream `mvcgen.onJoinPoint` would set up shared-continu
 proof construction. That port (Phase 6 of the plan) is not yet done; we throw an
 explicit error here so that enabling `jp := true` is honest about the gap rather
 than silently ignored. -/
-private meta def tryLetIntro (goal : MVarId) (target : Expr) :
+private def tryLetIntro (goal : MVarId) (target : Expr) :
     VCGenM (Option SolveResult) := do
   unless target.isLet do return none
   if (← read).useJP && Lean.Elab.Tactic.Do.isJP target.letName! then
@@ -84,14 +82,14 @@ private meta def tryLetIntro (goal : MVarId) (target : Expr) :
     return some <| .goals [← introsSimp goal m!"let-intro: {target.letName!}"]
 
 /-- Strategy 2: unfold a `Triple` target into the underlying `P ⊢ₛ wp⟦x⟧ Q`. -/
-private meta def tryTripleUnfold (goal : MVarId) (target : Expr) :
+private def tryTripleUnfold (goal : MVarId) (target : Expr) :
     VCGenM (Option SolveResult) := do
   unless target.getAppFn.isConstOf ``Triple do return none
   let goal ← tripleOfWP goal
   return some <| .goals [goal]
 
 /-- Strategy 4: eta-expand a lambda RHS via `entails_cons_intro`. -/
-private meta def tryTargetLambdaIntro (goal : MVarId) (T : Expr) :
+private def tryTargetLambdaIntro (goal : MVarId) (T : Expr) :
     VCGenM (Option SolveResult) := do
   unless T.isLambda do return none
   let .goals [goal] ← (← read).entailsConsIntroRule.applyChecked goal
@@ -99,7 +97,7 @@ private meta def tryTargetLambdaIntro (goal : MVarId) (T : Expr) :
   return some <| .goals [goal]
 
 /-- Strategy 5: head-reduce `H` and/or `T` and replace the target if either side reduced. -/
-private meta def tryHeadReduceHT (goal : MVarId) (ent σs H T : Expr) :
+private def tryHeadReduceHT (goal : MVarId) (ent σs H T : Expr) :
     VCGenM (Option SolveResult) := do
   let H? ← reduceHead? H
   let T? ← reduceHead? T
@@ -110,7 +108,7 @@ private meta def tryHeadReduceHT (goal : MVarId) (ent σs H T : Expr) :
 /-- Strategy 6: when the target's RHS isn't `wp⟦e⟧ Q s₁ ... sₙ`, attempt syntactic
 reflexivity, fall back to `solveSPredEntails`, otherwise classify as
 `.noProgramFoundInTarget`. -/
-private meta def tryRflOrSPred (goal : MVarId) (ent σs H T : Expr) :
+private def tryRflOrSPred (goal : MVarId) (ent σs H T : Expr) :
     VCGenM SolveResult := do
   trace[Elab.Tactic.Do.vcgen] "Trying rfl {goal}"
   if ← withAssignableSyntheticOpaque <| isDefEqS H T then
@@ -122,7 +120,7 @@ private meta def tryRflOrSPred (goal : MVarId) (ent σs H T : Expr) :
   return .noProgramFoundInTarget T
 
 /-- Replace the program in `goal`'s target with `e'` (which must be definitionally equal). -/
-private meta def replaceProgDefEq (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
+private def replaceProgDefEq (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
     (wpConst m ps instWP α e' : Expr) : VCGenM MVarId := do
   let wp ← Sym.Internal.mkAppS₅ wpConst m ps instWP α e'
   let T ← mkAppNS head (args.set! 2 wp)
@@ -130,7 +128,7 @@ private meta def replaceProgDefEq (goal : MVarId) (head H σs ent : Expr) (args
   goal.replaceTargetDefEq target
 
 /-- Hoist a `letE` from the program head to the goal target. -/
-private meta def tryLetHoist (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
+private def tryLetHoist (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
     (wpConst m ps instWP α e f : Expr) : VCGenM (Option SolveResult) := do
   let .letE x ty val body nonDep := f | return none
   trace[Elab.Tactic.Do.vcgen] "let-hoist: {x}"
@@ -143,7 +141,7 @@ private meta def tryLetHoist (goal : MVarId) (head H σs ent : Expr) (args : Arr
 
 /-- Split an `ite`/`dite`/match program head, or iota-reduce if the discriminant is
 constructor-shaped. Returns `none` when the program isn't a split. -/
-private meta def trySplit (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
+private def trySplit (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
     (wpConst m ps instWP α e : Expr) (excessArgs : Array Expr) : VCGenM (Option SolveResult) := do
   let some info ← liftMetaM <| Lean.Elab.Tactic.Do.getSplitInfo? e | return none
   -- Try iota reduction first (reduces matcher/recursor with concrete discriminant)
@@ -156,7 +154,7 @@ private meta def trySplit (goal : MVarId) (head H σs ent : Expr) (args : Array
   return some <| .goals goals
 
 /-- Zeta-unfold a local `let`-bound fvar that appears as the program head. -/
-private meta def tryFvarZeta (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
+private def tryFvarZeta (goal : MVarId) (head H σs ent : Expr) (args : Array Expr)
     (wpConst m ps instWP α e f : Expr) : VCGenM (Option SolveResult) := do
   let some fvarId := f.fvarId? | return none
   let some val ← fvarId.getValue? | return none
@@ -167,7 +165,7 @@ private meta def tryFvarZeta (goal : MVarId) (head H σs ent : Expr) (args : Arr
 /-- Look up a registered `@[spec]` theorem for the program head and apply its cached
 backward rule. Falls back to `.noSpecFoundForProgram` / `.noStrategyForProgram` when no
 spec applies. -/
-private meta def applySpec (goal : MVarId) (e : Expr) (excessArgs : Array Expr)
+private def applySpec (goal : MVarId) (e : Expr) (excessArgs : Array Expr)
     (m σs ps instWP : Expr) : VCGenM SolveResult := do
   let f := e.getAppFn
   if f.isConst || f.isFVar then
@@ -210,7 +208,7 @@ The function performs the following steps in order:
 10. **Spec application**: Look up a registered `@[spec]` theorem (triple or simp) and apply
     its cached backward rule.
 -/
-public meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
+public def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext do
   let target ← goal.getType
   trace[Elab.Tactic.Do.vcgen] "🎯 Target: {target}"
   -- Phase 1: simplify `target` until it is of the form `H ⊢ₛ T`.
@@ -265,3 +263,5 @@ public meta def solve (goal : MVarId) : VCGenM SolveResult := goal.withContext d
   applySpec goal e excessArgs m σs ps instWP
 
 end VCGen
+
+end Lean.Elab.Tactic.Do.Internal
diff --git a/tests/bench/mvcgen/sym/lib/VCGen/SpecDB.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.lean
similarity index 91%
rename from tests/bench/mvcgen/sym/lib/VCGen/SpecDB.lean
rename to src/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.lean
index 8c988f4cfd..4cf214991d 100644
--- a/tests/bench/mvcgen/sym/lib/VCGen/SpecDB.lean
+++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/SpecDB.lean
@@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Graf
 -/
 module
-public import Lean.Elab
-public import Lean.Meta
-public meta import Lean.Elab
-public meta import Lean.Meta
-meta import Lean.Meta.Sym.Pattern
-meta import Lean.Meta.Sym.Simp.DiscrTree
+
+prelude
+public import Lean.Elab.Tactic.Do.Attr
+public import Lean.Meta.Sym.Pattern
+import Lean.Meta.Sym.Simp.DiscrTree
+public import Lean.Meta.DiscrTree.Util
 
 open Lean Meta Elab Tactic Sym
 open Lean.Elab.Tactic.Do.SpecAttr
@@ -59,7 +59,7 @@ public structure SpecTheoremNew where
   priority : Nat  := eval_prio default
   deriving Inhabited
 
-public meta instance : BEq SpecTheoremNew where
+public instance : BEq SpecTheoremNew where
   beq thm₁ thm₂ := thm₁.proof == thm₂.proof
 
 /--
@@ -72,7 +72,7 @@ This method applies `congrFun` for each leading forall to reduce the equation to
 values of type `m α`, introducing fresh metavariables for the extra arguments.
 The number of extra args is stored in `SpecTheoremKind.simp etaArgs`.
 -/
-public meta def SpecTheoremNew.instantiate (specThm : SpecTheoremNew) :
+public def SpecTheoremNew.instantiate (specThm : SpecTheoremNew) :
     MetaM (Array Expr × Array BinderInfo × Expr × Expr) := do
   let (xs, bs, eqPrf, eqType) ← specThm.proof.instantiate
   let .simp etaArgs := specThm.kind | return (xs, bs, eqPrf, eqType)
@@ -89,12 +89,12 @@ public structure SpecTheoremsNew where
   erased : PHashSet SpecProof := {}
   deriving Inhabited
 
-public meta def mkTriplePatternFromExpr (expr : Expr) (levelParams : List Name := []) : SymM Pattern := do
+public def mkTriplePatternFromExpr (expr : Expr) (levelParams : List Name := []) : SymM Pattern := do
   Prod.fst <$> Sym.mkPatternFromExprWithKey expr levelParams fun type => do
     let_expr Triple _m _ps _inst _α prog _P _Q := type | throwError "conclusion is not a Triple {indentExpr type}"
     return (prog, ())
 
-public meta def mkSpecTheoremNew (proof : SpecProof) (prio : Nat) : SymM SpecTheoremNew := do
+public def mkSpecTheoremNew (proof : SpecProof) (prio : Nat) : SymM SpecTheoremNew := do
   -- cf. mkSimpTheoremCore
   let (levelParams, expr) ← proof.getProof
   let type ← Meta.inferType expr
@@ -130,7 +130,7 @@ This function takes a pattern (keyed on the LHS), the equation type `eqTy`, and:
 
 Returns the eta-expanded pattern and the number of extra args (0 if no expansion needed).
 -/
-private meta def etaExpandEqPattern (pattern : Sym.Pattern) (eqTy : Expr) : Sym.Pattern × Nat :=
+private def etaExpandEqPattern (pattern : Sym.Pattern) (eqTy : Expr) : Sym.Pattern × Nat :=
   if !eqTy.isForall then (pattern, 0)
   else
     -- Collect forall domains from eqTy
@@ -160,7 +160,7 @@ For unfold equations of class projections (e.g., `MonadState.modifyGet.eq_1`), t
 may be between functions rather than values. In that case, the pattern is eta-expanded
 so the discrimination tree key includes all arguments.
 -/
-public meta def mkSpecTheoremNewFromSimpDecl? (declName : Name) (prio : Nat) : MetaM (Option SpecTheoremNew) := do
+public def mkSpecTheoremNewFromSimpDecl? (declName : Name) (prio : Nat) : MetaM (Option SpecTheoremNew) := do
   let (pattern, (eqTy, rhs)) ← Sym.mkPatternFromDeclWithKey declName fun body => do
     let_expr Eq eqTy lhs rhs := body | throwError "conclusion is not an equality{indentExpr body}"
     return (lhs, (eqTy, rhs))
@@ -174,7 +174,7 @@ public meta def mkSpecTheoremNewFromSimpDecl? (declName : Name) (prio : Nat) : M
   if etaArgs == 0 && pattern.pattern == rhs then return none
   return some { pattern, proof := .global declName, kind := .simp etaArgs, priority := prio }
 
-public meta def migrateSpecTheoremsDatabase (database : SpecTheorems) (simpThms : SimpTheorems) :
+public def migrateSpecTheoremsDatabase (database : SpecTheorems) (simpThms : SimpTheorems) :
     SymM SpecTheoremsNew := do
   let mut specs : DiscrTree SpecTheoremNew := DiscrTree.empty
   for spec in database.specs.values do
@@ -211,12 +211,14 @@ public meta def migrateSpecTheoremsDatabase (database : SpecTheorems) (simpThms
 Look up `SpecTheoremNew`s in the `@[spec]` database.
 Takes all specs that match the given program `e` and sorts by descending priority.
 -/
-public meta def SpecTheoremsNew.findSpecs (database : SpecTheoremsNew) (e : Expr) :
+public def SpecTheoremsNew.findSpecs (database : SpecTheoremsNew) (e : Expr) :
     SymM (Except (Array SpecTheoremNew) SpecTheoremNew) := do
   let e ← instantiateMVars e
   let e ← shareCommon e
   let candidates := Sym.getMatch database.specs e
-  if h : candidates.size = 1 then return .ok candidates[0]
+  if h : candidates.size = 1 then
+    have : 0 < candidates.size := h ▸ Nat.zero_lt_one
+    return .ok candidates[0]
   -- It appears that insertion sort is *much* faster than qsort here.
   let candidates := candidates.insertionSort (·.priority > ·.priority)
   for spec in candidates do
diff --git a/tests/bench/mvcgen/sym/lib/VCGen/Util.lean b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Util.lean
similarity index 81%
rename from tests/bench/mvcgen/sym/lib/VCGen/Util.lean
rename to src/Lean/Elab/Tactic/Do/Internal/VCGen/Util.lean
index a6eae1a9ce..284a8bd758 100644
--- a/tests/bench/mvcgen/sym/lib/VCGen/Util.lean
+++ b/src/Lean/Elab/Tactic/Do/Internal/VCGen/Util.lean
@@ -4,15 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Graf
 -/
 module
-public import Lean.Meta
-public meta import Lean.Meta
-meta import Lean.Meta.Sym.Pattern
-meta import Lean.Meta.Sym.Simp.DiscrTree
-public meta import Lean.Meta.Sym.Util
-public meta import Lean.Meta.Tactic.Grind.Main
-public meta import Lean.Meta.Tactic.Grind.Solve
-public meta import VCGen.Context
-public meta import VCGen.Reduce
+
+prelude
+public import Lean.Meta.Tactic.Grind.Main
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Context
+public import Lean.Elab.Tactic.Do.Internal.VCGen.Reduce
+public import Lean.Meta.Sym.AlphaShareBuilder
+public import Lean.Meta.Sym.Intro
+public import Lean.Meta.Sym.Simp.Telescope
+public import Lean.Meta.Sym.Util
 
 open Lean Meta Sym
 open Std.Do
@@ -24,6 +24,8 @@ generalization of `applyRflAndAndIntro`. None of these know anything about
 `SPred` entailment specifically.
 -/
 
+namespace Lean.Elab.Tactic.Do.Internal
+
 /--
 `VCGenM` wrapper around `BackwardRule.apply`. Behaves identically to
 `rule.apply goal` unless the application fails and `Context.debug` is on.
@@ -35,8 +37,11 @@ the missing reduction.
 `ruleDesc?` describes the rule for debug output. When `none`, the description
 is reconstructed from `rule.expr.getAppFn` — works for the common case of a
 constant rule. Pass a custom message for dynamically-built rules.
+
+Designed for dot notation: `rule.applyChecked goal`. Requires
+`open Lean.Elab.Tactic.Do.Internal` in scope so that the dot lookup resolves.
 -/
-public meta def _root_.Lean.Meta.Sym.BackwardRule.applyChecked (rule : BackwardRule) (goal : MVarId)
+public def Lean.Meta.Sym.BackwardRule.applyChecked (rule : BackwardRule) (goal : MVarId)
     (ruleDesc? : Option MessageData := none) : VCGenM ApplyResult := do
   let r ← rule.apply goal
   match r with
@@ -65,23 +70,26 @@ public meta def _root_.Lean.Meta.Sym.BackwardRule.applyChecked (rule : BackwardR
 namespace VCGen
 
 open Sym Sym.Internal
+open Lean.Elab.Tactic.Do.Internal
 
-public meta def simpTargetTelescope (mvarId : MVarId) : VCGenM (MVarId × Bool) := do
+public def simpTargetTelescope (mvarId : MVarId) : VCGenM (MVarId × Bool) := do
   let some methods := (← read).hypSimpMethods | return (mvarId, false)
   let target ← mvarId.getType
   let simpState := (← get).simpState
   let methods := { methods with pre := Sym.Simp.simpTelescope }
   let (result, simpState') ← Sym.Simp.SimpM.run (Sym.Simp.simp target) methods {} simpState
   modify fun s => { s with simpState := simpState' }
-  let mvarId ← match result with
-    | .rfl .. => pure (mvarId, false)
-    | .step newTarget proof .. => pure (← mvarId.replaceTargetEq newTarget proof, true)
+  match result with
+  | .rfl .. => return (mvarId, false)
+  | .step newTarget proof .. =>
+    let mvarId' ← mvarId.replaceTargetEq newTarget proof
+    return (mvarId', true)
 
 /--
 Simplify the forall telescope of the target using `Sym.Simp.simpTelescope`,
 then introduce all binders via `Sym.intros`.
 -/
-public meta def introsSimp (mvarId : MVarId) (errorMsg : MessageData) : VCGenM MVarId := do
+public def introsSimp (mvarId : MVarId) (errorMsg : MessageData) : VCGenM MVarId := do
   let (mvarId, progress) ← simpTargetTelescope mvarId
   match ← Sym.intros mvarId with
   | .failed =>
@@ -98,7 +106,7 @@ contains stale proof data (the contradiction proof targets the parent's mvar, no
 In that case, restore the pre-internalization state so each child can discover the contradiction
 independently and construct its own proof via `closeGoal`.
 -/
-public meta def PreTac.processHypotheses (preTac : PreTac) (goal : Grind.Goal) : VCGenM Grind.Goal := do
+public def PreTac.processHypotheses (preTac : PreTac) (goal : Grind.Goal) : VCGenM Grind.Goal := do
   if preTac.isGrind then
     Grind.processHypotheses goal
   else
@@ -110,7 +118,7 @@ exactly the conjuncts that could not be solved.
 This procedure may assign metavariables in `e₁`/`e₂`, for example for `e = ?m` it will assign
 `?m := e`.
 -/
-public meta partial def repeatAndRfl (goal : MVarId) : VCGenM (Option MVarId) :=
+public partial def repeatAndRfl (goal : MVarId) : VCGenM (Option MVarId) :=
     goal.withContext do
   let ctx ← read
   let ty ← instantiateMVars (← goal.getType)
@@ -145,3 +153,4 @@ public meta partial def repeatAndRfl (goal : MVarId) : VCGenM (Option MVarId) :=
     return some goal
 
 end VCGen
+end Lean.Elab.Tactic.Do.Internal
diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean
index 89c38a59ea..baf8407e49 100644
--- a/src/Std/Tactic/Do/Syntax.lean
+++ b/src/Std/Tactic/Do/Syntax.lean
@@ -425,3 +425,12 @@ A hint tactic that expands to `mvcgen invariants?`.
 -/
 syntax (name := mvcgenHint) "mvcgen?" optConfig
   (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")? : tactic
+
+-- Prototypical Sym-based variant of `mvcgen`; see `mvcgen` for documentation.
+-- Same surface syntax modulo `vcAlts`, replaced by `simplifying_assumptions … with …`.
+@[tactic_alt Lean.Parser.Tactic.mvcgen'Macro]
+syntax (name := mvcgen') "mvcgen'" optConfig
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")?
+  (invariantAlts)?
+  (&" simplifying_assumptions" (ppSpace colGt ident)? (" [" ident,* "]")?)?
+  (&" with " tactic)? : tactic
diff --git a/tests/bench/mvcgen/sym/cases/Cases/AddSubCancel.lean b/tests/bench/mvcgen/sym/cases/Cases/AddSubCancel.lean
index 0084e199c1..44130bdaff 100644
--- a/tests/bench/mvcgen/sym/cases/Cases/AddSubCancel.lean
+++ b/tests/bench/mvcgen/sym/cases/Cases/AddSubCancel.lean
@@ -1,5 +1,5 @@
 import Lean
-import VCGen
+import Std.Tactic.Do
 
 open Lean Meta Elab Tactic Sym Std Do SpecAttr
 
diff --git a/tests/bench/mvcgen/sym/cases/Cases/AddSubCancelDeep.lean b/tests/bench/mvcgen/sym/cases/Cases/AddSubCancelDeep.lean
index 22f9925749..ddc6c9ff45 100644
--- a/tests/bench/mvcgen/sym/cases/Cases/AddSubCancelDeep.lean
+++ b/tests/bench/mvcgen/sym/cases/Cases/AddSubCancelDeep.lean
@@ -1,5 +1,5 @@
 import Lean
-import VCGen
+import Std.Tactic.Do
 
 open Lean Meta Elab Tactic Sym Std Do SpecAttr
 
diff --git a/tests/bench/mvcgen/sym/cases/Cases/AddSubCancelSimp.lean b/tests/bench/mvcgen/sym/cases/Cases/AddSubCancelSimp.lean
index 28f11ae4db..11b4ac5d0f 100644
--- a/tests/bench/mvcgen/sym/cases/Cases/AddSubCancelSimp.lean
+++ b/tests/bench/mvcgen/sym/cases/Cases/AddSubCancelSimp.lean
@@ -1,5 +1,5 @@
 import Lean
-import VCGen
+import Std.Tactic.Do
 
 open Lean Meta Elab Tactic Sym Std Do SpecAttr
 
diff --git a/tests/bench/mvcgen/sym/cases/Cases/DiteSplit.lean b/tests/bench/mvcgen/sym/cases/Cases/DiteSplit.lean
index 488f8a0532..6dc6a5e4c9 100644
--- a/tests/bench/mvcgen/sym/cases/Cases/DiteSplit.lean
+++ b/tests/bench/mvcgen/sym/cases/Cases/DiteSplit.lean
@@ -1,5 +1,5 @@
 import Lean
-import VCGen
+import Std.Tactic.Do
 
 open Lean Meta Elab Tactic Sym Std Do SpecAttr
 
diff --git a/tests/bench/mvcgen/sym/cases/Cases/GetThrowSet.lean b/tests/bench/mvcgen/sym/cases/Cases/GetThrowSet.lean
index 3fb60fd78e..3025e990a5 100644
--- a/tests/bench/mvcgen/sym/cases/Cases/GetThrowSet.lean
+++ b/tests/bench/mvcgen/sym/cases/Cases/GetThrowSet.lean
@@ -1,5 +1,5 @@
 import Lean
-import VCGen
+import Std.Tactic.Do
 
 open Lean Meta Elab Tactic Sym Std Do SpecAttr
 
diff --git a/tests/bench/mvcgen/sym/cases/Cases/LetBinding.lean b/tests/bench/mvcgen/sym/cases/Cases/LetBinding.lean
index 9491b61dda..18ec44b38d 100644
--- a/tests/bench/mvcgen/sym/cases/Cases/LetBinding.lean
+++ b/tests/bench/mvcgen/sym/cases/Cases/LetBinding.lean
@@ -1,5 +1,5 @@
 import Lean
-import VCGen
+import Std.Tactic.Do
 
 open Lean Meta Elab Tactic Sym Std Do SpecAttr
 
diff --git a/tests/bench/mvcgen/sym/cases/Cases/MatchIota.lean b/tests/bench/mvcgen/sym/cases/Cases/MatchIota.lean
index 9fbfd1abe1..6c4db17f49 100644
--- a/tests/bench/mvcgen/sym/cases/Cases/MatchIota.lean
+++ b/tests/bench/mvcgen/sym/cases/Cases/MatchIota.lean
@@ -1,5 +1,5 @@
 import Lean
-import VCGen
+import Std.Tactic.Do
 
 open Lean Meta Elab Tactic Sym Std Do SpecAttr
 
diff --git a/tests/bench/mvcgen/sym/cases/Cases/MatchSplit.lean b/tests/bench/mvcgen/sym/cases/Cases/MatchSplit.lean
index 7cac619f40..c5e3c36bae 100644
--- a/tests/bench/mvcgen/sym/cases/Cases/MatchSplit.lean
+++ b/tests/bench/mvcgen/sym/cases/Cases/MatchSplit.lean
@@ -1,5 +1,5 @@
 import Lean
-import VCGen
+import Std.Tactic.Do
 
 open Lean Meta Elab Tactic Sym Std Do SpecAttr
 
diff --git a/tests/bench/mvcgen/sym/cases/Cases/PurePrecond.lean b/tests/bench/mvcgen/sym/cases/Cases/PurePrecond.lean
index ba4e69ed5a..64409ab4bb 100644
--- a/tests/bench/mvcgen/sym/cases/Cases/PurePrecond.lean
+++ b/tests/bench/mvcgen/sym/cases/Cases/PurePrecond.lean
@@ -1,5 +1,5 @@
 import Lean
-import VCGen
+import Std.Tactic.Do
 
 open Lean Meta Elab Tactic Sym Std Do SpecAttr
 
diff --git a/tests/bench/mvcgen/sym/cases/Cases/ReaderState.lean b/tests/bench/mvcgen/sym/cases/Cases/ReaderState.lean
index 485cc4ec55..e7068e58f5 100644
--- a/tests/bench/mvcgen/sym/cases/Cases/ReaderState.lean
+++ b/tests/bench/mvcgen/sym/cases/Cases/ReaderState.lean
@@ -1,5 +1,5 @@
 import Lean
-import VCGen
+import Std.Tactic.Do
 
 open Lean Meta Elab Tactic Sym Std Do SpecAttr
 
diff --git a/tests/bench/mvcgen/sym/lakefile.lean b/tests/bench/mvcgen/sym/lakefile.lean
index 1caba0e44f..f9e2043ac5 100644
--- a/tests/bench/mvcgen/sym/lakefile.lean
+++ b/tests/bench/mvcgen/sym/lakefile.lean
@@ -4,9 +4,6 @@ open System Lake DSL
 package mvcgen_bench where
   precompileModules := true
 
-lean_lib VCGen where
-  srcDir := "lib"
-
 lean_lib Baseline where
   srcDir := "lib"
 
diff --git a/tests/bench/mvcgen/sym/mwe_frame.lean b/tests/bench/mvcgen/sym/mwe_frame.lean
index 7e8d62543c..b612594150 100644
--- a/tests/bench/mvcgen/sym/mwe_frame.lean
+++ b/tests/bench/mvcgen/sym/mwe_frame.lean
@@ -4,6 +4,8 @@ MWE: `mvcgen'` loses precondition facts in postcondition entailment VCs.
 import Cases
 import Driver
 
+set_option mvcgen.warning false
+
 open Lean Std Do
 
 @[irreducible] def myFun (n : Nat) : StateM Nat Nat := return n
diff --git a/tests/bench/mvcgen/sym/test_do_logic.lean b/tests/bench/mvcgen/sym/test_do_logic.lean
index d5fd15fb28..27e0d6d8f0 100644
--- a/tests/bench/mvcgen/sym/test_do_logic.lean
+++ b/tests/bench/mvcgen/sym/test_do_logic.lean
@@ -3,10 +3,11 @@ Copyright (c) 2025 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Graf
 -/
-module
 import Lean
 import Std
-import VCGen
+import Std.Tactic.Do
+
+set_option mvcgen.warning false
 
 /-!
 # Do-logic tests for `mvcgen'`
diff --git a/tests/bench/mvcgen/sym/test_vcgen.lean b/tests/bench/mvcgen/sym/test_vcgen.lean
index 871245cd72..1c802bd03a 100644
--- a/tests/bench/mvcgen/sym/test_vcgen.lean
+++ b/tests/bench/mvcgen/sym/test_vcgen.lean
@@ -6,6 +6,8 @@ Authors: Sebastian Graf
 import Cases
 import Driver
 
+set_option mvcgen.warning false
+
 /-!
 # VCGen Test Suite
 
diff --git a/tests/bench/mvcgen/sym/vcgen_add_sub_cancel.lean b/tests/bench/mvcgen/sym/vcgen_add_sub_cancel.lean
index f9ecf16bb1..e00a78bcab 100644
--- a/tests/bench/mvcgen/sym/vcgen_add_sub_cancel.lean
+++ b/tests/bench/mvcgen/sym/vcgen_add_sub_cancel.lean
@@ -6,6 +6,8 @@ Authors: Sebastian Graf
 import Cases.AddSubCancel
 import Driver
 
+set_option mvcgen.warning false
+
 open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
 open AddSubCancel
 
diff --git a/tests/bench/mvcgen/sym/vcgen_add_sub_cancel_deep.lean b/tests/bench/mvcgen/sym/vcgen_add_sub_cancel_deep.lean
index 310b81e609..4f26ff1667 100644
--- a/tests/bench/mvcgen/sym/vcgen_add_sub_cancel_deep.lean
+++ b/tests/bench/mvcgen/sym/vcgen_add_sub_cancel_deep.lean
@@ -6,6 +6,8 @@ Authors: Sebastian Graf
 import Cases.AddSubCancelDeep
 import Driver
 
+set_option mvcgen.warning false
+
 open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
 open AddSubCancelDeep
 
diff --git a/tests/bench/mvcgen/sym/vcgen_add_sub_cancel_simp.lean b/tests/bench/mvcgen/sym/vcgen_add_sub_cancel_simp.lean
index 876f2a0109..5864fe49c7 100644
--- a/tests/bench/mvcgen/sym/vcgen_add_sub_cancel_simp.lean
+++ b/tests/bench/mvcgen/sym/vcgen_add_sub_cancel_simp.lean
@@ -6,6 +6,8 @@ Authors: Sebastian Graf
 import Cases.AddSubCancelSimp
 import Driver
 
+set_option mvcgen.warning false
+
 open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
 open AddSubCancelSimp
 
diff --git a/tests/bench/mvcgen/sym/vcgen_get_throw_set.lean b/tests/bench/mvcgen/sym/vcgen_get_throw_set.lean
index 998583fee4..bf78a7faa4 100644
--- a/tests/bench/mvcgen/sym/vcgen_get_throw_set.lean
+++ b/tests/bench/mvcgen/sym/vcgen_get_throw_set.lean
@@ -6,6 +6,8 @@ Authors: Sebastian Graf
 import Cases.GetThrowSet
 import Driver
 
+set_option mvcgen.warning false
+
 open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
 open GetThrowSet
 
diff --git a/tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean b/tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean
index bcebf50ec7..26504feb8c 100644
--- a/tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean
+++ b/tests/bench/mvcgen/sym/vcgen_get_throw_set_grind.lean
@@ -1,6 +1,8 @@
 import Cases.GetThrowSet
 import Driver
 
+set_option mvcgen.warning false
+
 open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
 open GetThrowSet
 
diff --git a/tests/bench/mvcgen/sym/vcgen_match_split.lean b/tests/bench/mvcgen/sym/vcgen_match_split.lean
index 33f63a5f6d..7b3cec1c31 100644
--- a/tests/bench/mvcgen/sym/vcgen_match_split.lean
+++ b/tests/bench/mvcgen/sym/vcgen_match_split.lean
@@ -6,6 +6,8 @@ Authors: Sebastian Graf
 import Cases.MatchIota
 import Driver
 
+set_option mvcgen.warning false
+
 open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
 open MatchIota
 
diff --git a/tests/bench/mvcgen/sym/vcgen_pure_precond.lean b/tests/bench/mvcgen/sym/vcgen_pure_precond.lean
index 481438ae0a..ebe766ee50 100644
--- a/tests/bench/mvcgen/sym/vcgen_pure_precond.lean
+++ b/tests/bench/mvcgen/sym/vcgen_pure_precond.lean
@@ -6,6 +6,8 @@ Authors: Sebastian Graf
 import Cases.PurePrecond
 import Driver
 
+set_option mvcgen.warning false
+
 open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
 open PurePrecond
 
diff --git a/tests/bench/mvcgen/sym/vcgen_reader_state.lean b/tests/bench/mvcgen/sym/vcgen_reader_state.lean
index 71ddbdf8a5..f76565c521 100644
--- a/tests/bench/mvcgen/sym/vcgen_reader_state.lean
+++ b/tests/bench/mvcgen/sym/vcgen_reader_state.lean
@@ -6,6 +6,8 @@ Authors: Sebastian Graf
 import Cases.ReaderState
 import Driver
 
+set_option mvcgen.warning false
+
 open Lean Parser Meta Elab Tactic Sym Std Do SpecAttr
 open ReaderState