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.

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 effect 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)
}