# spectacle

[![ci](https://github.com/awakesecurity/spectacle/actions/workflows/ci.yml/badge.svg)](https://github.com/awakesecurity/spectacle/actions/workflows/ci.yml)

`Language.Spectacle` defines an embedded language for writing formal specifications of software in the temporal logic of actions. Specifications written in spectacle can be model-checked and shown to either be correct with respect to temporal properties or refuted by a counterexample. Examples of specifications written in spectacle are provided under `test/integration`.