Polar implements a novel static analysis technique to derive higher moments for program variables for a large class of probabilistic loops with potentially uncountable state spaces.
Mora is an automated tool for generating invariants of probabilistic programs. Inputs to Mora are so-called Prob-solvable loops, that is probabilistic programs with polynomial assignments over random variables and parametrized distributions.
HyperPAYNT is a synthesis tool for probabilistic hyperproperties.
Amber is an academic prototype to decide the probabilistic termination behavior of Prob-solvable loops.