diff --git a/pkgs/applications/science/logic/key/default.nix b/pkgs/applications/science/logic/key/default.nix
new file mode 100644
index 000000000000..b08c4d84d1fc
--- /dev/null
+++ b/pkgs/applications/science/logic/key/default.nix
@@ -0,0 +1,74 @@
+{ stdenv
+, fetchurl
+, unzip
+, jdk
+, ant
+, jre
+, makeWrapper
+, runCommand
+, key
+}:
+
+# get this from the download URL when changing version
+let gitRevision = "7d3deab0763c88edee4f7a08e604661e0dbdd450";
+
+in stdenv.mkDerivation rec {
+  pname = "key";
+  version = "2.6.3";
+
+  src = fetchurl {
+    url = "https://formal.iti.kit.edu/key/releases/${version}/key-src-${version}_${gitRevision}.zip";
+    sha256 = "1dr5jmrqs0iy76wdsfiv5hx929i24yzm1xypzqqvx7afc7apyawy";
+  };
+
+  sourceRoot = "key";
+
+  nativeBuildInputs = [
+    unzip
+    jdk
+    ant
+    makeWrapper
+  ];
+
+  buildPhase = ''
+    ant -buildfile scripts/build.xml \
+      -Dgit.revision=${gitRevision} \
+      compileAll deployAll
+  '';
+
+  postCheck = ''
+    ant -buildfile scripts/build.xml \
+      -Dgit.revision=${gitRevision} \
+      compileAllTests runAllTests test-deploy-all
+  '';
+
+  installPhase = ''
+    mkdir -p $out/share/java
+    # Wrong version in the code. On next version change 2.5 to ${version}:
+    unzip deployment/key-2.5_${gitRevision}.zip -d $out/share/java
+    mkdir -p $out/bin
+    makeWrapper ${jre}/bin/java $out/bin/KeY \
+      --add-flags "-cp $out/share/java/KeY.jar de.uka.ilkd.key.core.Main"
+  '';
+
+  passthru.tests.check-version = runCommand "key-help" {} ''
+    ${key}/bin/KeY --help | grep 2.5 # Wrong version in the code. On next version change to ${version}
+    touch $out
+  '';
+
+  meta = with stdenv.lib; {
+    description = "Java formal verification tool";
+    homepage = "https://www.key-project.org"; # also https://formal.iti.kit.edu/key/
+    longDescription = ''
+      The KeY System is a formal software development tool that aims to
+      integrate design, implementation, formal specification, and formal
+      verification of object-oriented software as seamlessly as possible.
+      At the core of the system is a novel theorem prover for the first-order
+      Dynamic Logic for Java with a user-friendly graphical interface.
+    '';
+    license = licenses.gpl2;
+    maintainers = with maintainers; [ fgaz ];
+    platforms = platforms.all;
+  };
+}
+
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 5482f922a03c..eddec3d6756b 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -26777,6 +26777,8 @@ in
       else smlnj;
   };
 
+  key = callPackage ../applications/science/logic/key { };
+
   lean = callPackage ../applications/science/logic/lean {};
   lean2 = callPackage ../applications/science/logic/lean2 {};
   lean3 = lean;