Alive2 turns an LLVM optimization into a proof obligation

An optimization that changes behaviour is a bug, not a slower program

The problem Alive2 addresses is narrow and technical. LLVM passes are supposed to preserve the meaning of a program, and a pass that does not is an undefined behaviour bug that no amount of testing is guaranteed to catch. The project describes itself as automatic verification of LLVM optimizations, and it does this by turning a candidate transformation into a formal question. That question is a refinement check: does the output program still accept every input the input program accepted, and reject the same ones? Rather than comparing output text or running a test corpus, Alive2 asks an SMT solver. The audience is compiler engineers and anyone who writes passes for LLVM, because a pass that passes the existing unit tests can still be wrong on inputs no test covers, and the whole point of the tool is to search a space much larger than any hand-written test.

The pipeline: LLVM IR to Alive2 IR to a symbolic execution to SMT

The repository is organised around the pipeline. The listed libraries are Alive2 IR, the symbolic executor, the LLVM to Alive2 IR converter, the refinement check that the documentation also calls the optimization verifier, and an SMT abstraction layer. A transformation you want to check is first converted into Alive2's own IR, then executed symbolically so that inputs become symbolic variables instead of concrete values, and finally handed to the SMT solver as a formula. The refinement check either proves the two programs equivalent or produces a counterexample. Z3 is the solver in the supported setup, and the build directory even carries a helper script for finding problems after a run. Two things follow from this design. First, the cost of a check is dominated by the solver, not by the simulation, which is why a timeout configuration exists for the compiler drivers. Second, the abstraction layer sits between Alive2 and the solver, so the SMT encoding is Alive2's own and not a direct transcription of LLVM semantics.

Building Alive2 with cmake and ninja

The build needs cmake, gcc or clang, re2c, and Z3, with LLVM and hiredis optional. The documented sequence is short:

git clone [email protected]:AliveToolkit/alive2.git
cd alive2
mkdir build
cd build
cmake -GNinja -DCMAKE_BUILD_TYPE=Release ..
ninja

If cmake cannot find the Z3 include directory, or finds the wrong one, the documentation tells you to point it at the right paths:

cmake -GNinja -DZ3_INCLUDE_DIR=/path/to/z3/include -DZ3_LIBRARIES=/path/to/z3/lib/libz3.so -DCMAKE_BUILD_TYPE=Release ..

The repository also ships a Dockerfile that does the same work from an ubuntu 24.04 base, installing the dependencies including z3, libz3-dev, re2c and libhiredis-dev, then cloning llvm-project and alive2 and running ninja and ninja check. That container path is the more reproducible option for CI, since the manual path depends on a Z3 install that already exists on the machine.

Translation validation needs an LLVM built with RTTI and exceptions

The opt and clang translation validation plugins do not build against a stock LLVM. The documentation states that they require a build of LLVM with RTTI and exceptions turned on, and that the latest version of Alive2 is always intended to be built against the latest version of LLVM, using the main branch of the LLVM repository. The LLVM build is therefore part of the setup, not an optional extra:

cd ~/llvm
mkdir build
cd build
cmake -GNinja -DLLVM_ENABLE_RTTI=ON -DBUILD_SHARED_LIBS=ON -DCMAKE_BUILD_TYPE=Release -DLLVM_ENABLE_ASSERTIONS=ON -DLLVM_ENABLE_PROJECTS="llvm;clang" ../llvm
ninja

Alive2 is then configured against that tree with the TV component enabled:

cd ~/alive2/build
cmake -GNinja -DCMAKE_PREFIX_PATH=~/llvm/build -DBUILD_TV=1 -DCMAKE_BUILD_TYPE=Release ..
ninja

This is the single biggest reason people do not run Alive2: a full LLVM build with RTTI and exceptions is a heavy artifact to maintain in a CI image, and it must track the LLVM main branch rather than a pinned release.

Checking one pass, then grepping the logs for unsound

With the build in place, translation validation of one or more passes over an IR file is a single command:

~/alive/build/alive-tv -passes=instcombine foo.ll

The opt wrapper does the same work inside LLVM's own driver:

~/alive2/build/opt-alive-test.sh -passes=instcombine foo.ll

Scale that up to the LLVM unit tests for IR-level transformations and you get the command the project runs on the main LLVM branch every day:

~/llvm/build/bin/llvm-lit -s -Dopt=~/alive2/build/opt-alive.sh ~/llvm/llvm/test/Transforms

The results of that daily run are tracked on a page the documentation links to. For a local run, the documented way to find unsound transformations is a fixed string search over the log directory:

grep -Fr "(unsound)" ~/alive2/build/logs/

That grep is the operationally important command. A pass that appears in that log is a pass that the solver proved changes behaviour, and the counterexample it produces is the input that exposes it.

alivecc and alive++ as drop-in clang replacements

The Clang plugin tries to validate every IR-level transformation that clang performs. The long form loads the plugin shared object directly:

clang -O3 ~/llvm/clang/test/C/C99/n505.c -S -emit-llvm \
  -fpass-plugin=~/alive2/build/tv/tv.so \
  -Xclang -load -Xclang ~/alive2/build/tv/tv.so

The drivers alivecc and alive++ wrap the same thing:

~/alive2/build/alivecc -O3 -c ~/llvm/clang/test/C/C99/n505.c

~/alive2/build/alive++ -O3 -c ~/llvm/clang/test/Analysis/aggrinit-cfg-output.cpp

They detect when they are invoked as assembler or linker and then skip loading the plugin, and the documentation notes a side effect: some projects cannot be built if command line options are given manually to Alive2, for example through -DCMAKE_C_FLAGS=..., so the drivers mirror the plugin interface through environment variables such as ALIVECC_PARALLEL_UNRESTRICTED, ALIVECC_PARALLEL_FIFO, ALIVECC_SMT_TO and ALIVECC_SUBPROCESS_TIMEOUT. Output volume is a real concern, and -mllvm -tv-quiet reduces it, with -mllvm -tv-report-dir placing result files in a chosen directory.

Inter-procedural transformations are explicitly out of scope

The limitation is stated in a warning section of the documentation, and it matters more than any of the build instructions. Alive2 does not support inter-procedural transformations, and it may produce spurious counterexamples when run with such passes. A pass that inlines across function boundaries, or that reasons about a call graph, is outside the model the translator implements, so the counterexample it reports may be an artifact of the abstraction rather than a real bug. This is the difference in approach between Alive2 and the alternative most compiler teams already have: LLVM's own lit unit test suite checks that a pass produces expected output for a given input, which is cheap, runs on every commit, and says nothing about inputs that were never written down. Alive2 asks a solver to cover the input space, which is why it is slow and why it needs a source build of LLVM, and also why it can find a miscompile that the test suite will never contain. The two are complementary, and a project that has lit configured already has half of the infrastructure Alive2 expects.

Maintained by a research lab, released under MIT

Alive2 is developed by a research group rather than by a vendor. The documentation thanks a list of sponsors, including Google, NLNet, Woven by Toyota and Matter Labs, and asks companies that have benefited to sponsor the research lab, which is a good indicator of who pays for the compute behind the daily LLVM run. The code is released under the MIT licence, and the repository carries a LICENSE file at the top level. Version tags show a regular release cadence in 2025, with v19.0 published on 2025-01-20, v20.0 on 2025-03-17 and v21.0 on 2025-08-12, and the last push was on 2026-10-13, so the tree is still moving even though the latest tagged release is older than the most recent commits. The MIT terms are permissive for commercial use and for modification, and since the project is a research tool sponsored by outside companies, using it inside a proprietary compiler pipeline is a licensing question that is straightforward on the face of the licence.

Editorial conclusion

Alive2 is worth the setup cost for compiler engineers and for anyone maintaining custom LLVM passes, because a refinement check finds unsound transformations that output comparison cannot. It is the wrong tool for whole-program or link-time optimisation, for proof of properties that are not expressible as a refinement, and for teams that cannot host Z3 and a source build of LLVM in CI. Before adopting it, run the lit command over the LLVM Transforms suite on your own checkout and check the unsound log with the documented grep, because the honest first result is how many of your existing passes are already flagged.

Frequently asked questions

Official sources

1. AliveToolkit/alive2 on GitHub
2. Issues
3. License: MIT
4. README
5. Releases