diff --git a/pkgs/applications/science/logic/klee/default.nix b/pkgs/applications/science/logic/klee/default.nix
index e0ace7e81c82..612d9fd57c7c 100644
--- a/pkgs/applications/science/logic/klee/default.nix
+++ b/pkgs/applications/science/logic/klee/default.nix
@@ -1,5 +1,5 @@
-{ stdenv
-, lib
+{ lib
+, callPackage
 , fetchFromGitHub
 , fetchpatch
 , cmake
@@ -14,13 +14,37 @@
 , sqlite
 , gtest
 , lit
+
+# Build KLEE in debug mode. Defaults to false.
 , debug ? false
+
+# Include debug info in the build. Defaults to true.
+, includeDebugInfo ? true
+
+# Enable KLEE asserts. Defaults to true, since LLVM is built with them.
+, asserts ? true
+
+# Build the KLEE runtime in debug mode. Defaults to true, as this improves
+# stack traces of the software under test.
+, debugRuntime ? true
+
+# Enable runtime asserts. Default false.
+, runtimeAsserts ? false
+
+# Extra klee-uclibc config.
+, extraKleeuClibcConfig ? {}
 }:
 
 let
+  # Python used for KLEE tests.
   kleePython = python3.withPackages (ps: with ps; [ tabulate ]);
+
+  # The klee-uclibc derivation.
+  kleeuClibc = callPackage ./klee-uclibc.nix {
+    inherit clang_9 llvmPackages_9 extraKleeuClibcConfig debugRuntime runtimeAsserts;
+  };
 in
-stdenv.mkDerivation rec {
+clang_9.stdenv.mkDerivation rec {
   pname = "klee";
   version = "2.2";
   src = fetchFromGitHub {
@@ -30,11 +54,12 @@ stdenv.mkDerivation rec {
     sha256 = "Ar3BKfADjJvvP0dI9+x/l3RDs8ncx4jmO7ol4MgOr4M=";
   };
   buildInputs = [
-    llvmPackages_9.llvm clang_9 z3 stp cryptominisat
+    llvmPackages_9.llvm
+    z3 stp cryptominisat
     gperftools sqlite
   ];
   nativeBuildInputs = [
-    cmake
+    cmake clang_9
   ];
   checkInputs = [
     gtest
@@ -46,14 +71,17 @@ stdenv.mkDerivation rec {
   ];
 
   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"
+    onOff = val: if val then "ON" else "OFF";
+  in [
+    "-DCMAKE_BUILD_TYPE=${if debug then "Debug" else if !debug && includeDebugInfo then "RelWithDebInfo" else "MinSizeRel"}"
+    "-DKLEE_RUNTIME_BUILD_TYPE=${if debugRuntime then "Debug" else "Release"}"
+    "-DKLEE_ENABLE_TIMESTAMP=${onOff false}"
+    "-DENABLE_KLEE_UCLIBC=${onOff true}"
+    "-DKLEE_UCLIBC_PATH=${kleeuClibc}"
+    "-DENABLE_KLEE_ASSERTS=${onOff asserts}"
+    "-DENABLE_POSIX_RUNTIME=${onOff true}"
+    "-DENABLE_UNIT_TESTS=${onOff true}"
+    "-DENABLE_SYSTEM_TESTS=${onOff true}"
     "-DGTEST_SRC_DIR=${gtest.src}"
     "-DGTEST_INCLUDE_DIR=${gtest.src}/googletest/include"
     "-Wno-dev"
@@ -66,21 +94,40 @@ stdenv.mkDerivation rec {
     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 [
+    /* 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.
+     */
     {
       name = "fix-gtest";
       sha256 = "F+/6videwJZz4sDF9lnV4B8lMx6W11KFJ0Q8t1qUDf4=";
       url = "https://github.com/klee/klee/pull/1458.patch";
     }
+
+    # This patch fixes test compile issues with glibc 2.33+.
+    {
+      name = "fix-glibc-2.33";
+      sha256 = "PzxqtFyLy9KF1eA9AAKg1tu+ggRdvu7leuvXifayIcc=";
+      url = "https://github.com/klee/klee/pull/1385.patch";
+    }
+
+    # /etc/mtab doesn't exist in the Nix build sandbox.
+    {
+      name = "fix-etc-mtab-in-tests";
+      sha256 = "2Yb/rJA791esNNqq8uAXV+MML4YXIjPKkHBOufvyRoQ=";
+      url = "https://github.com/klee/klee/pull/1471.patch";
+    }
   ];
 
   doCheck = true;
   checkTarget = "check";
 
+  passthru = {
+    # Let the user depend on `klee.uclibc` for klee-uclibc
+    uclibc = kleeuClibc;
+  };
+
   meta = with lib; {
     description = "A symbolic virtual machine built on top of LLVM";
     longDescription = ''
diff --git a/pkgs/applications/science/logic/klee/klee-uclibc.nix b/pkgs/applications/science/logic/klee/klee-uclibc.nix
new file mode 100644
index 000000000000..2e3826c50c42
--- /dev/null
+++ b/pkgs/applications/science/logic/klee/klee-uclibc.nix
@@ -0,0 +1,98 @@
+{ lib
+, fetchurl
+, fetchFromGitHub
+, which
+, linuxHeaders
+, clang_9
+, llvmPackages_9
+, python3
+, debugRuntime ? true
+, runtimeAsserts ? false
+, extraKleeuClibcConfig ? {}
+}:
+
+let
+  localeSrcBase = "uClibc-locale-030818.tgz";
+  localeSrc = fetchurl {
+    url = "http://www.uclibc.org/downloads/${localeSrcBase}";
+    sha256 = "xDYr4xijjxjZjcz0YtItlbq5LwVUi7k/ZSmP6a+uvVc=";
+  };
+  resolvedExtraKleeuClibcConfig = lib.mapAttrsToList (name: value: "${name}=${value}") (extraKleeuClibcConfig // {
+    "UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA" = "n";
+    "RUNTIME_PREFIX" = "/";
+    "DEVEL_PREFIX" = "/";
+  });
+in
+clang_9.stdenv.mkDerivation rec {
+  pname = "klee-uclibc";
+  version = "1.2";
+  src = fetchFromGitHub {
+    owner = "klee";
+    repo = "klee-uclibc";
+    rev = "klee_uclibc_v${version}";
+    sha256 = "qdrGMw+2XwpDsfxdv6swnoaoACcF5a/RWgUxUYbtPrI=";
+  };
+  nativeBuildInputs = [
+    clang_9
+    llvmPackages_9.llvm
+    python3
+    which
+  ];
+
+  # Some uClibc sources depend on Linux headers.
+  UCLIBC_KERNEL_HEADERS = "${linuxHeaders}/include";
+
+  # HACK: needed for cross-compile.
+  # See https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg03141.html
+  KLEE_CFLAGS = "-idirafter ${clang_9}/resource-root/include";
+
+  prePatch = ''
+    patchShebangs ./configure
+    patchShebangs ./extra
+  '';
+
+  # klee-uclibc configure does not support --prefix, so we override configurePhase entirely
+  configurePhase = ''
+    ./configure ${lib.escapeShellArgs (
+      ["--make-llvm-lib"]
+      ++ lib.optional (!debugRuntime) "--enable-release"
+      ++ lib.optional runtimeAsserts "--enable-assertions"
+    )}
+
+    # Set all the configs we care about.
+    configs=(
+      PREFIX=$out
+    )
+    for value in ${lib.escapeShellArgs resolvedExtraKleeuClibcConfig}; do
+      configs+=("$value")
+    done
+
+    for configFile in .config .config.cmd; do
+      for config in "''${configs[@]}"; do
+        prefix="''${config%%=*}="
+        if grep -q "$prefix" "$configFile"; then
+          sed -i "s"'\001'"''${prefix}"'\001'"#''${prefix}"'\001'"g" "$configFile"
+        fi
+        echo "$config" >> "$configFile"
+      done
+    done
+  '';
+
+  # Link the locale source into the correct place
+  preBuild = ''
+    ln -sf ${localeSrc} extra/locale/${localeSrcBase}
+  '';
+
+  makeFlags = ["HAVE_DOT_CONFIG=y"];
+
+  meta = with lib; {
+    description = "A modified version of uClibc for KLEE.";
+    longDescription = ''
+      klee-uclibc is a bitcode build of uClibc meant for compatibility with the
+      KLEE symbolic virtual machine.
+    '';
+    homepage = "https://klee.github.io/";
+    license = licenses.lgpl3;
+    maintainers = with maintainers; [ numinit ];
+  };
+}