Neutron Quint
Model how your system behaves when events race, messages arrive late, or a process fails. Protocol modeling for Neutron’s multi-language ecosystem.
Make the protocol explicit.
A service’s behavior spans more than one request. Sessions expire, workers retry, replicas exchange messages, and clients reconnect. Quint expresses those behaviors as states, actions, and invariants that can be explored independently of the implementation language.
Neutron already contains Quint models for database protocols, framework state machines, and real-time communication. The application-facing workflow and direct checks against live implementations are still in development.
Different checks answer different questions.
Type checking checks the specification’s structure. Scenario tests exercise selected traces. Random simulation samples possible behaviors. Model checking evaluates properties within the selected model and checker configuration.
The repository’s CI gate runs type checking, random simulation, Quint conformance scenarios, and a Rust model harness. A passing gate is not evidence that every reachable state or production execution has been checked.
Quint is the specification language. TLA+ is related specification technology; Apalache and TLC are model checkers. Current Quint supports both backends. See the Quint model-checker documentation for their different bounds and behavior.
Connect the model to the system.
The intended next step is to replay model traces against real Neutron services, compare observable results, and preserve failing traces as regression cases. That connection makes specifications useful across Rust, Go, Python, TypeScript, and other implementations.
Today the Rust conformance harness reimplements modeled state machines. It does not drive the live Nucleus engine. Direct model-to-implementation integration remains unfinished.
Part of the same Neutron system.
Neutron Lean is the planned home for reusable models and deductive proofs. Quint explores stateful protocols. Neutron Modelica simulates physical systems. Each contributes a different kind of evidence, with its assumptions and scope kept explicit.