diff --git a/CHANGELOG.md b/CHANGELOG.md
index b34a63be9..be2a4ece5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,10 +7,19 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Added
+
+- Support for SPARK Pro Wavefront 20230710 (eng/recordflux/RecordFlux#1403)
+
 ### Changed
 
 - Reject duplicate optional arguments in `rflx` CLI (eng/recordflux/RecordFlux#1342)
 
+### Removed
+
+- Support for GNAT Pro 20.2 and GNAT Community 2020 (eng/recordflux/RecordFlux#1403)
+- Support for SPARK Pro 23.1 (eng/recordflux/RecordFlux#1403)
+
 ## [0.12.0] - 2023-08-22
 
 ### Added
diff --git a/doc/user_guide/10-introduction.rst b/doc/user_guide/10-introduction.rst
index d9138e60a..45796a18d 100644
--- a/doc/user_guide/10-introduction.rst
+++ b/doc/user_guide/10-introduction.rst
@@ -110,8 +110,8 @@ The following versions of GNAT are supported:
 
 For compiling the generated code, one of the following versions of GNAT is required:
 
--  GNAT Pro 20.2, 21.2, 22.2 or 23.2
--  GNAT Community 2020 or 2021
+-  GNAT Pro 21.2, 22.2 or 23.2
+-  GNAT Community 2021
 -  FSF GNAT 11.2 or 12.1
 
 A successful installation of the native toolchain can be verified on the command line as follows:
@@ -141,7 +141,7 @@ The tool can be installed using either the system package manager (`python3-pip`
 
 For the formal verification of the generated code, the following SPARK Pro version is required:
 
--  SPARK Pro 23.1
+-  SPARK Pro Wavefront 20230710
 
 If you plan to use the RecordFlux Modeller, GNAT Studio needs to be installed and set up.