Announcing Spectacle - A language for Writing Checking Formal Specifications in Haskell

We are announcing the release of a formal specification language in Haskell intended to replace TLA+: https://awakesecurity.com/blog/spectacle-a-language-for-writing-and-checking-formal-specifications-in-haskell.

16 Likes

Are there any papers you used to guide your implementation? Or did you just reference the TLA+ codebase? Is your model checker based strictly off of TLC?

2 Likes