A model checker for implementing distributed systems.

• UpdatedOct 7, 2024
• Rust

Concuerror is a stateless model checking tool for Erlang programs.

• UpdatedMar 22, 2025
• Erlang

A Modern Probabilistic Model Checker

• UpdatedMar 27, 2025
• C++

The Git repository for the mCRL2 toolset.

• UpdatedMar 26, 2025
• C++

The Eldarica model checker

• UpdatedMar 20, 2025
• Scala

A model checker for infinite-state systems.

• UpdatedDec 20, 2024
• C++

The LTSmin model checking toolset

• UpdatedOct 31, 2024
• C

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

• UpdatedApr 1, 2024
• C

Experimental model checker for testing concurrent algorithms

• UpdatedDec 17, 2024
• OCaml

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

• UpdatedMar 19, 2025
• OCaml

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

• UpdatedNov 14, 2023
• Python

yet another model checker

• UpdatedMar 22, 2025
• C++

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

• UpdatedNov 28, 2024
• Python

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

• UpdatedAug 3, 2024
• PDDL

Intrepyd Model Checker

• UpdatedNov 5, 2021
• Python

Fully verified model checker for realtime systems

• UpdatedSep 2, 2022
• Isabelle

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

• UpdatedFeb 1, 2024
• Rust

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

• UpdatedFeb 20, 2025
• C++

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

• UpdatedFeb 23, 2019
• Rust

• UpdatedJan 2, 2020
• Scala