repository·main·Indexed 23 days ago
https://github.com/quint-co/quintDocumentation for Quint, a language featuring a Rust-based evaluator (quint_evaluator v0.2.0) and a TypeScript simulator. Includes guides on language syntax, API operators, design principles, and tooling such as the CLI and REPL. Provides setup instructions for editor support in Vim, Neovim, and Emacs, including integration with the quint-language-server via LSP. Covers model checking with TLC and Apalache, as well as practical examples for ICS 20, ICS23, and Tendermint specifications.
The builtin module provides a comprehensive set of primitives for Quint, including:
Quint is a specification language used to describe models (state machines) and properties (invariants or temporal properties). You can use Quint to verify these models using either a model checker or a simulator.
Quint is a CLI-first language. Users can perform the following via the command line:
The quint-modeling skill is used to produce a Quint specification from various starting points, such as ideas, requirements, source code, or existing TLA+ specifications. It is also used to audit or review existing .qnt files against a formal checklist.
When to use this skill:
When NOT to use this skill:
basicSpells. For those, use the quint-lang reference instead.The examples/ directory contains various protocol specifications written in Quint. These examples serve as learning resources for modeling different systems.
Note on availability: While all examples pass the parser and type checker, some may not be fully runnable or testable yet. Check the project dashboard for the current status of specific examples.
The Mafia game is a state-based implementation where players are assigned roles and the game alternates between Day and Night phases.
Mafia or Citizen.Alive or Dead.Day or Night.The game tracks its progress using a game_status variable which can be:
Role indicating the winner (either Mafia or Citizens).Night phase. Players are randomly assigned roles and set to Alive.Citizen players are Dead.Mafia players are Dead.testFixture/apalache directory contains specifications (specs) specifically designed to test the integration of the Quint model checker with Apalache. These specs serve as a validation suite to ensure that the translation or integration between Quint and the Apalache model checker is functioning correctly.Choreo is a structured framework for writing distributed protocol specifications in Quint. It provides abstractions for message passing, state management, and Byzantine fault tolerance. Use Choreo when modeling consensus protocols (e.g., Raft, Paxos, Tendermint, HotStuff), BFT protocols, multi-phase commit, or any message-passing protocol with $N$ processes.
To use Choreo, import it using the following syntax:
import choreo(processes = NODES) as choreo from "./choreo"import choreo(processes = NODES) as choreo from "./choreo"An inductive invariant is a logical formula (a predicate) over the variables of a system that characterizes a 'correct state'. To be considered an inductive invariant, the formula must satisfy two conditions:
In Quint, inductive invariants are used to prove that a system maintains a correct state throughout its execution. They are stronger than ordinary invariants because they must be preserved by every possible transition in the model.
Trace validation is the inverse of Model-based Testing. It uses real-world data from production or staging environments to verify that the implementation adheres to the Quint model.
The Trace Validation Workflow:
deposit("Bob", 100)) and/or states (sequential snapshots of relevant data, e.g., "Bob" -> 40).If Quint determines the sequence is impossible according to the model, it indicates a bug in the implementation (i.e., the code allowed a behavior that the specification forbids).
The Instance Flattener resolves the complexity of module instances by replacing each instance statement with an import statement and generating a new, dedicated module for that instance.
Key behaviors:
B::A1) with unique IDs for their definitions.import A(N=1)) are converted into pure val definitions in the new module.e depends on definitions in the current module, the flattener ensures those dependencies are copied into the new instance module so the expression remains resolvable.Original Code:
module A {
const N: int
val a = N
}
module B {
import A(N=1) as A1
val b = A1::a
}After Instance Flattening:
module A {
const N: int
val a = N
}
// A new module is generated for the instance
module B::A1 {
pure val B::A1::N = 1
pure val B::A1::a = B::A1::N
}
module B {
import B::A1.*
val b = B::A1::a
}module A {
const N: int // id 1
val a = N // id 2
}
module B {
import A(N=1) as A1
val b = A1::a // id 3
}
module C {
import A(N=0) as A1
val C = A1::a // id 4
}
// The instance flattener will create two new modules: B::A1 and C::A1
module B::A1 {
pure val B::A1::N = 1 // id 5
pure val B::A1::a = B::A1::N // id 6
}
module C::A1 {
pure val C::A1::N = 0 // id 7
pure val C::A1::a = C::A1::N // id 8
}
module B {
import B::A1.*
val b = B::A1::a // id 3
}
module C {
import C::A1.*
val c = C::A1::a // id 4
}