In Kotest's property-testing module, what is the difference in contract between `checkAll`, `forAll` and `forNone`, and how does each one decide that a property has failed?

## Two contracts, one engine Kotest's property testing (artifact `kotest-property`, package `io.kotest.property`) drives the same machinery in every case: build a stream of values from the supplied generators, run the body once per value, and on failure shrink the input down to a minimal counter-example and report it. What differs between the entry points is **the contract of the lambda you hand it** — and therefore how the engine learns that this iteration failed. ## `checkAll` — the assertion contract `checkAll` takes a lambda returning `Unit`. The body is an ordinary test body: you use Kotest matchers (`shouldBe`, `shouldContain`, `shouldThrow`, …) or any assertion mechanism that throws on failure. An iteration is a failure exactly when the block throws. ```kotlin checkAll(Arb.int(), Arb.int()) { a, b -> (a + b) shouldBe (b + a) } ``` Because the failure is an exception, the exception's message travels into the property failure report. You see the matcher's expected/actual diff *and* the inputs that produced it. That is the whole reason `checkAll` is the default choice in real suites: a red property test tells you what was wrong, not merely that something was. ## `forAll` / `forNone` — the predicate contract `forAll` takes a lambda returning `Boolean`. The property holds if every iteration returns `true`; it fails at the first `false`. ```kotlin forAll(Arb.string(), Arb.string()) { a, b -> (a + b).length == a.length + b.length } ``` `forNone` is the mirror image: it asserts the predicate is `false` for *every* generated value, failing at the first `true`. It expresses "no input in this space satisfies P" — e.g. no value produced by a sanitiser generator still contains a control character. Semantically `forNone { p }` and `forAll { !p }` agree, but `forNone` states the intent and reports it that way. The cost of the predicate contract is diagnostic poverty. When a boolean property fails you get the (shrunk) inputs and "property failed", nothing about which sub-expression was wrong. For a one-line law that is fine; for a multi-step property it is a debugging tax. ## Failure detection, shrinking and reporting On failure the engine does the same thing for all three: it records the failing inputs, runs shrinking to find a smaller input that still fails, and raises an `AssertionError` describing the property (attempt number, shrunk inputs, the underlying cause when there was one, and the seed to reproduce the run). By default the run **stops at the first failure** — it does not keep going and collect every failing input. That behaviour is only changed by raising `maxFailure` on `PropTestConfig`, which lets the run tolerate a budget of failures before it gives up. ## A type-system trap worth knowing Kotest matchers are not `Boolean`-returning — `shouldBe` returns the receiver value. So writing an assertion as the last expression of a `forAll` block is usually a *compile* error (`Unit`/`T` where `Boolean` is expected), which is the compiler telling you that you wanted `checkAll`. The one dangerous case is a property over `Boolean` values, where the types line up and the assertion result silently becomes the predicate. If your lambda contains matchers, use `checkAll`. Also note the name collision: `io.kotest.inspectors.forAll` is the *inspector* that asserts something about every element of an existing collection, and has nothing to do with property testing. If `forAll` behaves unexpectedly, check the import. ## Choosing between them - Use **`checkAll`** by default: for anything with more than one assertion, anything where the expected value is computed, and anything a colleague will have to debug at 3am. - Use **`forAll`** for compact algebraic laws — commutativity, associativity, idempotence, round-trips — where the boolean *is* the law and reads better than an assertion. - Use **`forNone`** to state a negative invariant explicitly, so the intent survives in the test name and the failure message. Both families accept the same configuration surface (explicit iteration counts, a `PropTestConfig`), the same generators, and the same arity overloads, so switching between them is mechanical — the choice is purely about how much the failure message needs to say.