diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index e6c6b0a3c4..40f29a3b3b 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -320,7 +320,6 @@ public enum ContractTestingMode {
     public PrintModes PrintMode = PrintModes.Everything; // Default to printing everything
     public bool DafnyVerify = true;
     public string DafnyPrintResolvedFile = null;
-    public string BoogieExtractionTargetFile = null;
     public List<string> DafnyPrintExportedViews = new List<string>();
     public bool Compile = true;
     public List<string> MainArgs = new List<string>();
diff --git a/Source/DafnyCore/Prelude/Makefile b/Source/DafnyCore/Prelude/Makefile
index 94e8c4b834..2010229bbe 100644
--- a/Source/DafnyCore/Prelude/Makefile
+++ b/Source/DafnyCore/Prelude/Makefile
@@ -15,6 +15,6 @@ DafnyPrelude.bpl: PreludeCore.bpl Sequences.bpl
 	sed -e "s|PRIME|'|g" -i "" PreludeCore.bpl Sequences.bpl DafnyPrelude.bpl
 
 Sequences.bpl: Lists.dfy Boxes.dfy Sequences.dfy
-	$(DAFNY) verify Lists.dfy Boxes.dfy Sequences.dfy --extract:Sequences.bpl
+	$(DAFNY) extract Sequences.bpl Lists.dfy Boxes.dfy Sequences.dfy
 	# Remove trailing spaces that the Boogie pretty printer emits
 	sed -e "s| *$$||" -i "" Sequences.bpl
diff --git a/Source/DafnyCore/Backends/BoogieExtractor.cs b/Source/DafnyDriver/Commands/BoogieExtractor.cs
similarity index 100%
rename from Source/DafnyCore/Backends/BoogieExtractor.cs
rename to Source/DafnyDriver/Commands/BoogieExtractor.cs
diff --git a/Source/DafnyDriver/Commands/ExtractCommand.cs b/Source/DafnyDriver/Commands/ExtractCommand.cs
new file mode 100644
index 0000000000..b8f12a5c7a
--- /dev/null
+++ b/Source/DafnyDriver/Commands/ExtractCommand.cs
@@ -0,0 +1,59 @@
+#nullable enable
+using System.Collections.Generic;
+using System.CommandLine;
+using System.IO;
+using System.Threading.Tasks;
+using DafnyDriver.Commands;
+using Microsoft.Boogie;
+using Microsoft.Dafny.Compilers;
+
+namespace Microsoft.Dafny;
+
+public static class ExtractCommand {
+  public static Command Create() {
+
+    var result = new Command("extract", "Can be used to generate DafnyPrelude.bpl. Uses the ':extract_boogie_name' attribute to rename symbols. Turns lemmas into universally quantified axioms, as opposed to verify which turns them into Boogie procedures. When translating Dafny expressions to Boogie ones, no well-formedness checks are created.");
+
+    result.IsHidden = true;
+    result.AddArgument(Target);
+    result.AddArgument(DafnyCommands.FilesArgument);
+    foreach (var option in ExtractOptions) {
+      result.AddOption(option);
+    }
+    DafnyNewCli.SetHandlerUsingDafnyOptionsContinuation(result, (options, _) => HandleExtraction(options));
+    return result;
+  }
+
+  private static readonly Argument<FileInfo> Target = new("The path of the extracted file.");
+
+  private static IReadOnlyList<Option> ExtractOptions =>
+    new Option[] { }.
+      Concat(DafnyCommands.ConsoleOutputOptions).
+      Concat(DafnyCommands.ResolverOptions);
+
+  public static async Task<int> HandleExtraction(DafnyOptions options) {
+    if (options.Get(CommonOptionBag.VerificationCoverageReport) != null) {
+      options.TrackVerificationCoverage = true;
+    }
+
+    var compilation = CliCompilation.Create(options);
+    compilation.Start();
+
+    var resolution = await compilation.Resolution;
+    if (resolution is not { HasErrors: false }) {
+      return await compilation.GetAndReportExitCode();
+    }
+
+    var outputPath = options.Get(Target).FullName;
+    using var engine = ExecutionEngine.CreateWithoutSharedCache(options);
+    try {
+      var extractedProgram = BoogieExtractor.Extract(resolution.ResolvedProgram);
+      engine.PrintBplFile(outputPath, extractedProgram, true, pretty: true);
+    } catch (ExtractorError extractorError) {
+      await options.OutputWriter.WriteLineAsync($"Boogie axiom extraction error: {extractorError.Message}");
+      return 1;
+    }
+
+    return await compilation.GetAndReportExitCode();
+  }
+}
diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs
index 6072bd5dd3..12a8e440e9 100644
--- a/Source/DafnyDriver/Commands/VerifyCommand.cs
+++ b/Source/DafnyDriver/Commands/VerifyCommand.cs
@@ -22,13 +22,6 @@ static VerifyCommand() {
     OptionRegistry.RegisterOption(FilterSymbol, OptionScope.Cli);
     OptionRegistry.RegisterOption(FilterPosition, OptionScope.Cli);
     OptionRegistry.RegisterOption(PerformanceStatisticsOption, OptionScope.Cli);
-    OptionRegistry.RegisterOption(ExtractTarget, OptionScope.Cli);
-
-    DafnyOptions.RegisterLegacyBinding(ExtractTarget, (options, f) => {
-      options.BoogieExtractionTargetFile = f;
-      options.ExpandFilename(options.BoogieExtractionTargetFile, x => options.BoogieExtractionTargetFile = x, options.LogPrefix,
-        options.FileTimestamp);
-    });
   }
 
   public static readonly Option<int> PerformanceStatisticsOption = new("--performance-stats",
@@ -42,13 +35,6 @@ static VerifyCommand() {
   public static readonly Option<string> FilterPosition = new("--filter-position",
     @"Filter what gets verified based on a source location. The location is specified as a file path suffix, optionally followed by a colon and a line number. For example, `dafny verify dfyconfig.toml --filter-position=source1.dfy:5` will only verify things that range over line 5 in the file `source1.dfy`. In combination with `--isolate-assertions`, individual assertions can be verified by filtering on the line that contains them. When processing a single file, the filename can be skipped, for example: `dafny verify MyFile.dfy --filter-position=:23`");
 
-  public static readonly Option<string> ExtractTarget = new("--extract", @"
-Extract Dafny types, functions, and lemmas to Boogie.
-(use - as <file> to output to console.)".TrimStart()) {
-    IsHidden = true,
-    ArgumentHelpName = "file",
-  };
-
   public static Command Create() {
     var result = new Command("verify", "Verify the program.");
     result.AddArgument(DafnyCommands.FilesArgument);
@@ -64,7 +50,6 @@ public static Command Create() {
         PerformanceStatisticsOption,
         FilterSymbol,
         FilterPosition,
-        ExtractTarget,
         DafnyFile.DoNotVerifyDependencies
       }.Concat(DafnyCommands.VerificationOptions).
       Concat(DafnyCommands.ConsoleOutputOptions).
@@ -91,21 +76,11 @@ public static async Task<int> HandleVerification(DafnyOptions options) {
       await verificationSummarized;
       await verificationResultsLogged;
       await proofDependenciesReported;
-
-      if (!resolution.HasErrors && options.BoogieExtractionTargetFile != null) {
-        using var engine = ExecutionEngine.CreateWithoutSharedCache(options);
-        try {
-          var extractedProgram = BoogieExtractor.Extract(resolution.ResolvedProgram);
-          engine.PrintBplFile(options.BoogieExtractionTargetFile, extractedProgram, true, pretty: true);
-        } catch (ExtractorError extractorError) {
-          await options.OutputWriter.WriteLineAsync($"Boogie axiom extraction error: {extractorError.Message}");
-          return 1;
-        }
-      }
     }
 
     return await compilation.GetAndReportExitCode();
   }
+
   public static async Task ReportVerificationSummary(
     CliCompilation cliCompilation,
     IObservable<CanVerifyResult> verificationResults) {
diff --git a/Source/DafnyDriver/DafnyNewCli.cs b/Source/DafnyDriver/DafnyNewCli.cs
index 2c95f92743..26ea4b8187 100644
--- a/Source/DafnyDriver/DafnyNewCli.cs
+++ b/Source/DafnyDriver/DafnyNewCli.cs
@@ -2,7 +2,6 @@
 using System;
 using System.Collections;
 using System.Collections.Generic;
-using System.Collections.Immutable;
 using System.CommandLine;
 using System.CommandLine.Builder;
 using System.CommandLine.Invocation;
@@ -11,16 +10,12 @@
 using System.IO;
 using System.Linq;
 using System.Reflection;
-using System.Security.AccessControl;
-using System.Text.RegularExpressions;
 using System.Threading.Tasks;
 using DafnyCore;
-using DafnyCore.Options;
 using DafnyDriver.Commands;
 using Microsoft.Boogie;
 using Microsoft.Dafny.Compilers;
 using Microsoft.Dafny.LanguageServer;
-using Microsoft.Dafny.LanguageServer.Workspace;
 
 namespace Microsoft.Dafny;
 
@@ -50,6 +45,7 @@ static DafnyNewCli() {
     AddCommand(AuditCommand.Create());
     AddCommand(CoverageReportCommand.Create());
     AddCommand(DocumentationCommand.Create());
+    AddCommand(ExtractCommand.Create());
 
     OptionRegistry.CheckOptionsAreKnown(AllOptions);
 
@@ -176,12 +172,7 @@ private static void ProcessOption(InvocationContext context, Option option, Dafn
   }
 
   public static Task<int> Execute(IConsole console, IReadOnlyList<string> arguments) {
-    bool allowHidden = arguments.All(a => a != ToolchainDebuggingHelpName);
     foreach (var symbol in AllSymbols) {
-      if (!allowHidden) {
-        symbol.IsHidden = false;
-      }
-
       if (symbol is Option option) {
         if (!option.Arity.Equals(ArgumentArity.ZeroOrMore) && !option.Arity.Equals(ArgumentArity.OneOrMore)) {
           option.AllowMultipleArgumentsPerToken = true;
@@ -261,8 +252,16 @@ private static CommandLineBuilder AddDeveloperHelp(RootCommand rootCommand, Comm
     var languageDeveloperHelp = new Option<bool>(ToolchainDebuggingHelpName,
       "Show help and usage information, including options designed for developing the Dafny language and toolchain.");
     rootCommand.AddGlobalOption(languageDeveloperHelp);
+    bool helpShown = false;
+    builder = builder.UseHelp(_ => helpShown = true);
+
     builder = builder.AddMiddleware(async (context, next) => {
-      if (context.ParseResult.FindResultFor(languageDeveloperHelp) is { }) {
+      if ((context.ParseResult.CommandResult.Command.IsHidden && helpShown) || context.ParseResult.FindResultFor(languageDeveloperHelp) is { }) {
+
+        foreach (var symbol in AllSymbols) {
+          symbol.IsHidden = false;
+        }
+
         context.InvocationResult = new HelpResult();
       } else {
         await next(context);