• NuITP - An Inductive Theorem Prover for Maude Specifications
• The Maude Formal Environment - Environment that integrates the Church-Rosser checker, the coherence checker, and the termination tool
• The Maude LTLR Model Checker
• The Maude LTL Logical Model Checker
• umaudemc - A unified tool to check Maude specifications using external qualitative, probabilistic, and stochastical model checkers
• PVeStA - A Parallel Statistical Model Checking and Quantitative Analysis Tool
• MultiVeStA - A Distributed Statistical Model Checking for Discrete Event Simulators
• Inductive Theorem Prover (ITP)
• Sufficient Completeness Checker
• Maude-NPA - Maude-NRL Protocol Analyzer
• Equality Enrichments for Order-Sorted Maude Theories
• createCINNI - Automatic Generation of CINNI Instances for the Maude System

Extensions of Maude

• Real-Time Maude
• Maude Strategy Language
• ACUOS. Order-Sorted Modular ACU (Least General) Generalization System

Tools to assist in the development of Maude specifications

• Declarative Debugger
• The Anima tool - Stepwise inspection of Maude computations
• ABETS. Assertion-based, Maude dynamic analyzer
• iJulienne. Backward Trace Slicer

Tools for other formalisms and logics developed on Maude

• Pathway Logic Assistant - Modeling of biological entities and processes
• OCC - An Open Calculus of Constructions
• CCS and LOTOS

Semantics and verification of programming languages

• Maude MSOS tool
• The K framework and Matching logic - Rewrite-based framework for the definition of formal operational semantics of programming languages
• Java+ITP - A tool to prove Java properties

Web and Model-driven engineering (UML, OCL, MOF, model transformation, ...)

• MR-SynchAADL - Multirate Synchronous AADL and the MR-SynchAADL tool
• MOMENT - A framework for model management
• e-Motions - Visual definition of domain-specific modeling languages
• mOdCL - UML/OCL specification, with static and dynamic evaluation of OCL expressions

Other tools

• Python's library Language bindings to use Maude from other programming languages like Python
• Maude MSOS tool Execution environment for Modular Structural Operational Semantics (MSOS) specifications