diff --git a/Source/Dafny.sln b/Source/Dafny.sln
index 88200dcc483..9f09cac0d87 100644
--- a/Source/Dafny.sln
+++ b/Source/Dafny.sln
@@ -34,6 +34,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AutoExtern", "AutoExtern\Au
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AutoExtern.Test", "AutoExtern.Test\AutoExtern.Test.csproj", "{A47E2F45-DEA3-4700-A82F-9506FEEB199A}"
 EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyAPI", "DafnyAPI\DafnyAPI.csproj", "{B7F0E978-15B2-43A6-A510-DB712FB53957}"
+EndProject
 Global
 	GlobalSection(SolutionConfigurationPlatforms) = preSolution
 		Debug|Any CPU = Debug|Any CPU
@@ -84,6 +86,10 @@ Global
 		{896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}.Debug|Any CPU.Build.0 = Debug|Any CPU
 		{896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}.Release|Any CPU.ActiveCfg = Release|Any CPU
 		{896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}.Release|Any CPU.Build.0 = Release|Any CPU
+		{B7F0E978-15B2-43A6-A510-DB712FB53957}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+		{B7F0E978-15B2-43A6-A510-DB712FB53957}.Debug|Any CPU.Build.0 = Debug|Any CPU
+		{B7F0E978-15B2-43A6-A510-DB712FB53957}.Release|Any CPU.ActiveCfg = Release|Any CPU
+		{B7F0E978-15B2-43A6-A510-DB712FB53957}.Release|Any CPU.Build.0 = Release|Any CPU
 		{F185BDC2-1327-47A4-A293-D3FCDC419867}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
 		{F185BDC2-1327-47A4-A293-D3FCDC419867}.Debug|Any CPU.Build.0 = Debug|Any CPU
 		{F185BDC2-1327-47A4-A293-D3FCDC419867}.Release|Any CPU.ActiveCfg = Release|Any CPU
diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
index 389edc2c1db..7debdfd4b07 100644
--- a/Source/Dafny/DafnyMain.cs
+++ b/Source/Dafny/DafnyMain.cs
@@ -66,7 +66,7 @@ public DafnyFile(string filePath, bool useStdin = false) {
         var asm = Assembly.LoadFile(filePath);
         string sourceText = null;
         foreach (var adata in asm.CustomAttributes) {
-          if (adata.Constructor.DeclaringType.Name == "DafnySourceAttribute") {
+          if (adata.Constructor.DeclaringType?.Name == "DafnySourceAttribute") {
             foreach (var args in adata.ConstructorArguments) {
               if (args.ArgumentType.FullName == "System.String") {
                 sourceText = (string)args.Value;
@@ -321,4 +321,4 @@ public static bool IsBoogieVerified(PipelineOutcome outcome, PipelineStatistics
     }
 
   }
-}
\ No newline at end of file
+}
diff --git a/Source/DafnyAPI/API.cs b/Source/DafnyAPI/API.cs
new file mode 100644
index 00000000000..f163021f04b
--- /dev/null
+++ b/Source/DafnyAPI/API.cs
@@ -0,0 +1,110 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
+// This is an experimental API for using Dafny as a library.
+// We expect it to change from version to version as we discover which features are needed by clients.
+
+using System.Runtime.Versioning;
+
+namespace Microsoft.Dafny {
+  public class DafnyEngine {
+    public DafnyOptions Options { get; }
+    public ErrorReporter Reporter { get; private set; }
+    public Boogie.ExecutionEngine BoogieEngine { get; }
+
+    private static DafnyEngine? _singleton;
+
+    public static DafnyEngine Init(ErrorReporter reporter, string[] commandLineOptions) {
+      _singleton ??= new DafnyEngine();
+      _singleton.Reporter = reporter;
+      _singleton.Options.Parse(commandLineOptions);
+      return _singleton;
+    }
+
+    private DafnyEngine() {
+      Options = DafnyOptions.Create();
+      Reporter = new ErrorReporterSink();
+      BoogieEngine = Boogie.ExecutionEngine.CreateWithoutSharedCache(Options);
+      DafnyOptions.Install(Options);
+    }
+
+    public DafnyInput CreateDafnyInput(string fname, string source) {
+      return new DafnyInput(this, fname, source);
+    }
+  }
+
+  public class DafnyInput {
+    private readonly DafnyEngine engine;
+    public string FileName { get; init; }
+    public string Source { get; init; }
+
+    internal DafnyInput(DafnyEngine engine, string fname, string source) {
+      this.engine = engine;
+      FileName = fname;
+      Source = source;
+    }
+
+    public bool Verify() {
+      return Translate() is { } boogieModules && VerifyBoogieModules(boogieModules);
+    }
+
+    public Program? Parse() {
+      var module = new LiteralModuleDecl(new DefaultModuleDecl(), null);
+      var builtIns = new BuiltIns();
+      var errors = new Errors(engine.Reporter);
+      if (Parser.Parse(Source, FileName, FileName, null, module, builtIns, errors) == 0 &&
+          Main.ParseIncludes(module, builtIns, new List<string>(), errors) == null) {
+        return new Program(FileName, module, builtIns, engine.Reporter);
+      }
+
+      return null;
+    }
+
+    public Program? Resolve() {
+      return Parse() is { } parsedProgram ? Resolve(parsedProgram) : null;
+    }
+
+    private Program? Resolve(Program parsedProgram) {
+      new Resolver(parsedProgram).ResolveProgram(parsedProgram);
+      return engine.Reporter.Count(ErrorLevel.Error) == 0 ? parsedProgram : null;
+    }
+
+    private List<Tuple<string, Boogie.Program>>? Translate(Program resolvedProgram) {
+      var flags = new Translator.TranslatorFlags {InsertChecksums = true, UniqueIdPrefix = FileName};
+      return Translator.Translate(resolvedProgram, engine.Reporter, flags).ToList();
+    }
+
+    public List<Tuple<string, Boogie.Program>>? Translate() {
+      return (Resolve() is { } resolvedProgram) ? Translate(resolvedProgram) : null;
+    }
+
+    public bool VerifyBoogieModule(string moduleName, Microsoft.Boogie.Program boogieProgram) {
+      if (boogieProgram.Resolve(engine.Options) == 0 && boogieProgram.Typecheck(engine.Options) == 0) {
+        engine.BoogieEngine.EliminateDeadVariables(boogieProgram);
+        engine.BoogieEngine.CollectModSets(boogieProgram);
+        engine.BoogieEngine.CoalesceBlocks(boogieProgram);
+        engine.BoogieEngine.Inline(boogieProgram);
+
+        // FIXME: Use reporter
+        switch (engine.BoogieEngine.InferAndVerify(Console.Out, boogieProgram, new Boogie.PipelineStatistics(),
+                  "ServerProgram_" + moduleName, null, DateTime.UtcNow.Ticks.ToString()).Result) {
+          case Boogie.PipelineOutcome.Done:
+          case Boogie.PipelineOutcome.VerificationCompleted:
+            return true;
+        }
+      }
+
+      return false;
+    }
+
+    public bool VerifyBoogieModules(List<Tuple<string, Boogie.Program>> boogieModules) {
+      foreach (var (moduleName, boogieProgram) in boogieModules) {
+        if (!VerifyBoogieModule(moduleName, boogieProgram)) {
+          return false;
+        }
+      }
+
+      return true;
+    }
+  }
+}
diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs
deleted file mode 100644
index 8696c806489..00000000000
--- a/Source/DafnyServer/DafnyHelper.cs
+++ /dev/null
@@ -1,149 +0,0 @@
-// Copyright by the contributors to the Dafny Project
-// SPDX-License-Identifier: MIT
-
-using System;
-using System.Collections.Generic;
-using System.IO;
-using System.Linq;
-using System.Runtime.Serialization.Json;
-using System.Text;
-using Microsoft.Boogie;
-using DafnyServer;
-using Bpl = Microsoft.Boogie;
-
-namespace Microsoft.Dafny {
-
-  class DafnyHelper {
-    private string fname;
-    private string source;
-    private readonly ExecutionEngine engine;
-    private string[] args;
-
-    private readonly Dafny.ErrorReporter reporter;
-    private Dafny.Program dafnyProgram;
-    private IEnumerable<Tuple<string, Bpl.Program>> boogiePrograms;
-
-    public DafnyHelper(ExecutionEngine engine, string[] args, string fname, string source) {
-      this.engine = engine;
-      this.args = args;
-      this.fname = fname;
-      this.source = source;
-      this.reporter = new Dafny.ConsoleErrorReporter();
-    }
-
-    public bool Verify() {
-      ServerUtils.ApplyArgs(args, DafnyOptions.O);
-      return Parse() && Resolve() && Translate() && Boogie();
-    }
-
-    private bool Parse() {
-      Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null);
-      Dafny.BuiltIns builtIns = new Dafny.BuiltIns();
-      var success = (Dafny.Parser.Parse(source, fname, fname, null, module, builtIns, new Dafny.Errors(reporter)) == 0 &&
-                     Dafny.Main.ParseIncludes(module, builtIns, new List<string>(), new Dafny.Errors(reporter)) == null);
-      if (success) {
-        dafnyProgram = new Dafny.Program(fname, module, builtIns, reporter);
-      }
-      return success;
-    }
-
-    private bool Resolve() {
-      var resolver = new Dafny.Resolver(dafnyProgram);
-      resolver.ResolveProgram(dafnyProgram);
-      return reporter.Count(ErrorLevel.Error) == 0;
-    }
-
-    private bool Translate() {
-      boogiePrograms = Translator.Translate(dafnyProgram, reporter,
-          new Translator.TranslatorFlags() { InsertChecksums = true, UniqueIdPrefix = fname }); // FIXME how are translation errors reported?
-      return true;
-    }
-
-    private bool BoogieOnce(string moduleName, Bpl.Program boogieProgram) {
-      if (boogieProgram.Resolve(DafnyOptions.O) == 0 && boogieProgram.Typecheck(DafnyOptions.O) == 0) { //FIXME ResolveAndTypecheck?
-        engine.EliminateDeadVariables(boogieProgram);
-        engine.CollectModSets(boogieProgram);
-        engine.CoalesceBlocks(boogieProgram);
-        engine.Inline(boogieProgram);
-
-        //NOTE: We could capture errors instead of printing them (pass a delegate instead of null)
-        switch (engine.InferAndVerify(Console.Out, boogieProgram, new PipelineStatistics(),
-                  "ServerProgram_" + moduleName, null, DateTime.UtcNow.Ticks.ToString()).Result) {
-          case PipelineOutcome.Done:
-          case PipelineOutcome.VerificationCompleted:
-            return true;
-        }
-      }
-
-      return false;
-    }
-
-    private bool Boogie() {
-      var isVerified = true;
-      foreach (var boogieProgram in boogiePrograms) {
-        isVerified = isVerified && BoogieOnce(boogieProgram.Item1, boogieProgram.Item2);
-      }
-      return isVerified;
-    }
-
-    public void Symbols() {
-      ServerUtils.ApplyArgs(args, DafnyOptions.O);
-      if (Parse() && Resolve()) {
-        var symbolTable = new SymbolTable(dafnyProgram);
-        var symbols = symbolTable.CalculateSymbols();
-        Console.WriteLine("SYMBOLS_START " + ConvertToJson(symbols) + " SYMBOLS_END");
-      } else {
-        Console.WriteLine("SYMBOLS_START [] SYMBOLS_END");
-      }
-    }
-
-    public void CounterExample() {
-      var listArgs = args.ToList();
-      listArgs.Add("/mv:" + CounterExampleProvider.ModelBvd);
-      ServerUtils.ApplyArgs(listArgs.ToArray(), DafnyOptions.O);
-      try {
-        if (Parse() && Resolve() && Translate()) {
-          var counterExampleProvider = new CounterExampleProvider();
-          foreach (var boogieProgram in boogiePrograms) {
-            RemoveExistingModel();
-            BoogieOnce(boogieProgram.Item1, boogieProgram.Item2);
-            var model = counterExampleProvider.LoadCounterModel();
-            Console.WriteLine("COUNTEREXAMPLE_START " + ConvertToJson(model) + " COUNTEREXAMPLE_END");
-          }
-        }
-      } catch (Exception e) {
-        Console.WriteLine("Error collection models: " + e.Message);
-      }
-    }
-
-    private void RemoveExistingModel() {
-      if (File.Exists(CounterExampleProvider.ModelBvd)) {
-        File.Delete(CounterExampleProvider.ModelBvd);
-      }
-    }
-
-    public void DotGraph() {
-      ServerUtils.ApplyArgs(args, DafnyOptions.O);
-
-      if (Parse() && Resolve() && Translate()) {
-        foreach (var boogieProgram in boogiePrograms) {
-          BoogieOnce(boogieProgram.Item1, boogieProgram.Item2);
-
-          foreach (var impl in boogieProgram.Item2.Implementations) {
-            using (StreamWriter sw = new StreamWriter(fname + impl.Name + ".dot")) {
-              sw.Write(boogieProgram.Item2.ProcessLoops(engine.Options, impl).ToDot());
-            }
-          }
-        }
-      }
-    }
-
-    private static string ConvertToJson<T>(T data) {
-      var serializer = new DataContractJsonSerializer(typeof(T));
-      using (var ms = new MemoryStream()) {
-        serializer.WriteObject(ms, data);
-        return Encoding.Default.GetString(ms.ToArray());
-      }
-    }
-  }
-}
\ No newline at end of file
diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj
index 70fde5e1914..7e033ee1255 100644
--- a/Source/DafnyServer/DafnyServer.csproj
+++ b/Source/DafnyServer/DafnyServer.csproj
@@ -20,6 +20,7 @@
   </PropertyGroup>
 
   <ItemGroup>
+    <ProjectReference Include="..\DafnyAPI\DafnyAPI.csproj" />
     <ProjectReference Include="..\Dafny\DafnyPipeline.csproj" />
   </ItemGroup>
 
diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs
index 1749cb207e0..2904a3205dc 100644
--- a/Source/DafnyServer/Server.cs
+++ b/Source/DafnyServer/Server.cs
@@ -3,6 +3,7 @@
 
 using System;
 using System.IO;
+using System.Runtime.Serialization.Json;
 using System.Text;
 using DafnyServer;
 using Microsoft.Boogie;
@@ -10,23 +11,20 @@
 namespace Microsoft.Dafny {
   public class Server {
     private bool running;
-    private readonly ExecutionEngine engine;
+    private bool inputIsPlaintext;
+    private readonly DafnyEngine engine;
 
     static void Main(string[] args) {
-      var options = DafnyOptions.Create();
-      ServerUtils.ApplyArgs(args, options);
-      var engine = ExecutionEngine.CreateWithoutSharedCache(options);
-      Server server = new Server(engine);
+      Server server = new Server(args);
 
       // read the optional flag (only one flag is allowed)
-      bool plaintext = false;
       bool selftest = false;
       bool decode = false;
       bool encode = false;
       var n = 0;  // number of consumed args
       var arg = n < args.Length ? args[n] : null;
       if (arg == "-plaintext") {
-        plaintext = true;
+        server.inputIsPlaintext = true;
         n++;
       } else if (arg == "-selftest") {
         selftest = true;
@@ -40,7 +38,7 @@ static void Main(string[] args) {
       }
 
       if (selftest) {
-        VerificationTask.SelfTest(engine);
+        server.SelfTest();
         return;
       }
 
@@ -59,7 +57,7 @@ static void Main(string[] args) {
       } else if (encode) {
         server.Encode();
       } else {
-        server.Loop(plaintext);
+        server.Loop();
       }
     }
 
@@ -68,10 +66,11 @@ private void SetupConsole() {
       Console.OutputEncoding = new UTF8Encoding(false, true);
     }
 
-    public Server(ExecutionEngine engine) {
-      this.engine = engine;
-      this.running = true;
+    private Server(string[] args) {
+      engine = DafnyEngine.Init(new ConsoleErrorReporter(), Array.Empty<string>());
+      running = true;
       SetupConsole();
+      ApplyArgs(args);
     }
 
     bool EndOfPayload(out string line) {
@@ -79,7 +78,7 @@ bool EndOfPayload(out string line) {
       return line == null || line == Interaction.CLIENT_EOM_TAG;
     }
 
-    string ReadPayload(bool inputIsPlaintext) {
+    string ReadPayload() {
       StringBuilder buffer = new StringBuilder();
       string line = null;
       while (!EndOfPayload(out line)) {
@@ -152,17 +151,17 @@ static void WriteAcrossLines(string s, int width) {
       }
     }
 
-    void Loop(bool inputIsPlaintext) {
+    void Loop() {
       for (int cycle = 0; running; cycle++) {
         var line = Console.ReadLine() ?? "quit";
         if (line != String.Empty && !line.StartsWith("#")) {
           var command = line.Split();
-          Respond(command, inputIsPlaintext);
+          Respond(command);
         }
       }
     }
 
-    void Respond(string[] command, bool inputIsPlaintext) {
+    void Respond(string[] command) {
       try {
         if (command.Length == 0) {
           throw new ServerException("Empty command");
@@ -171,34 +170,27 @@ void Respond(string[] command, bool inputIsPlaintext) {
         var verb = command[0];
         var msg = "Verification completed successfully!";
         if (verb == "verify") {
-          ServerUtils.checkArgs(command, 0);
-          var vt = ReadVerificationTask(inputIsPlaintext);
-          vt.Run(engine);
+          ReadDafnyInput().Verify();
         } else if (verb == "counterexample") {
           ServerUtils.checkArgs(command, 0);
-          var vt = ReadVerificationTask(inputIsPlaintext);
-          vt.CounterExample(engine);
+          CounterExample(ReadDafnyInput());
         } else if (verb == "dotgraph") {
           ServerUtils.checkArgs(command, 0);
-          var vt = ReadVerificationTask(inputIsPlaintext);
-          vt.DotGraph(engine);
+          DotGraph(ReadDafnyInput());
         } else if (verb == "symbols") {
           ServerUtils.checkArgs(command, 0);
-          var vt = ReadVerificationTask(inputIsPlaintext);
-          vt.Symbols(engine);
+          Symbols(ReadDafnyInput());
         } else if (verb == "version") {
           ServerUtils.checkArgs(command, 0);
-          var _ = ReadVerificationTask(inputIsPlaintext);
+          var _ = ReadDafnyInput();
           VersionCheck.CurrentVersion();
         } else if (verb == "unmarshal") {
           ServerUtils.checkArgs(command, 0);
-          var vt = ReadVerificationTask(false);
-          vt.Unmarshal(command);
+          ReadVerificationTask(false).Unmarshal(command);
           msg = null;
         } else if (verb == "marshal") {
           ServerUtils.checkArgs(command, 0);
-          var vt = ReadVerificationTask(true);
-          vt.Marshal(command);
+          ReadVerificationTask(true).Marshal(command);
           msg = null;
         } else if (verb == "quit") {
           ServerUtils.checkArgs(command, 0);
@@ -217,18 +209,93 @@ void Respond(string[] command, bool inputIsPlaintext) {
       }
     }
 
-    VerificationTask ReadVerificationTask(bool inputIsPlaintext) {
-      var payload = ReadPayload(inputIsPlaintext);
-      if (inputIsPlaintext) {
+    VerificationTask ReadVerificationTask(bool? plaintTextOverride = null) {
+      var payload = ReadPayload();
+      if (plaintTextOverride ?? inputIsPlaintext) {
         return new VerificationTask(Array.Empty<string>(), "transcript", payload, false);
       } else {
-        return VerificationTask.ReadTask(payload);
+        return VerificationTask.ReadSnapshot(payload);
+      }
+    }
+
+    DafnyInput ReadDafnyInput() {
+      var snapshot = ReadVerificationTask();
+      ApplyArgs(snapshot.Args);
+      return snapshot.AsDafnyInput(engine);
+    }
+
+    internal void SelfTest() {
+      var snapshot = new VerificationTask(new string[] { }, "<none>", "method selftest() { assert true; }", false);
+      try {
+        snapshot.AsDafnyInput(engine).Verify();
+        Interaction.EOM(Interaction.SUCCESS, (string)null);
+      } catch (Exception ex) {
+        Interaction.EOM(Interaction.FAILURE, ex);
       }
     }
 
+    public void Symbols(DafnyInput input) {
+      if (input.Resolve() is { } resolvedProgram) {
+        var symbolTable = new SymbolTable(resolvedProgram);
+        var symbols = symbolTable.CalculateSymbols();
+        Console.WriteLine("SYMBOLS_START " + ConvertToJson(symbols) + " SYMBOLS_END");
+      } else {
+        Console.WriteLine("SYMBOLS_START [] SYMBOLS_END");
+      }
+    }
+
+    public void CounterExample(DafnyInput input) {
+      engine.Options.ModelViewFile = CounterExampleProvider.ModelBvd;
+      try {
+        if (input.Translate() is { } boogiePrograms) {
+          var counterExampleProvider = new CounterExampleProvider();
+          foreach (var (moduleName, boogieProgram) in boogiePrograms) {
+            RemoveExistingModel();
+            input.VerifyBoogieModule(moduleName, boogieProgram);
+            var model = counterExampleProvider.LoadCounterModel();
+            Console.WriteLine("COUNTEREXAMPLE_START " + ConvertToJson(model) + " COUNTEREXAMPLE_END");
+          }
+        }
+      } catch (Exception e) {
+        Console.WriteLine("Error collection models: " + e.Message);
+      }
+    }
+
+    private void RemoveExistingModel() {
+      if (File.Exists(CounterExampleProvider.ModelBvd)) {
+        File.Delete(CounterExampleProvider.ModelBvd);
+      }
+    }
+
+    public void DotGraph(DafnyInput input) {
+      if (input.Translate() is { } boogiePrograms) {
+        foreach (var (moduleName, boogieProgram) in boogiePrograms) {
+          input.VerifyBoogieModule(moduleName, boogieProgram);
+
+          foreach (var impl in boogieProgram.Implementations) {
+            using (StreamWriter sw = new StreamWriter(input.FileName + impl.Name + ".dot")) {
+              sw.Write(boogieProgram.ProcessLoops(engine.Options, impl).ToDot());
+            }
+          }
+        }
+      }
+    }
+
+    private static string ConvertToJson<T>(T data) {
+      var serializer = new DataContractJsonSerializer(typeof(T));
+      using (var ms = new MemoryStream()) {
+        serializer.WriteObject(ms, data);
+        return Encoding.Default.GetString(ms.ToArray());
+      }
+    }
+
+    private void ApplyArgs(string[] args) {
+      ServerUtils.ApplyArgs(args, engine.Options);
+    }
+
     void Exit() {
       this.running = false;
     }
   }
 
-}
\ No newline at end of file
+}
diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs
index 7b0fed03a2b..e982e1533fc 100644
--- a/Source/DafnyServer/Utilities.cs
+++ b/Source/DafnyServer/Utilities.cs
@@ -47,16 +47,15 @@ internal static void checkArgs(string[] command, int expectedLength) {
     }
 
     internal static void ApplyArgs(string[] args, DafnyOptions options) {
-      Dafny.DafnyOptions.Install(options);
-      Dafny.DafnyOptions.O.TimeLimit = 10; //This is just a default; it can be overriden
-      DafnyOptions.O.VerifySnapshots = 3;
+      options.TimeLimit = 10; //This is just a default; it can be overriden
+      options.VerifySnapshots = 3;
 
-      if (DafnyOptions.O.Parse(args)) {
-        DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount / 2); // Don't use too many cores
-        DafnyOptions.O.PrintTooltips = true; // Dump tooltips (ErrorLevel.Info) to stdout
-        //DafnyOptions.O.UnicodeOutput = true; // Use pretty warning signs
-        DafnyOptions.O.ShowSnippets = false; // Server sometimes has filename == null, which crashes showSnippets
-        DafnyOptions.O.TraceProofObligations = true; // Show which method is being verified, but don't show duration of verification
+      if (options.Parse(args)) {
+        options.VcsCores = Math.Max(1, System.Environment.ProcessorCount / 2); // Don't use too many cores
+        options.PrintTooltips = true; // Dump tooltips (ErrorLevel.Info) to stdout
+        //options.UnicodeOutput = true; // Use pretty warning signs
+        options.ShowSnippets = false; // Server sometimes has filename == null, which crashes showSnippets
+        options.TraceProofObligations = true; // Show which method is being verified, but don't show duration of verification
       } else {
         throw new ServerException("Invalid command line options");
       }
diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs
index e8b4331ec4c..6c1353a8bce 100644
--- a/Source/DafnyServer/VerificationTask.cs
+++ b/Source/DafnyServer/VerificationTask.cs
@@ -24,6 +24,12 @@ class VerificationTask {
     [DataMember]
     bool sourceIsFile = false;
 
+    public string[] Args => args;
+
+    public DafnyInput AsDafnyInput(DafnyEngine engine) {
+      return engine.CreateDafnyInput(filename, ProgramSource);
+    }
+
     public VerificationTask(string[] args, string filename, string source, bool sourceIsFile) {
       this.args = args;
       this.filename = filename;
@@ -33,7 +39,7 @@ public VerificationTask(string[] args, string filename, string source, bool sour
 
     public string ProgramSource { get { return sourceIsFile ? File.ReadAllText(source) : source; } }
 
-    internal static VerificationTask ReadTask(string b64Repr) {
+    internal static VerificationTask ReadSnapshot(string b64Repr) {
       try {
         var json = Encoding.UTF8.GetString(System.Convert.FromBase64String(b64Repr));
         using (MemoryStream ms = new MemoryStream(Encoding.Unicode.GetBytes(json))) {
@@ -45,32 +51,6 @@ internal static VerificationTask ReadTask(string b64Repr) {
       }
     }
 
-    internal static void SelfTest(ExecutionEngine engine) {
-      var task = new VerificationTask(new string[] { }, "<none>", "method selftest() { assert true; }", false);
-      try {
-        task.Run(engine);
-        Interaction.EOM(Interaction.SUCCESS, (string)null);
-      } catch (Exception ex) {
-        Interaction.EOM(Interaction.FAILURE, ex);
-      }
-    }
-
-    internal void Run(ExecutionEngine engine) {
-      new DafnyHelper(engine, args, filename, ProgramSource).Verify();
-    }
-
-    internal void Symbols(ExecutionEngine engine) {
-      new DafnyHelper(engine, args, filename, ProgramSource).Symbols();
-    }
-
-    public void CounterExample(ExecutionEngine engine) {
-      new DafnyHelper(engine, args, filename, ProgramSource).CounterExample();
-    }
-
-    public void DotGraph(ExecutionEngine engine) {
-      new DafnyHelper(engine, args, filename, ProgramSource).DotGraph();
-    }
-
     public string EncodeProgram(out string json) {
       using (var ms = new MemoryStream()) {
         var serializer = new DataContractJsonSerializer(typeof(VerificationTask));