property-based-testing
- Use it when:
- Code has an algebraic shape, such as encode/decode pairs, parsers, normalizers, sort order or contract state, that example tests only spot-check.
- It does:
- Picks the strongest property the code supports from a catalog, and loads its guide for writing, refactoring, reviewing or reading a failure.
- You get:
- Property tests in the project's existing library, a review of existing ones, or a verdict that the code suits example tests better.
- Catches:
- Tests that restate the implementation, and assume() filters that let nearly every case pass untested.
- Works with:
- Hypothesis, fast-check, proptest, jqwik, rapid, and Echidna or Medusa for Solidity.
TL;DR
From Trail of Bits. An example test checks one input; a property states a rule, such as decode(encode(x)) == x, and lets a generator hunt for a counterexample. Its catalog covers roundtrip, inverse, oracle (matching a reference implementation), idempotence, invariants, easy-to-verify outputs, commutativity, associativity and identity, ranked from weakest (no crash) to strongest (roundtrip or oracle). When a calculation is buried in I/O or mutation, it looks for a refactor that exposes the property before concluding there is nothing to assert, and calling code a poor fit for property tests is a valid result. It also covers adding cases to existing suites, judging whether property tests assert anything real, and telling a wrong property from a genuine bug once a counterexample has shrunk. If the project has no property-testing library, it offers one once, with the property it would write, and leaves the choice to you. It isn't for coverage-guided fuzzing, mutation testing or end-to-end UI tests.
Summarizes the skill at e4dd0bb.
npx skills add https://github.com/trailofbits/skills --skill property-based-testing skills.sh pageSource on GitHubAll skills from trailofbits/skills
- Total Downloads
- 7,600 on skills.sh, Nov 9, 2026
- Repo stars
- 8,081 trailofbits/skills
- First seen
- Jan 19, 2026 on skills.sh
Weekly values
| Week to | Installs |
|---|---|
| Sep 21 | 188 |
| Sep 28 | 207 |
| Oct 5 | 211 |
| Oct 12 | 272 |
| Oct 19 | 278 |
| Oct 26 | 299 |
| Nov 2 | 344 |
| Nov 9 | 312 |
| Category |
Find root causes, review code and test what you built. Everything for building software: planning, coding, debugging, design, frameworks, cloud, agents and skills. |
|---|---|
| Type |
Knowledge and rules the agent applies while it works: best practices, design principles, API references. |
| Effect |
Adds no side effects of its own. It shapes how the agent thinks, writes or reviews. Guidelines and routers are always effect:none, even when the task they support edits code. |
| Needs |
Instructions only. Works in any agent that supports skills. |
| Publisher |
A verified publisher on skills.sh, or the company or maintainer behind the product the skill operates. |
| Topics |
SKILL.md
From trailofbits/skills at e4dd0bb. Checked daily, last changed Nov 6, 2026.
Frontmatter
name: property-based-testing
effort: low
description: "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.
The two ways a property test asserts nothing
- Tautology.
assert add(a, b) == a + brestates 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 whenfis 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-contradictoryassume()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.