MaudeSE extends Maude with SMT solving. It supports satisfiability checks and symbolic search, with Python connectors for Z3, Yices2, and cvc5. You can also write a connector for another solver.
The current release supports Python 3.10–3.14 on macOS and Linux. First, install the base MaudeSE package from PyPI:
python3 -m pip install maude-seThe base package includes the solver connectors, but not a solver. Install Z3 in the same Python environment:
maude-se-installer install z3Check that Z3 is available to MaudeSE:
maude-se-installer doctor z3The example below requires a checkout of this repository; the PyPI package
does not include the examples/ directory. From the repository root, open
an included example:
maude-se examples/smt-check-ex.maude -s z3At the MaudeSE> prompt, enter:
check in SIMPLE : X:Integer > 4 using QF_LRA .
The result should be sat.
For other solvers, installation alternatives, and local builds, see INSTALL.md. The website installation guide also covers release downloads and native solver plugins.
The MaudeSE documentation covers commands, examples, and the connector interface.