Model Checkers

Model checkers are tools that take models and properties as inputs and check if the properties are true for all states/behaviors of that model. If a model checker returns "OK", it means that the property is verified for the model, and it guarantees that there is no sequence of steps in the model that violate the property.

There are different types of model checkers that use different strategies to achieve verification. Quint specifications can be verified by two model checkers: TLC (opens in a new tab) and Apalache (opens in a new tab).

TLC

TLC (no acronym defined!) is the first model checker for TLA+, and can be used for Quint by transpiling Quint specs into TLA+. TLC is an explicit-state model checker, which means it enumerates all possible states and individually checks each one of them by keeping a reachability graph and a queue of states to check next.

This is arguably the most straightforward model checking approach, making it easier to predict than more complex approaches: the time spent to check a model depends directly on the size of the state-space and the computational complexity of the definitions in the model.

When using TLC, it is not possible to pick a number from the set of all integers, as that is infinite. So it is always necessary to define a constrained set from which to pick numbers, such as nondet amount = Set(1, 2, 100, 999).oneOf().

TLC Outline

• Not integrated with Quint, requires transpilation into TLA+
• Enumerates all possible states, state-space needs to me small enough
• Checks executions of any length
• Checks invariants and temporal properties

Apalache

Apalache is a symbolic model checker that is integrated with Quint tooling, and will be automatically downloaded and invoked when a quint verify is run.

Apalache translates the model and the properties into SMT (Satisfiability Modulo Theories) constraints and then uses the Z3 SMT solver to check for their satisfiability. Consider a simple model that increments x, and a property that states that x cannot be 2:

var x: int
 
action init = x' = 0
action step = x' = x + 1
 
val inv = x != 2

Some of the constraints generated by Apalache would look somewhat like this:

x0 = 0 // initial state
x1 = x0 + 1 // first transition
x2 = x1 + 1 // second transition
x2 = 2 // negated invariant

Then, Apalache asks Z3: "Is there any values for x0, x1 and x2 that satisfy these constraints?" and Z3 will respond "yes" and provide the values, which Apalache then uses to construct a counter-example and report a violation.

Notice how the example constraints above are specific for a sequence of 2 steps/transitions. This is important: Apalache cannot check an arbitrary number of steps - it needs to choose a specific number to generate the constraints for. This makes Apalache a bounded model-checker, and it needs a --max-steps argument (defaults to 10) that will define the bound of the verification. If someone checked the above model with --max-steps=1, no violation would be found. When something is verified using Apalache, it is always verified for a certain bound.

Using the symbolic strategy means that Apalache can check models that would never be checked by TLC as it would be unfeasible or impossible to enumerate all the states. For example, Apalache can check specifications that pick numbers from a large range of numbers, as Z3 is a good tool for solving equations with numbers.

Apalache Outline

• Integrated with Quint
• Translates model into constraints, some complex expressions might cause big slowdowns
• Checks executions of a user-defined max length
• Checks invariants. Temporal properties have partial support