quint VS recife

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

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 :)

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 ;)

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

You can open an issue with the code, https://github.com/pfeodrippe/recife.

You betcha o/ https://github.com/pfeodrippe/recife/tree/master/test

Recife (https://github.com/pfeodrippe/recife) is a Clojure library that leverages TLC, a model checker widely used (in a niche) to check formal specifications and, with a bit of thinking, to test your implementation according to this specification.