CsCheck

Use CsCheck to explore inputs and action sequences; keep the application's contract visible in the test. Let the library generate, shrink, print, and replay counterexamples. Start with the smallest test that can falsify the claim, rather than building a testing framework around CsCheck.

Choose the test shape

What needs checking	Start with	Read when needed
A function, round trip, algebraic law, or data transformation	Gen + Sample	Properties and generators
An implementation with a simpler reference representation	SampleModelBased / SampleModelBasedAsync	Stateful and async tests
A protocol or lifecycle with explicit state, guards, and requirements	Spec.From, then Exhaustive and Conform	Executable specifications
Async resources or expectations that must incorporate observed outcomes	Generated command arrays + SampleAsync, with cleanup inside each case	Stateful and async tests
A failing property, seed replay, or a before/after bug demonstration	Native sampling controls and a concrete regression	Failure discovery and replay

Read only the references needed for the task. These examples use xUnit, but CsCheck itself is test-framework independent. Preserve the project's existing framework and package-management conventions.

Establish the contract first

Identify an observable requirement and a plausible wrong result it would reject. Separate generated inputs, expected behavior, and actual observations. A model may consume observations, but must validate them against prior expectations before accepting them as new state. Do not use the implementation's answer to manufacture its expected answer.

Generate individual operations and their arguments, allowing CsCheck to compose arbitrary sequences. Finite domains, weighted boundary values, and preconditions are legitimate modeling choices. Handwritten whole scenarios are useful regressions, but are not a substitute for exploring action orderings.

Keep rejected requests testable when rejection is part of the contract. A guard saying “only withdraw when funds exist” cannot test insufficient-funds rejection. Preconditions describe what can be attempted; postconditions describe the response, including allowed failures.

Keep the test machinery small

• Prefer composed Gen values to Random, hand-chosen seed lists, custom shrinkers, or retries-until-green.
• Construct a fresh mutable implementation and model for each generated case, including shrinking.
• Use ordinary records, direct calls, and meaningful comparisons. equal: must compare behavior or state; cleanup belongs in finally/using, not an equality predicate that always returns true.
• Keep seeds out of ordinary discovery runs. Replay a seed emitted by a failure, then pin concrete inputs when the regression must survive generator changes.
• Preserve domain coverage and historical counterexamples when simplifying. Fewer lines alone do not establish that the replacement checks the same behavior.

Verify the right thing

Spec.Exhaustive checks the model. Spec.Conform checks the real implementation through the adapter and only for sampled traces and compared observations. Keep both claims explicit. Inspect unreachable requirements, deadlocks, and search cutoffs; a green run can be vacuous.

When practical, show that the test rejects a known broken implementation or a small deliberate defect in an isolated copy. Compile and execute examples rather than assuming similarly named FsCheck APIs exist in CsCheck. Reuse native model-based APIs when their independent transitions and comparison fit; a custom async loop is a useful alternative, not a universal replacement.

API baseline

The linked examples were compiled and run with CsCheck 4.9.1 on .NET 8. Its package identifies source revision 5050355. Check the installed package before adapting signatures. For upgrades, verify the NuGet package and upstream source; do not infer a major version or native async Spec.Conform support from another library's API.