Quint Specifications

View as Markdown

Neutron Quint models stateful protocols with state variables, actions, and invariants. The repository includes database protocols, framework state machines, and real-time communication models.

Source layout

  • quint/specs/common/: shared types, network, and crash models.
  • quint/specs/nucleus/: Multi-Raft, resharding, distributed transactions, replication, membership, and snapshot transfer.
  • quint/specs/framework/: circuit breaker, rate limiter, CSRF, and session lifecycle.
  • quint/specs/realtime/: WebSocket hub and hot reload.
  • quint/tests/: scenario tests.
  • quint/conformance/: additional Quint scenarios and a Rust model harness.

A specification models a design. Its presence does not mean the corresponding production feature is complete or verified.

Run checks

From quint/, with Quint installed:

quint typecheck specs/framework/circuit_breaker.qnt
quint test tests/circuit_breaker_test.qnt
quint run --max-samples=1000 --max-steps=50 --invariant=reject_bound specs/framework/circuit_breaker.qnt

For model checking, install a compatible checker toolchain and choose the property and bounds explicitly:

quint verify --max-steps=20 --invariant=reject_bound specs/framework/circuit_breaker.qnt

Type checking checks specification structure. Tests exercise selected scenarios; quint run samples behaviors. quint verify uses a model checker. The current upstream CLI supports Apalache and an alternative TLC backend; consult the checker documentation and your installed CLI version.

Apalache bounded checks cover the configured model and execution bound. TLC can enumerate reachable states of a finite model. Neither establishes arbitrary production behavior merely because a check passes.

What the repository CI runs

scripts/ci.sh runs type checking, randomized simulation against declared invariants, Quint conformance scenarios, and Rust harness tests. The workflow also runs a canary that must detect a violated invariant. The script does not run quint verify; its success must not be described as exhaustive model checking.

Connection to application code

The Rust harness currently reimplements modeled state machines. It does not execute the production Nucleus engine. The proposed quint-connect dependency remains commented out, so live-engine conformance is unfinished.

The recommended next step is a small trace adapter against a real service, with deliberately faulty behavior that the adapter must detect. See the proposed integration architecture.