Quint: A specification language based on the temporal logic of actions (TLA)

• quint

  6 584 9.8 TypeScript

  An executable specification language with delightful tooling based on the temporal logic of actions (TLA) (by informalsystems)

  

I can sympathize! We are aiming to maintain most of the expressive power of TLA+ -- ideally everything you need for a concise, high-high level specification, that can be simulated and/or verified -- but with surface syntax that is more approachable coming from a programming background. If you're interested in seeing how it maps to TLA+, you can find much of that in this document: https://github.com/informalsystems/quint/blob/main/doc/lang....

We still have lots of ways to improve, and -- we think -- lots of opportunities to improve our interop and complementary qualities in relation to TLA+ and TLC. But we have found the tools in their current state useful enough to be worth sharing :)

• salt

  2 190 0.0 Clojure
  

• WorkOS

  workos.com sponsored

  The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

  

• recife

  4 130 4.5 Clojure

  A Clojure model checker (using the TLA+/TLC engine)

I didn't take a very deep look yet, but this might be similar to https://github.com/pfeodrippe/recife

• tlaplus

  38 2,208 9.1 Java

  TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

  

```

https://github.com/tlaplus/tlaplus/blob/master/tlatools/org....

In any case, our whole team thinks TLA is great, and we're happy people like you and Ron find it so useful and insightful. We also think it is a very insightful.

Suggest a related project