A model checker for implementing distributed systems.

Concuerror is a stateless model checking tool for Erlang programs.

A Modern Probabilistic Model Checker

The Git repository for the mCRL2 toolset.

The Eldarica model checker

A model checker for infinite-state systems.

The LTSmin model checking toolset

Linear-time Temporal Logic guided Greybox Fuzzing (ICSE'22)

Experimental model checker for testing concurrent algorithms

SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).

IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.

Analytic tableau based minimal model generator, model checker and theorem prover for first-order logic with modal extensions

A toolbox for dealing with formal models from construction to analysis based on the JANI-model interchange format.

Intrepyd Model Checker

yet another model checker

Fully verified model checker for realtime systems

An on-the-fly, multi-threaded ATL model checker on concurrent game structures

An efficient Petri net model checker using Hierarchical Set Decision Diagrams.

A bounded model checker for an IMP-style imperative language.