Spot: a platform for LTL and ω-automata manipulation

Table of Contents

Spot is a C++14 library for LTL, ω-automata manipulation and model checking. It has the following notable features:

Latest version

The latest version is 2.8.1 and was released on 2019-07-18. Please see the download and installation instructions.


Try Spot On-line

  • Our on-line translator provides a convenient way to translate LTL or PSL formulas into automata, or to study/compare formulas.
  • spot-sandbox is a Jupyter notebook with a complete installation of Spot that allows you to try the command-line tools (using a shell interface) as well as the Python bindings (in an IPython notebook).


Spot is distributed under a GNU GPL v3 license.

A consequence is that if you distribute a tool built using Spot, you must make the source code of that tool available as well, under a compatible license.

Staying in touch

spot-announce@lrde.epita.fr is an extremely low-traffic and read-only mailing list for release announcements. If you want to stay informed about future releases of Spot, we invite you to subscribe.

spot@lrde.epita.fr is a list for general discussions and questions about Spot. Subscribe here if you want to join, but feel free to send in any question (in English) or bug report without subscribing.


Our citing page has a list of papers you could cite if you need to reference Spot in an academic publication.