diff --git a/RELEASE-NOTES.md b/RELEASE-NOTES.md
new file mode 100644
index 0000000000..e1e443e842
--- /dev/null
+++ b/RELEASE-NOTES.md
@@ -0,0 +1,22 @@
+## 0.9.0
+
+### Features
+
+* new sequential model checker that is using TransitionExecutor, see #467
+* new command-line options, see #467 and the manual for details:
+  * choose the algorithm: `--algo=(offline|incremental)`
+  * pre-check, whether a transition disabled, discard the disabled transitions: `--discard-disabled`
+  * do not check for deadlocks: `--no-deadlock`
+  * pass tuning parameters in CLI: `--tune-here`
+* parsing in-comment Java-like annotations, see #226
+* tracking the source of variable/constant declarations and operator
+  definitions in the TLA+ Parser, see #262
+
+### Bug fixes
+
+* the new sequential model checker has uncovered a bug that was not found
+  by the old model checker, see #467
+
+### Documentation
+
+* ADR004: In-comment annotations for declarations (of constants, variables, operators)
diff --git a/UNRELEASED.md b/UNRELEASED.md
index a8ef325ccf..84488f67af 100644
--- a/UNRELEASED.md
+++ b/UNRELEASED.md
@@ -1,32 +1,12 @@
 <!-- NOTE:
      Release notes for unreleased changes go here, following this format:
 
-        ### Feature Category 1
+        ### Features
 
          * Change description, see #123
 
-        ### Feature Category 2
+        ### Bug fixes
 
-         * Another change description, see #124
+         * Some bug fix, see #124
 
      DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE -->
-### Features
-
-* new sequential model checker that is using TransitionExecutor, see #467
-* new command-line options, see #467 and the manual for details:
-  * choose the algorithm: `--algo=(offline|incremental)`
-  * pre-check, whether a transition disabled, discard the disabled transitions: `--discard-disabled`
-  * do not check for deadlocks: `--no-deadlock`
-  * pass tuning parameters in CLI: `--tune-here`
-* parsing in-comment Java-like annotations, see #226
-* tracking the source of variable/constant declarations and operator
-  definitions in the TLA+ Parser, see #262
-
-### Bug fixes
-
-* the new sequential model checker has uncovered a bug that was not found
-  by the old model checker, see #467
-
-### Documentation
-
-* ADR004: In-comment annotations for declarations (of constants, variables, operators)
diff --git a/mod-distribution/pom.xml b/mod-distribution/pom.xml
index 4b51859739..197052eb5b 100644
--- a/mod-distribution/pom.xml
+++ b/mod-distribution/pom.xml
@@ -8,11 +8,11 @@
     <parent>
         <groupId>at.forsyte.apalache</groupId>
         <artifactId>apalache</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     </parent>
 
     <artifactId>apalache-pkg</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     <packaging>pom</packaging>
 
     <name>apalache-pkg</name>
diff --git a/mod-infra/pom.xml b/mod-infra/pom.xml
index 01fad2e745..68fa9b9757 100644
--- a/mod-infra/pom.xml
+++ b/mod-infra/pom.xml
@@ -4,11 +4,11 @@
     <parent>
         <groupId>at.forsyte.apalache</groupId>
         <artifactId>apalache</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     </parent>
 
     <artifactId>infra</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     <packaging>jar</packaging>
 
     <name>infra</name>
diff --git a/mod-tool/pom.xml b/mod-tool/pom.xml
index 2733155299..e31c4f60e9 100644
--- a/mod-tool/pom.xml
+++ b/mod-tool/pom.xml
@@ -4,14 +4,14 @@
     <parent>
         <groupId>at.forsyte.apalache</groupId>
         <artifactId>apalache</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     </parent>
 
     <!--
         All command line tooling and option parsing goes here... and nothing else!
     -->
     <artifactId>tool</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     <packaging>jar</packaging>
 
     <name>tool</name>
diff --git a/pom.xml b/pom.xml
index 85b068ecf0..be8fc08f82 100644
--- a/pom.xml
+++ b/pom.xml
@@ -4,7 +4,7 @@
     <groupId>at.forsyte.apalache</groupId>
     <artifactId>apalache</artifactId>
     <packaging>pom</packaging>
-    <version>0.8.4-SNAPSHOT</version>
+    <version>0.9.0</version>
 
     <name>APALACHE project</name>
     <url>https://github.com/informalsystems/apalache</url>
diff --git a/tla-assignments/pom.xml b/tla-assignments/pom.xml
index bb32a83735..5dcc9fdaa5 100644
--- a/tla-assignments/pom.xml
+++ b/tla-assignments/pom.xml
@@ -3,11 +3,11 @@
     <parent>
         <groupId>at.forsyte.apalache</groupId>
         <artifactId>apalache</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     </parent>
 
     <artifactId>tla-assignments</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     <packaging>jar</packaging>
 
     <name>tla-assignments</name>
diff --git a/tla-bmcmt/pom.xml b/tla-bmcmt/pom.xml
index 2d5ed47a01..e07717b330 100644
--- a/tla-bmcmt/pom.xml
+++ b/tla-bmcmt/pom.xml
@@ -4,11 +4,11 @@
     <parent>
         <groupId>at.forsyte.apalache</groupId>
         <artifactId>apalache</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     </parent>
 
     <artifactId>tla-bmcmt</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     <packaging>jar</packaging>
 
     <name>tla-bmcmt</name>
diff --git a/tla-import/pom.xml b/tla-import/pom.xml
index 12dbd4a391..3b80d59db6 100644
--- a/tla-import/pom.xml
+++ b/tla-import/pom.xml
@@ -4,11 +4,11 @@
     <parent>
         <groupId>at.forsyte.apalache</groupId>
         <artifactId>apalache</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     </parent>
 
     <artifactId>tla-import</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     <packaging>jar</packaging>
 
     <name>tla-import</name>
diff --git a/tla-pp/pom.xml b/tla-pp/pom.xml
index bf89546537..f4a6c36a65 100644
--- a/tla-pp/pom.xml
+++ b/tla-pp/pom.xml
@@ -4,11 +4,11 @@
     <parent>
         <groupId>at.forsyte.apalache</groupId>
         <artifactId>apalache</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     </parent>
 
     <artifactId>tla-pp</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     <packaging>jar</packaging>
 
     <name>tla-pp</name>
diff --git a/tla-types/pom.xml b/tla-types/pom.xml
index 585511b8eb..f42921952c 100644
--- a/tla-types/pom.xml
+++ b/tla-types/pom.xml
@@ -3,11 +3,11 @@
     <parent>
         <groupId>at.forsyte.apalache</groupId>
         <artifactId>apalache</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     </parent>
 
     <artifactId>tla-types</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     <packaging>jar</packaging>
 
     <name>tla-types</name>
diff --git a/tlair/pom.xml b/tlair/pom.xml
index e92c26651b..3eeb3802ff 100644
--- a/tlair/pom.xml
+++ b/tlair/pom.xml
@@ -4,11 +4,11 @@
     <parent>
         <groupId>at.forsyte.apalache</groupId>
         <artifactId>apalache</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     </parent>
 
     <artifactId>tlair</artifactId>
-        <version>0.8.4-SNAPSHOT</version>
+        <version>0.9.0</version>
     <packaging>jar</packaging>
 
     <name>tlair</name>