This page gives a few tips to download, install and/or configure external provers.

Automatic provers

Simplify (version 1.5.4): is available under binary form for various architectures from this page or directly here
Alt-Ergo (version 0.8): is available under binary form for Unix, or under source form to be compiled using the OCaml compiler, from this page. A Microsoft Windows installer (for version 0.7.3) is also available on this page
Z3 (version 1.3): is available under binary form for Microsoft Windows from this page. Running this program under Unix is also possible via the wine layer: install z3 using the msiexec command and then run it using this script where you have to modify the full path to z3.exe
A binary version of Z3 for linux is also available from SMT-COMP-08 site. Call the binary executable
```
z3-bin
```
and use this wrapper
Yices (version 1.0.17): available under binary form for various platform from this page
CVC3: available under source form and as a Unix binary from this page
Gappa: available under source form at this page

Proof assistants