Different tools are available (or currently in development/testing) for specifying and verifying CLIMB models:

• (ongoing) DEClipse is an Eclipse plug-in for designing extended DecSerFlow diagrams; designed specifications are automatically mapped onto CLIMB models by means of a model-transformation process;
• (available) SCIFF/g-SCIFF proof procedures are the operational counterparts used to verify and reason upon SCIFF specifications, used to formalize CLIMB models;
• (available) SOCS-SI is a JAVA-based tool which exploits the SCIFF proof-procedure to perform the run-time verification task;
• (under testing) SCIFF-Checker is a ProM plug-in which exploits Prolog to verify conformance a-posteriori and classify a set of MXML execution traces w.r.t. a set of business rules (specified following the CLIMB paradigm);
• (under testing) DecMiner is a ProM plug-in which relies on Inductive Logic Programming techniques to mine a declarative CLIMB specification starting from a set of MXML execution traces.