---
name: cscheck
description: Write and simplify C# property-based, model-based, and executable specification tests with CsCheck. Use for generators, shrinking, stateful command sequences, Spec guards and rules, implementation conformance, or replaying generated failures.
---

# 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](references/properties.md) |
| An implementation with a simpler reference representation | `SampleModelBased` / `SampleModelBasedAsync` | [Stateful and async tests](references/stateful-and-async.md) |
| A protocol or lifecycle with explicit state, guards, and requirements | `Spec.From`, then `Exhaustive` and `Conform` | [Executable specifications](references/specifications.md) |
| Async resources or expectations that must incorporate observed outcomes | Generated command arrays + `SampleAsync`, with cleanup inside each case | [Stateful and async tests](references/stateful-and-async.md) |
| A failing property, seed replay, or a before/after bug demonstration | Native sampling controls and a concrete regression | [Failure discovery and replay](references/failures.md) |

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`](https://github.com/AnthonyLloyd/CsCheck/tree/50503557f23266f140021f65632612ceb4ac248f).
Check the installed package before adapting signatures. For upgrades, verify the
[NuGet package](https://www.nuget.org/packages/CsCheck) and upstream source; do not infer a major version
or native async `Spec.Conform` support from another library's API.