Skip to content

The MERC Project

The goal of the MERC project is to provide a generic set of libraries and tools for (specification) language-agnostic model checking, written in the Rust language. The name is an acronym for "mCRL2 except Reliable & Concurrent", which should not be taken literally. Development of the merc project takes place on GitHub.

We aim to demonstrate efficient and correct implementations using (safe) Rust. The main focus is on clean interfaces to allow the libraries to be reused as well. The toolset supports and is tested on all major platforms: Linux, macOS and Windows.

Note

The first release v1.0 of MERC has been published in December 2025, and is available to download on the Github releases page. The corresponding crates have also been published on crates.io.

Overview

Various tools have been implemented so far:

  • merc-lts implement various (signature-based) bisimulation algorithms for labelled transition systems in the mCRL2 binary .lts format and the AUTomaton (or ALDEBARAN) .aut format.
  • merc-rewrite allows rewriting of Rewrite Engine Competition specifications (REC) using Sabre (Set Automaton Based Rewriting).
  • merc-vpg can be used to solve (variability) parity games in the PGSolver .pg format, and a slightly extended variability parity game .vpg format. Furthermore, it can generate variability parity games for model checking modal mu-calculus on LTSs.
  • merc-pbes can identify symmetries in paramerised boolean equation systems PBES, located in the tools/mcrl2 workspace.
  • merc-ltsgraph is a GUI tool to visualize LTSs, located in the tools/GUI workspace.

Various crates are also published on crates.io, see the crates directory for an overview.

Links

See the links on the left-hand navigation menu for easy access to the issue tracker, documentation and code coverage reports.