Quint Studio Onboarding guide
Getting started with Quint Studio
Quint Studio runs on your machine and works through the coding agent you already use. Set it up with a few commands, keep it running next to your agent, and it checks every change that touches the behavior you modeled.
On this page
Quint Studio is a local tool
Quint runs locally on your compute, using the models you provide. What leaves your machine is usage analytics and your agents' own traffic to your agent provider. Your code, specs, and coverage are never shared with Quint.
How it works
Quint Studio captures your codebase into several components that represent state machines, then writes a Quint specification for the components you select, and helps you leverage the spec by reproducing and fixing misbehavior, exploring correctness properties and assessing and improving test coverage.
Scan your codebase
Studio maps your code into components for meaningful modeling and reasoning.
★ RecommendedCentralOrder Return (RMA) Lifecyclenot modeledreading…Pick what to model
Studio recommends where to start, and you pick one or more components to model.
Set up Quint 22 selected
View selection ▾
★ RecommendedCentralOrder Return (RMA) Lifecyclenot modeledCentralOrdernot modeledAgents model them
For every model, Studio applies checks and techniques to ensure quality in many factors.
← OrderRunning…■ Stop1Model2Check3ReproduceRunning • 5m 00s • your-model • $0.48
Execution Logs
Reviewing the spec against the code
09:42:56Reviewing the spec against the code09:42:54The author is working on the spec09:42:53Readingsrc/modules/order/service.ts09:42:53Model order startedQuint spec Draft
order/order.qnt
module order { type Status = Draft | Pending | Completed | Archived | Canceled type OrderState = { version: int, status: Status,
For every modeled component, you'll get three tabs
Misbehavior
Bugs the model finds, reproduced as tests and fixable from Studio.
DashboardMisbehavior 4CorrectnessCoverage !Propose fixesno_reopen_of_archivedConfirmedProduct bug
Completing an archived order brings it back to Completed.
Found by the model
no_reopen_of_archived0 Initial state›1 archiveOrder›2 completeOrderReproduced by a test
packages/modules/order/integration-tests/__tests__/archive-order.spec.ts
Correctness
What is being checked on this model, and what caused a violation when there is one.
DashboardMisbehavior 4CorrectnessCoverage !Correctness properties1/4 violatedno_reopen_of_archivedAn archived order is never reopened to COMPLETED.Replayno_silent_cancel_of_completedA completed or archived order is never silently moved…version_tracks_confirmed_changesorder.version equals one plus the number of that order’s…applied_actions_not_reappliedAn already-applied order-change action never re-inflates…Observation targetsAll 4 observedorder_createdAn order has been created (promoted out of Draft).Replaychange_confirmedAn order change has been confirmed.Replayorder_completedAn order reached COMPLETED.Replayorder_archivedAn order reached ARCHIVED.ReplayCoverage
Which transitions your tests reach, and tests for the rest.
DashboardMisbehavior 4CorrectnessCoverage !21of 33 transitions testedtested (21)not tested (12)Not tested12Select allWrite testsAdd order transactions
When
orders.get(o).status != Draft→ pending_trx, orders, changes, returns, flags changeApply pending order actions (CPending, ch.applied)
When
ch.status == CPending or ch.status == CRequested→ changes, orders, returns changeDelete order transactions
When
pending_trx.length() > 0→ pending_trx, orders, changes, returns, flags changeUpdate order paid refundable amount
When
pending_trx.length() > 0→ orders, pending_trx, changes, returns, flags change
Install
Quint Studio is available for macOS and Linux. Install it with:
sh -c "$(curl -fsSL https://studio.quint.sh/install.sh)"Or download the binaries directly
Set up
In order to start using Studio, you'll need to connect it with your agent provider and choose your preferred models for cheap and for complex tasks. You can also set usage limits to keep it under control. If you want external agents to drive Studio for you, connect them in Studio by configuring the local MCP server connection.
Welcome
Sign in to open your workspace.
I accept the Terms and Conditions.
your-repo
Welcome to Quint Studio
Here are some quick setup steps to get you started.
Before this run: your models
Studio's agents run on your own AI provider account. Sign in once and pick the models. Change it any time in Settings › Models.
Sign in to at least one provider to go on.
your-repo
Welcome to Quint Studio
Here are some quick setup steps to get you started.
Before this run: your models
Studio's agents run on your own AI provider account. Sign in once and pick the models. Change it any time in Settings › Models.
Cheap tasks
Mapping components and checking specs
RecommendedGPT-5.6 Luna
Complex tasks
Writing specs and judging findings
RecommendedGPT-5.6 Sol
your-repo
Welcome to Quint Studio
Here are some quick setup steps to get you started.
Usage limit
What the agents' provider calls may cost, over every project on this machine.
At the limit, Studio stops a task before its next call and starts no new one. You are warned first, so you can raise it.
your-repo
Welcome to Quint Studio
Here are some quick setup steps to get you started.
Connect agents to the Studio MCP
Any number of agents can be connected at once, each in its own config.
Sign in
The Quint Studio server
The functionality of the app is provided by a server. If you open the desktop app, the server will be running and you can use it also from your agents via MCP. If you want to avoid having the desktop app running, you can spawn just the server from the terminal.
The desktop app manages the server for you
Running • 0m 00s • your-model • $0.01
Or run the server yourself
# Studio should be started from your repository.cd ~/code/your-repo# Check that everything is in placequint-studio status# Then start Studioquint-studio servehttp://127.0.0.1:7000/?token=0123
In this mode, you can also access the graphical interface from your browser, including on other machines if you serve to the network.
Using Quint Studio while you make changes
Keep your agent connected to Studio. On top of the MCP server, the agent connection adds a Quint pane to Claude Code, OpenCode and Pi: open it with /quint.
- See where you standMisbehavior, Correctness and Coverage for the components your edits touch, and which have gone stale.
- Act on itUpdate a stale model after your code changes, fix behavioral problems and add missing tests.
- Review before you push
/quint review: findings, coverage gaps and behavior changes on your branch.
If your agent's harness doesn't support the pane, you can still use the same features directly through MCP: ask your agent to run a Quint review of this branch.
Frequently Asked Questions
Do I need to read any Quint?
No, but you can. We recommend you start reading properties and observations, and the traces that break a property or witness an observation. You can find those in the Correctness tab of a component. Reading the transitions listed in the Coverage tab will also give you a good sense of what is in the model.
Where are my Quint specs?
In Studio's data folder, outside your repository:
- Linux:
~/.local/share/co.quint.studio/projects/ - macOS:
~/Library/Application Support/co.quint.studio/projects/
Studio updates specs as your code evolves, and not everyone on your team may be using Studio yet, so for now they stay out of version control. Copy them into your repository if you want to track them.
How is this different from asking my agent to write Quint or TLA+ specs?
Studio breaks your codebase into components small enough to model well, writes each spec and property with modeling techniques and quality checks, and runs several specialized Quint procedures on it. Every property violation is judged against your code, and real bugs are reproduced with regular software tests. Studio also assess your test suite quality in relation to the specs transitions, and when your code changes, it tells you which specs are stale and updates them. So it empowers you maintain and leverage specs as your code evolves, instead of playing around with formal methods once and abandoning specs when changes come.
Can I use Quint Studio with my own model and agent harness?
You always use your own model: Studio's agents run on the provider you configures. Your own harness can talk to Studio over MCP and drive it's usage. For internal tasks, Studio runs its own harness, based on the Pi agent, for control and efficiency. You can think of Studio as a self-hosted agentic service.
Does Studio keep running in the background?
Studio runs while the desktop app is open, or quint-studio serve is running in one of your terminals. One Quint Studio instance is tied to one project, so you'll need multiple instances for multiple projects.
Can I run Studio on a server, in a container, or in Windows WSL?
Yes: quint-studio serve is a server, like VS Code's remote server. Set Studio up on that machine or environment, and reach both its graphical interface and its MCP server from outside, so your coding agent can keep running where you are. Have Studio listen on every interface, on ports you choose:
QUINT_STUDIO_OPERATOR_ADDR=0.0.0.0:7001 quint-studio serve --bind 0.0.0.0 --port 7000Open port 7000 in your browser, and point your agent's MCP configuration at port 7001, path /operator. In a container, publish both ports, to your host's loopback only:
docker run -p 127.0.0.1:7000:7000 -p 127.0.0.1:7001:7001 your-imageThe token in the printed address is all that stands between the interface's port and a service that runs agents on your repositories, and the MCP server has no token of its own: keep both ports off networks you don't trust, and put Studio behind TLS before it crosses one.
Something isn't working. Where do I start?
Run quint-studio status in your repository to see if anything is missing. If your agent is connected to Studio, it should have access to information to help you debug issues and unstuck yourself. Email us for help at contact@quint.sh.
Quint Studio is in Beta
We hope you have a good experience with our beta.
If you face issues or have feature requests, please don't hesitate to reach out!
Email us at contact@quint.sh or schedule a call via the in-app help center.