KLEE is a dynamic symbolic execution engine built on LLVM. It automatically generates tests with high coverage and finds deep bugs that manual testing misses entirely.
KLEE is a dynamic symbolic execution engine built on LLVM, available under the UIUC open source license. Instead of running a program with one specific input, KLEE treats inputs as symbolic variables that can hold any value.
By doing this, KLEE simultaneously explores all feasible execution paths through a program. At each branch, it asks a constraint solver: "can this branch be taken?" — and forks the execution state for every feasible answer. When it finds a crash or violation, it hands you the exact concrete input that triggers it.
The original OSDI 2008 paper ran KLEE on 89 GNU Coreutils programs and found 56 bugs — including ones that had existed for years. It is now cited in thousands of research papers and used to analyze operating systems, cryptographic libraries, and firmware.
// 1. Include KLEE header #include <klee/klee.h> int main() { char buf[8]; // 2. Mark memory as symbolic klee_make_symbolic(buf, sizeof(buf), "input"); // KLEE explores ALL possible values of buf if (buf[0] == 'K' && buf[1] == 'L') { if (buf[2] == 'E' && buf[3] == 'E') { klee_assert(0); // KLEE finds this! } } return 0; }
Executes LLVM bitcode with symbolic values. Handles path forking, constraint collection, and error detection. Lives in lib/.
Makes files, pipes, env vars, and CLI arguments symbolic — enabling analysis of programs that interact with the OS.
Interfaces with STP, Z3, and MetaSMT to determine which branches are feasible and generate concrete triggering inputs.
Replays computed test inputs on native code with the exact environment state — files, pipes, arguments — that KLEE computed.
Choose your installation method below. All documentation is embedded — no external links needed.
Docker provides a fully pre-built KLEE environment that works identically on Linux, macOS, and Windows. This is the fastest and most reliable way to get started — no build steps, no dependency management.
If you don't already have Docker, install it for your OS. Docker provides containerised environments that are isolated from your system.
docker --version
Pull the official KLEE Docker image from DockerHub. The image is based on Ubuntu 22.04 LTS and includes KLEE, LLVM 13, Clang, and Z3/STP solvers pre-installed.
docker pull klee/klee
Or pull a specific tagged release:
docker pull klee/klee:3.2 # latest stable docker pull klee/klee:3.0 docker pull klee/klee:2.3
Run a temporary container and get a shell. The --rm flag destroys the container when you exit. The --ulimit flag sets unlimited stack size to prevent stack overflow issues inside KLEE.
docker run --rm -ti --ulimit='stack=-1:-1' klee/klee:3.2
If successful, your prompt changes to the klee user inside the container. Verify KLEE and Clang are available:
klee@container:~$ klee --version KLEE 3.2 (https://klee-se.org) Build mode: RelWithDebInfo (Asserts: TRUE) LLVM version 13.0.1 klee@container:~$ clang --version clang version 13.0.1 Target: x86_64-unknown-linux-gnu
Exit the temporary container:
klee@container:~$ exit
Create a persistent named container, write a simple C program, compile to LLVM bitcode, and run KLEE on it.
docker run -ti --name=my_klee --ulimit='stack=-1:-1' klee/klee
Inside the container, create a simple test program:
klee@container:~$ cat > test.c << 'EOF' #include <klee/klee.h> #include <assert.h> int main() { int x, y; klee_make_symbolic(&x, sizeof(x), "x"); klee_make_symbolic(&y, sizeof(y), "y"); if (x + y > 1000) { if (x > y) { klee_assert(0); /* KLEE will find this */ } } return 0; } EOF
klee@container:~$ clang -emit-llvm -g -c -O0 test.c -o test.bc klee@container:~$ klee test.bc KLEE: output directory is "klee-out-0" KLEE: Using STP solver backend KLEE: done: total instructions = 37 KLEE: done: completed paths = 3 KLEE: done: generated tests = 3 KLEE: ERROR: test.c:11: ASSERTION FAIL: 0 KLEE: NOTE: now ignoring this error at this location
klee-out-0/ contains .ktest files — one per path — including one that reproduces the assertion failure with concrete values of x and y.KLEE outputs a klee-out-N/ directory with one .ktest file per explored path. Use ktest-tool to inspect the concrete values, or use klee-replay to re-run your native binary with those exact inputs.
klee@container:~$ ls klee-last/ assembly.ll info messages.txt run.istats run.stats test000001.ktest test000002.ktest test000003.assert.err test000003.ktest klee@container:~$ ktest-tool klee-last/test000003.ktest ktest file : 'klee-last/test000003.ktest' args : ['test.bc'] num objects: 2 object 0: name: 'x' size: 4 value: 1001 object 1: name: 'y' size: 4 value: 0
The values x=1001, y=0 satisfy both conditions and trigger the assertion. KLEE generated this without you providing any inputs.
Stop and restart a named container — your files persist. Mount your host filesystem using --volume to analyse your own code.
# Exit the container (files persist) klee@container:~$ exit # See container still exists docker ps -a # Restart it docker start -ai my_klee # When done, remove it docker rm my_klee
docker run -ti --rm --ulimit='stack=-1:-1' \ --volume=$(pwd):/home/klee/mycode \ klee/klee
klee user has sudo access (password: klee) so you can install editors or tools. The image is based on Ubuntu 22.04 LTS. Do not use this image in production — the default user has sudo.If you prefer to build the Docker image yourself rather than pulling from DockerHub:
git clone https://github.com/klee/klee.git cd klee docker build -t klee/klee .
This builds from the Dockerfile in the root of the repository and takes 15–30 minutes depending on your machine.
Install KLEE directly from your distribution's package repositories. Quick and easy — no manual compilation. Package versions may trail the latest release slightly.
The Snap package works on Ubuntu, Fedora, Debian, and other major Linux distributions that support Snap.
sudo snap install klee
klee --version
# Compile to LLVM bitcode with debug info clang -emit-llvm -g -c -O0 yourfile.c -o yourfile.bc # Run KLEE klee yourfile.bc
KLEE is available in the Arch User Repository.
yay -S klee
git clone https://aur.archlinux.org/klee.git cd klee makepkg -si
Install the latest KLEE release via pkg or build from the ports tree.
pkg install klee
cd /usr/ports/security/klee make install clean
zypper install klee
Nix is even faster than Docker if you already have it installed. Nix handles all dependencies declaratively and reproducibly without modifying your system.
If you don't have Nix installed yet, the official installer handles everything:
curl -L https://nixos.org/nix/install | sh
Use nix run to try KLEE instantly without permanently installing anything:
nix run nixpkgs#klee
nix shell nixpkgs#klee nixpkgs#clang
Your shell now has klee and clang available. Compile to bitcode and run KLEE as usual.
For reproducible project environments, add KLEE to a flake.nix:
{
inputs.nixpkgs.url = "github:NixOS/nixpkgs";
outputs = { nixpkgs, ... }: {
devShells.x86_64-linux.default =
nixpkgs.legacyPackages.x86_64-linux.mkShell {
packages = with nixpkgs.legacyPackages.x86_64-linux; [
klee clang z3 llvm
];
};
};
}
nix develop
Homebrew works on both macOS and Linux. This installs the latest KLEE release with a single command.
brew install klee
Homebrew handles all dependencies (LLVM, Z3, etc.) automatically.
klee --version which klee # should show brew path
# Use the Clang from LLVM (not Apple Clang) $(brew --prefix llvm)/bin/clang \ -emit-llvm -g -c -O0 test.c -o test.bc klee test.bc
clang (from the brew formula), not Apple's built-in Clang. Apple Clang does not support -emit-llvm for producing KLEE-compatible bitcode.Full control over the build configuration. Recommended for researchers and contributors who need custom KLEE configurations, specific solver combinations, or want to modify KLEE itself.
KLEE requires LLVM 16, a C++ compiler, CMake, and at least one SMT solver.
sudo apt update sudo apt install -y \ build-essential cmake git python3 \ llvm-16 llvm-16-dev clang-16 \ libz3-dev zlib1g-dev libssl-dev
STP is KLEE's default solver and often faster for certain workloads. Z3 is also supported.
git clone https://github.com/stp/stp.git mkdir stp/build && cd stp/build cmake -DBUILD_SHARED_LIBS:BOOL=OFF \ -DENABLE_PYTHON_INTERFACE:BOOL=OFF .. make -j$(nproc) sudo make install cd ../..
git clone https://github.com/klee/klee.git mkdir klee/build && cd klee/build cmake \ -DENABLE_SOLVER_STP=ON \ -DENABLE_SOLVER_Z3=ON \ -DENABLE_POSIX_RUNTIME=ON \ -DKLEE_RUNTIME_BUILD_TYPE=Release+Debug+Asserts \ -DLLVM_CONFIG_BINARY=$(which llvm-config-16) \ .. make -j$(nproc) sudo make install
-DCMAKE_BUILD_TYPE=Release for a faster binary. Use RelWithDebInfo (default) if you need debug symbols for development.klee --version make check # run the test suite
For building arbitrary KLEE configurations — including different LLVM versions, solver combinations, and optional components — use the automated build script from the repo.
git clone https://github.com/klee/klee.git cd klee ./scripts/build/build.sh --help
The script supports flags for LLVM version, solver selection, coverage builds, and more. See the build script documentation for all options.
Systematically explores all feasible execution paths using search heuristics like coverage-guided and random-path selection.
Generates high-coverage test suites automatically. Each test corresponds to a distinct path, including corner cases humans miss.
Finds memory errors, division by zero, buffer overflows, assertion failures — with a concrete input to reproduce each one.
Interfaces with STP, Z3, and MetaSMT. Supports query caching, solver chaining, and counterexample-guided optimisation.
Makes file systems, env vars, pipes, and CLI arguments symbolic — for analysing programs that interact with the OS.
Built on LLVM — supports C, C++, Rust, and any language that compiles to LLVM IR. Works with the modern toolchain.
Detailed branch, line, and instruction coverage stats. Outputs .ktest files compatible with standard replay tools.
Sophisticated caching and independence-based solver optimisations. Avoids re-solving previously seen constraints.
Official images updated with every release. Pull and analyse in minutes — no build environment setup required.
KLEE forks execution at every branch, building a tree of all reachable program states. Each node is a constraint set; each leaf is a test case.
Use klee_make_symbolic() to declare variables that should hold all possible values.
Compile with Clang using -emit-llvm to produce LLVM bitcode for KLEE to interpret.
At each conditional, KLEE asks an SMT solver whether each branch is feasible and forks execution.
Every explored path becomes a .ktest file with concrete inputs. Errors include the triggering input.
Cristian Cadar, Daniel Dunbar, Dawson R. Engler. Found 56 bugs in GNU Coreutils including issues that had existed for years — with higher branch coverage than the manually-written test suite.
OSDI 2008Dozens of published extensions to KLEE for floating-point analysis, multi-node execution, symbolic network, and more.
Various Venues4,200+ papers cite KLEE. Topics include OS kernels, cryptographic libraries, embedded firmware, network protocols, and compilers.
View All Publications →Ask questions, report bugs, and get answers from the KLEE team and community.
KLEE is open source under the UIUC license. All contributions welcome.
The International KLEE Workshop brings researchers and practitioners together annually.
Free, open source, and battle-tested since 2008. Get a shell with KLEE in 60 seconds.