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 is just a backronym for its name. 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.

Announcement

The release v2.0 of merc has been published in June 2026, and is available to download on the Github releases page. The corresponding crates have also been published on crates.io. This release comes with a lot of general improvements, and the addition of the merc-lps tool for exploring linear process specifications.

Overview

Various tools have been implemented so far:

  • merc-lts implement various bisimulation algorithms for labelled transition systems in the mCRL2 binary .lts format and the AUTomaton (or ALDEBARAN) .aut format. Using CADP it can also read and write the .bcg 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-lps can explore linear process specifications using symbolic exploration techniques, it is located in the tools/mcrl2 workspace.
  • merc-pbes can identify symmetries in parameterised 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.
  • merc-sym can explore a symbolic state space given in Sylvan's binary .ldd format, or the mCRL2 symbolic binary .sym format. It can also compute orderings using kahypar using the MINCE algorithm, which also requires the kahypar tool to be available.

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

Slint

The GUI tools are implemented using Slint, a Rust-based GUI toolkit.

Made with Slint

Links

See the links section of the navigation bar for various useful links related to the merc project.