Property Based Testing
Writes, reviews, and debugs property-based tests, Hypothesis, fast-check, proptest...
Install
npx skills add trailofbits/skills --skill property-based-testing -g -a claude-code -y- Repository
- trailofbits/skills7.9k
- Category
- Design
- Updated
- 7d ago
- License
- CC-BY-SA-4.0
- Context cost
- Lightabout 843 tokens
- Runs scripts
- No, instructions only
What it does
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.
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.
