Egor Urvanov

How model checking differs from testingQuint, QUnit and TLA+

A test checks a scenario you thought of, model checking tries every order of actions. What QUnit, Jest, Vitest catch, and what Quint, TLA+, Alloy catch.

created · updated · 9 min · · Specs and context

A test checks a scenario you thought of, while model checking tries every order of actions and finds a rule violation nobody imagined. Test frameworks such as QUnit, Jest and Vitest check finished code on examples. Quint and TLA+ check the rules of a system even before any code exists, including code from an AI agent.

QUnitQuint≠input:1 and 2the addfunctionanswer 3:rightpaymentconnectionlostmoney gone,no orderchecks a function on a given inputchecks rules on every chain of movesone scenario that you thought upincluding those nobody thought of● model, people, systems, data  ● agent and harness  ● risk, stop, boundary

How Quint differs from QUnit: two similar names

QUnit is an engine for JavaScript tests, from the same family as Jest and Vitest. You write a function, then a test with an input and an expected answer, and the engine says whether they match. Quint is a language for describing how a system must behave. The program itself tries all possible moves and looks for those where a rule breaks. The mix-up comes from the name, while in essence these are programs of different classes. A comparison of the test engines themselves is in the article Jest vs Vitest vs QUnit.

What a QUnit test looks like. It takes a finished function, for example addition, feeds it one and two and compares the answer with three: assert.equal(add(1, 2), 3), an example from the QUnit site. If the answer is right, the test passes. All the test knows about the world is the input and the expected answer that you chose in advance.

A Quint model is built differently: there is no function and no answer in it. You describe which states the system can be in, which actions move it from one state to another and which rules must always hold. Quint itself runs such a model, simulates it and checks it before the code ships. So it does not matter whether the code is written: it checks the intent, not the implementation.

QUnit (test engine)
Quint (modeling language)
What it is
an engine for JavaScript code tests, like Jest and Vitest
a language for rules, the program itself tries every possible move
What it checks
that a finished function returns the right answer for given inputs
that the described system never reaches a forbidden state, even in combinations nobody thought of
What it needs
written code
only a description of the rules, the code may not exist
Example
a test that a date-parsing function returns the right date
a model that found that a crash mid-recording leaves a recording without a trace
What is hard
thinking up inputs
stating the rules so that they reflect reality

The table is best read row by row. The row "What it checks" shows the main difference: a test answers "does this function work correctly on this data", a model answers "is a situation that the rules forbid possible at all". A test is limited by what you thought up. A model is limited by what you put into it.

Takeaway
In this exampleQUnit checks code that is already written, while Quint checks an intent that may not be in the code yet.
In generalSo QUnit, Jest and Vitest do not replace Quint, and the other way round: they answer different questions.
Next stepIf someone says "it is the same as Jest", ask what exactly is meant: checking a function or checking rules.

Quint or Jest and Vitest: what a test checks and what a model checks

A testQuintpaymentorder createdmoney gone, no order?walkednot checkedpaymentorder createdmoney gone, no order!walkedwalkedwalked the one road that was thought ofwalked both and found the one where money goes without an order● model, people, systems, data  ● agent and harness  ● risk, stop, boundary

A test engine finds an error on the inputs you thought up. If you did not think about two admins at once, no test about them gets written, and the error stays. A model works differently: it builds combinations of steps itself, including ones nobody thought of, and shows the first where a rule broke.

Test engine
Quint
What it finds
an error on the inputs you thought up
an error in a combination of steps nobody thought up
When it is needed
the code already exists
the code is not written yet or does not exist at all
Weak spot
does not see what you did not think of
a model may not match reality, so it is checked against confirmed facts

What a test catches well: an error in the function itself, for example a wrong discount calculation or a wrong date parse. The input is known in advance here, and the test quickly shows what broke. What a test misses: race conditions and other errors that appear only in a certain order of events. In practical examples this is how an admin login and logout overlapping in time and a crash in the middle of a meeting recording were found. Neither action is wrong on its own, so a test for each of them passes.

The weak spot of Quint is that it checks a model, not the code. If the model is described inexactly, it proves something about an imaginary system. So the model is checked against real cases that are already confirmed, and keep an "as is and as required" pair in it. More about this in the article about the models.

Takeaway
In this exampleA test and a model answer different questions, so "which is better" is the wrong question.
In generalFor checking "can two people at once break the order of actions" a test engine is almost useless, and for checking "is the date parsed correctly" a model is excessive.
Next stepFor every rule you want to check, write down what it is about: input data or the order of actions.

How Quint differs from TLA+ and Alloy

The same rule, two languagesthe rule: no money charged without an orderpaid implies hasOrder□ ( paid ⇒ ∃ o ∈ Orders )implies means “this leads to”□ always · ⇒ leads to · ∃ exists · ∈ belongs to?Quint: reads almost like textclear without preparationTLA+ and Alloy: like a formulathe symbols have to be learned first● model, people, systems, data  ● agent and harness  ● risk, stop, boundary

TLA+ and Alloy are formal languages of the same kind: in them you also describe rules and look for their violations. They are older than Quint and better covered in books. But the notation in TLA+ is mathematical, and a newcomer needs time to read it. Quint was designed as a more accessible notation for the same task: it looks like ordinary code, and engineers without a math background read it. A detailed comparison of all three languages is in the article TLA+ vs Alloy vs Quint.

What is writtenWhat checksWhat comes outQuintTLA+TLCgoes through states one by oneApalachereasons about all at oncevia translation to TLA+a rule violationand the chain of steps to itboth languages are checked by the same two programs● model, people, systems, data  ● agent and harness  ● risk, stop, boundary

What “the same programs” means. Quint can be checked by two programs: TLC and Apalache. TLC is the very first checking program for TLA+: it goes through states one by one, so for Quint it needs the model translated into TLA+. Such a search is predictable, but the world must be small.

Apalache is built into Quint: it translates the model into conditions and asks the Z3 solver. It can check chains only up to a given length, so its “ok” means “no violations within that length”. TLA+ is checked by the same two programs, while Alloy has its own analyzer. Besides checking, Quint has a quick random simulation: it looks for violations by sampling and does not prove that there are none.

Quint
TLA+ / Alloy
Notation
looks like ordinary code, engineers read it
mathematical notation, a higher entry step
What checks it
TLC or Apalache
TLA+: the same TLC and Apalache; Alloy: its own analyzer
Maturity
younger
older, more examples

Each of the three languages rests on its own idea. TLA+ is built on Leslie Lamport’s thought that the most precise way to describe a system is simple mathematics. Alloy describes evolving structures and a program for exploring them. Quint gives the same task in a notation engineers understand: the description can be run, simulated and checked before the code ships.

2026, todayAlloysince 199729 yearsTLA+since 199927 yearsApalachesince 201511 yearsQuintsince 20215 years● model, people, systems, data  ● agent and harness  ● risk, stop, boundary

Maturity matters when heavy proofs are needed: large systems, strict guarantees for distributed protocols. The first version of the Alloy language appeared in 1997. TLA+ was created by Leslie Lamport, and according to Wikipedia the language dates to 1999. The Apalache checker was started in 2015, and the Quint repository was created in 2021, according to GitHub. So TLA+ has about 27 years of history and Quint about five.

Over those years TLA+ gathered books, courses and write-ups of real systems, while Quint has fewer. But the language develops fast: edits were pushed to the project repository on the day before the date of this article. For product rules like “a private recording never reaches shared storage” depth of proof is needed less often, and readability matters more.

Takeaway
In this exampleQuint gives the same task and the same class of checks in a more readable notation, at the price of lower maturity.
In generalFor product rules this is a reasonable trade, because rules are read and discussed by people without math, and models are easier to write together with an AI agent.
Next stepIf you need heavy proofs, move the model to TLA+: the ideas and rules stay the same.

What to choose: Quint, tests or TLA+

?Testa finished functionQuintproduct rulesTLA+heavy proofs● model, people, systems, data  ● agent and harness
A finished functionCheck that a function returns the right answer for given inputs: a test engine, QUnit, Jest or Vitest
Order of actionsFind a combination of steps where a product rule breaks, even if the code does not exist yet: Quint
Heavy proofsStrict guarantees for a large distributed system: TLA+, with more experience and examples

The choice is set by the question, not by a favorite program. If the question is "does this function work correctly", take a test. If the question is "can a rule break in some sequence of events", take a model. If you need guarantees at the level of a distributed protocol, take TLA+ and set aside time to learn it.

Takeaway
In this exampleThree options answer three different questions, and one does not replace another.
In generalFor product logic with agents and several participants you most often need both tests and Quint.
Next stepWrite down three questions about your product and put a suitable option against each using the table above.

How they work together

In practice tests and models stand side by side. A test protects a specific function from breaking under edits. A model protects a rule that crosses several functions and depends on the order of events. When a model finds a chain of steps, a short regression test comes out of it: it fails on the old code and passes on the fixed one.

So the model hands the tests what it found, and the tests hold it in the code. A detailed account of the findings, the "as is and as required" pair and the checking of the checks is in the main article about Quint, and the context borders the models are written for are covered in the article about agents per context.

Takeaway
In this exampleA model finds a chain of steps, and a test pins it in the code so the error does not return.
In generalThe result is a pair: the model looks for the unknown, the test guards the found.
Next stepTurn the next chain of steps you find into a short test and put it next to the others.

FAQ

How is Quint different from QUnit?
QUnit runs tests of finished JavaScript code, while Quint describes the rules of a system and tries the orders of actions itself. The names are similar, but these are programs of different kinds.
How is Quint different from TLA+?
They describe the same thing, and only the notation differs: Quint looks like ordinary code, while TLA+ uses mathematical notation. The same programs check both notations, TLC and Apalache.
What should I choose: Quint, Jest or TLA+?
If the question is whether a function works correctly, take a test. If it is whether a rule can break in some sequence of events, take Quint; for heavy proofs about a distributed system, people take TLA+.
Can Quint be used together with tests?
Yes, they complement each other. A model finds the chain of steps where a rule breaks, and a short test pins it in the code so the error does not come back.
Facts: as of 25 October 2026, Quint, TLA+ and Alloy documentation. The choice depends on the team and the task.

Same terms

© 2026 Egor Urvanov