tool

Quint Verification

27 Quint specs covering Nucleus, framework, and realtime protocols. Multi-Raft consensus, resharding, distributed transactions, presence CRDTs — modeled and explored before the implementation.

Break the design before the design breaks production.

Available

27Spec Files

12Invariant Tests

TLA+Model Checker

TS-likeSyntax

Design bugs are the expensive ones.

Distributed systems don't fail where your tests look. They fail when a message arrives in the wrong order, a node crashes mid-commit, a network partition flips a leader. Quint lets you model the protocol first, explore every reachable state with TLC under the hood, and find the 40-step trace that violates your invariant — before you write a line of Go or Rust.

specs/raft/log_safety.qnt
module raftLogSafety {
  var log: Node -> List[Entry]
  var commitIndex: Node -> Int
  var currentTerm: Node -> Int

  action appendEntry(leader: Node, follower: Node, entry: Entry): bool = {
    // ... transition rules ...
  }

  val logMatchingInvariant =
    forall n1, n2 in nodes:
      forall i in 0.to(min(length(log.get(n1)), length(log.get(n2))) - 1):
        log.get(n1)[i].term == log.get(n2)[i].term
          implies log.get(n1)[i] == log.get(n2)[i]
}
Simplified fragment. The real spec models elections, replication, and crash recovery.

Nucleus specs

Multi-Raft replication, resharding, distributed transactions, vector-clock merge rules. Each spec has invariant properties checked exhaustively.

Framework specs

Middleware ordering, request-context isolation, graceful-shutdown drain semantics — the protocol-level guarantees the SDKs must uphold.

Realtime specs

Presence CRDTs, channel membership under node failure, pubsub fan-out ordering. Correctness you can't get from testing alone.

Modern syntax

TypeScript-ish keywords, structural types, pattern matching. Compiles to TLA+ where the actual checking happens.

Simulation mode

Run randomized simulations for fast feedback (seconds). Switch to exhaustive checking for the final pass (minutes).

Counterexample traces

When an invariant fails, Quint prints the exact sequence of events that violated it. Fix the design, re-run.

	Unit tests	Integration tests	Quint + TLC
Concurrency coverage	One interleaving	A few	Every reachable state
Failure modes	Mocked manually	Chaos tools sample	All crash / delay combos
Runs in	Milliseconds	Seconds	Seconds to minutes
Caught before implementation	No	No	Yes
Output when broken	Assertion fail	Flaky test	Exact counterexample trace

Where this shows up in Neutron

Every distributed protocol in Nucleus has a Quint spec. When we design a new one — say, a change to resharding — the spec comes first. We run exhaustive model checking, fix the invariant violations the checker finds, and only then implement. The spec and the implementation live in the same repo; they drift together, they're reviewed together.

What about my application code?

You don't need to write Quint specs for a regular web app — the hard protocols are ours to verify. If you're designing a custom distributed algorithm, Quint is the tool. If you want to verify Rust implementation code, use Shuttle or Kani instead.

Part of a bigger system

Quint at the design layer. Lean 4 for algorithm-level correctness. Verus for Rust code proofs. Shuttle for concurrency bugs in running Rust. Four complementary tools; each finds what the others can't.