diff --git a/pkgs/applications/science/logic/klee/default.nix b/pkgs/applications/science/logic/klee/default.nix
new file mode 100644
index 000000000000..e0ace7e81c82
--- /dev/null
+++ b/pkgs/applications/science/logic/klee/default.nix
@@ -0,0 +1,110 @@
+{ stdenv
+, lib
+, fetchFromGitHub
+, fetchpatch
+, cmake
+, llvmPackages_9
+, clang_9
+, python3
+, zlib
+, z3
+, stp
+, cryptominisat
+, gperftools
+, sqlite
+, gtest
+, lit
+, debug ? false
+}:
+
+let
+  kleePython = python3.withPackages (ps: with ps; [ tabulate ]);
+in
+stdenv.mkDerivation rec {
+  pname = "klee";
+  version = "2.2";
+  src = fetchFromGitHub {
+    owner = "klee";
+    repo = "klee";
+    rev = "v${version}";
+    sha256 = "Ar3BKfADjJvvP0dI9+x/l3RDs8ncx4jmO7ol4MgOr4M=";
+  };
+  buildInputs = [
+    llvmPackages_9.llvm clang_9 z3 stp cryptominisat
+    gperftools sqlite
+  ];
+  nativeBuildInputs = [
+    cmake
+  ];
+  checkInputs = [
+    gtest
+
+    # Should appear BEFORE lit, since lit passes through python rather
+    # than the python environment we make.
+    kleePython
+    (lit.override { python3 = kleePython; })
+  ];
+
+  cmakeFlags = let
+    buildType = if debug then "Debug" else "Release";
+  in
+  [
+    "-DCMAKE_BUILD_TYPE=${buildType}"
+    "-DKLEE_RUNTIME_BUILD_TYPE=${buildType}"
+    "-DENABLE_POSIX_RUNTIME=ON"
+    "-DENABLE_UNIT_TESTS=ON"
+    "-DENABLE_SYSTEM_TESTS=ON"
+    "-DGTEST_SRC_DIR=${gtest.src}"
+    "-DGTEST_INCLUDE_DIR=${gtest.src}/googletest/include"
+    "-Wno-dev"
+  ];
+
+  # Silence various warnings during the compilation of fortified bitcode.
+  NIX_CFLAGS_COMPILE = ["-Wno-macro-redefined"];
+
+  prePatch = ''
+    patchShebangs .
+  '';
+
+  /* This patch is currently necessary for the unit test suite to run correctly.
+   * See https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg03136.html
+   * and https://github.com/klee/klee/pull/1458 for more information.
+   */
+  patches = map fetchpatch [
+    {
+      name = "fix-gtest";
+      sha256 = "F+/6videwJZz4sDF9lnV4B8lMx6W11KFJ0Q8t1qUDf4=";
+      url = "https://github.com/klee/klee/pull/1458.patch";
+    }
+  ];
+
+  doCheck = true;
+  checkTarget = "check";
+
+  meta = with lib; {
+    description = "A symbolic virtual machine built on top of LLVM";
+    longDescription = ''
+      KLEE is a symbolic virtual machine built on top of the LLVM compiler
+      infrastructure. Currently, there are two primary components:
+
+      1. The core symbolic virtual machine engine; this is responsible for
+         executing LLVM bitcode modules with support for symbolic values. This
+         is comprised of the code in lib/.
+
+      2. A POSIX/Linux emulation layer oriented towards supporting uClibc, with
+         additional support for making parts of the operating system environment
+         symbolic.
+
+      Additionally, there is a simple library for replaying computed inputs on
+      native code (for closed programs). There is also a more complicated
+      infrastructure for replaying the inputs generated for the POSIX/Linux
+      emulation layer, which handles running native programs in an environment
+      that matches a computed test input, including setting up files, pipes,
+      environment variables, and passing command line arguments.
+    '';
+    homepage = "https://klee.github.io/";
+    license = licenses.ncsa;
+    platforms = [ "x86_64-linux" ];
+    maintainers = with maintainers; [ numinit ];
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index e43ad8707db8..6d0addc1d591 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -26574,6 +26574,8 @@ with pkgs;
 
   klayout = libsForQt5.callPackage ../applications/misc/klayout { };
 
+  klee = callPackage ../applications/science/logic/klee { };
+
   kmetronome = libsForQt5.callPackage ../applications/audio/kmetronome { };
 
   kmplayer = libsForQt5.callPackage ../applications/video/kmplayer { };