Stay in CommandBy Understanding What Matters

Name: Quint
Author: Informal Systems

Quint Studio is your structured way to adopt formal methods and learn as you get value. The more you check, the more you understand.

SEE HOW IT WORKS

DOWNLOAD FREE BETALinux and macOS

WORKSPACE

shop

shop1

Orders1

Payments

CartSETUP 1/3

MCP · Your harness

Chip, the beaver

chip@quint.sh

shop

Code

Misbehavior1 open · 0 fixed

Correctness10 of 11 · 1 broken

Coverage12 of 40 tested

Modeled2 of 5 components

Select components0★ Recommended

1 component selectedView selection ▾Set up Quint110+ min per component

Peripheral

Cart

not modeled

Central

Payments

4/16 tested

modeled

Central

Inventory

not modeled

Central

Orders

8/24 tested

modeled1 misbehavior

★ RecommendedCentral

Returns

not modeled

← CartRunning…■ Stop

1Model

2Check

3Reproduce

Running • 0m 00s • your-model • $0.01

Execution Logs

Starting the model

Quint specDraft

cart/cart.qnt

Code is scaling.
Understanding isn't.

Developers need to understand how their software works, how it behaves, and the implications of changes, but traditional development workflows don't scale with AI-generated code.

Don't Drown in Markdown

If you switched from reading code to reading markdown files as your main activity, Quint specs can bring you the executability you are missing.

glossary.md

disputes.md

inventory.md

refunds.md

sessions.md

payments.md

checkout.md

## Retries

A payment retry should never charge the customer twice. Expired sessions release their items.

## Provider timeouts

When the provider times out we re-queue the order, unless it was already accepted, in which case we settle it and move on.

ReadableStaticDrifts from code

checkout.qnt

invariant settledOnce =
  payments.forall(p =>
    p.settlements.size() <= 1)

ReadableRuns & checksStays in sync

retry.test.ts

ledger.ts

provider.ts

session.ts

settle.ts

queue.ts

retry.ts

export async function retry(ord, n, ctx) {
  const res = await prov.charge(ord, ctx)
  if (res.status === 408 && !ctx.idem) {
    await queue.push({ ...ord, try: n+1 })
  } else if (await prov.accepted(ord.id)) {
    await settle(ord, { force: true })
  }
  return res
}

RunsToo detailed

How Quint Works

Your codebase is broken down into components

Capturing your whole code base in one huge state machine wouldn't be helpful. Quint Studio breaks it up into multiple components so you can reason about it one state machine at a time.

Cart

not modeled

Payments

not modeled

Inventory

not modeled

Orders

★ Recommended

Returns

not modeled

Agents write a Quint specification

The spec is authored automatically taking your code and documentation as input. Modeling techniques and several checks are applied to ensure the spec meets quality standards.

← OrderRunning…■ Stop

1Model

2Check

3Reproduce

Running • 5m 00s • your-provider/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:53Reading src/modules/order/service.ts09:42:53Model order started

Quint specDraft

order/order.qnt

module order {
  type Status = Draft | Pending | Completed | Archived | Canceled

  type OrderState = {
    version: int,
    status: Status,
    canceled_at: bool,
    item_total: int,     // summary item_total at the current version
    expected_item: int,  // independently tracked correct item_total
    paid_total: int,
    fulfilled: bool,
  }

Issues get reproduced against code in a test

Each violation found by Studio is judged, and real bugs are reproduced as a test against your code. Interactively explore the behavior to understand the violation better.

Hover over the property to understand what broke

no_orphaned_return Confirmed Product bug

Undoing the last change strands a return created on top of it.

Found by the model no_orphaned_return violated in a run of up to 20 steps

Propertyat state 5false

val no_orphaned_return: bool = RETURNS.forall(r‹1/1› => not(returns.get(r).activetrue and not(returns.get(r).deleted)true and returns.get(r).order_version > orders.get(returns.get(r).order_id).versiontrue))

Behavior

0 Initial state›1 Create orders›2 Create order change›3 Confirm order change›4 Create returns›5 Undo last change

Reproduced by a test

packages/modules/order/integration-tests/__tests__/undo-change-return.spec.ts

Undoing an order change does not strand a return created on top of it

it('does not strand a return when the last change is undone', async () => {
  const order = await anOrder({ status: 'pending' })
  await service.confirmOrderChange(await aChange(order.id))
  const ret = await service.createReturn({ order_id: order.id })
  await service.undoLastChange(order.id)
  const current = await service.retrieveOrder(order.id)
  expect((await service.retrieveReturn(ret.id)).order_version)
    .toBeLessThanOrEqual(current.version)
})

No fix proposed yet

Keep specs in your workflow and check behavioral changes

Quint plugs into your coding agent. When a change touches a modeled component, Studio checks if the spec needs to be updated and flags any new violations.

>Can we deduct items from the inventory when adding them to a cart, to reduce the failure rate of checkouts?

⏺Checkouts fail when stock sells out before payment. I'll take items out of inventory as they're added.

⏺Search(pattern: "inventory", path: "src/modules/cart")

⎿Found 2 files

⏺Read(src/modules/cart/service.ts)

⎿Read 184 lines

⏺Update(src/modules/cart/service.ts)

⎿Updated src/modules/cart/service.ts with 2 additions

52 async addItem(cartId, item) {

53 + await this.inventory.take(item.sku, item.qty)

...

91 const item = cart.find(itemId)

92 + await this.inventory.put(item.sku, item.qty)

⏺Bash(npm test -- cart)

⎿Tests: 42 passed, 42 total

⏺Done: adding an item takes it out of inventory, and removing it puts it back.

Cart outdated ✓ 3/4 tested 8/12

Quint

Base mainRefresh

‹CartoutdatedUpdate

Misbehavior ░░░░░░░░░░░░ 0 open issues

Correctness █████████░░░ 3/4 1 broken

Coverage ████████░░░░ 8/12 tested

Todo

Cart → Update

▾ Properties 3/4

✓ itemsNeverNegative✓ paidCartsHoldStock

✗ addedItemsCountedOnce

// each unit: in stock, in a cart or soldval addedItemsCountedOnce = VARIANTS.forall(v => available.get(v) + held(v) + sold.get(v) == STOCK.get(v))

✓ completedCartsAreClosed

▸ Tests 8/12

▸ Bugs 0 open

The result: A continuously maintained source of control over your software, from design through development and production.

Quint is battle-testedand Studio packages what those battles have taught us

Quint, the language, is open source. It launched in 2022 and has been used across industries since, from databases and protocols to UI interactions.

10+ bugs found and fixed in SQLite

An open-source contributor modeled SQLite’s C API in Quint and replayed its traces against the real library.

Read the Turso post →

10 gaps found in Ethereum’s SEACAST

The broadcast protocol’s Quint model, checked by simulation and TLC, found gaps in delivery and expiry; 8 are already fixed. One of many blockchain protocols specified in Quint.

Read on Ethereum Research →

Quint is an excellent lightweight approach to formal verification, particularly well suited for systems that are still evolving. It allowed us to reach a high degree of confidence in the correctness and security properties of our systems — and helped surface a surprising number of issues that would otherwise have been difficult to detect.

Denis Firsov,Input Output Group

Quint’s typed, executable spec language, with clean syntax and TLA+-style semantics, makes modeling complex state machines and invariants like lock-free ring buffer safety genuinely straightforward. The quint-connect crate generates ITF traces I replay against real Rust code, combined with proptest fuzzing to verify that atomic usage and lock-free primitives match the spec under all interleavings.

Debasish Ghosh,Conviva

Quint has been an invaluable tool for my AI agents to find implementation bugs or specification flaws in distributed systems protocols and implementations. My belief is that a formal language lets the models see the big picture and reason beyond the limits of their current context window. Right now, multiple file and whole system reasoning is still a pain point for models and working with formal tools like Quint is a powerful strategy for producing reliably software.

Zaki Manian,iqlusion

Quint is by far the most approachable formal specification tool I’ve seen. Using it alongside an agent, we were able to quickly formalize an existing system and find real production bugs on our very first attempt. This allowed us to get a handle on some subtle synchronization logic that had eluded us for months. Consider adding Quint to your toolbox!

Ray Myers,Chief Architect at OpenHands