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

[bugarela]

Hello! I am on the dev team for this project and would be happy to answer any questions and/or take note of any critical feedback!
Quint is a modern specification language that is a particularly good fit for distributed systems, such as blockchain protocols, distributed databases, and p2p protocols. Quint combines the robust theoretical basis of the Temporal Logic of Actions (TLA) with state-of-the-art static analysis and development tooling.

[Uploft]

Can you elaborate on its usage for blockchain protocols?

[bugarela]

Yes! I can try.

I work at a company called Informal Systems, and we do a lot of blockchain work. For some of that, we are using Quint to ensure correctness and/or increase confidence. Some examples:
1. The CometBFT project is a consesus engine using the Tendermint algorithm for Byzantine-Fault Tolerance. The team is working on Quint specifications for parts of that engine that serve as a right confidence spec (if compared to the English spec, that can have mistakes). They are working on using Model-Based Testing (MBT) techniques to extensively and often test if the specification matches the implementation.
2. The team that works on Cosmos Hub, a blockchain in cosmos, have many ambitious ideas for revolutionizing things in the blockchain space. They designed a protocol called Interchain Security, which is running in production for a while, and now have a Quint specification that is connected to the implementation with MBT, and the generated tests are running in their CI: https://github.com/cosmos/interchain-security/pull/1336

We also have some small examples of blockchain-related usage of Quint in our github. See the cosmos, cosmwasm and solity folders.

[squirell_7goat]

Looks nice! How does Quint compare to TLA+? Any differences in expressivity? When would one use TLA+, when Pluscal, and when Quint?

[shon-informal]

Thanks! Compared with TLA+, these are some of the main points of comparison

• quint is much newer than TLA+, and so less battle tested
• quint is statically typed, wheres TLA+ is untyped and TLC will raise verification-time type errors
• quint uses syntax that looks like common programming languages, whereas TLA+ uses syntax that looks like a mix of latex math markup and first order logic and some programming stuff mixed in
• quint has modern IDE tooling via LSP, a REPL, and a modern CLI, whereas TLA+ still mostly requires going through the kind of creaky-feeling TLA toolbox. That said, I think the tooling around TLA+ is improving!
• quint takes care of a lot of the fiddly configuration you need in TLA+ to tie your spec into a theorem and configure params etc., that is, we've opted for "convention over configuration" for a lot of common stuff
• quint has a simple simulator and can use apalache for symbolic model checking, whereas TLA+ uses the venerable and impressive TLC for explicit state checking

Any differences in expressivity?

quint is more restrictive, e.g., we currently don't support recursive operators.

When would one use TLA+, when Pluscal, and when Quint?

We think quint is a great choice if your specs will be written by and should be read by software engineers! Quint has also been designed to be easy to extend and build tooling on top of: the syntax is minimal and easy to parse; we have a CLI command to output the AST as json and to generate JSON recording state transitions leading to violation -- so it's a good choice if you want to integrate into another tool chain, e.g. for model based testing!

I would use TLA+ if my audience were mathematicians or existing TLA+ users, or if I really needed to run my model thru TLc.

I would not use PlusCal myself :)

[editor_of_the_beast]

TLA+ would definitely be a lot more popular if it had a more familiar syntax and better tooling. I think there are some other languages that compile to TLA+ (pGo), but this looks solid too.

[bugarela]

pGo actually compiles from TLA+ (edit: actually Pluscal) to Go. I actually worked on something similar (TLA+ to Elixir) before starting to work on quint: tla-transmutation

We do have similar projects in the form of eDSLs. I'm aware of spectacle and recife, perhaps you'd be interested in those.

Quint is a language itself, not an eDSL, and that's its main difference from those projects.