diff --git a/doc/release-notes/rl-2505.section.md b/doc/release-notes/rl-2505.section.md
index 8ae1797aaf1a..537ccfc101a2 100644
--- a/doc/release-notes/rl-2505.section.md
+++ b/doc/release-notes/rl-2505.section.md
@@ -272,7 +272,7 @@
 
 - `nodePackages.meshcommander` has been removed, as the package was deprecated by Intel.
 
-- The default version of `z3` has been updated from 4.8 to 4.14, and all old versions have been dropped. Note that `fstar` still depends on specific versions, and maintains them as overrides.
+- The default version of `z3` has been updated from 4.8 to 4.15, and all old versions have been dropped. Note that `fstar` still depends on specific versions, and maintains them as overrides.
 
 - `prometheus` has been updated from 2.55.0 to 3.1.0.
   Read the [release blog post](https://prometheus.io/blog/2024/11/14/prometheus-3-0/) and
diff --git a/pkgs/by-name/z3/z3/package.nix b/pkgs/by-name/z3/z3/package.nix
index cc80e0151581..3883b4d3840e 100644
--- a/pkgs/by-name/z3/z3/package.nix
+++ b/pkgs/by-name/z3/z3/package.nix
@@ -1,6 +1,129 @@
 {
-  z3_4_14,
-  ...
-}@args:
+  lib,
+  stdenv,
+  fetchFromGitHub,
+  python3,
+  fixDarwinDylibNames,
+  nix-update-script,
+  versionCheckHook,
 
-z3_4_14.override args
+  javaBindings ? false,
+  ocamlBindings ? false,
+  pythonBindings ? true,
+  jdk ? null,
+  ocaml ? null,
+  findlib ? null,
+  zarith ? null,
+  ...
+}:
+
+assert javaBindings -> jdk != null;
+assert ocamlBindings -> ocaml != null && findlib != null && zarith != null;
+
+stdenv.mkDerivation (finalAttrs: {
+  pname = "z3";
+  version = "4.15.0";
+
+  src = fetchFromGitHub {
+    owner = "Z3Prover";
+    repo = "z3";
+    rev = "z3-${finalAttrs.version}";
+    hash = "sha256-fk3NyV6vIDXivhiNOW2Y0i5c+kzc7oBqaeBWj/JjpTM=";
+  };
+
+  strictDeps = true;
+
+  nativeBuildInputs =
+    [ python3 ]
+    ++ lib.optionals stdenv.hostPlatform.isDarwin [ fixDarwinDylibNames ]
+    ++ lib.optionals javaBindings [ jdk ]
+    ++ lib.optionals ocamlBindings [
+      ocaml
+      findlib
+    ];
+  propagatedBuildInputs = [ python3.pkgs.setuptools ] ++ lib.optionals ocamlBindings [ zarith ];
+  enableParallelBuilding = true;
+
+  postPatch = lib.optionalString ocamlBindings ''
+    export OCAMLFIND_DESTDIR=$ocaml/lib/ocaml/${ocaml.version}/site-lib
+    mkdir -p $OCAMLFIND_DESTDIR/stublibs
+  '';
+
+  configurePhase = ''
+    runHook preConfigure
+
+    ${python3.pythonOnBuildForHost.interpreter} \
+      scripts/mk_make.py \
+      --prefix=$out \
+      ${lib.optionalString javaBindings "--java"} \
+      ${lib.optionalString ocamlBindings "--ml"} \
+      ${lib.optionalString pythonBindings "--python --pypkgdir=$out/${python3.sitePackages}"}
+
+    cd build
+
+    runHook postConfigure
+  '';
+
+  doCheck = true;
+  checkPhase = ''
+    runHook preCheck
+
+    make -j $NIX_BUILD_CORES test
+    ./test-z3 -a
+
+    runHook postCheck
+  '';
+
+  postInstall =
+    ''
+      mkdir -p $dev $lib
+      mv $out/lib $lib/lib
+      mv $out/include $dev/include
+    ''
+    + lib.optionalString pythonBindings ''
+      mkdir -p $python/lib
+      mv $lib/lib/python* $python/lib/
+      ln -sf $lib/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary} $python/${python3.sitePackages}/z3/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary}
+    ''
+    + lib.optionalString javaBindings ''
+      mkdir -p $java/share/java
+      mv com.microsoft.z3.jar $java/share/java
+      moveToOutput "lib/libz3java.${stdenv.hostPlatform.extensions.sharedLibrary}" "$java"
+    '';
+
+  doInstallCheck = true;
+  nativeInstallCheckInputs = [ versionCheckHook ];
+
+  outputs =
+    [
+      "out"
+      "lib"
+      "dev"
+      "python"
+    ]
+    ++ lib.optionals javaBindings [ "java" ]
+    ++ lib.optionals ocamlBindings [ "ocaml" ];
+
+  passthru = {
+    updateScript = nix-update-script {
+      extraArgs = [
+        "--version-regex"
+        "^z3-([0-9]+\\.[0-9]+\\.[0-9]+)$"
+      ];
+    };
+  };
+
+  meta = {
+    description = "High-performance theorem prover and SMT solver";
+    mainProgram = "z3";
+    homepage = "https://github.com/Z3Prover/z3";
+    changelog = "https://github.com/Z3Prover/z3/releases/tag/z3-${finalAttrs.version}";
+    license = lib.licenses.mit;
+    platforms = lib.platforms.unix;
+    maintainers = with lib.maintainers; [
+      thoughtpolice
+      ttuegel
+      numinit
+    ];
+  };
+})
diff --git a/pkgs/by-name/z3/z3_4_14/package.nix b/pkgs/by-name/z3/z3_4_14/package.nix
deleted file mode 100644
index 60339b94e30f..000000000000
--- a/pkgs/by-name/z3/z3_4_14/package.nix
+++ /dev/null
@@ -1,130 +0,0 @@
-{
-  lib,
-  stdenv,
-  fetchFromGitHub,
-  python3,
-  fixDarwinDylibNames,
-  nix-update-script,
-  javaBindings ? false,
-  ocamlBindings ? false,
-  pythonBindings ? true,
-  jdk ? null,
-  ocaml ? null,
-  findlib ? null,
-  zarith ? null,
-  versionInfo ? {
-    regex = "^v(4\\.14\\.[0-9]+)$";
-    version = "4.14.1";
-    hash = "sha256-pTsDzf6Frk4mYAgF81wlR5Kb1x56joFggO5Fa3G2s70=";
-  },
-  ...
-}:
-
-assert javaBindings -> jdk != null;
-assert ocamlBindings -> ocaml != null && findlib != null && zarith != null;
-
-stdenv.mkDerivation (finalAttrs: {
-  pname = "z3";
-  inherit (versionInfo) version;
-
-  src = fetchFromGitHub {
-    owner = "Z3Prover";
-    repo = "z3";
-    rev = "z3-${finalAttrs.version}";
-    inherit (versionInfo) hash;
-  };
-
-  strictDeps = true;
-
-  nativeBuildInputs =
-    [ python3 ]
-    ++ lib.optional stdenv.hostPlatform.isDarwin fixDarwinDylibNames
-    ++ lib.optional javaBindings jdk
-    ++ lib.optionals ocamlBindings [
-      ocaml
-      findlib
-    ];
-  propagatedBuildInputs = [ python3.pkgs.setuptools ] ++ lib.optionals ocamlBindings [ zarith ];
-  enableParallelBuilding = true;
-
-  postPatch = lib.optionalString ocamlBindings ''
-    export OCAMLFIND_DESTDIR=$ocaml/lib/ocaml/${ocaml.version}/site-lib
-    mkdir -p $OCAMLFIND_DESTDIR/stublibs
-  '';
-
-  configurePhase =
-    lib.concatStringsSep " " (
-      [ "${python3.pythonOnBuildForHost.interpreter} scripts/mk_make.py --prefix=$out" ]
-      ++ lib.optional javaBindings "--java"
-      ++ lib.optional ocamlBindings "--ml"
-      ++ lib.optional pythonBindings "--python --pypkgdir=$out/${python3.sitePackages}"
-    )
-    + "\n"
-    + "cd build";
-
-  doCheck = true;
-  checkPhase = ''
-    make -j $NIX_BUILD_CORES test
-    ./test-z3 -a
-  '';
-
-  postInstall =
-    ''
-      mkdir -p $dev $lib
-      mv $out/lib $lib/lib
-      mv $out/include $dev/include
-    ''
-    + lib.optionalString pythonBindings ''
-      mkdir -p $python/lib
-      mv $lib/lib/python* $python/lib/
-      ln -sf $lib/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary} $python/${python3.sitePackages}/z3/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary}
-    ''
-    + lib.optionalString javaBindings ''
-      mkdir -p $java/share/java
-      mv com.microsoft.z3.jar $java/share/java
-      moveToOutput "lib/libz3java.${stdenv.hostPlatform.extensions.sharedLibrary}" "$java"
-    '';
-
-  doInstallCheck = true;
-  installCheckPhase = ''
-    $out/bin/z3 -version 2>&1 | grep -F "Z3 version $version"
-  '';
-
-  outputs =
-    [
-      "out"
-      "lib"
-      "dev"
-      "python"
-    ]
-    ++ lib.optional javaBindings "java"
-    ++ lib.optional ocamlBindings "ocaml";
-
-  passthru = {
-    updateScript = nix-update-script {
-      extraArgs =
-        [
-          "--version-regex"
-          versionInfo.regex
-        ]
-        ++ lib.optionals (versionInfo.autoUpdate or null != null) [
-          "--override-filename"
-          versionInfo.autoUpdate
-        ];
-    };
-  };
-
-  meta = {
-    description = "High-performance theorem prover and SMT solver";
-    mainProgram = "z3";
-    homepage = "https://github.com/Z3Prover/z3";
-    changelog = "https://github.com/Z3Prover/z3/releases/tag/z3-${finalAttrs.version}";
-    license = lib.licenses.mit;
-    platforms = lib.platforms.unix;
-    maintainers = with lib.maintainers; [
-      thoughtpolice
-      ttuegel
-      numinit
-    ];
-  };
-})
diff --git a/pkgs/top-level/aliases.nix b/pkgs/top-level/aliases.nix
index e8e9d8b79e75..ad609df10c42 100644
--- a/pkgs/top-level/aliases.nix
+++ b/pkgs/top-level/aliases.nix
@@ -2092,6 +2092,12 @@ mapAliases {
 
   ### Z ###
 
+  z3_4_11 = throw "'z3_4_11' has been removed in favour of the latest version. Use 'z3'."; # Added 2025-05-18
+  z3_4_12 = throw "'z3_4_12' has been removed in favour of the latest version. Use 'z3'."; # Added 2025-05-18
+  z3_4_13 = throw "'z3_4_13' has been removed in favour of the latest version. Use 'z3'."; # Added 2025-05-18
+  z3_4_14 = throw "'z3_4_14' has been removed in favour of the latest version. Use 'z3'."; # Added 2025-05-18
+  z3_4_8_5 = throw "'z3_4_8_5' has been removed in favour of the latest version. Use 'z3'."; # Added 2025-05-18
+  z3_4_8 = throw "'z3_4_8' has been removed in favour of the latest version. Use 'z3'."; # Added 2025-05-18
   zabbix50 = throw "'zabbix50' has been removed, it would have reached its End of Life a few days after the release of NixOS 25.05. Consider upgrading to 'zabbix60' or 'zabbix70'.";
   zabbix64 = throw "'zabbix64' has been removed because it reached its End of Life. Consider upgrading to 'zabbix70'.";
   zeroadPackages = recurseIntoAttrs {