diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
index 84fe844b5f6..5447954396f 100644
--- a/RELEASE_NOTES.md
+++ b/RELEASE_NOTES.md
@@ -2,6 +2,100 @@
 
 See [docs/dev/news/](docs/dev/news/).
 
+# 4.1.0
+
+## New features
+
+- 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.
+  (https://github.com/dafny-lang/dafny/pull/2907)
+
+- Recognize the `{:only}` attribute on `assert` statements to temporarily transform other assertions into assumptions (https://github.com/dafny-lang/dafny/pull/3095)
+
+- * Exposes the --output and --spill-translation options for the dafny test command (https://github.com/dafny-lang/dafny/pull/3612)
+
+- The `dafny audit` command now reports instances of the `{:concurrent}` attribute, intended to flag code that is intended, but can't be proven, to be safe for use in a concurrent setting. (https://github.com/dafny-lang/dafny/pull/3660)
+
+- Added option --no-verify for language server (https://github.com/dafny-lang/dafny/pull/3732)
+
+- * Added `.GetDocstring(DafnyOptions)` to every AST node
+  * Plugin support for custom Docstring formatter, 
+  * Activatable plugin to support a subset of Javadoc through `--javadoclike-docstring-plugin`
+  * Support for displaying docstring in VSCode
+  (https://github.com/dafny-lang/dafny/pull/3756)
+
+- Documentation of the syntax for docstrings added to the reference manual (https://github.com/dafny-lang/dafny/pull/3773)
+
+- Labelled assertions and requires in functions (https://github.com/dafny-lang/dafny/pull/3804)
+
+- API support for obtaining the Dafny expression that is being checked by each assertion (https://github.com/dafny-lang/dafny/pull/3888)
+
+- Added a "Dafny Library" backend, which produces self-contained, pre-verified `.doo` files ideal for distributing shared libraries.
+  `.doo` files are produced with commands of the form `dafny build -t:lib ...`.
+  (https://github.com/dafny-lang/dafny/pull/3913)
+
+- Semantic interpretation of dots in names for `{:extern}` modules when compiling to Python (https://github.com/dafny-lang/dafny/pull/3919)
+
+- Code actions in editor to explicit failing assertions.
+  In VSCode, place the cursor on a failing assertion that support being made explicit and either
+  - Position the caret on a failing assertion, press CTRL+; and then ENTER
+  - Hover over the failing division by zero, click "quick fix", press ENTER
+  Both scenarios will explicit the failing assertion.
+  If you don't see a quick fix, it means that the assertion cannot be automatically made explicit for now.
+
+  Here is a initial list of assertions that can now be made explicit:
+  - Division by zero
+  - "out of bound" on sequences index, sequence slices, or array index
+  - "Not in domain" on maps
+  - "Could not prove unicity" of `var x :| ...` statement  
+  - "Could not prove existence" of `var x :| ...` statement
+  (https://github.com/dafny-lang/dafny/pull/3940)
+
+## Bug fixes
+
+- * dafny test accepts a --methods-to-test option whose value is a regular expression selecting which tests to include in the test run (https://github.com/dafny-lang/dafny/pull/3221)
+
+- * The deprecated attributes :dllimport, :handle, and :heapQuantifier are no longer recognized. (https://github.com/dafny-lang/dafny/pull/3398)
+
+- While using `dafny translate --target=java`, the `--include-sources` option works as intended, while before it had no affect. (https://github.com/dafny-lang/dafny/pull/3611)
+
+- Tested support for paths with spaces in them (https://github.com/dafny-lang/dafny/pull/3683)
+
+- Crash related to the override check for generic functions (https://github.com/dafny-lang/dafny/pull/3692)
+
+- Opaque functions guaranteed to be opaque until revealed (https://github.com/dafny-lang/dafny/pull/3719)
+
+- Support for Corretto tests (https://github.com/dafny-lang/dafny/pull/3731)
+
+- Right shift on native byte has the same consistent semantics even in Java (https://github.com/dafny-lang/dafny/pull/3734)
+
+- * Main and {:test} methods may now be in the same program (https://github.com/dafny-lang/dafny/pull/3744)
+
+- The formatter now produces the same output whether invoked on the command-line or from VSCode (https://github.com/dafny-lang/dafny/pull/3790)
+
+- The --solver-log option is now hidden from help unless --help-internal is used. (https://github.com/dafny-lang/dafny/pull/3798)
+
+- Highlight "inconclusive" as errors in the gutter icons (https://github.com/dafny-lang/dafny/pull/3821)
+
+- Docstring for functions with ensures (https://github.com/dafny-lang/dafny/pull/3840)
+
+- Prevent a compiler crash that could occur when a datatype constructor was defined that has multiple parameters with the same name. (https://github.com/dafny-lang/dafny/pull/3860)
+
+- Improved rules for nameonly parameters and parameter default-value expressions (https://github.com/dafny-lang/dafny/pull/3864)
+
+- Fixes several compilation issues, mostly related to subset types defined by one of its type parameter (https://github.com/dafny-lang/dafny/pull/3893)
+
+- Explicitly define inequality of `multiset`s in Python for better backwards compatibility (https://github.com/dafny-lang/dafny/pull/3904)
+
+- Format for comprehension expressions (https://github.com/dafny-lang/dafny/pull/3912)
+
+- Formatting for parameter default values (https://github.com/dafny-lang/dafny/pull/3944)
+
+- Formatting issue in forall statement range (https://github.com/dafny-lang/dafny/pull/3960)
+
+- Select alternative default calc operator only if it doesn't clash with given step operators (https://github.com/dafny-lang/dafny/pull/3963)
+
 # 4.0.0
 
 ## Breaking changes
diff --git a/docs/dev/news/2907.feat b/docs/dev/news/2907.feat
deleted file mode 100644
index 50694c4db32..00000000000
--- a/docs/dev/news/2907.feat
+++ /dev/null
@@ -1,3 +0,0 @@
-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
diff --git a/docs/dev/news/3095.feat b/docs/dev/news/3095.feat
deleted file mode 100644
index 3f002ba12e4..00000000000
--- a/docs/dev/news/3095.feat
+++ /dev/null
@@ -1 +0,0 @@
-Recognize the `{:only}` attribute on `assert` statements to temporarily transform other assertions into assumptions
\ No newline at end of file
diff --git a/docs/dev/news/3221.fix b/docs/dev/news/3221.fix
deleted file mode 100644
index f3068dadeff..00000000000
--- a/docs/dev/news/3221.fix
+++ /dev/null
@@ -1 +0,0 @@
-* dafny test accepts a --methods-to-test option whose value is a regular expression selecting which tests to include in the test run
diff --git a/docs/dev/news/3398.fix b/docs/dev/news/3398.fix
deleted file mode 100644
index ca097cde7af..00000000000
--- a/docs/dev/news/3398.fix
+++ /dev/null
@@ -1 +0,0 @@
-* The deprecated attributes :dllimport, :handle, and :heapQuantifier are no longer recognized.
diff --git a/docs/dev/news/3611.fix b/docs/dev/news/3611.fix
deleted file mode 100644
index f1afe5f1fe3..00000000000
--- a/docs/dev/news/3611.fix
+++ /dev/null
@@ -1 +0,0 @@
-While using `dafny translate --target=java`, the `--include-sources` option works as intended, while before it had no affect.
diff --git a/docs/dev/news/3612.feat b/docs/dev/news/3612.feat
deleted file mode 100644
index 51aae071eb6..00000000000
--- a/docs/dev/news/3612.feat
+++ /dev/null
@@ -1,2 +0,0 @@
-* Exposes the --output and --spill-translation options for the dafny test command
-
diff --git a/docs/dev/news/3660.feat b/docs/dev/news/3660.feat
deleted file mode 100644
index c0750015577..00000000000
--- a/docs/dev/news/3660.feat
+++ /dev/null
@@ -1 +0,0 @@
-The `dafny audit` command now reports instances of the `{:concurrent}` attribute, intended to flag code that is intended, but can't be proven, to be safe for use in a concurrent setting.
diff --git a/docs/dev/news/3683.fix b/docs/dev/news/3683.fix
deleted file mode 100644
index 8299ab88aa3..00000000000
--- a/docs/dev/news/3683.fix
+++ /dev/null
@@ -1 +0,0 @@
-Tested support for paths with spaces in them
\ No newline at end of file
diff --git a/docs/dev/news/3692.fix b/docs/dev/news/3692.fix
deleted file mode 100644
index 9c8747fb230..00000000000
--- a/docs/dev/news/3692.fix
+++ /dev/null
@@ -1 +0,0 @@
-Crash related to the override check for generic functions
diff --git a/docs/dev/news/3719.fix b/docs/dev/news/3719.fix
deleted file mode 100644
index 3cdbc981d76..00000000000
--- a/docs/dev/news/3719.fix
+++ /dev/null
@@ -1 +0,0 @@
-Opaque functions guaranteed to be opaque until revealed
\ No newline at end of file
diff --git a/docs/dev/news/3731.fix b/docs/dev/news/3731.fix
deleted file mode 100644
index 9e9441c3379..00000000000
--- a/docs/dev/news/3731.fix
+++ /dev/null
@@ -1 +0,0 @@
-Support for Corretto tests
\ No newline at end of file
diff --git a/docs/dev/news/3734.fix b/docs/dev/news/3734.fix
deleted file mode 100644
index b04d0fb8ac8..00000000000
--- a/docs/dev/news/3734.fix
+++ /dev/null
@@ -1 +0,0 @@
-Right shift on native byte has the same consistent semantics even in Java
\ No newline at end of file
diff --git a/docs/dev/news/3744.fix b/docs/dev/news/3744.fix
deleted file mode 100644
index 7cfa339368a..00000000000
--- a/docs/dev/news/3744.fix
+++ /dev/null
@@ -1 +0,0 @@
-* Main and {:test} methods may now be in the same program
diff --git a/docs/dev/news/3773.feat b/docs/dev/news/3773.feat
deleted file mode 100644
index 0bb455660a5..00000000000
--- a/docs/dev/news/3773.feat
+++ /dev/null
@@ -1 +0,0 @@
-Documentation of the syntax for docstrings added to the reference manual
diff --git a/docs/dev/news/3790.fix b/docs/dev/news/3790.fix
deleted file mode 100644
index d9940286188..00000000000
--- a/docs/dev/news/3790.fix
+++ /dev/null
@@ -1 +0,0 @@
-The formatter now produces the same output whether invoked on the command-line or from VSCode
\ No newline at end of file
diff --git a/docs/dev/news/3804.feat b/docs/dev/news/3804.feat
deleted file mode 100644
index 5cd8fc9cb03..00000000000
--- a/docs/dev/news/3804.feat
+++ /dev/null
@@ -1 +0,0 @@
-Labelled assertions and requires in functions
\ No newline at end of file
diff --git a/docs/dev/news/3821.fix b/docs/dev/news/3821.fix
deleted file mode 100644
index c52b2826432..00000000000
--- a/docs/dev/news/3821.fix
+++ /dev/null
@@ -1 +0,0 @@
-Highlight "inconclusive" as errors in the gutter icons
\ No newline at end of file
diff --git a/docs/dev/news/3840.fix b/docs/dev/news/3840.fix
deleted file mode 100644
index 759b2ea7b72..00000000000
--- a/docs/dev/news/3840.fix
+++ /dev/null
@@ -1 +0,0 @@
-Docstring for functions with ensures
\ No newline at end of file
diff --git a/docs/dev/news/3860.fix b/docs/dev/news/3860.fix
deleted file mode 100644
index 07f5f38fe68..00000000000
--- a/docs/dev/news/3860.fix
+++ /dev/null
@@ -1 +0,0 @@
-Prevent a compiler crash that could occur when a datatype constructor was defined that has multiple parameters with the same name.
\ No newline at end of file
diff --git a/docs/dev/news/3864.fix b/docs/dev/news/3864.fix
deleted file mode 100644
index 5284870ff43..00000000000
--- a/docs/dev/news/3864.fix
+++ /dev/null
@@ -1 +0,0 @@
-Improved rules for nameonly parameters and parameter default-value expressions
diff --git a/docs/dev/news/3893.fix b/docs/dev/news/3893.fix
deleted file mode 100644
index 1cf3cb5963b..00000000000
--- a/docs/dev/news/3893.fix
+++ /dev/null
@@ -1 +0,0 @@
-Fixes several compilation issues, mostly related to subset types defined by one of its type parameter
diff --git a/docs/dev/news/3904.fix b/docs/dev/news/3904.fix
deleted file mode 100644
index 970135665fb..00000000000
--- a/docs/dev/news/3904.fix
+++ /dev/null
@@ -1 +0,0 @@
-Explicitly define inequality of `multiset`s in Python for better backwards compatibility
diff --git a/docs/dev/news/3912.fix b/docs/dev/news/3912.fix
deleted file mode 100644
index b6f48a2d3fd..00000000000
--- a/docs/dev/news/3912.fix
+++ /dev/null
@@ -1 +0,0 @@
-Format for comprehension expressions
\ No newline at end of file
diff --git a/docs/dev/news/3913.feat b/docs/dev/news/3913.feat
deleted file mode 100644
index fcbbcaa4394..00000000000
--- a/docs/dev/news/3913.feat
+++ /dev/null
@@ -1,2 +0,0 @@
-Added a "Dafny Library" backend, which produces self-contained, pre-verified `.doo` files ideal for distributing shared libraries.
-`.doo` files are produced with commands of the form `dafny build -t:lib ...`.
\ No newline at end of file
diff --git a/docs/dev/news/3919.feat b/docs/dev/news/3919.feat
deleted file mode 100644
index 2cc921f7bf5..00000000000
--- a/docs/dev/news/3919.feat
+++ /dev/null
@@ -1 +0,0 @@
-Semantic interpretation of dots in names for `{:extern}` modules when compiling to Python
diff --git a/docs/dev/news/3944.fix b/docs/dev/news/3944.fix
deleted file mode 100644
index 8dd5df37f33..00000000000
--- a/docs/dev/news/3944.fix
+++ /dev/null
@@ -1 +0,0 @@
-Formatting for parameter default values
\ No newline at end of file
diff --git a/docs/dev/news/3960.fix b/docs/dev/news/3960.fix
deleted file mode 100644
index 49ac7a14f47..00000000000
--- a/docs/dev/news/3960.fix
+++ /dev/null
@@ -1 +0,0 @@
-Formatting issue in forall statement range
\ No newline at end of file
diff --git a/docs/dev/news/3963.fix b/docs/dev/news/3963.fix
deleted file mode 100644
index 2dd31f418c1..00000000000
--- a/docs/dev/news/3963.fix
+++ /dev/null
@@ -1 +0,0 @@
-Select alternative default calc operator only if it doesn't clash with given step operators
diff --git a/docs/dev/news/docstring.feat b/docs/dev/news/docstring.feat
deleted file mode 100644
index 67514e4843b..00000000000
--- a/docs/dev/news/docstring.feat
+++ /dev/null
@@ -1,4 +0,0 @@
-* Added `.GetDocstring(DafnyOptions)` to every AST node
-* Plugin support for custom Docstring formatter, 
-* Activatable plugin to support a subset of Javadoc through `--javadoclike-docstring-plugin`
-* Support for displaying docstring in VSCode
\ No newline at end of file
diff --git a/docs/dev/news/explicit-failing-assertions.feat b/docs/dev/news/explicit-failing-assertions.feat
deleted file mode 100644
index 553133587eb..00000000000
--- a/docs/dev/news/explicit-failing-assertions.feat
+++ /dev/null
@@ -1,13 +0,0 @@
-Code actions in editor to explicit failing assertions.
-In VSCode, place the cursor on a failing assertion that support being made explicit and either
-- Position the caret on a failing assertion, press CTRL+; and then ENTER
-- Hover over the failing division by zero, click "quick fix", press ENTER
-Both scenarios will explicit the failing assertion.
-If you don't see a quick fix, it means that the assertion cannot be automatically made explicit for now.
-
-Here is a initial list of assertions that can now be made explicit:
-- Division by zero
-- "out of bound" on sequences index, sequence slices, or array index
-- "Not in domain" on maps
-- "Could not prove unicity" of `var x :| ...` statement  
-- "Could not prove existence" of `var x :| ...` statement
diff --git a/docs/dev/news/expressions-on-assertions.feat b/docs/dev/news/expressions-on-assertions.feat
deleted file mode 100644
index 3db264a49c4..00000000000
--- a/docs/dev/news/expressions-on-assertions.feat
+++ /dev/null
@@ -1 +0,0 @@
-API support for obtaining the Dafny expression that is being checked by each assertion
\ No newline at end of file
diff --git a/docs/dev/news/no-verify-server.feat b/docs/dev/news/no-verify-server.feat
deleted file mode 100644
index ccf1b99974f..00000000000
--- a/docs/dev/news/no-verify-server.feat
+++ /dev/null
@@ -1 +0,0 @@
-Added option --no-verify for language server
diff --git a/docs/dev/news/solverLog.fix b/docs/dev/news/solverLog.fix
deleted file mode 100644
index 9ce718afc92..00000000000
--- a/docs/dev/news/solverLog.fix
+++ /dev/null
@@ -1 +0,0 @@
-The --solver-log option is now hidden from help unless --help-internal is used.