www.prismmodelchecker.org

Download PRISM

PRISM is free and open source software, distributed under the GNU General Public License (GPL), version 2.

Download:

PRISM should run on 32/64-bit versions of all major operating systems.

We distribute various pre-built binaries:

For non-Windows platforms, it is usually easy to build from source code:

Older versions are available on the GitHub releases page.

Latest version: 4.9

The current version of PRISM is 4.9 (first released 11 August 2025).

The main changes since the last major release (4.8.1) are listed below. See the CHANGELOG for full details.

  • Explicit engine improvements
    • support for actions and transition rewards in Markov chains
  • Export functionality
    • new exports: exact/parametric models, Markov chain actions, DRN (Storm) output
    • extended functionality for -exportmodel switches
  • Model import functionality (from explicit files)
    • new imports: exact models, LTSs
    • efficiency improvements
  • Minor modelling language updates
    • new power operator a^b, equivalent to pow(a,b)
    • fix: implication (=>) is right-associative
  • New/improved functionality
    • simplified/updated LTL-to-automaton scripts
    • exact model checking supported from GUI
    • optimal strategy synthesis for Rmax=? [ C ] (explicit)
  • Bugfixes and multiple significant code-level changes

Installation

See the installation instructions, included in the PRISM manual (which is also distributed with the tool).

If you have any problems, first check the list of common problems and questions.

If you are still stuck, post a message in the forum.

Once you have installed PRISM, you might want to look at:

Downloads