CafeOBJ is a most advanced formal specification language which inherits many advanced features (e.g. flexible mix-fix syntax, powerful and clear typing system with ordered sorts, parameteric modules and views for instantiating the parameters, and module expressions, etc.) from OBJ (or more exactly OBJ3) algebraic specification language.

CafeOBJ is 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.

CafeOBJ has state-of-art rigorous logical semantics based on institutions. The CafeOBJ cube shows the structure of the various logics underlying the combination of the various paradigms implemented by the language. Proof scores in CafeOBJ are also based on institution based rigorous semantics, and can be constructed using a complete set of proof rules.


  • CafeOBJ 1.5.7 released - We have released a new version of CafeOBJ, which incorporates mostly fixes for CITP as well as updates to work with newer versions of SBCL. Please see the for the source release, binary packages, and installation instructions. For the moment Windows builds are only available based on Allegro CL due to incompatibilities between Windows SBCL […]
  • Book published: Introduction to programming for model description and validation (in Japanese) - Prof. Futatsugi’s book Introduction to programming for model description and validation (モデルの記述と検証のためのプログラミング入門) has been published this week and will be available from various outlets and online. The web site of the book provides access to downloadable versions of the code given in the book.
  • CafeOBJ Tutorial at ICFEM 2016 - Lecturer FUTATSUGI, Kokichi OGATA, Kazuhiro JAIST, Japan Place/Time 2016-11-15 10:00-17:30, TKP Ichigaya Conference Center, Tokyo, Japan. Web site Please see this page for details. Abstract CafeOBJ is a most advanced algebraic formal specification language system with rewriting/reduction engine which can be used for interactive verification. Proof scores are scripts for verifications and provide versatile ways […]
  • ESSLLI 2016 Course: Algebraic Specification and Verification with CafeOBJ - During this year’s ESSLLI (European Summer School in Logic, Language and Information) I was teaching a course on Algebraic Specification and Verification with CafeOBJ. Please this post for the course materials like slides and code example. Abstract Ensuring correctness of complex systems like computer programs or communication protocols is gaining ever increasing importance. For correctness […]
  • CafeOBJ 1.5.5 released - We have released a new version of CafeOBJ, which incorporates besides other fixes the following changes: Enhancemets of a family of Bool term inspector commands: binspect [ in : <Modexpr> ] <bool-term> . converts given <bool-term> into abstracted xor-and normal form bshow [ tree | grind ] shows abstracted Bool term bresolve [ <num1> [ […]