Maude 2 has been released, and is available for download. The new release has many new features, including more efficient algorithms for rewriting, new commands for fair rewriting, new pre-defined modules, an LTL model checker, a META-LEVEL supporting reflective computation, and parametrised theories and view. The content below refers to Maude 1 and is available primarily for archival purposes. Also, once the tools below have been ported to Maude 2, the content would be removed.

Maude Documentation

Maude Manual

Maude Tutorial

Maude Applications

A Set of Proving Tools for Maude Specifications	Mobile Maude
Maude Case Studies

Obtaining and Using Maude

Download Maude	Maude License