This page gives information on how to download Vampire. See Usage for how to use Vampire.

We encourage users to sign up to our Mailing List to receive updates about new releases and other news.


The binaries of the new Vampire can be downloaded and used under the terms of the Vampire License. All binaries are statically linked, which means that you should be able to run them out of the box.

Currently we're only providing binaries for Linux as this is the easy case. For other platforms (e.g. Mac), the easiest route is often to compile from source (see below). We can provide Mac binaries but these can be OS X version specific due to linking issues — please contact Giles Reger for any queries.

We will usually provide each version with and without Z3 included as Z3 adds a lot to the size of the binary and is only useful in certain contexts. To be precise, if you are not reasoning with theories or want to make use of the most efficient finite model builder, then you can select the no-Z3 version. If there is an historic version that does not appear here that you want for whatever reason then please contact us.


Please access the source via the GitHub repository. The source of the new Vampire is provided under the terms of the Vampire License.

The README file should contain the necessary information for building with GNU Make. To build with Z3 you will need a statically linked Z3 binary. If you have any bug reports or feature requests then please use the GitHub functionality for this.

Below are some links to (stable) releases and some experimental branches. If you are going to use Vampire in experiments then please only use one of these stable versions and make sure you refer to the version as this is the only way to guarantee reproducibility of your results.