Latest Release

Details of the ProB Licence can be found here. Note: please use the provided start scripts ( or StartProBWin.bat) to start ProB.

ProB is free to use and open source; commercial support is provided by the spin-off company Formal Mind. In particular, Formal Mind can also provide access to the validation report for using ProB as a tool of class T2 or T3 within the European norm EN50128.

Platform Release Date Download Dependencies
Linux 29. August 2014 Tarball (32bit),
Tarball (64bit)
Java Runtime Environment (5.0 or newer), Tcl/Tk 8.5
Windows 29. August 2014 Zipfile (with probcli) Tcl/Tk 8.5 for Windows,

Java Runtime Environment (5.0 or newer), Windows Installation Instructions

Mac OS X, Snow Leopard, Intel (64-bit) 29. August 2014 Tarball (with probcli) Tcl/TK 8.5 (do not use version, use 8.5.11 or use at least 8.5.13)

Graphviz for Mac OS X

Note: for Mac OS you may have to install the ActiveTcl version of Tcl/Tk as indicated above (the distribution provided by Apple is typically broken). On Linux you can typically install Tcl/Tk using sudo apt-get install tcl8.5 tk8.5.

Prior Versions

Prior Versions of ProB going back to 1.3.1 are still are available for download here.. If you are interested in still earlier releases, please have a look at the Download directory.


Please note that Tcl/Tk 8.6 is not yet generally supported by SICStus Prolog. There is a version of ProB available for Tcl/Tk 8.6 on Mac OS X Lion. Also note that on Mac OS X you may have to reinstall Tcl/Tk using one of the links given above (because the Tcl/Tk provided by Apple crashes after opening a file using the standard file selection dialog; however, even the version of Active Tcl/Tk on Mac seem quite unreliable and prone to crashing; for example version 8.5.12 has a serious bug related to copying text, see also here; you can use the older version instead). This issue seems to have been fixed in version 8.5.13. On Snow Leopard (Mac OS X 10.6.x) you have to install Tcl/Tk as indicated above for ProB 1.3.3.

Starting with ProB 1.3.5 you can now use ProB with Tcl/Tk 8.5 on Windows. If you have the older version of Tcl/Tk 8.4 you have to install the newer one 8.5 (you should be able to also keep the older version). For Windows we recommend installing ActiveTcl-8.5 (the win32-ix86-threaded version). Note: On Windows 64 bit machines, you have to install the 32 bit Tcl/Tk 8.5 version!

On Linux you can typically install Tcl/Tk using sudo apt-get install tcl8.5 tk8.5. On Linux OpenSuse (12.3) you may have to perform the following for ProB to work:

ln -s /usr/lib/ /usr/lib/
ln -s /usr/lib/ /usr/lib/

Tklib for ProB 1.3.4

ProB 1.3.4 requires the text module from tklib. This should come pre-installed on Mac and often on Windows as well (see below). On Linux you need to install tklib. On Ubuntu just type sudo apt-get install tklib. If you used the Active Tcl distribution, you need to type

sudo /opt/ActiveTcl-8.5/bin/teacup install tklib85

on Linux. On Windows, ActiveTcl-8.5 installs an additional tool "Teacup", with which you can install Tcl/Tk library extensions like tcllib and tklib. To use the latest Tcl/Tk version of ProB you may have to install tklib. This library can be installed on Windows with Teacup by typing

teacup install tklib85

into the Command Prompt, when you are logged in as an administrator.

Nightly Build

You can download our nightly integration build from here. The latest nightly build requires a Java Runtime Environment (JRE) 7 or newer for the B parser. Note: on some systems (Mountain Lion OS X) you may have to install the Oracle JDK (and not just the JRE) so that Java 7 or 8 becomes available to the command-line tools (type java -version to check which version is used by default for command-line tools). In case you have trouble starting the Java parser you can now set the JAVA_PATH preference to point to the java tool (or java.exe on Windows). The 64-Bit Windows version of ProB Tcl/Tk now requires the 64-bit version of Tcl/Tk. If you wish to use Windows XP you need the service pack SP3 installed.

Automatically generated test coverage reports are also available.

Nightly builds of ProB for Rodin 3 can be obtained from within Rodin by using the update site

Nightly builds of ProB for Rodin 2 can be obtained from within Rodin by using the update site

Nightly builds of ProB 2 (experimental) for Rodin 3 can be obtained from within Rodin using the update site

Timed-CSP Simulator

A version of ProB with built-in support for timed CSP developed by Swansea University (UK) is available on here:


You can download the latest sourcecode snapshot from:

Short Release History

29/8/2014 ProB 1.4.1, a small bugfix-only release is available. For a list of new features in 1.4.0 see below.

18/8/2014 ProB 1.4.0 is available. Highlights: CLP(FD)-based constraint solver enabled by default, kernel can handle more operations symbolically, integration of the TLC model checker, bug fixes and performance improvements.

4/3/2013 ProB 1.3.6 is available. Highlights: improved constraint propagation for division, modulo, intervals, model checking progress bar, performance improvements, improved Kodkod backend and use within REPL, and many more.

8/10/2012 ProB 1.3.5 is available. Highlights: support for external and recursive functions, optional Kodkod backend, TLA+ support, performance improvements, pragmas, units inference, and many more.

30/03/2012 A first prototype of an online ProB Logic Calculator is available.

21/11/2011 ProB 1.3.4 is available. Highlights: Evaluation View and Eval window, CSP assertion checking, improved editor, 64-bit version for Mac and Linux, performance improvements, and many more.

10/02/2011 ProB 1.3.3 and ProB for Rodin 2.3 is available. Highlights: improved performance, constrained-based deadlock checking, record detection, and many more.

07/30/2010 ProB 1.3.2 is available. Highlights: improved performance, constraint solving over integers (enable in Advanced Preferences), much improved Z support, and many more.

12/07/2009 ProB 1.3.1 is available. Highlights: new data-structure for large sets and relations (see FM 2009), multi-level validation for Event-B, improved constraint propagation for boolean connectives, and many more.

03/20/2009 ProB 1.3.0 is available for download. Highlights: New parser and integrated typechecker, install as AtelierB plugin, improved kernel with support for large sets/relations, improved CSP support, faster LTL model checker, Undo/Redo in text editor, graphical formula viewer, user definable custom animations with gifs.