Spot: a platform for LTL and ω-automata manipulation

Table of Contents

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

Latest version

The latest version is 2.12 and was released on 2024-05-14. 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.

One consequence is that any work based on Spot is covered by that license as well. For instance if you distribute a tool that links with Spot, you should distribute the source code of that tool as well.

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.