diff --git a/Source/DafnyCore/Backends/ExecutableBackend.cs b/Source/DafnyCore/Backends/ExecutableBackend.cs
index f54fbd79826..add4996feac 100644
--- a/Source/DafnyCore/Backends/ExecutableBackend.cs
+++ b/Source/DafnyCore/Backends/ExecutableBackend.cs
@@ -6,9 +6,10 @@
 using System.IO;
 using System.Linq;
 using System.Threading.Tasks;
+using Microsoft.Dafny.Compilers;
 using Microsoft.Dafny.Plugins;
 
-namespace Microsoft.Dafny.Compilers;
+namespace Microsoft.Dafny;
 
 public abstract class ExecutableBackend : IExecutableBackend {
   // May be null for backends that don't use the single-pass compiler logic
diff --git a/Source/DafnyCore/Backends/GoLang/GoBackend.cs b/Source/DafnyCore/Backends/GoLang/GoBackend.cs
index 6b3068e48ff..2b67b0c83c9 100644
--- a/Source/DafnyCore/Backends/GoLang/GoBackend.cs
+++ b/Source/DafnyCore/Backends/GoLang/GoBackend.cs
@@ -5,8 +5,9 @@
 using System.IO;
 using System.Text.RegularExpressions;
 using System.Threading.Tasks;
+using Microsoft.Dafny.Compilers;
 
-namespace Microsoft.Dafny.Compilers;
+namespace Microsoft.Dafny;
 
 public class GoBackend : ExecutableBackend {
 
@@ -190,7 +191,7 @@ bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram, TextW
 
   private static string FindPackageName(string externFilename) {
     using var rd = new StreamReader(new FileStream(externFilename, FileMode.Open, FileAccess.Read));
-    while (rd.ReadLine() is string line) {
+    while (rd.ReadLine() is { } line) {
       var match = PackageLine.Match(line);
       if (match.Success) {
         return match.Groups[1].Value;
diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs
index bd14bbb398b..37b38cbe198 100644
--- a/Source/DafnyCore/Pipeline/Compilation.cs
+++ b/Source/DafnyCore/Pipeline/Compilation.cs
@@ -462,17 +462,21 @@ public void Dispose() {
     CancelPendingUpdates();
   }
 
-  public static List<DafnyDiagnostic> GetDiagnosticsFromResult(DafnyOptions options, Uri uri, IVerificationTask task, VerificationRunResult result) {
+  public static List<DafnyDiagnostic> GetDiagnosticsFromResult(DafnyOptions options, Uri uri, ICanVerify canVerify,
+    IVerificationTask task, VerificationRunResult result) {
     var errorReporter = new ObservableErrorReporter(options, uri);
     List<DafnyDiagnostic> diagnostics = new();
     errorReporter.Updates.Subscribe(d => diagnostics.Add(d.Diagnostic));
 
-    ReportDiagnosticsInResult(options, task, result, errorReporter);
+    ReportDiagnosticsInResult(options, canVerify.NameToken.val, task.ScopeToken,
+      task.Split.Implementation.GetTimeLimit(options), result, errorReporter);
 
     return diagnostics.OrderBy(d => d.Token.GetLspPosition()).ToList();
   }
 
-  public static void ReportDiagnosticsInResult(DafnyOptions options, IVerificationTask task, VerificationRunResult result,
+  public static void ReportDiagnosticsInResult(DafnyOptions options, string name, Boogie.IToken token,
+    uint timeLimit,
+    VerificationRunResult result,
     ErrorReporter errorReporter) {
     var outcome = GetOutcome(result.Outcome);
     result.CounterExamples.Sort(new CounterexampleComparer());
@@ -485,10 +489,9 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, IVerification
     // The Boogie API forces us to create a temporary engine here to report the outcome, even though it only uses the options.
     var boogieEngine = new ExecutionEngine(options, new VerificationResultCache(),
       CustomStackSizePoolTaskScheduler.Create(0, 0));
-    var implementation = task.Split.Implementation;
     boogieEngine.ReportOutcome(null, outcome, outcomeError => errorReporter.ReportBoogieError(outcomeError, false),
-      implementation.VerboseName, implementation.tok, null, TextWriter.Null,
-      implementation.GetTimeLimit(options), result.CounterExamples);
+      name, token, null, TextWriter.Null,
+      timeLimit, result.CounterExamples);
   }
 
   public static VcOutcome GetOutcome(SolverOutcome outcome) {
diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs
index f978623dfa6..319302df28f 100644
--- a/Source/DafnyCore/ProofDependencyWarnings.cs
+++ b/Source/DafnyCore/ProofDependencyWarnings.cs
@@ -8,17 +8,19 @@
 
 namespace Microsoft.Dafny;
 
+public record VerificationTaskResult(IVerificationTask Task, VerificationRunResult Result);
+
 public class ProofDependencyWarnings {
 
 
-  public static void ReportSuspiciousDependencies(DafnyOptions options, IEnumerable<(IVerificationTask Task, Completed Result)> parts,
+  public static void ReportSuspiciousDependencies(DafnyOptions options, IEnumerable<VerificationTaskResult> parts,
     ErrorReporter reporter, ProofDependencyManager manager) {
     foreach (var resultsForScope in parts.GroupBy(p => p.Task.ScopeId)) {
       WarnAboutSuspiciousDependenciesForImplementation(options,
         reporter,
         manager,
         resultsForScope.Key,
-        resultsForScope.Select(p => p.Result.Result).ToList());
+        resultsForScope.Select(p => p.Result).ToList());
     }
   }
 
diff --git a/Source/DafnyDriver/CliCanVerifyState.cs b/Source/DafnyDriver/CliCanVerifyState.cs
index 110a6c7cc0a..e74c060d737 100644
--- a/Source/DafnyDriver/CliCanVerifyState.cs
+++ b/Source/DafnyDriver/CliCanVerifyState.cs
@@ -9,6 +9,6 @@ namespace DafnyDriver.Commands;
 public record CliCanVerifyState {
   public Func<IVerificationTask, bool> TaskFilter = _ => true;
   public readonly TaskCompletionSource Finished = new();
-  public readonly ConcurrentBag<(IVerificationTask Task, Completed Result)> CompletedParts = new();
+  public readonly ConcurrentQueue<(IVerificationTask Task, Completed Result)> CompletedParts = new();
   public readonly ConcurrentBag<IVerificationTask> Tasks = new();
 }
\ No newline at end of file
diff --git a/Source/DafnyDriver/CliCompilation.cs b/Source/DafnyDriver/CliCompilation.cs
index 63a99dd426b..f1449aaf8ea 100644
--- a/Source/DafnyDriver/CliCompilation.cs
+++ b/Source/DafnyDriver/CliCompilation.cs
@@ -4,6 +4,7 @@
 using System.Collections.Generic;
 using System.IO;
 using System.Linq;
+using System.Reactive.Subjects;
 using System.Text.RegularExpressions;
 using System.Threading;
 using System.Threading.Tasks;
@@ -13,23 +14,22 @@
 using Microsoft.Dafny.LanguageServer.Language.Symbols;
 using Microsoft.Dafny.LanguageServer.Workspace;
 using Microsoft.Extensions.Logging;
-using VC;
 using Token = Microsoft.Dafny.Token;
 using Util = Microsoft.Dafny.Util;
 
 namespace DafnyDriver.Commands;
 
-
-public record VerificationTaskResult(IVerificationTask Task, VerificationRunResult Result);
-
 public record CanVerifyResult(ICanVerify CanVerify, IReadOnlyList<VerificationTaskResult> Results);
 
-public class CliCompilation {
+public class CliCompilation : IDisposable {
   private readonly DafnyOptions options;
 
   private Compilation Compilation { get; }
   private readonly ConcurrentDictionary<MessageSource, int> errorsPerSource = new();
   private int errorCount;
+  private bool verifiedAssertions;
+
+  private readonly List<IDisposable> disposables = new();
 
   private CliCompilation(
     CreateCompilation createCompilation,
@@ -74,6 +74,22 @@ bool HasErrorsFromSource(MessageSource source) {
 
   public Task<ResolutionResult> Resolution => Compilation.Resolution;
 
+  public static CliCompilation Create(DafnyOptions options) {
+    var fileSystem = OnDiskFileSystem.Instance;
+    ILoggerFactory factory = new LoggerFactory();
+    var telemetryPublisher = new CliTelemetryPublisher(factory.CreateLogger<TelemetryPublisherBase>());
+    return new CliCompilation(CreateCompilation, options);
+
+    Compilation CreateCompilation(ExecutionEngine engine, CompilationInput input) =>
+      new(factory.CreateLogger<Compilation>(), fileSystem,
+        new TextDocumentLoader(factory.CreateLogger<ITextDocumentLoader>(),
+          new DafnyLangParser(options, fileSystem, telemetryPublisher,
+            factory.CreateLogger<DafnyLangParser>(),
+            factory.CreateLogger<CachingParser>()),
+          new DafnyLangSymbolResolver(factory.CreateLogger<DafnyLangSymbolResolver>(), factory.CreateLogger<CachingResolver>(), telemetryPublisher)),
+        new DafnyProgramVerifier(factory.CreateLogger<DafnyProgramVerifier>()), engine, input);
+  }
+
   public void Start() {
     if (Compilation.Started) {
       throw new InvalidOperationException("Compilation was already started");
@@ -114,25 +130,20 @@ public void Start() {
     Compilation.Start();
   }
 
-  public static CliCompilation Create(DafnyOptions options) {
-    var fileSystem = OnDiskFileSystem.Instance;
-    ILoggerFactory factory = new LoggerFactory();
-    var telemetryPublisher = new CliTelemetryPublisher(factory.CreateLogger<TelemetryPublisherBase>());
-    return new CliCompilation(CreateCompilation, options);
-
-    Compilation CreateCompilation(ExecutionEngine engine, CompilationInput input) =>
-      new(factory.CreateLogger<Compilation>(), fileSystem,
-        new TextDocumentLoader(factory.CreateLogger<ITextDocumentLoader>(),
-          new DafnyLangParser(options, fileSystem, telemetryPublisher,
-            factory.CreateLogger<DafnyLangParser>(),
-            factory.CreateLogger<CachingParser>()),
-          new DafnyLangSymbolResolver(factory.CreateLogger<DafnyLangSymbolResolver>(), factory.CreateLogger<CachingResolver>(), telemetryPublisher)),
-        new DafnyProgramVerifier(factory.CreateLogger<DafnyProgramVerifier>()), engine, input);
+  public IObservable<CanVerifyResult> VerificationResults => verificationResults;
+  private readonly Subject<CanVerifyResult> verificationResults = new();
+  private bool didVerification;
+
+  public Task VerifyAll() {
+    var task = new TaskCompletionSource();
+    verificationResults.Subscribe(_ => { }, e =>
+      task.TrySetException(e), () =>
+      task.TrySetResult());
+    VerifyAllLazily().ToObservable().Subscribe(verificationResults);
+    return task.Task;
   }
 
-  public async Task VerifyAllAndPrintSummary() {
-    var statistics = new VerificationStatistics();
-
+  private async IAsyncEnumerable<CanVerifyResult> VerifyAllLazily() {
     var canVerifyResults = new Dictionary<ICanVerify, CliCanVerifyState>();
     Compilation.Updates.Subscribe(ev => {
 
@@ -152,42 +163,12 @@ public async Task VerifyAllAndPrintSummary() {
         canVerifyResult.Finished.SetException(boogieException.Exception);
       }
 
-      if (ev is BoogieUpdate boogieUpdate) {
-        if (boogieUpdate.BoogieStatus is Completed completed) {
-          var canVerifyResult = canVerifyResults[boogieUpdate.CanVerify];
-          canVerifyResult.CompletedParts.Add((boogieUpdate.VerificationTask, completed));
-
-          switch (completed.Result.Outcome) {
-            case SolverOutcome.Valid:
-            case SolverOutcome.Bounded:
-              Interlocked.Increment(ref statistics.VerifiedSymbols);
-              Interlocked.Add(ref statistics.VerifiedAssertions, completed.Result.Asserts.Count);
-              break;
-            case SolverOutcome.Invalid:
-              var total = completed.Result.Asserts.Count;
-              var errors = completed.Result.CounterExamples.Count;
-              Interlocked.Add(ref statistics.VerifiedAssertions, total - errors);
-              Interlocked.Add(ref statistics.ErrorCount, errors);
-              break;
-            case SolverOutcome.TimeOut:
-              Interlocked.Increment(ref statistics.TimeoutCount);
-              break;
-            case SolverOutcome.OutOfMemory:
-              Interlocked.Increment(ref statistics.OutOfMemoryCount);
-              break;
-            case SolverOutcome.OutOfResource:
-              Interlocked.Increment(ref statistics.OutOfResourceCount);
-              break;
-            case SolverOutcome.Undetermined:
-              Interlocked.Increment(ref statistics.InconclusiveCount);
-              break;
-            default:
-              throw new ArgumentOutOfRangeException();
-          }
-
-          if (canVerifyResult.CompletedParts.Count == canVerifyResult.Tasks.Count) {
-            canVerifyResult.Finished.TrySetResult();
-          }
+      if (ev is BoogieUpdate { BoogieStatus: Completed completed } boogieUpdate) {
+        var canVerifyResult = canVerifyResults[boogieUpdate.CanVerify];
+        canVerifyResult.CompletedParts.Enqueue((boogieUpdate.VerificationTask, completed));
+
+        if (canVerifyResult.CompletedParts.Count == canVerifyResult.Tasks.Count) {
+          canVerifyResult.Finished.TrySetResult();
         }
       }
     });
@@ -197,107 +178,66 @@ public async Task VerifyAllAndPrintSummary() {
       resolution = await Compilation.Resolution;
     } catch (OperationCanceledException) {
       // Failed to resolve the program due to a user error.
-      return;
+      yield break;
     }
 
     if (errorCount > 0) {
-      return;
+      yield break;
     }
 
+    didVerification = true;
+
     var canVerifies = resolution.CanVerifies?.DistinctBy(v => v.Tok).ToList();
 
-    var verifiedAssertions = false;
-    if (canVerifies != null) {
-      canVerifies = FilterCanVerifies(canVerifies, out var line);
-      verifiedAssertions = line != null;
-
-      var orderedCanVerifies = canVerifies.OrderBy(v => v.Tok.pos).ToList();
-      foreach (var canVerify in orderedCanVerifies) {
-        var results = new CliCanVerifyState();
-        canVerifyResults[canVerify] = results;
-        if (line != null) {
-          results.TaskFilter = t => KeepVerificationTask(t, line.Value);
-        }
+    if (canVerifies == null) {
+      yield break;
+    }
 
-        await Compilation.VerifyCanVerify(canVerify, results.TaskFilter);
-      }
+    canVerifies = FilterCanVerifies(canVerifies, out var line);
+    verifiedAssertions = line != null;
 
-      var usedDependencies = new HashSet<TrackedNodeComponent>();
-      var proofDependencyManager = resolution.ResolvedProgram.ProofDependencyManager;
-      VerificationResultLogger? verificationResultLogger = null;
-      try {
-        verificationResultLogger = new VerificationResultLogger(options, proofDependencyManager);
-      } catch (ArgumentException e) {
-        Compilation.Reporter.Error(MessageSource.Verifier, Compilation.Project.StartingToken, e.Message);
+    var orderedCanVerifies = canVerifies.OrderBy(v => v.Tok.pos).ToList();
+    foreach (var canVerify in orderedCanVerifies) {
+      var results = new CliCanVerifyState();
+      canVerifyResults[canVerify] = results;
+      if (line != null) {
+        results.TaskFilter = t => KeepVerificationTask(t, line.Value);
       }
 
-      foreach (var canVerify in orderedCanVerifies) {
-        var results = canVerifyResults[canVerify];
-        try {
-          var timeLimitSeconds = TimeSpan.FromSeconds(options.Get(BoogieOptionBag.VerificationTimeLimit));
-          var tasks = new List<Task>() { results.Finished.Task };
-          if (timeLimitSeconds.Seconds != 0) {
-            tasks.Add(Task.Delay(timeLimitSeconds));
-          }
-
-          await Task.WhenAny(tasks);
-          if (!results.Finished.Task.IsCompleted) {
-            Compilation.Reporter.Error(MessageSource.Verifier, canVerify.Tok,
-              "Dafny encountered an internal error while waiting for this symbol to verify. Please report it at <https://github.com/dafny-lang/dafny/issues>.\n");
-            break;
-          }
-
-          await results.Finished.Task;
-
-          // We use an intermediate reporter so we can sort the diagnostics from all parts by token
-          var batchReporter = new BatchErrorReporter(options);
-          foreach (var (task, completed) in results.CompletedParts) {
-            Compilation.ReportDiagnosticsInResult(options, task, completed.Result, batchReporter);
-          }
-
-          foreach (var diagnostic in batchReporter.AllMessages.OrderBy(m => m.Token)) {
-            Compilation.Reporter.Message(diagnostic.Source, diagnostic.Level, diagnostic.ErrorId, diagnostic.Token,
-              diagnostic.Message);
-          }
-
-          var parts = results.CompletedParts;
-          ProofDependencyWarnings.ReportSuspiciousDependencies(options, parts,
-            resolution.ResolvedProgram.Reporter, resolution.ResolvedProgram.ProofDependencyManager);
-
-          verificationResultLogger?.Report(new CanVerifyResult(canVerify,
-            results.CompletedParts.Select(t => new VerificationTaskResult(t.Task, t.Result.Result))
-              .OrderBy(t => t.Result.VcNum).ToList()));
-
-          foreach (var used in results.CompletedParts.SelectMany(part => part.Result.Result.CoveredElements)) {
-            usedDependencies.Add(used);
-          }
-
+      await Compilation.VerifyCanVerify(canVerify, results.TaskFilter);
+    }
 
-        } catch (ProverException e) {
-          Interlocked.Increment(ref statistics.SolverExceptionCount);
-          Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok, e.Message);
-        } catch (OperationCanceledException) { } catch (Exception e) {
-          Interlocked.Increment(ref statistics.SolverExceptionCount);
-          Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok,
-            $"Internal error occurred during verification: {e.Message}\n{e.StackTrace}");
+    foreach (var canVerify in orderedCanVerifies) {
+      var results = canVerifyResults[canVerify];
+      try {
+        var timeLimitSeconds = TimeSpan.FromSeconds(options.Get(BoogieOptionBag.VerificationTimeLimit));
+        var tasks = new List<Task> { results.Finished.Task };
+        if (timeLimitSeconds.Seconds != 0) {
+          tasks.Add(Task.Delay(timeLimitSeconds));
         }
 
-        canVerifyResults.Remove(canVerify); // Free memory
-      }
+        await Task.WhenAny(tasks);
+        if (!results.Finished.Task.IsCompleted) {
+          Compilation.Reporter.Error(MessageSource.Verifier, canVerify.Tok,
+            "Dafny encountered an internal error while waiting for this symbol to verify. Please report it at <https://github.com/dafny-lang/dafny/issues>.\n");
+          break;
+        }
 
-      verificationResultLogger?.Finish();
+        await results.Finished.Task;
+      } catch (ProverException e) {
+        Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok, e.Message);
+        throw;
+      } catch (OperationCanceledException) {
 
-      var coverageReportDir = options.Get(CommonOptionBag.VerificationCoverageReport);
-      if (coverageReportDir != null) {
-        new CoverageReporter(options).SerializeVerificationCoverageReport(
-          proofDependencyManager, resolution.ResolvedProgram,
-          usedDependencies,
-          coverageReportDir);
+      } catch (Exception e) {
+        Compilation.Reporter.Error(MessageSource.Verifier, ResolutionErrors.ErrorId.none, canVerify.Tok,
+          $"Internal error occurred during verification: {e.Message}\n{e.StackTrace}");
+        throw;
       }
-    }
-
+      yield return new CanVerifyResult(canVerify, results.CompletedParts.Select(c => new VerificationTaskResult(c.Task, c.Result.Result)).ToList());
 
-    WriteTrailer(options, /* TODO ErrorWriter? */ options.OutputWriter, verifiedAssertions, statistics);
+      canVerifyResults.Remove(canVerify); // Free memory
+    }
   }
 
   private List<ICanVerify> FilterCanVerifies(List<ICanVerify> canVerifies, out int? line) {
@@ -337,45 +277,144 @@ private bool KeepVerificationTask(IVerificationTask task, int line) {
     return task.ScopeToken.line == line || task.Token.line == line;
   }
 
-  static void WriteTrailer(DafnyOptions options, TextWriter output, bool reportAssertions, VerificationStatistics statistics) {
+  public void ReportVerificationDiagnostics() {
+    VerificationResults.Subscribe(result => {
+      // We use an intermediate reporter so we can sort the diagnostics from all parts by token
+      var batchReporter = new BatchErrorReporter(options);
+      foreach (var completed in result.Results) {
+        Compilation.ReportDiagnosticsInResult(options, result.CanVerify.FullDafnyName, result.CanVerify.NameToken,
+          (uint)completed.Result.RunTime.Seconds,
+          completed.Result, batchReporter);
+      }
+
+      foreach (var diagnostic in batchReporter.AllMessages.OrderBy(m => m.Token)) {
+        Compilation.Reporter.Message(diagnostic.Source, diagnostic.Level, diagnostic.ErrorId, diagnostic.Token,
+          diagnostic.Message);
+      }
+    });
+  }
+
+  public void ReportVerificationSummary() {
+    var statistics = new VerificationStatistics();
+
+    VerificationResults.Subscribe(result => {
+      foreach (var taskResult in result.Results) {
+        var runResult = taskResult.Result;
+
+        switch (runResult.Outcome) {
+          case SolverOutcome.Valid:
+          case SolverOutcome.Bounded:
+            Interlocked.Increment(ref statistics.VerifiedSymbols);
+            Interlocked.Add(ref statistics.VerifiedAssertions, runResult.Asserts.Count);
+            break;
+          case SolverOutcome.Invalid:
+            var total = runResult.Asserts.Count;
+            var errors = runResult.CounterExamples.Count;
+            Interlocked.Add(ref statistics.VerifiedAssertions, total - errors);
+            Interlocked.Add(ref statistics.ErrorCount, errors);
+            break;
+          case SolverOutcome.TimeOut:
+            Interlocked.Increment(ref statistics.TimeoutCount);
+            break;
+          case SolverOutcome.OutOfMemory:
+            Interlocked.Increment(ref statistics.OutOfMemoryCount);
+            break;
+          case SolverOutcome.OutOfResource:
+            Interlocked.Increment(ref statistics.OutOfResourceCount);
+            break;
+          case SolverOutcome.Undetermined:
+            Interlocked.Increment(ref statistics.InconclusiveCount);
+            break;
+          default:
+            throw new ArgumentOutOfRangeException();
+        }
+      }
+    }, e => {
+      Interlocked.Increment(ref statistics.SolverExceptionCount);
+    }, () => {
+      disposables.Add(WriteTrailer(options.OutputWriter, verifiedAssertions, statistics));
+    });
+  }
+
+  private async Task WriteTrailer(TextWriter output, bool reportAssertions, VerificationStatistics statistics) {
     if (options.Verbosity <= CoreOptions.VerbosityLevel.Quiet) {
       return;
     }
 
-    output.WriteLine();
+    if (!didVerification) {
+      return;
+    }
+
+    await output.WriteLineAsync();
 
     if (reportAssertions) {
-      output.Write("{0} finished with {1} assertions verified, {2} error{3}", options.DescriptiveToolName,
-        statistics.VerifiedAssertions, statistics.ErrorCount,
-        Util.Plural(statistics.ErrorCount));
+      await output.WriteAsync($"{options.DescriptiveToolName} finished with {statistics.VerifiedAssertions} assertions verified, {statistics.ErrorCount} error{Util.Plural(statistics.ErrorCount)}");
 
     } else {
-      output.Write("{0} finished with {1} verified, {2} error{3}", options.DescriptiveToolName,
-        statistics.VerifiedSymbols, statistics.ErrorCount,
-        Util.Plural(statistics.ErrorCount));
+      await output.WriteAsync($"{options.DescriptiveToolName} finished with {statistics.VerifiedSymbols} verified, {statistics.ErrorCount} error{Util.Plural(statistics.ErrorCount)}");
     };
     if (statistics.InconclusiveCount != 0) {
-      output.Write(", {0} inconclusive{1}", statistics.InconclusiveCount, Util.Plural(statistics.InconclusiveCount));
+      await output.WriteAsync($", {statistics.InconclusiveCount} inconclusive{Util.Plural(statistics.InconclusiveCount)}");
     }
 
     if (statistics.TimeoutCount != 0) {
-      output.Write(", {0} time out{1}", statistics.TimeoutCount, Util.Plural(statistics.TimeoutCount));
+      await output.WriteAsync($", {statistics.TimeoutCount} time out{Util.Plural(statistics.TimeoutCount)}");
     }
 
     if (statistics.OutOfMemoryCount != 0) {
-      output.Write(", {0} out of memory", statistics.OutOfMemoryCount);
+      await output.WriteAsync($", {statistics.OutOfMemoryCount} out of memory");
     }
 
     if (statistics.OutOfResourceCount != 0) {
-      output.Write(", {0} out of resource", statistics.OutOfResourceCount);
+      await output.WriteAsync($", {statistics.OutOfResourceCount} out of resource");
     }
 
     if (statistics.SolverExceptionCount != 0) {
-      output.Write(", {0} solver exceptions", statistics.SolverExceptionCount);
+      await output.WriteAsync($", {statistics.SolverExceptionCount} solver exceptions");
     }
 
-    output.WriteLine();
-    output.Flush();
+    await output.WriteLineAsync();
+    await output.FlushAsync();
+  }
+
+  public void RecordProofDependencies(ResolutionResult resolution) {
+    var usedDependencies = new HashSet<TrackedNodeComponent>();
+    var proofDependencyManager = resolution.ResolvedProgram.ProofDependencyManager;
+    VerificationResultLogger? verificationResultLogger = null;
+    try {
+      verificationResultLogger = new VerificationResultLogger(options, proofDependencyManager);
+    } catch (ArgumentException e) {
+      Compilation.Reporter.Error(MessageSource.Verifier, Compilation.Project.StartingToken, e.Message);
+    }
+
+    verificationResults.Subscribe(result => {
+      ProofDependencyWarnings.ReportSuspiciousDependencies(options, result.Results,
+        resolution.ResolvedProgram.Reporter, resolution.ResolvedProgram.ProofDependencyManager);
+
+      verificationResultLogger?.Report(result);
+
+      foreach (var used in result.Results.SelectMany(part => part.Result.CoveredElements)) {
+        usedDependencies.Add(used);
+      }
+    },
+      e => { },
+      () => {
+        verificationResultLogger?.Finish();
+
+        var coverageReportDir = options.Get(CommonOptionBag.VerificationCoverageReport);
+        if (coverageReportDir != null) {
+          new CoverageReporter(options).SerializeVerificationCoverageReport(
+            proofDependencyManager, resolution.ResolvedProgram,
+            usedDependencies,
+            coverageReportDir);
+        }
+      });
+  }
+
+  public void Dispose() {
+    foreach (var disposable in disposables) {
+      disposable.Dispose();
+    }
   }
 }
 
diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs
index 29cd03b20c4..78d569bc50c 100644
--- a/Source/DafnyDriver/Commands/VerifyCommand.cs
+++ b/Source/DafnyDriver/Commands/VerifyCommand.cs
@@ -1,7 +1,5 @@
-using System;
 using System.Collections.Generic;
 using System.CommandLine;
-using System.Linq;
 using System.Threading.Tasks;
 using DafnyCore;
 using DafnyDriver.Commands;
@@ -36,9 +34,17 @@ public static async Task<int> HandleVerification(DafnyOptions options) {
       options.TrackVerificationCoverage = true;
     }
 
-    var compilation = CliCompilation.Create(options);
+    using var compilation = CliCompilation.Create(options);
     compilation.Start();
-    await compilation.VerifyAllAndPrintSummary();
+
+    try {
+      var resolution = await compilation.Resolution;
+      compilation.ReportVerificationDiagnostics();
+      compilation.ReportVerificationSummary();
+      compilation.RecordProofDependencies(resolution);
+      await compilation.VerifyAll();
+    } catch (TaskCanceledException) {
+    }
 
     return compilation.ExitCode;
   }
diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs
index 83dab60a87b..df4c793f6af 100644
--- a/Source/DafnyLanguageServer/Workspace/IdeState.cs
+++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs
@@ -467,7 +467,8 @@ private IdeState HandleBoogieUpdate(DafnyOptions options, ILogger logger, Boogie
       counterExamples = counterExamples.Concat(completed.Result.CounterExamples);
       hitErrorLimit |= completed.Result.MaxCounterExamples == completed.Result.CounterExamples.Count;
       var newDiagnostics =
-        Compilation.GetDiagnosticsFromResult(options, previousState.Uri, boogieUpdate.VerificationTask, completed.Result);
+        Compilation.GetDiagnosticsFromResult(options, previousState.Uri, boogieUpdate.CanVerify,
+          boogieUpdate.VerificationTask, completed.Result);
       diagnostics = newDiagnostics.Select(d => d.ToLspDiagnostic()).ToList();
       logger.LogTrace(
         $"Completed received for {previousState.Input} and found #{diagnostics.Count} diagnostics and #{completed.Result.CounterExamples.Count} counterexamples.");
@@ -487,7 +488,7 @@ private IdeState HandleBoogieUpdate(DafnyOptions options, ILogger logger, Boogie
       errorReporter.Updates.Subscribe(d => verificationCoverageDiagnostics.Add(d.Diagnostic));
 
       ProofDependencyWarnings.ReportSuspiciousDependencies(options,
-        scopeGroup.Select(s => (s.Task, (Completed)s.RawStatus)),
+        scopeGroup.Select(s => new VerificationTaskResult(s.Task, ((Completed)s.RawStatus).Result)),
         errorReporter, boogieUpdate.ProofDependencyManager);
 
       newCanVerifyDiagnostics = previousVerificationResult.Diagnostics.Concat(verificationCoverageDiagnostics.Select(d => d.ToLspDiagnostic())).ToList();
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy.expect
index 6e55a3eb560..1a1f32ef221 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue106.dfy.expect
@@ -1,3 +1,3 @@
-git-issue106.dfy(6,32): Error: Verification out of resource (L (correctness))
+git-issue106.dfy(6,32): Error: Verification out of resource (L)
 
 Dafny program verifier finished with 1 verified, 0 errors, 1 out of resource
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect
index 5ff8e24f08a..7ea9364805f 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect
@@ -1,5 +1,5 @@
 git-issue-3855.dfy(800,0): Warning: attribute :ignore is deprecated
-git-issue-3855.dfy(800,11): Error: Verification of 'Memory.dynMove (correctness)' timed out after 1 seconds
+git-issue-3855.dfy(800,11): Error: Verification of 'Memory.dynMove' timed out after 1 seconds
 git-issue-3855.dfy(943,17): Error: a precondition for this call could not be proved
 git-issue-3855.dfy(429,29): Related location: this is the precondition that could not be proved
 git-issue-3855.dfy(943,17): Error: a precondition for this call could not be proved
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-2563.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-2563.dfy.expect
index e87c48015aa..2bb78fc775a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-2563.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-2563.dfy.expect
@@ -1,4 +1,2 @@
 github-issue-2563.dfy(1,0): Warning: File contains no code
 CLI: Error: unknown parameter to `/verificationLogger:csv`: log.csv
-
-Dafny program verifier finished with 0 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4804.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4804.dfy.expect
index f2c63c4f576..18aaa834ec7 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4804.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4804.dfy.expect
@@ -1,3 +1,3 @@
-github-issue-4804.dfy(19,8): Error: Verification out of resource (Power.LemmaPowSubAddCancel (correctness))
+github-issue-4804.dfy(19,8): Error: Verification out of resource (Power.LemmaPowSubAddCancel)
 
 Dafny program verifier finished with 3 verified, 0 errors, 1 out of resource
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy.expect
index d879d58152f..0337e36f8f0 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/nonLinearArithmetic.dfy.expect
@@ -1,7 +1,7 @@
-nonLinearArithmetic.dfy(97,8): Error: Verification out of resource (Power3.LemmaPowSubAddCancel (correctness))
+nonLinearArithmetic.dfy(97,8): Error: Verification out of resource (Power3.LemmaPowSubAddCancel)
 
 Dafny program verifier finished with 15 verified, 0 errors, 1 out of resource
-nonLinearArithmetic.dfy(21,8): Error: Verification out of resource (Power0.LemmaPowSubAddCancel (correctness))
-nonLinearArithmetic.dfy(97,8): Error: Verification out of resource (Power3.LemmaPowSubAddCancel (correctness))
+nonLinearArithmetic.dfy(21,8): Error: Verification out of resource (Power0.LemmaPowSubAddCancel)
+nonLinearArithmetic.dfy(97,8): Error: Verification out of resource (Power3.LemmaPowSubAddCancel)
 
 Dafny program verifier finished with 14 verified, 0 errors, 2 out of resource
diff --git a/docs/DafnyRef/Attributes.4.expect b/docs/DafnyRef/Attributes.4.expect
index 2d8ea2d4069..6abe439773d 100644
--- a/docs/DafnyRef/Attributes.4.expect
+++ b/docs/DafnyRef/Attributes.4.expect
@@ -1,3 +1,3 @@
-text.dfy(1,23): Error: Verification out of resource (f (correctness))
+text.dfy(1,23): Error: Verification out of resource (f)
 
 Dafny program verifier finished with 0 verified, 0 errors, 1 out of resource