A race condition is found by checking every order in which two operations can run. Tests cover only the orders you imagine, while a Quint model tries all of them itself and prints the chain of steps where a rule breaks, for example a crash mid-write or two admins at once, including in code written by an AI agent.
A test follows the scenario you imagined; a model walks every scenario of a small world.
How a Quint model works: every scenario instead of guessing
The name Quint is easy to mix up with the QUnit test engine, but it is a different program: a comparison with tests and TLA+. How Quint differs from TLA+ and Alloy is covered in the comparison of the three languages. An ordinary test is one scenario you thought up in advance: click, wait, check the result. A bug you never thought about is not in that scenario. A model works differently. You describe the states of the system and the allowed actions, and the program tries every order of actions in a small world and shows the first one where a rule breaks.
One model describes one area of logic, such as the life of a meeting recording or a member’s access rights, and takes from a few dozen to a few hundred lines. Next come a few stories: what exactly the model found and why a test did not.
Here is how it works step by step. First you choose a small world: say, one admin, one bot and one session. Then you describe what can happen in that world: log in, log out, a process crash, a new message. The program tries every order of those events and checks the rules after each step. This kind of search is called model checking. If a rule breaks, you get the exact chain of steps, which you can repeat by hand.
The world is small on purpose. The number of orders grows fast with the size of the world, so two or three entities and five or six actions usually give a result in seconds. That is enough for races: two actions need only two participants to overlap.
What errors a Quint model finds: examples
The main value of a model is the findings nobody was looking for. Below are the two most telling ones and a list of the rest. They share one shape, a race condition: two actions, each correct on its own, together cause a loss or a mix-up.
Let us go through the first story in detail. Suppose a person has a Telegram session in the system, and an admin can end it. At the same moment a bot may use that session to send a message. The code first checked that the session was alive, then went to send. Between the check and the send the admin managed to log out. As a result the message went out in the name of a person whose access had already been closed.
No test caught this, because every step on its own works correctly. The error lives only in the order "check, logout, send", and the model found that order by itself.
An admin logs out while a bot logs in with the old session. The code checked rights once, at the start, and trusted the result afterwards.
The second story is about data loss. A transcription system records a meeting and at some point must mark that a recording is in progress. If the process crashes between the start of the recording and that mark, after a restart the system does not know the recording existed. The file is there, the database entry is not. The user sees an empty spot where the meeting should be.
The cure is simple: set the mark before the recording starts, not after. But to notice the problem you have to imagine a crash in exactly that gap, and the model does it effortlessly, because a crash is one of its ordinary actions.
A recording was running, the process crashed, and no "recording in progress" mark was left anywhere. After a restart the system believes there was no recording, and the data is lost without a trace.
How to read the list above. Each row has the error class on the left and an example on the right. "An item on two cards" and "a lost ☑" belong to meeting tasks, "deleting a non-empty item" and "keys wider than rights" to the admin side, "a message to a stranger" and "a foreign quote" to messaging.
All six share one trait: data belonged to one owner and then ended up with another or vanished. That is why checking the owner at the moment of the action, not in advance, closes almost the whole list.
A pair of models: as is and as required
For each area two versions of the model are kept in one file. The first copies the code as it is now and must reproduce a known bug. The second describes the requirement: the rule is never broken. A switch at the top of the file turns the fixes on, so the difference between versions is visible at once.
On the left the path to the red room, the violation, is open. On the right a barrier stands on that path and the rule holds.
The table has three rows. The first says what each model is for: the left one reproduces the found bug, the right one shows that the requirement can be met. The second row shows the expected check result: on the left the rule is violated, on the right it holds. If on the left it suddenly is not violated, the model has stopped reflecting the code, and that is a signal to update it.
The third row is about fixes. Every difference of the right model from the left one carries a tag like П1, П2 (the letter П stands for the Russian word for “fix”) and a note "was: …". These tags let you walk from the requirement to a concrete place in the code and see exactly what to change.
A model for every domain
Each bounded context has its own rules, written as MUST in an aggregate card. A formal model makes those rules checkable, and an agent per context works inside their borders.
What stands behind each example. "Meeting" is the rule that people from the previous recording do not carry over into the next one, even if the meeting link is the same. "Private data" means a private recording cannot end up in shared storage under any order of actions. "Member" means one Telegram account matches one member record, and history survives a merge. "Vacancy" means a status on a vacancy belongs to a specific pair of candidate and vacancy, not to the candidate in general.
Checking the checks
A green result can mean "all correct" or "the check checked nothing". So the checks themselves are checked: the author or an agent breaks the model on purpose (for example, removes one condition) to see whether the rule notices. If it does not, the rule is useless.
The bars show what share of rules the current code violates. The longer the bar, the more rules the model caught on real code. "Participants 2 of 2" means both checks found a problem. "Privacy 1 of 4" means the code mostly holds, but one hole exists.
This is not a quality grade for the code. A bar depends on which rules were chosen, and shows more where the model brought the most benefit.
A broken copy of the model must trip the rule. If it passes through and nothing fires, the rule checks nothing.
After every model edit a check runs automatically. If a rule is violated, the agent gets the chain of steps and fixes the model or the code at once.
What each row means. "A header as a contract" means the top of the file lists the rules, the expected violations and the situations that must occur. "A broken copy" checks that a rule is able to fire at all. "Situations that must occur" guards against "if A then B" rules where A never happened. "Dead ends" are cases where the program silently drops a run and "ok" comes out by itself.
The last two rows concern people and agents. "Intent kept apart" means the person's wish is recorded in the model independently of the field under test, otherwise the rule compares a field with itself. "Automatic check" (in effect a hook) means an agent cannot forget to run the model: it runs by itself after every edit.
Where humans step in
A model checks whatever can be written as a finite list of conditions: whether a recording vanished, whether participants got mixed, whether there is a way out of a dead end. Clear labels, convenience and the overall feel of a screen cannot be described that way, so a person judges them on a mockup.
- whether a recording vanished
- whether participants got mixed
- whether a dangerous action asks for confirmation
- whether there is a way out of a dead end
- whether labels are clear
- whether the panel is overloaded
- whether picking is convenient
- whether the extension installs on a clean profile
The list on the left holds everything that can be phrased as "always" or "never": a recording does not vanish, participants do not mix, a dangerous action asks for confirmation. The model checks such rules completely.
The list on the right holds things with no finite list of features. Whether a label is clear is decided by the reader. So in the requirements table "needs a human check" rows are marked in advance and do not try to formalize them.
Weak spots of model checking
The method has limits, and it is better to know them before starting. A model does not follow the code by itself, does not check "eventually", and sees only the world you put into it.
No link to the code: a model is written by hand, and nothing forces it to change with the code. A month later it may describe what no longer exists. The remedy: keep in the header the commit the model was taken from and update it with the code. A stronger remedy is to run model traces through the real handler, but that step does not exist yet. A related task, keeping the desired state, the code and the measurement in agreement, is covered in the article on the reconcile loop for specs.
No "eventually" checks: that a bug finally reaches the team is checked only indirectly. A tiny world: a bug that needs five entities at once can slip through. Empty greens: a rule holds only because the needed feature is not in the code yet, and the green color is misleading.
Where to start with Quint: a first model in one evening
An order for your first evening. Open the list of fixed bugs and choose one whose cause is the order or timing of events. Write out the participants and the actions that led to it. Describe them in a model, run it and wait until the program finds the chain by itself. Then add the fix under a switch and make sure the rule holds. Finally, break the model on purpose and check that the rule notices.
There is no need to model the whole product at once. Take one recent bug that had to be fixed twice or that a user found. Describe its participants and two or three actions in a model, run the search, and make sure the program finds that bug without a hint. Then fix it and make sure the rule holds.
How to start together with an agent
1. Install Quint. The agent installs it itself through npm.
Install Quint for yourself and make sure it runs.
2. Requirements first, not code. That way the agent first describes the world and edits code afterwards.
Do not change the code. Make requirements in Quint for [area]. For each rule show two versions: as it is now and as it should be.
3. Check the result.
4. Logic and screen are separate. By default an agent mixes them up: it writes screen rules as logic and skips cases in the logic.
Make two lists of requirements. 1. Logic: only "always" and "never", checked by a Quint model. 2. Screen: clarity and convenience, which I will check myself on a mockup.
FAQ
Quint is a language for describing the states of a system, its actions and the rules that must always hold. A program tries every order of actions and shows the chain of steps where a rule breaks.
Describe the participants and two or three actions in a model and run the search. The model finds orders such as "check, log out, send" that nobody thought to write as a test.
No, they answer different questions. A test protects one function, while a model checks rules that depend on the order of events; a chain of steps found by the model turns into a short regression test.
Take a recently fixed bug whose cause lies in the order or timing of events. Describe its participants and two or three actions, run the search and check that the program finds the bug by itself.