diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean
index 0410b6b3bb0d..dc12594dc77e 100644
--- a/src/Lean/Elab/Tactic/Do/VCGen.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen.lean
@@ -464,7 +464,7 @@ where
 @[builtin_tactic Lean.Parser.Tactic.mvcgen]
 def elabMVCGen : Tactic := fun stx => withMainContext do
   if mvcgen.warning.get (← getOptions) then
-    logWarningAt stx "The `mvcgen` tactic is experimental and still under development. Avoid using it in production projects."
+    logWarningAt stx "The `mvcgen` tactic is new and its behavior may change in the future. This project has used `set_option mvcgen.warning true` to discourage its use."
   let ctx ← mkSpecContext stx[1] stx[2]
   let fuel := match ctx.config.stepLimit with
     | some n => .limited n
diff --git a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean
index 031f9be54206..5a5cbc954d14 100644
--- a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean
@@ -18,9 +18,9 @@ open Lean Parser Elab Tactic Meta Do SpecAttr
 builtin_initialize registerTraceClass `Elab.Tactic.Do.vcgen
 
 register_builtin_option mvcgen.warning : Bool := {
-  defValue := true
+  defValue := false
   group    := "debug"
-  descr    := "disable `mvcgen` usage warning"
+  descr    := "enable `mvcgen` usage warning"
 }
 
 inductive Fuel where