#quint-connect-moonbit

1. Quint generates one or more allowed execution traces.
2. The adapter reads those traces in Informal Trace Format (ITF).
3. A domain driver maps each Quint action to an operation in the MoonBit implementation.
4. After every action, the adapter compares an observable implementation snapshot with the state expected by Quint.

#Why this repository exists

• Action mapping: which implementation operation corresponds to each Quint action?
• Input mapping: how are Quint's nondeterministic choices decoded into implementation arguments?
• State projection: which implementation fields are observable and compared with the model?

#How it works

Quint specification
  -> quint run --mbt or quint test
  -> temporary ITF JSON traces
  -> parse_itf_with_config
  -> fresh MoonBit driver for each trace
  -> apply(action, nondet_picks)
  -> project(driver)
  -> compare with expected Quint state

• mbt::actionTaken: the action selected for the step
• mbt::nondetPicks: values selected by relevant nondet expressions

#Quick start

• the MoonBit toolchain installed at ~/.moon/bin
• Nix with flakes enabled, or local installations of Quint 0.32, just, and rg

nix develop -c just check

just check

#Repository layout

#Core API

#Trace parsing

• parse_itf(text) parses standard quint run --mbt --out-itf output.
• parse_itf_with_config(text, config) additionally projects nested state and custom action data.
• TraceConfig.state_path selects the model state that should be decoded by the domain adapter.
• TraceConfig.nondet_path selects a custom Quint variant containing the action tag and its arguments.
• required_nondet and optional_nondet decode named choices after Quint Some/None normalization.
• decode_itf_bigint decodes the canonical ITF #bigint representation without precision loss.
• decode_itf_int converts an ITF integer only after checking the MoonBit 32-bit Int range.

#Stateful replay

apply    : (Driver, String, Json) -> Result[Driver, String]
project  : (Driver) -> Snapshot
expected : (Json) -> Result[Snapshot, String]

#Stateless replay

#Trace generation

• RunConfig describes randomized simulation with quint run --mbt.
• TestConfig describes a named scenario selected with quint test --match.
• runner.generate_run and runner.generate_test start Quint, collect all generated ITF files, and parse them.
• CLI seed precedence is explicit: command-line seed, then QUINT_SEED, then a generated seed.

#Failure model

#Examples

• an executable Quint model (*.qnt)
• a MoonBit driver that maps actions and decodes expected state
• a runnable native executable under cmd/
• MoonBit contract tests
• a deliberate broken mode used by the integration script

#Relationship to official Quint Connect

#Guarantees and limitations

• every generated trace was accepted by the driver;
• every selected action and nondeterministic input was mapped successfully;
• every field included in the state projection matched after every checked step.

• the implementation is formally verified;
• all possible executions were explored;
• fields omitted from the projection are correct;
• real network, clock, concurrency, failure injection, or external I/O semantics were tested;
• the Quint specification itself correctly represents the intended system.

• Quint sets, maps, tuples, and variants remain raw ITF JSON until a domain adapter decodes them.
• ITF requires every integer, large or small, to use { "#bigint": "..." }; JSON numbers are rejected by the decoder.
• decode_itf_bigint uses MoonBit core BigInt, preserving values such as 2^53 + 1 on JavaScript, Wasm, and native.
• decode_itf_int is an explicit narrowing operation. Domains that need arbitrary precision should retain BigInt instead of converting it.
• Action callbacks are synchronous. Async production operations need an additional driver abstraction.
• Quint's --mbt metadata is documented as experimental and may change between Quint versions.

#Development commands

just fmt          # format MoonBit source
just --fmt        # format the justfile
just fmt-check    # verify MoonBit formatting
just typecheck    # all-target MoonBit type checking with warnings denied
just test-js      # 16 unit/contract tests on JavaScript
just test-wasm    # the same 16 tests on Wasm
just test-native  # the same 16 tests on native
just test         # run all three runtime test suites
just wasm-demo    # replay an embedded ITF trace in Wasm
just integration  # generate and replay real Quint traces on native
just check        # run everything

#References

• Quint model-based testing
• Quint CLI and --mbt metadata
• Official Quint Connect for Rust
• Quint Connect announcement
• Informal Trace Format

#License