maude2lean [RuRi22] is a translator of specifications in Rewriting Logic [Mes92] to the Calculus of Inductive Constructions [PfPa89]. Given a module in the Maude specification language, the tool produces a program for the Lean proof assistant where theorems about the original specification can be proven. Terms, sort membership, equational, and rewriting relations are inductively defined, which enables reasoning about both positive and negative properties of the original models.
Its syntax is
$ maude2lean <Maude source or configuration file>+ [-o <output file>]
where the first argument is the path of either a Maude file or a JSON, YAML, TOML, or Python dictionary specification to customize the translation. The available options are documented in this JSON schema, which can be obtained by invoking maude2lean --dump schema, and most of them can also be passed as command-line arguments (use --help to obtain a list of them). Examples are available in the test directory of the repository.
Moreover, the releases page also includes an executable bundlepip install https://github.com/fadoss/maude2lean/releases/download/latest/maude2lean-1.2.2-py3-none-any.whl
maude2lean to be run as a program in Unix-like systems or invoked as python maude2lean. If using the bundle, the maude Python library should be explicitly installed with pip install maude or equivalent methods.