Getting Started

Install Quint with npm

Install node/npm (opens in a new tab) if you don't have it already. Then, open your terminal and run:

npm i @informalsystems/quint -g

Setup your code editor

For the best experience writting Quint, you should set up your code editor with the Quint tools. The VSCode setup is, by far, the easiest, so you might want to use it if you want a quick start.

Install the Quint extension (opens in a new tab):

1. Open the extensions panel by pressing Ctrl+Shift+X or clicking the extensions icon.
2. Search for Quint and click Install.

Write a specification

In order to run Quint, we first need a specification. Let's use this simple bank specification, which has a bug.

module bank {
  /// A state variable to store the balance of each account
  var balances: str -> int
 
  pure val ADDRESSES = Set("alice", "bob", "charlie")
 
  action deposit(account, amount) = {
    // Increment balance of account by amount
    balances' = balances.setBy(account, curr => curr + amount)
  }
 
  action withdraw(account, amount) = {
    // Decrement balance of account by amount
    balances' = balances.setBy(account, curr => curr - amount)
  }
 
  action init = {
    // At the initial state, all balances are zero
    balances' = ADDRESSES.mapBy(_ => 0)
  }
 
  action step = {
    // Non-deterministically pick an address and an amount
    nondet account = ADDRESSES.oneOf()
    nondet amount = 1.to(100).oneOf()
    // Non-deterministically choose to either deposit or withdraw
    any {
      deposit(account, amount),
      withdraw(account, amount),
    }
  }
 
  /// An invariant stating that all accounts should have a non-negative balance
  val no_negatives = ADDRESSES.forall(addr => balances.get(addr) >= 0)
}

Create a bank.qnt file and add the contents above to it. Then, let's try to check the invariant no_negatives. This invariant states that none of the balances should be less then zero, ever. An invariant is something that needs to be true for all reachable states.

Find a violation

To look for violations of this invariant, we can use the run subcommand, which will simulate a bunch of executions while checking the invariant. In a terminal, whilw on the directory of this file, execute:

quint run bank.qnt --invariant=no_negatives

This should result in a violation. You can inspect the balances and find a negative value. If you want to understand better how we got to such state, try using the --mbt flag, which includes additional metadata on the violation trace (usually used for testing purposes. MBT stands for Model Based Testing):

quint run bank.qnt --invariant=no_negatives --mbt

Now, you should see that a withdraw action was taken right before the balances went negative.

Fix the issue

Let's update the withdraw definition to prevent this scenario - users should not be able to withdraw more than they currently have.

action withdraw(account, amount) = all { // <- all of the following need to hold
  // A precondition, there should be enough to withdraw
  balances.get(account) >= amount,
  // Decrement balance of account by amount
  balances' = balances.setBy(account, curr => curr - amount),
}

We can run the simulator again. This time, it should find no violation and return an [ok] result:

quint run bank.qnt --invariant=no_negatives

Verify the result

However, the simulator might miss several executions. To make sure we fixed the problem, we should run the model checker, by using the verify subcommand.

quint verify bank.qnt --invariant=no_negatives

This will verify all possible executions of up to 10 steps. We can be confident that we fixed the issue after seeing the [ok] result from the verify command.