The initial state of the model, before any actions are performed. Any transactions submitted during initialization will not be subjected to tests. If you want to test the initialization transactions, you can add an initialization action, and keep the initialize method minimal.

Generate a random action given the current state. The generated action should be appropriate for the current state.

Precondition that must hold before an action can be executed. Return False to indicate that an action is not valid in the current state. Default: all actions are always valid.

Perform the action on the real blockchain (mockchain). This should execute the actual transaction(s) that implement the action. The current model state is provided to allow access to tracked blockchain state. The returned state should reflect the expected effect of the action on the contract state.

Validate that the blockchain state matches the model state. Default: no validation (always succeeds).

Called after each successful action to wrap the enclosing QuickCheck property. This hook runs only after perform and validate succeed. Use it for property-level checks, labels, and counterexamples that should be attached to valid state transitions. Default: no additional checks.

Whether to discard (skip) test cases where the invalid action fails due to a user-level error (e.g., off-chain balancing failure) rather than an on-chain validator rejection during negative testing.

When True, negative tests that throw user exceptions are discarded (via QuickCheck's discard), so only on-chain rejections count as successful negative tests.

When False (the default), user exceptions also cause the test case to be discarded — meaning both off-chain and on-chain failures are treated the same way.

Override this in your TestingInterface instance if you need finer control over which failure modes are accepted in negative testing.

Optional RedeemerTagger (Tier 2) that maps a script input's parsed Plutus redeemer Data to a human-readable RedeemerTag (label + optional JSON payload). The label surfaces in the streamed TxInputSummary as redeemerKind / redeemerPayload.

Default: a no-op tagger, so Tier 1 (redeemerRaw / redeemerConstr) is still streamed and Tier 2 fields stay Nothing. See autoRedeemerTag and labelRedeemer for ergonomics.

Optional AddressLabeler that maps an address's credential hash to a human-readable label. The label surfaces in the streamed TxInputSummary / TxOutputSummary as addressLabel.

Default: mockWalletAddressLabeler, which labels the standard mock wallets (mockWallets) as "Wallet 1".."Wallet 10". Since those are the wallets nearly every test already uses, this default costs nothing and rarely needs overriding — extend it with (<>) to add labels for a model's own script hashes or extra keys.

Threat models the contract claims to resist. This is a coverage claim, checked in both directions: a listed model that never applies to any generated transaction fails the suite (the claim is unverifiable), and one that finds a vulnerability fails it too (the claim is false).

Default: nothing claimed. Listing a model here is the outcome of triage — you ran it, saw that it applies, and saw the contract hold. Models you have not triaged belong in candidateModels, which is where they start.

Threat models run for information rather than as a claim: reported, but never failed for not applying. This is where every model starts, and what an empty instance runs.

Default: every parameterless threat model not already spoken for by another slot. A detection still fails — a finding is a finding, whether or not you asked for the model — but the message asks you to triage it into threatModels, expectedVulnerabilities, acceptedFindings or notApplicable rather than accusing the contract of a broken promise.

Set to [] to opt out of the survey entirely.

Vulnerabilities the contract is known to have, each with the reason it is declared. Inverted pass/fail: detecting one is the required outcome, and failing to detect it means the contract (or the attack) improved and this declaration is now stale.

The reason travels into the failure message and the streamed summary, so a stale entry explains itself. Write what a reader six months from now needs in order to tell a deliberate declaration from an unexamined one.

Use this only for *genuine* vulnerabilities. A benign finding — an attack that "succeeds" against a design artifact that is not exploitable — belongs in acceptedFindings: listing it here advertises the contract as vulnerable, and fails the suite the moment the finding stops being reproduced.

Findings that are known, accepted artifacts of the contract's design rather than exploitable bugs, each with the reason it is accepted. A detection is the required outcome, and the report labels it as accepted by design rather than as a vulnerability.

Judged exactly like expectedVulnerabilities - an acceptance is a declaration too, so the case fails when the run disproves it ("NO LONGER DETECTED") or never verifies it. What differs is only what the declaration means: this slot says the attack lands on something harmless, where expectedVulnerabilities says the contract has a bug nobody has fixed. Prefer this one for anything that is not genuinely exploitable - the other advertises the contract as vulnerable in every report.

Threat models reviewed and found not to apply to this contract, each with the reason. The inverse claim to threatModels: these must not apply, and one that starts applying fails the suite.

That is the point of the slot. "Does not apply here" is a prediction about the contract's transaction shapes, and predictions break — a contract that grows a script output, or a harness change that widens what counts as applicable, should tell you rather than pass in silence. Deleting a model from the lists instead records the same triage where nothing can check it.

A generator for values of the given type.

It is worth spending time thinking about what sort of test data you want - good generators are often the difference between finding bugs and not finding them. You can use sample, label and classify to check the quality of your test data.

There is no generic arbitrary implementation included because we don't know how to make a high-quality one. If you want one, consider using the testing-feat or generic-random packages.

The QuickCheck manual goes into detail on how to write good generators. Make sure to look at it, especially if your type is recursive!

Produces a (possibly) empty list of all the possible immediate shrinks of the given value.

The default implementation returns the empty list, so will not try to shrink the value. If your data type has no special invariants, you can enable shrinking by defining shrink = genericShrink, but by customising the behaviour of shrink you can often get simpler counterexamples.

Most implementations of shrink should try at least three things:

1. Shrink a term to any of its immediate subterms. You can use subterms to do this.
2. Recursively apply shrink to all immediate subterms. You can use recursivelyShrink to do this.
3. Type-specific shrinkings such as replacing a constructor by a simpler constructor.

For example, suppose we have the following implementation of binary trees:

data Tree a = Nil | Branch a (Tree a) (Tree a)

We can then define shrink as follows:

shrink Nil = []
shrink (Branch x l r) =
  -- shrink Branch to Nil
  [Nil] ++
  -- shrink to subterms
  [l, r] ++
  -- recursively shrink subterms
  [Branch x' l' r' | (x', l', r') <- shrink (x, l, r)]

There are a couple of subtleties here:

• QuickCheck tries the shrinking candidates in the order they appear in the list, so we put more aggressive shrinking steps (such as replacing the whole tree by Nil) before smaller ones (such as recursively shrinking the subtrees).
• It is tempting to write the last line as [Branch x' l' r' | x' <- shrink x, l' <- shrink l, r' <- shrink r] but this is the wrong thing! It will force QuickCheck to shrink x, l and r in tandem, and shrinking will stop once one of the three is fully shrunk.

There is a fair bit of boilerplate in the code above. We can avoid it with the help of some generic functions. The function genericShrink tries shrinking a term to all of its subterms and, failing that, recursively shrinks the subterms. Using it, we can define shrink as:

shrink x = shrinkToNil x ++ genericShrink x
  where
    shrinkToNil Nil = []
    shrinkToNil (Branch _ l r) = [Nil]

genericShrink is a combination of subterms, which shrinks a term to any of its subterms, and recursivelyShrink, which shrinks all subterms of a term. These may be useful if you need a bit more control over shrinking than genericShrink gives you.

A final gotcha: we cannot define shrink as simply shrink x = Nil:genericShrink x as this shrinks Nil to Nil, and shrinking will go into an infinite loop.

If all this leaves you bewildered, you might try shrink = genericShrink to begin with, after deriving Generic for your type. However, if your data type has any special invariants, you will need to check that genericShrink can't break those invariants.