diff --git a/pkgs/development/ada-modules/gnatprove/0001-fix-install.patch b/pkgs/development/ada-modules/gnatprove/0001-fix-install-fsf-14.patch
similarity index 100%
rename from pkgs/development/ada-modules/gnatprove/0001-fix-install.patch
rename to pkgs/development/ada-modules/gnatprove/0001-fix-install-fsf-14.patch
diff --git a/pkgs/development/ada-modules/gnatprove/0001-fix-install-fsf-15.patch b/pkgs/development/ada-modules/gnatprove/0001-fix-install-fsf-15.patch
new file mode 100644
index 000000000000..eebd974ebffc
--- /dev/null
+++ b/pkgs/development/ada-modules/gnatprove/0001-fix-install-fsf-15.patch
@@ -0,0 +1,35 @@
+From fc15667c867a96887c8c37faf9cc7480f04e6bc5 Mon Sep 17 00:00:00 2001
+From: Thomas Heijligen <src@posteo.de>
+Date: Mon, 2 Jun 2025 14:52:57 +0200
+Subject: [PATCH] fix install
+
+---
+ Makefile | 12 ++++++------
+ 1 file changed, 6 insertions(+), 6 deletions(-)
+
+diff --git a/Makefile b/Makefile
+index 03a1da5c31..b70fbec613 100644
+--- a/Makefile
++++ b/Makefile
+@@ -107,12 +107,12 @@ install:
+ 	$(CP) share/spark/theories/*why $(THEORIESDIR)
+ 	$(CP) share/spark/theories/*mlw $(THEORIESDIR)
+ 	$(CP) share/spark/runtimes/README $(RUNTIMESDIR)
+-	@echo "Generate Coq files by preprocessing context files:"
+-	$(MAKE) -C include generate
+-	$(CP) include/src/*.ad? $(INCLUDEDIR)
+-	$(CP) include/*.gpr $(LIBDIR)
+-	$(CP) include/*.gpr.templ $(LIBDIR)
+-	$(CP) include/proof $(LIBDIR)
++	#@echo "Generate Coq files by preprocessing context files:"
++	#$(MAKE) -C include generate
++	#$(CP) include/src/*.ad? $(INCLUDEDIR)
++	#$(CP) include/*.gpr $(LIBDIR)
++	#$(CP) include/*.gpr.templ $(LIBDIR)
++	#$(CP) include/proof $(LIBDIR)
+ 
+ doc: $(DOC)
+ 
+-- 
+2.49.0
+
diff --git a/pkgs/development/ada-modules/gnatprove/default.nix b/pkgs/development/ada-modules/gnatprove/default.nix
index 1f0a82871ea0..cd835b0e5e59 100644
--- a/pkgs/development/ada-modules/gnatprove/default.nix
+++ b/pkgs/development/ada-modules/gnatprove/default.nix
@@ -29,6 +29,10 @@ let
         };
       });
 
+  # TODO:
+  # Build why3 (github.com/AdaCore/why3) as separate package and not as submodule.
+  # The relevant tags on why3 may get changed without the submodule pointer being updated.
+
   fetchSpark2014 =
     { rev, hash }:
     fetchFromGitHub {
@@ -64,7 +68,7 @@ let
       };
       patches = [
         # Disable Coq related targets which are missing in the fsf-14 branch
-        ./0001-fix-install.patch
+        ./0001-fix-install-fsf-14.patch
 
         # Suppress warnings on aarch64: https://github.com/AdaCore/spark2014/issues/54
         ./0002-mute-aarch64-warnings.patch
@@ -74,6 +78,17 @@ let
       ];
       commit_date = "2024-01-11";
     };
+    "15" = {
+      src = fetchSpark2014 {
+        rev = "22bf1510e0829ba74f9d8d686badb65c7365ee91";
+        hash = "sha256-KjAWMgMT3Tp/s/DQ20ZZajty9Zrv8aPFocwgv5LkjSw=";
+      };
+      patches = [
+        # Disable Coq related targets which are missing in the fsf-15 branch
+        ./0001-fix-install-fsf-15.patch
+      ];
+      commit_date = "2025-06-10";
+    };
   };
 
   thisSpark =
@@ -118,6 +133,9 @@ stdenv.mkDerivation {
   ])
   ++ (lib.optionals (gnat_version == "14") [
     gpr2_24_2_next
+  ])
+  ++ (lib.optionals (gnat_version == "15") [
+    gpr2
   ]);
 
   propagatedBuildInputs = [