salt
quint
| salt | quint | |
|---|---|---|
| 2 | 6 | |
| 190 | 589 | |
| 0.0% | 4.4% | |
| 0.0 | 9.8 | |
| over 4 years ago | 9 days ago | |
| Clojure | TypeScript | |
| MIT License | Apache License 2.0 |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
salt
- Quint: A specification language based on the temporal logic of actions (TLA)
-
TLA+ Action Properties
We're seeing more people create DSLs that compile to TLA+. For example, salt lets you write TLA+ specs in Clojure: https://github.com/Viasat/salt
quint
-
Holiday protocols: secret Santa with Quint
Hi! I wrote a blogpost exploring a formal specification in Quint [1] for the secret santa game, and verifying some of its properties with Apalache [2].
Hope you enjoy it, and any feedback is welcome. Happy holidays!
[1]: https://github.com/informalsystems/quint
-
Quint: A specification language based on the temporal logic of actions (TLA)
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 :)
- Quint – a new language based on TLA+ with modern syntax and developer tooling
-
Programming Languages Going Above and Beyond
It's still in pretty early development, but you may be interested in https://github.com/informalsystems/quint
> It combines the robust theoretical basis of the Temporal Logic of Actions (TLA) with state-of-the-art static analysis and development tooling.
And it is typed ;)
What are some alternatives?
timewinder - Temporal Logic of Actions in Rust via Starlark
evm-dafny - An EVM interpreter in Dafny
recife - A Clojure model checker (using the TLA+/TLC engine)
TypeScript - TypeScript is a superset of JavaScript that compiles to clean JavaScript output.