Start with the queue example. Core replay needs only .NET and FSharp.Core. Tool generation, sampled exploration, bounded verification and implementation replay are distinct evidence; the library does not turn one into another.
Itf.read accepts bytes and explicit limits, returning an ItfDocument or diagnostics.
Defaults bound bytes (16 MiB), depth (64), states (10,000), and collection members
(100,000). It rejects invalid UTF-8, duplicate object keys, duplicate set members/map
keys, malformed or unsupported tagged values, invalid state ordinals and binding drift.
Raw metadata is not a success verdict. Action/source attribution is caller-owned.
Supported raw values: null, booleans, strings, exact decimal integers / #bigint, arrays,
#set, #tup, #map, and ordinary records. Quint 0.32.0 variants are tag/value records;
these stay lossless records. Map keys are arbitrary values; tuples never become lists.
The rich fixture in tests/values.itf.json was generated by Quint 0.32.0's TypeScript
evaluator because its Rust evaluator rejects integers outside signed 64-bit range.
The reader preserves arbitrary magnitudes independently of the evaluator.
QuintReplay retains schema-v1 values and fingerprints from SDD. That envelope's value
subset has no tuple or map case; its decoder rejects those tags. Use the raw reader
and an explicit domain projection when richer values are required. Itf.canonical
is raw canonicalization v1 and is distinct from schema-v1 replay canonicalization;
use it with decoded, valid values. Neither identity implies authenticity.
Build states using QuintReplay.stateFingerprint, supply consumer-owned actions,
source positions and environment fingerprints, then compute traceFingerprint.
Replay.run timeout cancellation driver trace validates the complete trace before
Initialize, observes initial state, and applies/observes each step once. It stops at
the first mismatch. Initial divergence has no invented action/source. Difference paths
identify the first differing top-level binding; nested structural diff is not claimed.
A successful test requires Outcome = Equivalent and CleanupFailure = None.
Observe must supply valid state fingerprints. Driver exceptions become DriverFailure;
cleanup errors remain separate so they never hide the original result. Initialize
must dispose partially created resources if it fails before returning a runtime.
Cancellation/deadlines require cooperative callbacks. Cleanup uses a fresh token and
can itself block: isolate untrusted code in a worker process for hard deadlines.
Apply is never retried automatically.
FsQuint.Tooling.Quint.run takes an absolute tool path, SHA-256, version, directory,
source/module, typed command and finite process limits. It invokes argument arrays
without a shell. Supported: Linux x64, Quint 0.32.0, Rust backend for tests/samples.
Named tests need a positive executed count. Sample success needs the supported Quint
result and trace-statistics markers. Counterexamples are distinct from incomplete,
nonzero exit, timeout, cancellation, output overflow and identity failure. Typechecking
uses Quint's exit contract and makes no replay/verification claim. Output limits apply
to each invocation; the request deadline includes hashing and version selection.
Owned process trees are terminated on cancellation/overflow on the qualified platform.
This is not a sandbox against malicious executables or detached processes.
Neither package downloads or installs tools itself. The external Quint process may attempt downloads if its evaluator is missing; offline users must provision both tools as described below and restore packages from a prepopulated NuGet cache. FsQuint version updates never select a new Quint version automatically.
Quint 0.32.0 uses Rust evaluator 0.6.0 for the supported test/run matrix. Provision both before running checks; otherwise Quint itself attempts a GitHub API download. The repository provisioning script verifies both published asset checksums and is used by CI and release qualification. The library does not invoke this script.
bash eng/provision-quint.sh /tmp/fsquint-tools
QUINT_BIN=/tmp/fsquint-tools/quint QUINT_HOME=/tmp/fsquint-tools/home bash eng/check.shCallers running the optional tooling package provide the same QUINT_HOME when
using this provisioned evaluator. Package updates do not upgrade either tool.