diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 036ee0710..4dd4533b7 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -5,9 +5,9 @@ variables:
   ADASAT_ORIGIN: https://gitlab-ci-token:${CI_JOB_TOKEN}@${CI_SERVER_HOST}:${CI_SERVER_PORT}/eng/libadalang
 
   GNAT_PLATFORM: "x86_64-linux"
-  GNAT_VERSION: "24.2"
+  GNAT_VERSION: "25.0"
   GNAT_BUILD_DATE: "all"
-  SPARK_VERSION: "24.2"
+  SPARK_VERSION: "25.0"
   SPARK_BUILD_DATE: "all"
   PYTHON_VERSION: "3.11"
   NODE_VERSION: "20.5.1"
@@ -364,6 +364,8 @@ gnat_pro_compatibility:
         CLEAN_RECORDFLUX_SETUP: 1
       - GNAT_VERSION: "23.2"
         CLEAN_RECORDFLUX_SETUP: 1
+      - GNAT_VERSION: "24.2"
+        CLEAN_RECORDFLUX_SETUP: 1
   script:
     - git fetch --unshallow
     - *update_timestamps_of_generated_code
@@ -447,8 +449,8 @@ verification_tests:
     matrix:
       - SPARK_VERSION: "24.0"
         SPARK_BUILD_DATE: "all"
-      - SPARK_VERSION: "wave"
-        SPARK_BUILD_DATE: "20240303"
+      - SPARK_VERSION: "25.0"
+        SPARK_BUILD_DATE: "all"
   script:
     - *show_gnatprove_cache_stats
     - *setup_spark
@@ -469,8 +471,8 @@ verification_python_tests:
     matrix:
       - SPARK_VERSION: "24.0"
         SPARK_BUILD_DATE: "all"
-      - SPARK_VERSION: "wave"
-        SPARK_BUILD_DATE: "20240522"
+      - SPARK_VERSION: "25.0"
+        SPARK_BUILD_DATE: "all"
   script:
     - *show_gnatprove_cache_stats
     - *setup_gnat
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 101c57cff..c7f49869d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,6 +10,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Added
 
 - Style check for unsigned integer syntax (eng/recordflux/RecordFlux#1775)
+- Support for SPARK Pro 25.0 (eng/recordflux/RecordFlux#1823)
+- Support for GNAT Pro 25.0 (eng/recordflux/RecordFlux#1823)
 
 ## [0.25.0] - 2024-11-05
 
diff --git a/doc/user_guide/10-introduction.rst b/doc/user_guide/10-introduction.rst
index 44cb6dda6..8edc07849 100644
--- a/doc/user_guide/10-introduction.rst
+++ b/doc/user_guide/10-introduction.rst
@@ -105,7 +105,7 @@ The software has successfully been used on various other versions of Linux, incl
 For installing RecordFlux itself, a *native* GNAT compiler for the host system must be installed.
 The following versions of GNAT are supported:
 
--  GNAT Pro 22.2, 23.2 or 24.2
+-  GNAT Pro 22.2, 23.2, 24.2 and 25.0
 -  GNAT Community 2021
 -  FSF GNAT 11.2, 12.2, 13.2 or 14.1
 
@@ -120,7 +120,7 @@ The latest release of GNAT Pro for Rust is also supported.
 
 For compiling the generated code, one of the following versions of GNAT is required:
 
--  GNAT Pro 21.2, 22.2, 23.2 or 24.2
+-  GNAT Pro 21.2, 22.2, 23.2, 24.2 and 25.0
 -  GNAT Community 2021
 -  FSF GNAT 11.2, 12.2, 13.2 or 14.1
 
@@ -150,9 +150,9 @@ To run RecordFlux one of the following Python versions is needed:
 In addition, the Python package installer `pip` is needed to install RecordFlux from the Python Package Index (PyPI).
 The tool can be installed using either the system package manager (`python3-pip` on Debian/Ubuntu/Fedora, `python-pip` on Arch Linux) or any other way described in the pip `installation guide <https://pip.pypa.io/en/stable/installation/>`__.
 
-For the formal verification of the generated code, the following SPARK Pro version is required:
+For the formal verification of the generated code, one of the following SPARK Pro versions is required:
 
--  SPARK Pro 24.2
+-  SPARK Pro 24.2 or 25.0
 
 If you plan to use the RecordFlux Modeller, GNAT Studio needs to be installed and set up.
 
diff --git a/examples/apps/dhcp_client/Makefile b/examples/apps/dhcp_client/Makefile
index aac88f6e7..8ec1772aa 100644
--- a/examples/apps/dhcp_client/Makefile
+++ b/examples/apps/dhcp_client/Makefile
@@ -12,7 +12,7 @@ test: $(BIN) test_binary_size
 	../../../devutils/linux/run $(CWD) tests/run
 
 test_binary_size: $(BIN_OPTIMIZED)
-	test $(shell size -A -d obj_optimized/dhcp_client | grep .text | awk '{ print $$2 }') -le 173000
+	test $(shell size -A -d obj_optimized/dhcp_client | grep .text | awk '{ print $$2 }') -le 181000
 
 build: $(BIN)
 
diff --git a/examples/apps/dhcp_client/dhcp_client.gpr b/examples/apps/dhcp_client/dhcp_client.gpr
index 8ec377ca1..180ff8bce 100644
--- a/examples/apps/dhcp_client/dhcp_client.gpr
+++ b/examples/apps/dhcp_client/dhcp_client.gpr
@@ -15,7 +15,7 @@ project DHCP_Client is
          for Object_Dir use "obj_optimized";
    end case;
    for Create_Missing_Dirs use "True";
-   for Main use ("dhcp_client");
+   for Main use ("dhcp_client.adb");
 
    package Naming is
       for Spec_Suffix ("RecordFlux") use ".rflx";
diff --git a/examples/apps/dhcp_client/obj/.gitkeep b/examples/apps/dhcp_client/obj/.gitkeep
deleted file mode 100644
index e69de29bb..000000000