diff --git a/README.md b/README.md index 915813c..4d277c7 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # Spectacle -Spectacle logo + Spectacle is an interactive, web-based tool for exploring, visualizing, and sharing formal specifications written in the [TLA+ specification language](https://lamport.azurewebsites.net/tla/tla.html). The motivation is to have a better way to quickly interact with a formal specification and easily share results. For example, it provides a way to share protocol behaviors and counterexample traces in a convenient, portable, and repeatable manner.