A language for writing formal (i.e. mathematical) specifications of models for wide varieties of software and systems, and verifying properties of them.
CafeOBJ implements equational logic by rewriting and can be used as a powerful interactive theorem proving system. Specifiers can write proof scores also in CafeOBJ and doing proofs by executing the proof scores.