Quint FAQ

Quint is an executable specification language built on the Temporal Logic of Actions (TLA). You write a model of your system, define invariants and properties, then run or verify the model to find bugs before they reach code. The result is something between a design document and a test suite: an artifact that you interact with during development, not just write and file away.

The core idea: most specs are documentation that describes what a system should do. A Quint spec is something you execute. That distinction matters because executable specs can catch subtle bugs that documentation cannot, and can be leveraged for testing and runtime observability.

Quint gives you multiple ways to check a system:

Simulation (quint run) picks random execution paths through your model and checks whether any invariants are violated. It is fast, gives you immediate feedback, and is a good starting point.

Deterministic Tests (quint test): Checks specific scenarios you have in mind, rather than exploring random paths like quint run.

Model checking (quint verify) exhaustively explores all reachable states and reports any invariant violation with a precise counterexample trace.

Model-based testing (via Quint Connect) bridges the gap between a verified spec and the implementation. Quint Connect generates tests out of the spec model, with the spec acting as an oracle that drives and checks those tests against your actual code in CI.

Quint is for engineers who build or maintain distributed systems, protocols, or any system where correctness matters and bugs happen in edge cases. In practice, this includes system designers who want to validate a design before writing implementation code, software engineers who want to catch bugs that unit tests miss, security auditors who need exhaustive property checking, and engineering teams building AI-accelerated workflows who want to define intent with more precision and feedback and check that intent against what AI produced.

Quint is a particularly good fit for distributed and concurrent systems, and any system where the interesting bugs emerge from the interaction of multiple components over time, including consensus algorithms, database transactions, token economics, access control, smart contracts, and p2p networking protocols. The underlying Temporal Logic of Actions was designed specifically for reasoning about state changes over time, which maps naturally onto these problem domains.

Yes. Quint is open source and available at github.com/informalsystems/quint. It is maintained by the Quint core team and can be installed via npm, brew, nix, or by downloading the binaries directly from GitHub Releases.

Quint is actively used in production specification and testing workflows by multiple engineering teams. The language, CLI, and VS Code extension are stable and in active use.

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 what it can verify and where it is useful. Below we discuss several differences that motivate the use of Quint.

Syntax: This is the most obvious difference if you look at a Quint spec and a TLA+ spec next to each other. Quint uses programming-style syntax inspired by TypeScript and functional languages. TLA+ uses mathematical and LaTeX-style notation. If you can read TypeScript, you can read a Quint spec.

TLA+ actions typically mix multiple aspects: nondeterministic choices, guards that restrict the environment (and applicability of actions), conditions and updates of the business logic, the updates of the local state of a process, and the updates of the global state of the system. As a result, the TLA+ notation is quite disconnected from the production code that many people are familiar with. In contrast, Quint has a functional layer that allows you to encode the business logic as pure functions independently of how applying these functions changes the state of the system. This makes the Quint language a seamless communication tool within teams, while even reading TLA+ typically involves a steep learning curve for many people.

If you already know TLA+, you will find Quint familiar, and indeed most TLA+ specs can be directly translated into the Quint syntax. However, you will benefit from Quint by using its idiomatic style, e.g., by separating the action layer from the functional layer. If you are new to formal specification, Quint is likely the faster path, both due to the more modern syntax and the editor integration.

Types: TLA+ is purposely untyped so that designers can focus on algorithmic concepts. On the one hand, this makes a lot of sense as your consensus algorithm will not look much different whether you need to agree on an integer or whether you need to agree on a string. On the other hand, this complicates tooling a lot and defers bug finding to runtime, e.g., if your algorithm unintentionally puts a string in a set that otherwise holds integers, you might only observe this in a counterexample generated by the model checker.

Quint is built on the idea that tool support is as important as the ease of specifying, and that these two goals are not necessarily opposing. For instance, while you need to care about types a bit (with most types being inferred), as a benefit you get Quint's static analysis, which has a type checker and an effect system that catches a class of spec errors already in your editor before you even run anything. TLA+ has no native type system and no explicit distinction between pure functions and state-accessing operations that would allow this rapid feedback.

Tooling: Quint is built with developer tooling first: near-instant feedback in the VS Code extension, a REPL, a CLI for random simulation, testing, and model checking that all install via one npm command. As Quint is a fragment of TLA+, a Quint specification can be automatically translated to a TLA+ specification. From the Quint CLI you can use TLA+ tools like the Apalache and TLC model checkers.

Test-friendly output: Quint has the concept of a run as a first-class citizen, which is a concrete execution path (sequence of actions) that can serve as a test or test pattern, e.g., runs may contain non-deterministic choices which together with matching assertions correspond to property-based tests. TLA+ has no direct equivalent.

Constraints: Quint intentionally restricts you to a fragment of TLA. In practice, we have not encountered any limitations in expressing the systems we like to express (except some forms of recursion that require some workaround). At the same time, the restriction prevents accidental use of operators that lead to hard-to-debug scenarios. In theory, however, TLA+ gives you more expressive power. Also, TLA+ has the TLAPS proof system, which Quint does not have.

No, but they have some common goals, e.g., making the benefits of executable specs and TLA+ more approachable to engineers. However, the strategies are different. PlusCal is a language on top of TLA+ that is precompiled into TLA+. It then uses TLA+'s tooling for verification. PlusCal introduces imperative constructs (while loops, assignments) into what is otherwise a fully declarative language. Quint introduces a new syntax but keeps the declarative approach: you describe state transitions, not sequential steps. Regarding the tooling, Quint does not use TLA+ as an intermediate language (except for model checking). The REPL, the simulator, and the testing tools are all Quint-native.

If you are choosing between them for a new project, Quint's broader tooling ecosystem is worth considering.

Alloy is focused on sets and relations and is well-suited for specifying requirements and data structures. Quint is natively time-oriented, making it a better fit for concurrent and distributed systems where the interesting properties involve how state changes across transitions.

Alloy added temporal operators in Alloy 6, but for most of its history, modeling the passage of time required complex workarounds. Alloy verification can be faster than Quint for time-free specifications because it can use SAT solving instead of the SMT solving Apalache uses.

If your main concern is data structure or relational constraints without time, Alloy may be a better fit. For distributed system behavior, consensus protocols, or anything that requires reasoning about sequences of events, Quint maps more naturally.

Coq, Lean, and Isabelle are proof assistants: they help you write a formal proof, but you do most of the work. Learning to use a proof assistant effectively typically takes years. In practice, proof assistants are predominantly used in research contexts, or for highly critical but stable codebases. Changing the code might involve redoing the proof, which involves manual work. So this typically comes towards the end of a project after the code has stabilized.

In contrast, Quint brings value and increases confidence from the very beginning. This ranges from type checking while writing the specification, to finding concurrency bugs through random simulation, and model-based testing. In addition, Quint supports model checking, where you define the model and the properties and the verification is fully automated, which however, in practice requires you to limit the scope (e.g., a small number of replicated components, or integers of small width).

If you want to verify a protocol design or catch a class of bugs before production, Quint is the more practical starting point. If after simulation, model checking, and model-based testing, you still need the extra confidence provided by a full formal proof of correctness, proof assistants are the appropriate tool.

Agda and Idris are dependently-typed programming languages where correctness properties are expressed through the type system. They function as both programming languages and proof systems. Like Coq and Lean, they require significant expertise and the proofs are not automated.

Quint is a specification language, not a programming language; you model behavior rather than write executable programs. The tradeoff is the same as with proof assistants: Quint is faster to learn and produces automated results; Agda and Idris provide stronger guarantees at the cost of significant effort.

Like fuzzing, Quint can also be used to look for bugs, but through different mechanisms and at different levels.

A fuzzer generates random or coverage-guided inputs to your actual implementation looking for crashes, assertion failures, or unexpected behavior. Quint's simulator does something similar but at the spec level, randomly exploring execution paths through a model of your system. Model checking Quint specifications goes further, exhaustively exploring all reachable states.

The key difference is that fuzzers can miss rare bugs; the rare sequence of events that triggers a bug may never be generated. Quint's verify command, if it terminates, tells you definitively whether a violation exists within the checked state space.

Quint and fuzzing are complementary. You can generate fuzz test inputs from Quint traces. The typical workflow is to use Quint to find the bug at the design level and then use fuzzing or model-based testing to validate the implementation against the specification.

Static analyzers find bugs in code. Quint finds bugs in designs. Quint is strong in protocol-level flaws like concurrency issues, data races, safety violations, liveness failures, non-termination, or invariant breaks that exist regardless of which language you implement in or how carefully you code it. Static analyzers are strong in finding code-level bugs like null checks, type mismatches, memory errors. For such checks, static analyzers are fast and require no additional modeling work, and should be used, of course. For instance, in Rust, the compiler does static analysis for you and brings a lot of value.

However, even a replication engine implemented in Rust might still run into safety and liveness issues, obviously. If you want to reason about concurrency, using static analyzers becomes more involved. You need to figure out abstraction, invariants, pre/post conditions, etc., and even with guidance, the tools might produce false positives for complex behavioral properties.

However, finding a bug is one thing, understanding it is another. A bug that is demonstrated by a concrete sequence of actions as an outcome of simulation in Quint is much easier to share and explain than potentially violated invariants in an abstract state. So static analysis and Quint address genuinely different aspects of bringing confidence. By the way, the Quint typechecker (that is also used in IDEs) is a static analysis tool.

You can write a reference implementation in Python or TypeScript and build a simulator on top of it. Some teams do this. However, there are many benefits that come from Quint:

Quint already includes a highly efficient simulator (that automatically parallelizes over all your cores), a model checker integration, an IDE with type checking, and a testing engine based on Quint runs that allows you to express scenarios in distributed or concurrent systems. Building this from scratch in a general-purpose language is a significant engineering project, while your team's focus should be building the actual system, not the tooling.

Quint specs have a standardized format (the ITF trace format) that tools like Quint Connect can consume directly to drive model-based tests against your implementation.

And finally, Quint is a specification language, not a programming language. Its restrictions force you to describe behavior in a way that is compatible with formal verification. Arbitrary code in a general-purpose programming language is much harder to reason about and to formally verify.

AI generates code faster than ever, but the reasoning process that used to generate confidence has been removed from the workflow. When engineers wrote code themselves, they built understanding of the system in the act of writing. When AI generates code, that understanding no longer happens organically. Quint restores that process by making the spec the verification artifact.

A practical workflow: use an LLM to write or translate a Quint spec from an English description of your system, then use Quint's tools to validate the spec. Quint does not hallucinate; a spec either satisfies the invariants or it does not, in which case it will produce a counterexample trace that leads to the bug. You can take a look at the trace and share it with your colleagues, and you don't need to trust some LLM's explanation. In the next step, you can use the validated spec to guide AI-generation of implementation code, and use Quint Connect to set up tests that check that code against the specification.

The Quint LLM Kit (available at github.com/informalsystems/quint-llm-kit) includes Claude Code agents that write Quint specs from English requirements and validate them using Quint tools.

Yes. The Quint LLM Kit includes agents that generate and validate Quint specs from natural language descriptions. Because Quint specs are executable, an LLM-generated spec can be immediately checked for type errors, semantic issues, and invariant violations, unlike any English spec, which cannot be automatically validated. Moreover, an agentic coding tool can call Quint tools in a feedback loop until a Quint spec satisfies a requirement, e.g., is type correct or satisfies given invariants.

For instance, we used LLMs to refactor a consensus specification for our Fast Tendermint protocol change: AI modified the existing Quint spec based on an English protocol description, and the new Quint spec then guided the code change. This found two bugs in the English protocol spec within an afternoon. Finding these bugs would have taken several days to surface with a traditional workflow, where engineers first need to understand and manually encode the English spec in Quint. With AI handling that initial encoding, engineers focused entirely on validation using Quint tools interactively. The result: a code change traditionally estimated at multiple weeks was completed in about one week. The Quint LLM Kit and agentic coding tools make this workflow available out of the box.

We have a full blog post on this. Read more here.

Cognitive debt (or comprehension debt) is the accumulated loss of understanding and trust that engineering teams experience when LLMs write code on their behalf. The traditional software development process built trust to a large extent through the act of writing (and reviewing) code; engineers understood the system because they built it. LLMs short-circuit this process.

Quint addresses cognitive debt by providing a separate design artifact, the spec, that engineers interact with to build understanding of the system before implementation. A Quint spec is something to interact with, not just review. Validation happens during design, where fixing a bug is cheap, rather than after code review, where it is expensive. Read more.

Quint Connect is a Rust library that bridges Quint specifications to their implementations. It enables model-based testing: the verified Quint spec acts as an oracle that drives tests against your actual Rust code.

You define two things: how to extract relevant application state, and how to reproduce state transitions from the spec in the implementation. Quint Connect provides the interfaces for both. LLMs are well-suited to generating this bridge code, which historically made model-based testing expensive to set up and maintain.

Quint Connect is available at github.com/informalsystems/quint-connect.

The Emerald EVM network framework team set up Quint Connect in less than one person-week. AI wrote the initial Quint spec and most of the bridge code that connects the spec to the implementation. The result: ~80% test coverage at the application layer from Quint Connect, along with a memory leak found where completed data streams were kept indefinitely (eventually exhausting memory).

The historically high cost of setting up model-based testing has been mitigated by LLMs substantially due to their effectiveness at generating the bridge code between spec and implementation.

Start with the simulator. Running quint run against your spec is fast and catches most design-level bugs. Once the spec is stable, Quint Connect lets you run the same scenarios against your actual implementation, checking whether the code matches the spec's behavior under real execution.

The AWS DynamoDB production incident in October 2025 is a concrete example of why spec validation alone is not always enough: the original design was correct, but code diverged from the spec through incremental changes over time, and a race condition emerged that only showed up in production. Quint Connect catches this class of spec drift automatically in CI.

npm install -g @informalsystems/quint

That is the full install. A VS Code extension is also available in the VS Code marketplace (search for "Quint").

The best starting points:

The Telegram community at t.me/quint_lang is active and the team responds directly to questions.

Yes. The VS Code extension provides near-instant feedback as you type: type checking, syntax highlighting, and located error messages. An LSP server is also available for integration with other editors like Vim, Emacs and Helix.

quint run is the simulator. It randomly picks execution paths and checks invariants along the way. It is fast and gives you immediate counterexamples when it finds a violation, but it does not guarantee exhaustive coverage.

quint verify exhaustively explores all reachable states (often up to a given bound) and reports any invariant violation with a precise counterexample trace. It is often slower than the simulator but provides stronger guarantees. Quint supports two model checkers: Apalache, which uses SMT solving, and TLC.

Start with quint run for fast feedback during development, then use quint verify for deeper checking.

An invariant is a property that must hold in every state of every execution. For example: "no account can have a negative balance." Invariants are the most common type of property and should be used preferably as they are fast to check in both the simulator and the model checker.

A temporal property expresses something about the relationship between states over time, for example "if a transaction is submitted, it will eventually be processed." Temporal properties can only be checked with quint verify --backend=tlc (Apalache has partial support, and the Quint simulator doesn't support them).

A practical note: to verify that a certain state is reachable (rather than that it never occurs), use a witness: define the state you want to reach and write it as a negated invariant. Quint will find an execution path that gets you there if one exists.

Yes, by default. This is inherited from TLA+'s requirement to be explicit about what changes in a transition. It can feel verbose, but it serves as a check: if you forget to specify what a variable does in a transition, Quint will tell you.

One practical workaround used by many Quint users: put all global state into a single record variable and use Quint's spread syntax ({ ...state, fieldToUpdate: newValue }) to express partial updates cleanly. This reduces the verbosity while keeping the explicitness the model checker relies on.

pure def defines a function that cannot read state variables. It always returns the same result for the same inputs, regardless of the current state. def allows reading state variables, which means the result may vary depending on the current state.

Use pure def by default for any computation that does not need to see the current state; it is more composable and easier to reason about.

def takes at least one parameter. val takes no parameters. A pure val is a constant; it never changes over executions. An impure val with no parameters can still depend on state variables, meaning its value changes as the state evolves.

A pure val is a concrete, fixed value defined in the spec. A const declares a value that will be fixed when the module is instantiated; the spec is parameterized, and the value is supplied by the caller. For example, const N: int lets you write a spec for N validators and then test it with N = 4 by importing the module with import parameterized(N = 4) as I.

Spells are Quint modules that contain commonly used definitions. There is nothing special about them syntactically; they are just modules with useful utility definitions that have been thought through more carefully than what you would write on the spot. The Spells page on GitHub has examples.

Quint supports two model checkers: Apalache, which uses SMT solving, and TLC. One is not better than the other, so we recommend experimenting with both.

Apalache is a symbolic model checker integrated directly with Quint tooling; it is automatically downloaded and invoked when you run quint verify. It translates the model and properties into SMT constraints and uses the Z3 solver to check them. This allows Apalache to verify models that would be infeasible for explicit-state checkers, such as specs that pick numbers from a large range. Because it checks executions up to a user-defined bound (--max-steps, defaulting to 10), it is a bounded model checker. It supports invariants, with partial support for temporal properties.

TLC is the original model checker for TLA+. It works with Quint via transpilation of Quint specs into TLA+. TLC is an explicit-state model checker: it enumerates all possible states individually, which makes its behavior straightforward to predict. Time depends directly on state-space size. Because TLC enumerates states, the state space must be finite and small enough to be feasible. It supports invariants and temporal properties.

Yes, and you can even use Literate Specifications to interleave Quint blocks with natural language explanations in the same document.

Markdown accepts all kinds of errors: undefined names, type mismatches, impossible claims and ambiguous interfaces, because it is not executable. A Quint spec gives you name resolution, type checking, and the ability to catch contradictions and undefined references automatically. You get a better spec document and something you can run and verify, and that can be used to generate test inputs and assertions.

No. Quint works alongside your existing test suite, code review process, and CI pipeline. It adds a verification layer at the design and spec level, which can also be leveraged for testing code with Quint Connect, a model-based testing layer that checks whether implementation behavior matches the spec. It does not replace tests for implementation-level concerns like performance or integration behavior.

A few concrete examples from production use:

Neutron liquidity pool migration ($23M pool): Quint's model-based testing found a rewards attribution bug before the migration reached production. When new liquidity was added to a pool, incentives_rewards_per_share was not updated, meaning rewards were incorrectly attributed to later depositors.

Emerald (EVM network framework): Found a memory leak (completed data streams were never cleaned up, eventually exhausting memory) and a subtle stale node behavior in the Malachite consensus layer. Both found during an initial setup that took less than one person-week.

Turso database: A community contributor used Quint with Claude to write specs for MVCC and found two corruption bugs, including one described as "fairly nasty, probably would have taken many days to discover otherwise."

Fast Tendermint: Two bugs in the English-language protocol spec found in one afternoon during Quint spec validation, before any implementation work began.