Storm is a tool for the analysis of systems involving random or probabilistic phenomena. Given an input model and a quantitative specification, it can determine whether the input model conforms to the specification. It has been designed with performance and modularity in mind.

Modeling formalisms

Storm is built around discrete- and continuous-time Markov models:
  • Discrete-time Markov Chains
  • Markov Decision Processes
  • Continuous-time Markov Chains
  • Markov Automata
  • Parametric Markov Models
  • Partially Observable Markov Models

Input languages

Storm supports several types of input:
  • JANI
  • GSPNs
  • DFTs
  • explicit


Supported model checking queries include
  • Reachability and Reach-Avoid Probabilities
  • PCTL, CSL, and LTL Specifications
  • Expected Accumulated Rewards
  • Long-run Average Rewards
  • Conditional Probabilities
  • Multi-objective Analysis


13 June 2023

New version 1.8.0

We are happy to announce the next stable releases of Storm and stormpy in version 1.8.0.

21 March 2023

SAFEST tool for fault tree analysis based on Storm

The SAFEST tool for modeling and analysing static and dynamic fault trees has been released. SAFEST is based on the Storm model checker.

02 August 2022

Storm featured in UAI Tutorial

Storm has recently been featured in a tutorial on probabilistic verification at UAI 2022.