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 v1.1 of merc has been published in January 2026, and is available to download on the Github releases page. The corresponding crates have also been published on crates.io. This release was mostly to force a Zenodo upload, and no important changes were made.

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. 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-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.

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

Links

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