Property-Based Testing
An example test asserts one point. A property asserts a rule over the whole input
domain and lets the generator hunt for the counterexample. That trade is worth making
when the code has an algebraic shape — an inverse, an invariant, an oracle — and not
otherwise. Code with no such shape gets example tests; saying so is a valid outcome.
Check first whether the shape is missing or merely buried. A calculation wrapped in I/O,
a string built by concatenation, an in-place mutation — each has a property and no seam
to assert it through. See references/refactoring.md before
concluding there is nothing to assert.
Property catalog
| Property |
Formula |
Where it applies |
| Roundtrip |
decode(encode(x)) == x |
Serialization, conversion pairs |
| Inverse |
f(g(x)) == x |
encrypt/decrypt, compress/decompress |
| Oracle |
new(x) == reference(x) |
Optimization, refactoring, reimplementation |
| Idempotence |
f(f(x)) == f(x) |
Normalization, formatting, sorting |
| Invariant |
Holds before and after |
Any transformation, contract state |
| Easy to verify |
is_sorted(sort(x)) |
Complex algorithms with cheap checkers |
| Commutativity |
f(a, b) == f(b, a) |
Binary and set operations |
| Associativity |
f(f(a,b), c) == f(a, f(b,c)) |
Combining operations |
| Identity |
f(x, e) == x |
Operations with a neutral element |
Strength ordering, weakest to strongest:
no crash → type preservation → invariant → idempotence → roundtrip / oracle.
Assert the strongest property the code supports. "No crash" alone rarely justifies the
dependency — if that is all you can find, either a small rearrangement exposes something
stronger, or the honest report is that this code is a poor PBT candidate. Rule out the
first before settling for the second.
The two ways a property test asserts nothing
- Tautology.
assert add(a, b) == a + b restates the implementation; no bug they
share can fail it. Pick a property that constrains the function without recomputing
it. Note the exception: f(x) == f(x) is a genuine determinism property when f
is not obviously pure — serializers over dicts or sets, hashing, anything reading
the clock.
- Vacuity.
assume() that filters out nearly every input passes without
exercising anything, and self-contradictory assume() passes having run zero cases.
Push constraints into the strategy so the generator produces valid inputs directly.
Where to look next
Load the one that matches the task in front of you:
| Task |
File |
| Writing new tests, designing strategies |
references/generating.md |
| The code has no property to assert yet |
references/refactoring.md |
| Reviewing existing property tests |
references/reviewing.md |
| A property test just failed |
references/interpreting-failures.md |
| Library choice, Echidna and Medusa |
references/libraries.md |
Introducing PBT to a project that lacks it
If the project already uses a PBT library, just write the tests in it. If it does not,
adding one is a dependency decision that belongs to the user — offer it once with the
specific property you would write, and take the answer either way.
1---2name: property-based-testing3description: Writes, reviews, and debugs property-based tests — Hypothesis, fast-check, proptest, jqwik, rapid, and Echidna or Medusa for Solidity invariants. Use whenever tests should cover a whole input domain instead of a hand-picked list of examples: encode/decode and serialize/deserialize pairs, parsers, canonicalizers and normalizers, validators, numeric and Decimal types, comparators and sort order, data structures, and smart-contract state invariants. Also use when adding cases to an existing @given, fast-check, or proptest suite, when judging whether existing property tests assert anything real, and when a generator has shrunk a counterexample and you need to tell a wrong property from a genuine bug. Not for coverage-guided binary fuzzing (libFuzzer, AFL), mutation-testing campaigns, static analysis, benchmarking, or end-to-end UI tests.4---5
6# Property-Based Testing
7
8An example test asserts one point. A property asserts a rule over the whole input
9domain and lets the generator hunt for the counterexample. That trade is worth making
10when the code has an algebraic shape — an inverse, an invariant, an oracle — and not
11otherwise. Code with no such shape gets example tests; saying so is a valid outcome.
12
13Check first whether the shape is missing or merely buried. A calculation wrapped in I/O,
14a string built by concatenation, an in-place mutation — each has a property and no seam
15to assert it through. See [references/refactoring.md](references/refactoring.md) before
16concluding there is nothing to assert.
17
18## Property catalog
19
20| Property | Formula | Where it applies |
21|---|---|---|
22| Roundtrip | `decode(encode(x)) == x` | Serialization, conversion pairs |
23| Inverse | `f(g(x)) == x` | encrypt/decrypt, compress/decompress |
24| Oracle | `new(x) == reference(x)` | Optimization, refactoring, reimplementation |
25| Idempotence | `f(f(x)) == f(x)` | Normalization, formatting, sorting |
26| Invariant | Holds before and after | Any transformation, contract state |
27| Easy to verify | `is_sorted(sort(x))` | Complex algorithms with cheap checkers |
28| Commutativity | `f(a, b) == f(b, a)` | Binary and set operations |
29| Associativity | `f(f(a,b), c) == f(a, f(b,c))` | Combining operations |
30| Identity | `f(x, e) == x` | Operations with a neutral element |
31
32Strength ordering, weakest to strongest:
33`no crash → type preservation → invariant → idempotence → roundtrip / oracle`.
34
35Assert the strongest property the code supports. "No crash" alone rarely justifies the
36dependency — if that is all you can find, either a small rearrangement exposes something
37stronger, or the honest report is that this code is a poor PBT candidate. Rule out the
38first before settling for the second.
39
40## The two ways a property test asserts nothing
41
42- **Tautology.** `assert add(a, b) == a + b` restates the implementation; no bug they
43 share can fail it. Pick a property that constrains the function without recomputing
44 it. Note the exception: `f(x) == f(x)` is a genuine determinism property when `f`
45 is not obviously pure — serializers over dicts or sets, hashing, anything reading
46 the clock.
47- **Vacuity.** `assume()` that filters out nearly every input passes without
48 exercising anything, and self-contradictory `assume()` passes having run zero cases.
49 Push constraints into the strategy so the generator produces valid inputs directly.
50
51## Where to look next
52
53Load the one that matches the task in front of you:
54
55| Task | File |
56|---|---|
57| Writing new tests, designing strategies | [references/generating.md](references/generating.md) |
58| The code has no property to assert yet | [references/refactoring.md](references/refactoring.md) |
59| Reviewing existing property tests | [references/reviewing.md](references/reviewing.md) |
60| A property test just failed | [references/interpreting-failures.md](references/interpreting-failures.md) |
61| Library choice, Echidna and Medusa | [references/libraries.md](references/libraries.md) |
62
63## Introducing PBT to a project that lacks it
64
65If the project already uses a PBT library, just write the tests in it. If it does not,
66adding one is a dependency decision that belongs to the user — offer it once with the
67specific property you would write, and take the answer either way.
gabrielmoreira