diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj
index 43713d9ab17..4a8b2f89b56 100644
--- a/Source/DafnyCore/DafnyCore.csproj
+++ b/Source/DafnyCore/DafnyCore.csproj
@@ -27,10 +27,12 @@
   <ItemGroup>
       <PackageReference Include="JetBrains.Annotations" Version="2021.1.0" />
       <PackageReference Include="Microsoft.CodeAnalysis.CSharp" Version="3.7.0" />
+      <PackageReference Include="Microsoft.Extensions.FileSystemGlobbing" Version="5.0.0" />
       <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
       <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
       <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
       <PackageReference Include="Boogie.ExecutionEngine" Version="2.16.4" />
+      <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 
   <ItemGroup>
diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index 144288058f0..b3e10524fbe 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -35,7 +35,8 @@ public enum QuantifierSyntaxOptions {
   public record Options(IDictionary<Option, object> OptionArguments);
 
   public class DafnyOptions : Bpl.CommandLineOptions {
-
+    public static DafnyOptions Default = new DafnyOptions();
+    public ProjectFile ProjectFile { get; set; }
     public bool NonGhostsUseHeap => Allocated == 1 || Allocated == 2;
     public bool AlwaysUseHeap => Allocated == 2;
     public bool CommonHeapUse => Allocated >= 2;
diff --git a/Source/DafnyCore/Options/ICommandSpec.cs b/Source/DafnyCore/Options/ICommandSpec.cs
index 6a59acf3093..6fe4c4d1ac9 100644
--- a/Source/DafnyCore/Options/ICommandSpec.cs
+++ b/Source/DafnyCore/Options/ICommandSpec.cs
@@ -15,7 +15,7 @@ public interface ICommandSpec {
   static ICommandSpec() {
     FilesArgument = new("file", r => {
       return r.Tokens.Where(t => !string.IsNullOrEmpty(t.Value)).Select(t => new FileInfo(t.Value)).ToList();
-    }, true, "input files");
+    }, true, "Dafny input files and/or a Dafny project file");
   }
 
   public static Argument<List<FileInfo>> FilesArgument { get; }
diff --git a/Source/DafnyCore/Options/ProjectFile.cs b/Source/DafnyCore/Options/ProjectFile.cs
new file mode 100644
index 00000000000..a06c164e6d9
--- /dev/null
+++ b/Source/DafnyCore/Options/ProjectFile.cs
@@ -0,0 +1,90 @@
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.CommandLine;
+using System.IO;
+using System.Linq;
+using System.Reflection.Metadata;
+using System.Runtime.Serialization;
+using System.Text.Json;
+using System.Text.RegularExpressions;
+using Microsoft.CodeAnalysis;
+using Microsoft.Extensions.FileSystemGlobbing;
+using Microsoft.Extensions.FileSystemGlobbing.Abstractions;
+using Tomlyn;
+
+namespace Microsoft.Dafny; 
+
+public class ProjectFile {
+  public const string FileName = "dfyconfig.toml";
+
+  [IgnoreDataMember]
+  public Uri Uri { get; set; }
+  public string[] Includes { get; set; }
+  public string[] Excludes { get; set; }
+  public Dictionary<string, object> Options { get; set; }
+
+  public static ProjectFile Open(Uri uri, TextWriter errorWriter) {
+    if (Path.GetFileName(uri.LocalPath) != FileName) {
+      Console.WriteLine($"Warning: only Dafny project files named {FileName} are recognised by the Dafny IDE.");
+    }
+    try {
+      var file = File.Open(uri.LocalPath, FileMode.Open);
+      var model = Toml.ToModel<ProjectFile>(new StreamReader(file).ReadToEnd(), null, new TomlModelOptions());
+      model.Uri = uri;
+      return model;
+
+    } catch (IOException e) {
+      errorWriter.WriteLine(e.Message);
+      return null;
+    } catch (TomlException tomlException) {
+      errorWriter.WriteLine($"The Dafny project file {uri.LocalPath} contains the following errors:");
+      var regex = new Regex(
+        @$"\((\d+),(\d+)\) : error : The property `(\w+)` was not found on object type {typeof(ProjectFile).FullName}");
+      var newMessage = regex.Replace(tomlException.Message,
+        match =>
+          $"({match.Groups[1].Value},{match.Groups[2].Value}): the property {match.Groups[3].Value} does not exist.");
+      errorWriter.WriteLine(newMessage);
+      return null;
+    }
+  }
+
+  public void AddFilesToOptions(DafnyOptions options) {
+    var matcher = new Matcher();
+    foreach (var includeGlob in Includes ?? new[] { "**/*.dfy" }) {
+      matcher.AddInclude(includeGlob);
+    }
+    foreach (var includeGlob in Excludes ?? Enumerable.Empty<string>()) {
+      matcher.AddExclude(includeGlob);
+    }
+
+    var root = Path.GetDirectoryName(Uri.LocalPath);
+    var result = matcher.Execute(new DirectoryInfoWrapper(new DirectoryInfo(root!)));
+    var files = result.Files.Select(f => Path.Combine(root, f.Path));
+    foreach (var file in files) {
+      options.AddFile(file);
+    }
+  }
+
+  public void Validate(IEnumerable<Option> possibleOptions) {
+    var possibleNames = possibleOptions.Select(o => o.Name).ToHashSet();
+    foreach (var optionThatDoesNotExist in Options.Where(option => !possibleNames.Contains(option.Key))) {
+      Console.WriteLine($"Warning: option '{optionThatDoesNotExist.Key}' that was specified in the project file, is not a valid Dafny option.");
+    }
+  }
+
+  public bool TryGetValue(Option option, TextWriter errorWriter, out object value) {
+    if (!Options.TryGetValue(option.Name, out value)) {
+      return false;
+    }
+
+    if (value.GetType() != option.ValueType) {
+      errorWriter.WriteLine(
+        $"Error: property '{option.Name}' is of type '{value.GetType().Name}' but should be of type '{option.ValueType.Name}'");
+      return false;
+    }
+
+    return true;
+
+  }
+}
\ No newline at end of file
diff --git a/Source/DafnyDriver/Commands/CommandRegistry.cs b/Source/DafnyDriver/Commands/CommandRegistry.cs
index 7975d84c438..6aec275c670 100644
--- a/Source/DafnyDriver/Commands/CommandRegistry.cs
+++ b/Source/DafnyDriver/Commands/CommandRegistry.cs
@@ -37,13 +37,13 @@ static CommandRegistry() {
     AddCommand(new TranslateCommand());
     AddCommand(new FormatCommand());
     AddCommand(new MeasureComplexityCommand());
-    AddCommand(new ServerCommand());
+    AddCommand(ServerCommand.Instance);
     AddCommand(new TestCommand());
     AddCommand(new GenerateTestsCommand());
     AddCommand(new DeadCodeCommand());
     AddCommand(new AuditCommand());
 
-    FileArgument = new Argument<FileInfo>("file", "input file");
+    FileArgument = new Argument<FileInfo>("file", "Dafny input file or Dafny project file");
   }
 
   public static Argument<FileInfo> FileArgument { get; }
@@ -60,7 +60,7 @@ public static ParseArgumentResult Create(string[] arguments) {
     dafnyOptions.Environment = "Command-line arguments: " + string.Join(" ", arguments);
     dafnyOptions.Options = options;
 
-    foreach (var option in Commands.SelectMany(c => c.Options)) {
+    foreach (var option in AllOptions) {
       if (!allowHidden) {
         option.IsHidden = false;
       }
@@ -105,6 +105,7 @@ public static ParseArgumentResult Create(string[] arguments) {
       rootCommand.AddCommand(command);
     }
 
+    var failedToProcessFile = false;
     void CommandHandler(InvocationContext context) {
       wasInvoked = true;
       var command = context.ParseResult.CommandResult.Command;
@@ -112,17 +113,28 @@ void CommandHandler(InvocationContext context) {
 
       var singleFile = context.ParseResult.GetValueForArgument(FileArgument);
       if (singleFile != null) {
-        dafnyOptions.AddFile(singleFile.FullName);
+        if (!ProcessFile(dafnyOptions, singleFile)) {
+          failedToProcessFile = true;
+          return;
+        }
       }
       var files = context.ParseResult.GetValueForArgument(ICommandSpec.FilesArgument);
       if (files != null) {
         foreach (var file in files) {
-          dafnyOptions.AddFile(file.FullName);
+          if (!ProcessFile(dafnyOptions, file)) {
+            failedToProcessFile = true;
+            return;
+          }
         }
       }
 
       foreach (var option in command.Options) {
-        var value = context.ParseResult.GetValueForOption(option);
+        var result = context.ParseResult.FindResultFor(option);
+        object projectFileValue = null;
+        var hasProjectFileValue = dafnyOptions.ProjectFile?.TryGetValue(option, Console.Error, out projectFileValue) ?? false;
+        var value = result == null && hasProjectFileValue
+          ? projectFileValue
+          : context.ParseResult.GetValueForOption(option);
         options.OptionArguments[option] = value;
         dafnyOptions.ApplyBinding(option);
       }
@@ -137,6 +149,11 @@ void CommandHandler(InvocationContext context) {
 #pragma warning disable VSTHRD002
     var exitCode = builder.Build().InvokeAsync(arguments).Result;
 #pragma warning restore VSTHRD002
+
+    if (failedToProcessFile) {
+      return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR);
+    }
+
     if (!wasInvoked) {
       if (exitCode == 0) {
         return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.OK_EXIT_EARLY);
@@ -151,6 +168,34 @@ void CommandHandler(InvocationContext context) {
     return new ParseArgumentFailure(DafnyDriver.CommandLineArgumentsResult.PREPROCESSING_ERROR);
   }
 
+  private static bool ProcessFile(DafnyOptions dafnyOptions, FileInfo singleFile) {
+    if (Path.GetExtension(singleFile.FullName) == ".toml") {
+      if (dafnyOptions.ProjectFile != null) {
+        Console.Error.WriteLine($"Only one project file can be used at a time. Both {dafnyOptions.ProjectFile.Uri.LocalPath} and {singleFile.FullName} were specified");
+        return false;
+      }
+
+      if (!File.Exists(singleFile.FullName)) {
+        Console.Error.WriteLine($"Error: file {singleFile.FullName} not found");
+        return false;
+      }
+      var projectFile = ProjectFile.Open(new Uri(singleFile.FullName), Console.Error);
+      if (projectFile == null) {
+        return false;
+      }
+      projectFile.Validate(AllOptions);
+      dafnyOptions.ProjectFile = projectFile;
+      projectFile.AddFilesToOptions(dafnyOptions);
+    } else {
+      dafnyOptions.AddFile(singleFile.FullName);
+    }
+    return true;
+  }
+
+  private static IEnumerable<Option> AllOptions {
+    get { return Commands.SelectMany(c => c.Options); }
+  }
+
   private static CommandLineBuilder AddDeveloperHelp(RootCommand rootCommand, CommandLineBuilder builder) {
     var languageDeveloperHelp = new Option<bool>(ToolchainDebuggingHelpName,
       "Show help and usage information, including options designed for developing the Dafny language and toolchain.");
diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj
index 4cc3ec4ad04..e270e4be9d5 100644
--- a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj
+++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj
@@ -68,6 +68,21 @@
     <None Update="Various\TestFiles\includesAincludesB.dfy">
       <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
     </None>
+    <None Update="ProjectFiles\TestFiles\src\foo.dfy">
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </None>
+    <None Update="ProjectFiles\TestFiles\Nesting\dfyconfig.toml">
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </None>
+    <None Update="ProjectFiles\TestFiles\dfyconfig.toml">
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </None>
+    <None Update="ProjectFiles\TestFiles\noWarnShadowing.dfy">
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </None>
+    <None Update="ProjectFiles\TestFiles\Nesting\src\foo.dfy">
+      <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+    </None>
   </ItemGroup>
 
   <ItemGroup>
diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs
index 64e77f043bc..1e7fb744a56 100644
--- a/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs
+++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs
@@ -84,12 +84,12 @@ void NewServerOptionsAction(LanguageServerOptions options) {
 
     private static void ApplyDefaultOptionValues(DafnyOptions dafnyOptions) {
       var testCommand = new System.CommandLine.Command("test");
-      foreach (var serverOption in new ServerCommand().Options) {
+      foreach (var serverOption in ServerCommand.Instance.Options) {
         testCommand.AddOption(serverOption);
       }
 
       var result = testCommand.Parse("test");
-      foreach (var option in new ServerCommand().Options) {
+      foreach (var option in ServerCommand.Instance.Options) {
         if (!dafnyOptions.Options.OptionArguments.ContainsKey(option)) {
           var value = result.GetValueForOption(option);
 
diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs
index e9641526d04..faa82646d0c 100644
--- a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs
+++ b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs
@@ -15,7 +15,7 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup {
   public class HoverTest : ClientBasedLanguageServerTest {
     protected override async Task SetUp(Action<DafnyOptions> modifyOptions = null) {
       void ModifyOptions(DafnyOptions options) {
-        options.ProverOptions.Add("-proverOpt:SOLVER=noop");
+        options.ProverOptions.Add("SOLVER=noop");
         modifyOptions?.Invoke(options);
       }
 
diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs
new file mode 100644
index 00000000000..984a601c35b
--- /dev/null
+++ b/Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs
@@ -0,0 +1,33 @@
+using System.IO;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Xunit;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest; 
+
+public class ProjectFilesTest : ClientBasedLanguageServerTest {
+  [Fact]
+  public async Task ClosestProjectFileIsFound() {
+    var filePath = Path.Combine(Directory.GetCurrentDirectory(), "ProjectFiles/TestFiles/Nesting/src/foo.dfy");
+    var source = await File.ReadAllTextAsync(filePath);
+    var documentItem = CreateTestDocument(source, filePath);
+    await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+    var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken);
+
+    Assert.Single(diagnostics);
+    Assert.Equal("Shadowed local-variable name: x", diagnostics[0].Message);
+  }
+
+  [Fact]
+  public async Task ProjectFileOverridesOptions() {
+    await SetUp(options => options.WarnShadowing = true);
+    var filePath = Path.Combine(Directory.GetCurrentDirectory(), "ProjectFiles/TestFiles/noWarnShadowing.dfy");
+    var source = await File.ReadAllTextAsync(filePath);
+    var documentItem = CreateTestDocument(source, filePath);
+    await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+    var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken);
+
+    Assert.Empty(diagnostics);
+  }
+}
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/Nesting/dfyconfig.toml b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/Nesting/dfyconfig.toml
new file mode 100644
index 00000000000..a450e981c8b
--- /dev/null
+++ b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/Nesting/dfyconfig.toml
@@ -0,0 +1,4 @@
+includes = ["src/**/*.dfy"]
+
+[options]
+warn-shadowing = true
diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/Nesting/src/foo.dfy b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/Nesting/src/foo.dfy
new file mode 100644
index 00000000000..49a3a161baa
--- /dev/null
+++ b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/Nesting/src/foo.dfy
@@ -0,0 +1,6 @@
+method Foo() {
+  var x := 3;
+  if (true) {
+    var x := 4;
+  }
+}
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/dfyconfig.toml b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/dfyconfig.toml
new file mode 100644
index 00000000000..59f848c998a
--- /dev/null
+++ b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/dfyconfig.toml
@@ -0,0 +1,4 @@
+includes = ["**/*.dfy"]
+
+[options]
+warn-shadowing = false
diff --git a/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/noWarnShadowing.dfy b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/noWarnShadowing.dfy
new file mode 100644
index 00000000000..49a3a161baa
--- /dev/null
+++ b/Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/noWarnShadowing.dfy
@@ -0,0 +1,6 @@
+method Foo() {
+  var x := 3;
+  if (true) {
+    var x := 4;
+  }
+}
\ No newline at end of file
diff --git a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs
index 39ca329e553..41c6bfc0b31 100644
--- a/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs
+++ b/Source/DafnyLanguageServer.Test/Unit/TextDocumentLoaderTest.cs
@@ -53,7 +53,7 @@ public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() {
       var source = new CancellationTokenSource();
       parser.Setup(p => p.Parse(It.IsAny<TextDocumentItem>(), It.IsAny<ErrorReporter>(), It.IsAny<CancellationToken>())).Callback(() => source.Cancel())
         .Throws<TaskCanceledException>();
-      var task = textDocumentLoader.LoadAsync(CreateTestDocument(), source.Token);
+      var task = textDocumentLoader.LoadAsync(DafnyOptions.Default, CreateTestDocument(), source.Token);
       try {
         await task;
         Assert.Fail("document load was not cancelled");
@@ -68,7 +68,7 @@ public async Task LoadReturnsCanceledTaskIfOperationIsCanceled() {
     public async Task LoadReturnsFaultedTaskIfAnyExceptionOccured() {
       parser.Setup(p => p.Parse(It.IsAny<TextDocumentItem>(), It.IsAny<ErrorReporter>(), It.IsAny<CancellationToken>()))
         .Throws<InvalidOperationException>();
-      var task = textDocumentLoader.LoadAsync(CreateTestDocument(), default);
+      var task = textDocumentLoader.LoadAsync(DafnyOptions.Default, CreateTestDocument(), default);
       try {
         await task;
         Assert.Fail("document load did not fail");
diff --git a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs
index 56f7e7a004d..f18d1caf969 100644
--- a/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs
+++ b/Source/DafnyLanguageServer.Test/Various/ExceptionTests.cs
@@ -123,11 +123,12 @@ public IdeState CreateUnloaded(DocumentTextBuffer textDocument, CancellationToke
       return loader.CreateUnloaded(textDocument, cancellationToken);
     }
 
-    public Task<DocumentAfterParsing> LoadAsync(DocumentTextBuffer textDocument, CancellationToken cancellationToken) {
+    public Task<DocumentAfterParsing> LoadAsync(DafnyOptions options, DocumentTextBuffer textDocument,
+      CancellationToken cancellationToken) {
       if (tests.CrashOnLoad) {
         throw new IOException("crash");
       }
-      return loader.LoadAsync(textDocument, cancellationToken);
+      return loader.LoadAsync(options, textDocument, cancellationToken);
     }
   }
 }
diff --git a/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs b/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs
index c9ca0677875..8acd9bc90dc 100644
--- a/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs
+++ b/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs
@@ -99,7 +99,7 @@ private ModuleSymbol ProcessModule(Symbol scope, ModuleDefinition moduleDefiniti
           case DatatypeDecl dataTypeDeclaration:
             return ProcessDataType(moduleSymbol, dataTypeDeclaration);
           default:
-            logger.LogDebug("encountered unknown top level declaration {Name} of type {Type}", topLevelDeclaration.Name, topLevelDeclaration.GetType());
+            logger.LogTrace("encountered unknown top level declaration {Name} of type {Type}", topLevelDeclaration.Name, topLevelDeclaration.GetType());
             return null;
         }
       }
@@ -276,7 +276,7 @@ public void Resolve(Expression bodyExpression) {
       }
 
       public override void VisitUnknown(object node, IToken token) {
-        logger.LogDebug("encountered unknown syntax node of type {NodeType} in {Filename}@({Line},{Column})",
+        logger.LogTrace("encountered unknown syntax node of type {NodeType} in {Filename}@({Line},{Column})",
           node.GetType(), token.GetDocumentFileName(), token.line, token.col);
       }
 
diff --git a/Source/DafnyLanguageServer/ServerCommand.cs b/Source/DafnyLanguageServer/ServerCommand.cs
index 35aea9985c7..9a347965d63 100644
--- a/Source/DafnyLanguageServer/ServerCommand.cs
+++ b/Source/DafnyLanguageServer/ServerCommand.cs
@@ -8,6 +8,10 @@
 namespace Microsoft.Dafny.LanguageServer;
 
 public class ServerCommand : ICommandSpec {
+  public static readonly ServerCommand Instance = new();
+
+  private ServerCommand() {
+  }
 
   static ServerCommand() {
     DafnyOptions.RegisterLegacyBinding(VerifySnapshots, (options, u) => options.VerifySnapshots = (int)u);
@@ -53,8 +57,7 @@ related locations
     Concat(ICommandSpec.ResolverOptions);
 
   public Command Create() {
-    var command = new Command("server", "Start the Dafny language server");
-    return command;
+    return new Command("server", "Start the Dafny language server");
   }
 
   public void PostProcess(DafnyOptions dafnyOptions, Options options, InvocationContext context) {
diff --git a/Source/DafnyLanguageServer/Workspace/Compilation.cs b/Source/DafnyLanguageServer/Workspace/Compilation.cs
index 09ecf63f3e8..356e71b8e4f 100644
--- a/Source/DafnyLanguageServer/Workspace/Compilation.cs
+++ b/Source/DafnyLanguageServer/Workspace/Compilation.cs
@@ -52,9 +52,10 @@ public class Compilation {
   public Task<DocumentAfterTranslation> TranslatedDocument { get; }
 
   public Compilation(IServiceProvider services,
+    DafnyOptions options,
     DocumentTextBuffer textBuffer,
     VerificationTree? migratedVerificationTree) {
-    options = services.GetRequiredService<DafnyOptions>();
+    this.options = options;
     logger = services.GetRequiredService<ILogger<Compilation>>();
     documentLoader = services.GetRequiredService<ITextDocumentLoader>();
     notificationPublisher = services.GetRequiredService<INotificationPublisher>();
@@ -79,7 +80,7 @@ public void Start() {
   private async Task<DocumentAfterParsing> ResolveAsync() {
     try {
       await started.Task;
-      var documentAfterParsing = await documentLoader.LoadAsync(TextBuffer, cancellationSource.Token);
+      var documentAfterParsing = await documentLoader.LoadAsync(options, TextBuffer, cancellationSource.Token);
 
       // TODO, let gutter icon publications also used the published CompilationView.
       var state = documentAfterParsing.InitialIdeState(options);
@@ -337,14 +338,14 @@ public void CancelPendingUpdates() {
   private readonly DafnyOptions options;
 
   public void MarkVerificationStarted() {
-    logger.LogDebug("MarkVerificationStarted called");
+    logger.LogTrace("MarkVerificationStarted called");
     if (verificationCompleted.Task.IsCompleted) {
       verificationCompleted = new TaskCompletionSource();
     }
   }
 
   public void MarkVerificationFinished() {
-    logger.LogDebug("MarkVerificationFinished called");
+    logger.LogTrace("MarkVerificationFinished called");
     verificationCompleted.TrySetResult();
   }
 
diff --git a/Source/DafnyLanguageServer/Workspace/DocumentManager.cs b/Source/DafnyLanguageServer/Workspace/DocumentManager.cs
index 80de9a8b72b..e4b1b956cc0 100644
--- a/Source/DafnyLanguageServer/Workspace/DocumentManager.cs
+++ b/Source/DafnyLanguageServer/Workspace/DocumentManager.cs
@@ -1,5 +1,6 @@
 using System;
 using System.Collections.Generic;
+using System.IO;
 using System.Linq;
 using System.Reactive.Linq;
 using System.Threading;
@@ -10,6 +11,7 @@
 using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
 using Microsoft.Extensions.DependencyInjection;
 using Microsoft.Extensions.Logging;
+using OmniSharp.Extensions.LanguageServer.Protocol;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
@@ -54,6 +56,7 @@ public DocumentManager(
       document);
     Compilation = new Compilation(
       services,
+      DetermineDocumentOptions(options, document.Uri),
       document,
       null);
 
@@ -104,8 +107,11 @@ public void UpdateDocument(DidChangeTextDocumentParams documentChange) {
             relocator.RelocateRange(range, documentChange, CancellationToken.None))).
           Where(r => r != null).Take(MaxRememberedChanges).ToList()!;
     }
+
+    var dafnyOptions = DetermineDocumentOptions(options, documentChange.TextDocument.Uri);
     Compilation = new Compilation(
       services,
+      dafnyOptions,
       updatedText,
       // TODO do not pass this to CompilationManager but instead use it in FillMissingStateUsingLastPublishedDocument
       migratedVerificationTree
@@ -127,6 +133,40 @@ public void UpdateDocument(DidChangeTextDocumentParams documentChange) {
     Compilation.Start();
   }
 
+  private static DafnyOptions DetermineDocumentOptions(DafnyOptions serverOptions, DocumentUri uri) {
+    ProjectFile? projectFile = null;
+
+    var folder = Path.GetDirectoryName(uri.GetFileSystemPath());
+    while (!string.IsNullOrEmpty(folder)) {
+      var children = Directory.GetFiles(folder, "dfyconfig.toml");
+      if (children.Length > 0) {
+        var errorWriter = TextWriter.Null;
+        projectFile = ProjectFile.Open(new Uri(children[0]), errorWriter);
+        if (projectFile != null) {
+          break;
+        }
+      }
+      folder = Path.GetDirectoryName(folder);
+    }
+
+    if (projectFile != null) {
+      var result = new DafnyOptions(serverOptions);
+
+      foreach (var option in ServerCommand.Instance.Options) {
+        object? projectFileValue = null;
+        var hasProjectFileValue = projectFile?.TryGetValue(option, TextWriter.Null, out projectFileValue) ?? false;
+        if (hasProjectFileValue) {
+          result.Options.OptionArguments[option] = projectFileValue;
+          result.ApplyBinding(option);
+        }
+      }
+
+      return result;
+    }
+
+    return serverOptions;
+  }
+
   private Dictionary<ImplementationId, IdeImplementationView> MigrateImplementationViews(DidChangeTextDocumentParams documentChange,
     IReadOnlyDictionary<ImplementationId, IdeImplementationView> oldVerificationDiagnostics) {
     var result = new Dictionary<ImplementationId, IdeImplementationView>();
diff --git a/Source/DafnyLanguageServer/Workspace/DocumentManagerDatabase.cs b/Source/DafnyLanguageServer/Workspace/DocumentManagerDatabase.cs
index 4977992cac9..65026b8702a 100644
--- a/Source/DafnyLanguageServer/Workspace/DocumentManagerDatabase.cs
+++ b/Source/DafnyLanguageServer/Workspace/DocumentManagerDatabase.cs
@@ -18,7 +18,6 @@ public class DocumentManagerDatabase : IDocumentDatabase {
     private readonly Dictionary<DocumentUri, DocumentManager> documents = new();
 
     public DocumentManagerDatabase(IServiceProvider services) {
-
       this.services = services;
     }
 
diff --git a/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs
index b66fb55baf1..e7cb0536492 100644
--- a/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs
+++ b/Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs
@@ -26,11 +26,10 @@ public interface ITextDocumentLoader {
     /// Loads the specified document item of the language server and applies the necessary steps
     /// to generate a dafny document instance.
     /// </summary>
-    /// <param name="textDocument">The text document to load.</param>
-    /// <param name="cancellationToken">A token to cancel the update operation before its completion.</param>
     /// <returns>The loaded dafny document.</returns>
     /// <exception cref="System.OperationCanceledException">Thrown when the cancellation was requested before completion.</exception>
     /// <exception cref="System.ObjectDisposedException">Thrown if the cancellation token was disposed before the completion.</exception>
-    Task<DocumentAfterParsing> LoadAsync(DocumentTextBuffer textDocument, CancellationToken cancellationToken);
+    Task<DocumentAfterParsing> LoadAsync(DafnyOptions options, DocumentTextBuffer textDocument,
+      CancellationToken cancellationToken);
   }
 }
diff --git a/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs b/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs
index 42898c31cbb..3e04f890321 100644
--- a/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs
+++ b/Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs
@@ -56,7 +56,7 @@ public void OnError(Exception exception) {
   }
 
   public void OnNext(IdeState snapshot) {
-    logger.LogDebug($"IdeStateObserver.OnNext entered, threadId: {Thread.CurrentThread.ManagedThreadId}");
+    logger.LogTrace($"IdeStateObserver.OnNext entered, threadId: {Thread.CurrentThread.ManagedThreadId}");
     lock (lastPublishedStateLock) {
       if (snapshot.Version < LastPublishedState.Version) {
         return;
diff --git a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
index cf2f449398c..73edeb83bb3 100644
--- a/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
+++ b/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs
@@ -23,7 +23,6 @@ public class TextDocumentLoader : ITextDocumentLoader {
     private const int ResolverMaxStackSize = 0x10000000; // 256MB
     private static readonly ThreadTaskScheduler ResolverScheduler = new(ResolverMaxStackSize);
 
-    private readonly DafnyOptions options;
     private readonly IDafnyParser parser;
     private readonly ISymbolResolver symbolResolver;
     private readonly ISymbolTableFactory symbolTableFactory;
@@ -33,7 +32,6 @@ public class TextDocumentLoader : ITextDocumentLoader {
     protected readonly INotificationPublisher NotificationPublisher;
 
     protected TextDocumentLoader(
-      DafnyOptions options,
       ILoggerFactory loggerFactory,
       IDafnyParser parser,
       ISymbolResolver symbolResolver,
@@ -41,7 +39,6 @@ protected TextDocumentLoader(
       IGhostStateDiagnosticCollector ghostStateDiagnosticCollector,
       ICompilationStatusNotificationPublisher statusPublisher,
       INotificationPublisher notificationPublisher) {
-      this.options = options;
       this.parser = parser;
       this.symbolResolver = symbolResolver;
       this.symbolTableFactory = symbolTableFactory;
@@ -61,7 +58,7 @@ public static TextDocumentLoader Create(
       ILoggerFactory loggerFactory,
       INotificationPublisher notificationPublisher
       ) {
-      return new TextDocumentLoader(options, loggerFactory, parser, symbolResolver, symbolTableFactory, ghostStateDiagnosticCollector, statusPublisher, notificationPublisher);
+      return new TextDocumentLoader(loggerFactory, parser, symbolResolver, symbolTableFactory, ghostStateDiagnosticCollector, statusPublisher, notificationPublisher);
     }
 
     public IdeState CreateUnloaded(DocumentTextBuffer textDocument, CancellationToken cancellationToken) {
@@ -75,16 +72,16 @@ public IdeState CreateUnloaded(DocumentTextBuffer textDocument, CancellationToke
       );
     }
 
-    public async Task<DocumentAfterParsing> LoadAsync(DocumentTextBuffer textDocument,
+    public async Task<DocumentAfterParsing> LoadAsync(DafnyOptions options, DocumentTextBuffer textDocument,
       CancellationToken cancellationToken) {
 #pragma warning disable CS1998
       return await await Task.Factory.StartNew(
-        async () => LoadInternal(textDocument, cancellationToken), cancellationToken,
+        async () => LoadInternal(options, textDocument, cancellationToken), cancellationToken,
 #pragma warning restore CS1998
         TaskCreationOptions.None, ResolverScheduler);
     }
 
-    private DocumentAfterParsing LoadInternal(DocumentTextBuffer textDocument,
+    private DocumentAfterParsing LoadInternal(DafnyOptions options, DocumentTextBuffer textDocument,
       CancellationToken cancellationToken) {
       var errorReporter = new DiagnosticErrorReporter(options, textDocument.Text, textDocument.Uri);
       statusPublisher.SendStatusNotification(textDocument, CompilationStatus.ResolutionStarted);
@@ -124,7 +121,7 @@ IReadOnlyList<Diagnostic> diagnostics
         textDocument,
         diagnostics,
         SymbolTable.Empty(),
-        SignatureAndCompletionTable.Empty(options, textDocument),
+        SignatureAndCompletionTable.Empty(DafnyOptions.Default, textDocument),
         new Dictionary<ImplementationId, IdeImplementationView>(),
         Array.Empty<Counterexample>(),
         false,
diff --git a/Test/cli/projectFile/badTypes/badTypes.dfy b/Test/cli/projectFile/badTypes/badTypes.dfy
new file mode 100644
index 00000000000..3aff32ba633
--- /dev/null
+++ b/Test/cli/projectFile/badTypes/badTypes.dfy
@@ -0,0 +1,8 @@
+// RUN: echo ""
+
+method Foo() {
+  var x := 3;
+  if (true) {
+    var x := 4;
+  }
+}
\ No newline at end of file
diff --git a/Test/cli/projectFile/badTypes/dfyconfig.toml b/Test/cli/projectFile/badTypes/dfyconfig.toml
new file mode 100644
index 00000000000..e5c8d4481ce
--- /dev/null
+++ b/Test/cli/projectFile/badTypes/dfyconfig.toml
@@ -0,0 +1,4 @@
+includes = ["**/*"]
+
+[options]
+warn-shadowing = 3
\ No newline at end of file
diff --git a/Test/cli/projectFile/broken/dfyconfig.toml b/Test/cli/projectFile/broken/dfyconfig.toml
new file mode 100644
index 00000000000..3fe6323945a
--- /dev/null
+++ b/Test/cli/projectFile/broken/dfyconfig.toml
@@ -0,0 +1,4 @@
+includdddes = ["src/**/*"]
+
+[options]
+warn-shadowing = true
\ No newline at end of file
diff --git a/Test/cli/projectFile/broken/invalidOption.toml b/Test/cli/projectFile/broken/invalidOption.toml
new file mode 100644
index 00000000000..6ffb7c3e8aa
--- /dev/null
+++ b/Test/cli/projectFile/broken/invalidOption.toml
@@ -0,0 +1,3 @@
+includes = ["../src/input.dfy"]
+[options]
+does-not-exist = true
diff --git a/Test/cli/projectFile/dfyconfig.toml b/Test/cli/projectFile/dfyconfig.toml
new file mode 100644
index 00000000000..48c886a1b0f
--- /dev/null
+++ b/Test/cli/projectFile/dfyconfig.toml
@@ -0,0 +1,5 @@
+includes = ["src/**/*"]
+excludes = ["**/excluded.dfy"]
+
+[options]
+warn-shadowing = true
\ No newline at end of file
diff --git a/Test/cli/projectFile/noIncludes/dfyconfig.toml b/Test/cli/projectFile/noIncludes/dfyconfig.toml
new file mode 100644
index 00000000000..39b81f42b08
--- /dev/null
+++ b/Test/cli/projectFile/noIncludes/dfyconfig.toml
@@ -0,0 +1,2 @@
+[options]
+warn-shadowing = true
\ No newline at end of file
diff --git a/Test/cli/projectFile/noIncludes/src/input.dfy b/Test/cli/projectFile/noIncludes/src/input.dfy
new file mode 100644
index 00000000000..3aff32ba633
--- /dev/null
+++ b/Test/cli/projectFile/noIncludes/src/input.dfy
@@ -0,0 +1,8 @@
+// RUN: echo ""
+
+method Foo() {
+  var x := 3;
+  if (true) {
+    var x := 4;
+  }
+}
\ No newline at end of file
diff --git a/Test/cli/projectFile/noIncludes/src/moreNested/moreInput.dfy b/Test/cli/projectFile/noIncludes/src/moreNested/moreInput.dfy
new file mode 100644
index 00000000000..d05a03de449
--- /dev/null
+++ b/Test/cli/projectFile/noIncludes/src/moreNested/moreInput.dfy
@@ -0,0 +1,8 @@
+// RUN: echo ""
+
+method Bar() {
+  var x := 3;
+  if (true) {
+    var x := 4;
+  }
+}
\ No newline at end of file
diff --git a/Test/cli/projectFile/notInput.dfy b/Test/cli/projectFile/notInput.dfy
new file mode 100644
index 00000000000..0e5bca9d1d3
--- /dev/null
+++ b/Test/cli/projectFile/notInput.dfy
@@ -0,0 +1,8 @@
+// RUN: echo ""
+
+method Foo() {
+  var y := 3;
+  if (true) {
+    var y := 4;
+  }
+}
\ No newline at end of file
diff --git a/Test/cli/projectFile/projectFile.dfy b/Test/cli/projectFile/projectFile.dfy
new file mode 100644
index 00000000000..8f57479d67c
--- /dev/null
+++ b/Test/cli/projectFile/projectFile.dfy
@@ -0,0 +1,34 @@
+// A project file can specify input files and configure options
+// RUN: %baredafny resolve --use-basename-for-filename "%S/dfyconfig.toml" > "%t"
+
+// Test using a URL instead of a local file as a project file
+// RUN: ! %baredafny resolve --use-basename-for-filename "https://github.com/dafny-lang/dafny/blob/master/dfyconfig.toml"
+
+// Test option override behavior
+// RUN: %baredafny resolve --use-basename-for-filename "%S/dfyconfig.toml" --warn-shadowing=false >> "%t"
+
+// Multiple project files are not allowed
+// RUN: ! %baredafny resolve --use-basename-for-filename "%S/dfyconfig.toml" "%S/broken/dfyconfig.toml"
+
+// Project files may not contain unknown properties
+// RUN: ! %baredafny resolve --use-basename-for-filename "%S/broken/dfyconfig.toml"
+
+// Warn if file contains options that don't exist
+// RUN: %baredafny resolve --use-basename-for-filename "%S/broken/invalidOption.toml" >> "%t"
+
+// Project files must be files on disk.
+// RUN: ! %baredafny resolve --use-basename-for-filename "%S/doesNotExist/dfyconfig.toml"
+
+// Project file options must have the right type
+// RUN: ! %baredafny resolve --use-basename-for-filename "%S/badTypes/dfyconfig.toml" 2>> "%t"
+
+// A project file without includes will take all .dfy files as input
+// RUN: %baredafny resolve --use-basename-for-filename "%S/noIncludes/dfyconfig.toml" >> "%t"
+
+// Files included by the project file and on the CLI, duplicate is ignored.
+// RUN: %baredafny resolve --use-basename-for-filename "%S/dfyconfig.toml" "%S/src/input.dfy" >> "%t"
+
+// Files excluded by the project file and included on the CLI, are included
+// RUN: ! %baredafny resolve --use-basename-for-filename "%S/dfyconfig.toml" "%S/src/excluded.dfy" >> "%t"
+
+// RUN: %diff "%s.expect" "%t"
\ No newline at end of file
diff --git a/Test/cli/projectFile/projectFile.dfy.expect b/Test/cli/projectFile/projectFile.dfy.expect
new file mode 100644
index 00000000000..55f569deeeb
--- /dev/null
+++ b/Test/cli/projectFile/projectFile.dfy.expect
@@ -0,0 +1,21 @@
+input.dfy(6,8): Warning: Shadowed local-variable name: x
+
+Dafny program verifier did not attempt verification
+
+Dafny program verifier did not attempt verification
+Warning: only Dafny project files named dfyconfig.toml are recognised by the Dafny IDE.
+Warning: option 'does-not-exist' that was specified in the project file, is not a valid Dafny option.
+
+Dafny program verifier did not attempt verification
+Error: property 'warn-shadowing' is of type 'Int64' but should be of type 'Boolean'
+input.dfy(6,8): Warning: Shadowed local-variable name: x
+moreInput.dfy(6,8): Warning: Shadowed local-variable name: x
+
+Dafny program verifier did not attempt verification
+input.dfy(6,8): Warning: Shadowed local-variable name: x
+
+Dafny program verifier did not attempt verification
+excluded.dfy(3,7): Error: Duplicate member name: Foo
+input.dfy(6,8): Warning: Shadowed local-variable name: x
+excluded.dfy(6,8): Warning: Shadowed local-variable name: z
+1 resolution/type errors detected in the_program
diff --git a/Test/cli/projectFile/src/excluded.dfy b/Test/cli/projectFile/src/excluded.dfy
new file mode 100644
index 00000000000..ec506c35223
--- /dev/null
+++ b/Test/cli/projectFile/src/excluded.dfy
@@ -0,0 +1,8 @@
+// RUN: echo ""
+
+method Foo() {
+  var z := 3;
+  if (true) {
+    var z := 4;
+  }
+}
\ No newline at end of file
diff --git a/Test/cli/projectFile/src/input.dfy b/Test/cli/projectFile/src/input.dfy
new file mode 100644
index 00000000000..3aff32ba633
--- /dev/null
+++ b/Test/cli/projectFile/src/input.dfy
@@ -0,0 +1,8 @@
+// RUN: echo ""
+
+method Foo() {
+  var x := 3;
+  if (true) {
+    var x := 4;
+  }
+}
\ No newline at end of file
diff --git a/customBoogie.patch b/customBoogie.patch
index a71499bcc71..5bfb4c1f360 100644
--- a/customBoogie.patch
+++ b/customBoogie.patch
@@ -54,15 +54,15 @@ index 426b132e2..18db4aebb 100644
  	EndGlobalSection
  EndGlobal
 diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj
-index 0f17aa923..6b937ebcb 100644
+index 4a8b2f89b..a308be9bf 100644
 --- a/Source/DafnyCore/DafnyCore.csproj
 +++ b/Source/DafnyCore/DafnyCore.csproj
-@@ -30,7 +30,7 @@
+@@ -31,7 +31,7 @@
        <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
        <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
        <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
 -      <PackageReference Include="Boogie.ExecutionEngine" Version="2.16.4" />
 +      <ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
+       <PackageReference Include="Tomlyn" Version="0.16.2" />
    </ItemGroup>
  
-   <ItemGroup>
diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md
index 0b3e446da00..7d9dbb0f892 100644
--- a/docs/DafnyRef/UserGuide.md
+++ b/docs/DafnyRef/UserGuide.md
@@ -571,6 +571,25 @@ Most output from `dafny` is directed to the standard output of the shell invokin
 - Dafny `expect` statements (when they fail) send a message to **standard-out**.
 - Dafny I/O libraries send output explicitly to either **standard-out or standard-error**
 
+### 13.5.5. Project files
+
+Commands on the Dafny CLI that can be passed a Dafny file, can also be passed a Dafny project file. Such a project file may define which Dafny files the project contains, and which Dafny options it uses. The project file must be a [TOML](https://toml.io/en/) file named `dfyconfig.toml` for it to work on both the CLI and in the Dafny IDE, although the CLI will accept any `.toml` file. Here's an example of a Dafny project file:
+
+```toml
+includes = ["src/**/*.dfy"]
+excludes = ["**/ignore.dfy"]
+
+[options]
+enforce-determinism = true
+warn-shadowing = true
+```
+
+Under the section `[options]`, any options from the Dafny CLI can be specified using the option's name without the `--` prefix. When executing a `dafny` command using a project file, any options specified in the file that can be applied to the command, will be. Options that can't be applied or are misspelled, are ignored.
+
+When using a Dafny IDE based on the `dafny server` command, the IDE will search for project files by traversing up the file tree looking for the closest `dfyconfig.toml` file it can find. Options from the project file will override options passed to `dafny server`.
+
+It's not possible to use Dafny project files in combination with the legacy CLI UI.
+
 ## 13.6. Verification {#sec-verification}
 
 In this section, we suggest a methodology to figure out [why a single assertion might not hold](#sec-verification-debugging), we propose techniques to deal with [assertions that slow a proof down](#sec-verification-debugging-slow), we explain how to [verify assertions in parallel or in a focused way](#sec-assertion-batches), and we also give some more examples of [useful options and attributes to control verification](#sec-command-line-options-and-attributes-for-verification).
diff --git a/docs/dev/news/2907.feat b/docs/dev/news/2907.feat
new file mode 100644
index 00000000000..50694c4db32
--- /dev/null
+++ b/docs/dev/news/2907.feat
@@ -0,0 +1,3 @@
+Added support for `.toml` based Dafny project files. For now the project file only allows specifying which Dafny files to include and exclude, and what options to use.
+The CLI commands that take Dafny files as input, such as build, run, translate, will now also accept Dafny project files.
+When using an IDE based on `dafny server`, such as the Dafny VSCode extension, the IDE will look for a Dafny project file by traversing up the file tree from the currently opened file, until it finds it `dfyconfig.toml`. The project file will override options specified in the IDE. 
\ No newline at end of file