Quint Launch Event Follow-Up Q&A and Recap
Quint Launch Event: Follow-Up Q&A and Recap
We recently held our official launch event for Quint, and it was a fantastic experience! We were thrilled to see such a vibrant turnout and engage with so many enthusiastic community members. For those who couldn't make it, or for those who want a recap, here's a quick overview of what we covered. We also want to address some of the insightful questions raised during the Q&A session.
Event Recap#
I (Gabriela Moreira, Lead Developer of Quint) shared the journey of Quint this far, including its vision and the problems it aims to solve. Giuliano Losa (Senior Researcher, Stellar Development Foundation) and Julian Compagni Portis (Head of Exchange, Neutron) provided valuable insights into how formal methods and Quint are being used in industrial scenarios. We also had a live demo showcasing Quint's capabilities and announced the open-sourcing of Quint’s new Rust core. The demo is available on GitHub, including the Quint code and Quint commands I ran during the event.
Addressing Your Questions#
We received many excellent questions during the Q&A, and we want to ensure everyone gets the answers they need. Here are the questions and our responses:
On Using Quint Beyond Blockchain#
Q: Do you think it's a good idea to use Quint outside "classic" distributed systems (i.e. not blockchains, consensus etc, but something simpler like client-server)?
A: Quint is worth using when we need more confidence about a system. If we are already completely confident, it might be that Quint won’t add any value. If you are concerned that a complex sequence of events involving communication by several components may drive your system into a weird unwanted situation, then the Quint tools might help you to build confidence that such a dangerous sequence doesn’t exist. In the event, I mentioned Hillel Wayne’s rule of thumb for writing a spec: if it takes less than a week to implement it, it might not be worth writing a spec for it. I like to think in terms of confidence/insecurity. If I feel insecure about some part of the system, modeling it is valuable.
On Asynchronous Communication#
Q: Does Quint support asynchronous communication between the finite state machines? Like with buffers, for example?
A: All sorts of communication are supported, since Quint is general-purpose, but you have to implement it yourself. On our repository you will find examples for different kinds of communication patterns. Regarding the mentioned buffered communication, we usually abstract the communication in something like a global set of messages that all parties can access. As long as the abstraction follows the same assumptions as the real-world communication, they can be used to detect any issues. For example, if the messaging follows a “delivery at least once” model, we can use a set of messages where we don’t remove the message when consuming it, so behaviors where we consume the same message twice are allowed.
On Formal Methods Trends#
Q: What trends do you see emerging in the field of formal methods, and how does Quint fit into these trends?
A: Making formal methods more accessible is something that many people are pursuing, but there are different approaches. PlusCal was made on top of TLA+ to make it more like an imperative language, but it didn’t solve the syntax and the tooling issue, like Quint does.
Some projects aim to take away all of the “burden” from the user: they should not have to write any spec at all and still get the benefits of having a spec (or maybe, some LLM writes the spec for them). I believe that writing the spec is very valuable, and that we can make this experience rich by using a good language, good tools, and leveraging automation/LLMs for any remaining annoying parts. Quint is this tool that helps you think while you are creating or understanding a new system/algorithm/protocol, and our goal is to add more and more value to this process. It’s a matter of reducing cost and increasing value, but we don’t believe that the cost needs to be zero - it is worth writing specs, and Quint makes it even more worthwhile.
On Language Integrations#
Q: Will there be more integrations with languages? Like Haskell?
A: We believe that the best way to bridge the gap between specification and implementation currently is Model-Based Testing. Writing the “glue code” to execute Quint traces in any language is quite straightforward, but we can make libraries to help with that in different languages. Currently, we have a library to parse traces produced by Quint in Rust (see the itf crate), and here’s an example of how it can be used. A good next target for a lib like that is Python, as recently I have seen a lot of value in graphic visualization of traces, and Python has great tooling for rendering this type of graphics. I’d love to write one for Haskell if people start writing Quint specs for systems in Haskell 😀.
On Counterexample Checking#
Q: How does Quint check for the counterexample? Is it a bounded checking?
A: When running quint verify, Quint uses Apalache, which performs bounded model checking with the Z3 SMT solver (read more here). For unbounded model checking, you can use TLC. We are working on having a seamless integration soon (so you can run quint verify --backend=tlc), but for now, there is a shell script to transpile Quint into TLA+ and then call TLC on in with the proper parameters. Note that by “bounded” I mean the length of the execution. While Apalache only checks executions up to a bounded length, it is able to reason about, e.g., unbounded integer variables very efficiently due to SMT. In contrast, TLC forces you to use bounded (small) integers, as it tries to enumerate all evaluations of these variables. So which model checker works better for you will depend on the type of your properties and the data types in your specification.
If you are asking specifically about how Apalache constructs the counterexample, it is a bit too much to explain here, but it basically constructs the SMT constraints in such a way that, if there is a valuation for the variables that satisfies the constraints, that valuation (the Z3 model) is the counterexample. You can read more about it in the Apalache paper at OOPSLA19.
On Code Generation#
Q: Can Quint specs be transpiled into target languages?
A: While theoretically possible, practical code generation from specs is challenging since specifications are more abstract than implementations. Model-Based Testing offers a more realistic approach — specifications guide test creation that validate implementation correctness against the spec.
On Model Checker Selection#
Q: Is Apalache + Z3 the sanctioned way to model-check, going forward?
A: Not only, we are integrating TLC and we consider making it the default backend, as its behavior is more predictable and understandable. Apalache and TLC are both great tools and one can out-perform the other in some classes of specifications, so I don’t see us choosing a favorite and sticking with it. You can read about the comparison here.
On Quint's Self-Verification#
Q: Is Quint itself formally verified by Quint?
A: No. Most model-checking tools are not verified, just like Apalache and TLC are not. The Quint tool itself is mostly a compiler, and verifying compilers is a tough task, usually done with proof assistants like Coq or Lean, which are a better fit at this level of the stack.
On Example Coverage#
Q: Are batteries included? I didn't find examples of several state machines communicating. Can this be included, as it's common when working with real models?
A: We are working on having some templates for the most common use-cases, and I’ll also (very soon) improve the documentation about examples to make sure we include examples that are hosted in stand-alone repositories, like Malachite and Mysticeti, which cover how you can model communication.
On Lean Integration#
Q: Do you plan to integrate it with Lean?
A: Well, my answer would have been “no”, but then I saw this post on X: https://x.com/ilyasergey/status/1912011803753894159
On Model-Based Testing with Rust#
Q: Can I use the Quint Rust library to test my actual implementation in Rust? Or do I need to translate the Quint spec into code and accept this translation risk?
A: You can use your existing code. You just need to write some “glue code” that reads the traces from Quint and calls the corresponding functions in your Rust code. See an example here.
On Community Platforms#
Q: Do you consider having Slack for better structure instead of Telegram?
A: We have a Zulip stream, which has the same structure as Slack. I like the structure, but we do have much more messages in Telegram. I’m happy to use whatever the community prefers.
On Built-in Types#
Q: Is there a plan to add more built-in types to Quint or should they be spells based on the existing primitives? For example the BoundedUInt?
A: The plan is that the spells become a standard library and eventually we have some package system. The philosophy is that anything that can be written in Quint (i.e. as a spell) doesn’t need to go into the built-ins, as that would just mean more maintenance work. From the user perspective, using the standard library should be as easy as using the built-ins (which is not the case at the moment).
On Type Systems#
Q: Does Quint have a type system?
A: Yes, it has. You are only required to annotate the types of state variables and constants (constants work as module parameters, not the same as Javascript constants you use all the time), which usually are just a handful of definitions. Everything else is inferred, but you can annotate it if you want. It also has an effect system that makes sure you stay in the right modes and don’t read/update variables where you are not supposed to.
On Rust Project Integration#
Q: What do I need to use Quint with my Rust project? (Can I do cargo quint init?) 😃
A: The language of your project only matters if you want to write Model-Based Tests. Before that, you need a Quint model, so you just start a Quint file from scratch - there’s no boilerplate, really. Once you have the model, you can write the “glue code” for the Model-Based Tests by using the itf library (for Rust), like in here.
On Learning Quint#
Q: What is the quickest way to learn Quint?
A: I thought a lot about Quint’s website structure and it encapsulates what I think it’s best for learning. I’d start there and then try to write your own spec for something. It can be for a fun game you like, or something like the protocol to follow to clean your cat’s litter box and make sure any cat issues are detected in less than 12 hours. During this process, you can ask questions on Telegram, Zulip or GitHub. Once you have something, you can open a PR to add your example to Quint’s examples folder, and I’ll review your PR and give you feedback. This way, you contribute to the next people learning Quint, and get my (and maybe some more) pair of eyes on your model.
We're excited to see what you build with Quint. If you haven’t started yet, follow our Getting Started tutorial and tell us what your experience has been on the Telegram chat! If you want some help from our specialized team to get started, you can find us at audits@informal.systems or https://informal.systems/security-and-engineering.