Frequently Asked Questions

Main similarities:

• It is possible to get fuzz tests out of Quint
• Both require some sort of property to check

Main differences:

• Writing a Quint model is very different from setting up a fuzzer
• Fuzzers can fail to find rare bugs, while quint verify will always find issues if there are any.

Adding a new language to an ecosystem often finds resistance, and you might be tempted to use Python or Typescript or whatever you already know. It is possible to write a reference implementation in some language and then implement some simulation for it, looking for bugs. Here are some reasons to use Quint instead of that:

• Quint is a specification language. It is more restrictive so you are forced to write things in a way that's possible to formally verify your model. It is very hard to formally verifying arbitrary code in programming languages.
• Quint already has a simulator! We are on the path to making it the best simulator ever. While it is probably not there yet, it's likely better than something you'll hack in a couple of weeks. If your project's focus is not writing a simulator, you might want to use ours.

Yes, and you probably want to use Literate Specifications to interleave Quint blocks with natural language descriptions.

While Markdown accepts all sorts of errors, Quint specs are executable. You get name resolution and type checking for your spec, even if you don't want to run it. This means you'll get rid of ambiguity, references to names that are never defined and incompatible interfaces - which are the biggest problems in common specifications.

Quint is based on TLA+ and uses the same underlying logic (Temporal Logic of Actions), so it is very similar to TLA+ in terms of where it is useful. The main differences between Quint and TLA+ are:

1. Quint has programming-style syntax, while TLA+ uses math/latex symbols.
2. Quint has more static analysis, such as type checking and different modes (pure def, action, etc), while TLA+ has no native support for types nor explicit distinction between the modes (or levels, as they are called in TLA+'s documentation).
3. Quint tooling is more similar to what we have for programming languages: near-instant feedback as you type the code, CLI-first executable, an easy way to obtain one execution of your spec in the terminal, a REPL, located error messages, etc. These are all not currently available in TLA+, or available with significant constraints.
4. Quint won't let you write many things that are allowed in TLA+. TLA+ has a proof system (TLAPS), while Quint doesn't. Therefore, it is possible to write more advanced formulas in TLA+ than in Quint, even ones that are not supported by the existing model checkers, and then prove them using the proof system. Quint restricts you to a fragment of TLA with the intention of preventing unintentional usage of operators that lead to complicated behaviors that are hard to debug and understand. Our understanding is that anything outside of Quint's fragment is only written by people with a strong mathematical mindset, and those people will probably appreciate TLA+'s mathematical syntax much better.
5. Quint has the concept of a run to define executions to be used as tests. There is no corresponding feature in TLA+.
6. TLA+ has model values and symmetry sets, which are not available in Quint at this time.

On a less concrete note, TLA+ supporters will often say that the mathematical syntax helps to put people in the correct mindset of formal specification, while Quint as a project hopes to teach people this mindset without a big syntax and tool disruption.

No. Although both Quint and PlusCal have the goal of making TLA+ more approachable to engineers, the strategies are very different. PlusCal uses the same tooling and similar syntax to TLA+, but introduces imperative constructs (while TLA+ is fully declarative). Quint, on the other hand, introduces new tooling and syntax, but keeps the declarative aspect.

It would be possible to add the imperative constructs from PlusCal to Quint. We currently don't have a lot of clarity on how useful that would be.

We experienced situations where the expressiveness constraints imposed by PlusCal were a problem for some of our systems, while Quint has always been enough.

Alloy is very focused on sets, and is good for specifying requirements and data structures, while Quint is natively time oriented, fitting really well with concurrent and distributed systems. As everything in Alloy is a set/relation, it requires a quite abstract and specific way of modeling.

While Alloy 6 added temporal operators, for the longest time, handling the passage of time required complex workarounds, and therefore having the language be used mostly for other things.

Alloy verification can be faster than Quint for specifications without time, as it can use SAT solving instead of SMT solving, and the tooling looks very different, with Alloy Analyzer being very visual.

Coq, Isabelle and Lean are proof assistants. They will assist you to write a proof, but you still have to do most of the work. Quint uses model checking, where you only need to define the model and the properties, and the verification process is fully automated. Learning and mastering how to use a proof assistant is much harder (usually taking years) than learning and mastering Quint.

Proof assistants require you to write deductive proofs, while model checkers (as in Quint), use an inductive approach, exploring all reachable states in a model. Proof assistants are mostly used for research, and model checking techniques are more present in the industry. Some instances of proof assistants in the industry do exist, as some properties of DemiBFT (formerly LibraBFT) (opens in a new tab) and ZK circuit verifiers (opens in a new tab) being proven with Coq. However, it is a lot of work formalize and prove real systems and protocols, and proof assistants are used in much smaller scopes than what Quint is set up for.

Proving something using one of these tools provides a much stronger guarantee than verifying something with a model checker. Proof assistants are software and thus can have bugs too, but they are generally more trustworthy than model checkers because they usually rely on a small kernel implementing the core logical rules. All proofs reduce to the rules in the kernel. The kernel is very small, probably a few hundred lines of code, so it's easier to check and trust that it faithfully implement the rules. Model checkers are much larger implementations and, therefore, more prone to bugs.

While proof assistants enable very general proofs (such as length(m) + length(n) = length(m + n)), model checkers will always operate over some constraint state space (i.e. integers between 0 and 2^256).

Another difference is that these tools are able to generate code from the formalization, meaning the code will be correct by construction. For example, you can generate Haskell code from Coq. This is very useful if you want to extract some sequential library, but code for distributed systems definitions might not be so applicable to real world usage.

Agda and Idris are programming languages, while Quint is a specification language. Even so, Agda and Idris are formal methods tools, because you can write formal specification through dependent types, typing your program in a way that guarantees it has a certain behavior.

They also work as proof systems (see "How does Quint compare to Coq/Isabelle/Lean?") and, similarly, they require a lot of expertise and time to prove things. Proving through dependent types shifts some of this burden to the type system, but still demand an advanced understanding. Model checking (as in Quint) will usually provide weaker guarantees in comparison, but the proofs are fully automated.

Another difference is that programs in Agda and Idris need to be total - that is, they need to terminate, and the writer may need to convince the type system that in fact it does terminate every time.

Abstract State Machines (ASMs) are a precise way to write pseudocode to define the requirements of a system, and they are mostly used to reason about and analyze designs, while Quint is more focused on executing and verifying specifications.

This report (opens in a new tab) explores the differences and similarities between Quint, TLA+ and ASM in more detail.

There is a big advantage and a big disadvantage for using some formal verification tool designed for your programming language of choice instead of using Quint.

• Advantage: you don't have to write a Quint specification, you can use your own code
• Disadvantage: the verification capabilities will be extremely limited, because reasoning about generic programming language constructs and concrete program states is incredibly complex.

More generally, the state space of programs are often really large and unfeasible for any tool to handle. The solution is to abstract things and work on a higher level. Doing so in the same programming language is possible, but can be tricky. Using a specific language to do so can help to keep a more abstract mindset.

Anything you write in Quint is guaranteed to be compatible with the Temporal Logic of Actions (TLA - the logic, not TLA+ the language), and therefore verifiable with a model checker. If we were to try and translate arbitrary programs to TLA, this would only support a fragment of the language that obeys certain rules of the logic. This is also true for other verification techniques, and that's why formal verification of generic programs is so limited.

Quint is used to reason about behaviors of programs and how things change over time, and it does so by simulating or model checking executions. Static analyzers, on the other hand, find problems without any execution of the analyzed code, and only by looking at the code itself. A type checker is a static analyzer. You can also have a static analyzer that flags every time you write a division without checking that the divisor is not zero before - which doesn't necessarily mean that a division by zero will happen in runtime.

If you can use a static analyzer to search for a class of errors (i.e. null checks), you should definitely use that. Use Quint for what you cannot do with a static analyzer (which is a lot!).

This is also one of the reasons why Quint has a type system. Although we could check typing using invariants, as people often do in TLA+, we can do it statically with a regular type checker - and that is much better.

Static analyzers won't be able to tell you if your consensus algorithm does consensus as you expect, but Quint will. Also, trying to use static analyzers to find complex problems usually results in many false positives, while model checking doesn't have that problem - if it finds an issue, you'll get a counterexample with a precise way of reproducing the problem.

Spells are simply Quint modules that contain often-used definitions. There is nothing special about these definitions. They are probably a bit more thought-out than a definition someone would write on the spot. Check the page on Spells (opens in a new tab).

Definitions that are tagged as pure def are not allowed to read state variables (that is, the names declared with var). Definitions that are tagged with def are allowed to read state variables, though they do not have to.

Pure definitions have the following important property: A pure definition always returns the same result for the same parameter values.

Consider the following operator definition:

pure def min(x, y) = if (x < y) x else y

Whenever we call min(2, 3), we get 2 as a result, no matter what the values of state variables are.

Impure definitions have the following important property: An impure definition may produce different results for the same parameter values. An impure definition may read the values of state variables, which may affect in different results.

Consider the following definitions:

var limit: int
 
def minWithLimit(x, y) = min(min(x, y), limit)

In the above example, minWithLimit(10, 20) produces the value 10, when limit == 100, whereas minWithLimit(10, 20) produces the value 5, when limit == 5.

The definitions that have at least one parameter should be tagged with def, whereas the definitions that have no parameters should be tagged with val. We could say that val's are nullary def's.

As a result, a pure val is never changing its value in an execution. For example:

pure val avogadro = 602214076^(23 - 8)

Note that an impure val may still depend on the value of a state variable. For example:

var time: int
var velocity: int
 
val distance = velocity * time

In the above example, distance does not need any parameters, as it only depends on the state variables. However, the value of distance is still changing with the values of time and velocity.

A value that is defined via pure val is constant in the sense that it never changes in an execution. A const definition also declares a constant value. However, the value of const is not fixed at the time of specification writing, but it has to be fixed by instantiating the module.

Here is an example that illustrates the difference between pure val and const:

module fixed {
  // this module is written for N=4, e.g., for N processes
  pure val N = 4
 
  pure val procs = 1.to(N)
  // etc.
}
 
module parameterized {
  // this module is written for a parameter N
  const N: int
 
  pure val procs = 1.to(N)
  // etc.
}
 
module instance4 {
  import parameterized(N = 4) as I
 
  pure val procs = 1.to(I::N)
}