Property Based Testing — Agent Skill by Trail of Bits

From the author

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.

— the description by Trail of Bits

AutoGineer summary

Written by AutoGineer from the skill’s own files, not by the author

Property-based testing (PBT) shifts the focus from testing individual examples to verifying rules across an entire input domain. This skill provides a framework for identifying algebraic properties—such as roundtrips, invariants, and oracles—that allow automated generators to hunt for counterexamples. It covers the full lifecycle of PBT, from designing effective strategies and pinning edge cases to interpreting shrunk failures and distinguishing between genuine bugs, ambiguous specifications, and poorly defined properties.

What it does

Identifies suitable algebraic properties for code verification.
Guides the design of robust input generation strategies.
Assists in debugging and interpreting shrunk counterexamples.
Provides a catalog of common properties like roundtrip, idempotence, and commutativity.
Helps distinguish between code bugs, test artifacts, and specification ambiguities.
Offers best practices for integrating PBT into existing test suites.

When to use it

When code exhibits algebraic shapes like inverses, invariants, or reference oracles.
When you need to verify complex data structures, parsers, or serialization logic.
When existing example-based tests fail to cover critical edge cases.
When a property test fails and you need to determine if the bug is in the code or the test.
When you need to optimize test strategies to avoid vacuous or tautological assertions.

Advantages

Uncovers edge cases that are difficult to identify through manual test writing.
Reduces reliance on hand-picked examples by covering the entire input domain.
Provides a structured approach to triaging test failures.
Improves the reliability of complex transformations and state-based logic.
Helps clarify ambiguous specifications by forcing explicit definitions of valid inputs.

Usage examples

“I have a serialization function. How do I verify it using property-based testing?”: The agent will suggest a roundtrip property (decode(encode(x)) == x) and guide you in setting up a generator for the input domain to ensure the property holds across all valid inputs.
“My property test failed with a shrunk counterexample. How do I know if it is a real bug?”: The agent will help you ground the property against your documentation or specs to determine if the failure violates a guarantee, is an undefined edge case, or indicates an over-broad test strategy.
“How can I improve my property test that keeps failing due to exhausted filters?”: The agent will advise you to move constraints from assume() calls into the generator strategy itself to ensure the generator only produces valid inputs from the start.

Install

Download the skill as a ZIP:
https://autogineer.com/agent-skills/trailofbits/property-based-testing/download

Unzip it into the cross-client skills folder of your project:

mkdir -p .agents/skills && unzip property-based-testing.zip -d .agents/skills

Documentation by Trail of Bits

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.

Files

ATTRIBUTION.mdAdded by AutoGineer960 B
LICENSELicence file added by AutoGineer19.7 KiB
README.md15.0 KiB
SKILL.md4.2 KiB
agents/openai.yaml254 B
assets/trail-of-bits-mark.svg3.0 KiB
references/generating.md2.6 KiB
references/interpreting-failures.md3.3 KiB
references/libraries.md2.9 KiB
references/refactoring.md4.7 KiB
references/reviewing.md2.8 KiB

Requirements and compatibility

Written for: Claude Code

Works with: Claude Code, Claude apps, OpenAI Codex, GitHub Copilot, Cursor, Gemini CLI, Kiro, OpenCode, Goose, Amp, Roo Code, JetBrains Junie, Factory Droid, Devin (ex-Windsurf), Mistral Vibe, OpenHands, Letta

“Works with” means the tool reads the open Agent Skills format; a skill written for one tool may use features others lack.

Needs: Claude Code frontmatter

Security

No issues found by our static scan· No issues found

A static scan is not a guarantee. Skills are third-party content: review a skill before you let an agent use it.

Migrate To Shoehorn
Matt Pocock· Community
Automate the migration of TypeScript test assertions from unsafe as-casting to the type-safe shoehorn library.
Software developmentClaude CodeClaude appsOpenAI Codex+14 more
MITGitHub stars of the source repository317.5k
Tdd
Matt Pocock· Community
A reference guide for implementing the red-green-refactor loop in test-driven development.
Software developmentClaude CodeClaude appsOpenAI Codex+14 more
MITGitHub stars of the source repository317.5k
Test Driven Development
Jesse Vincent (obra)· Community
A rigorous framework for Test-Driven Development, mandating that failing tests precede all production code.
Software developmentClaude CodeClaude appsOpenAI Codex+14 more
MITGitHub stars of the source repository314k
Webapp Testing
AnthropicOfficial
A toolkit for automating local web application testing using Playwright and server management helpers.
Software developmentClaude CodeClaude appsOpenAI Codex+14 more
Apache-2.0Low riskHas scriptsGitHub stars of the source repository188.6k
Test Driven Development
Addy Osmani· Community
A systematic approach to software development using the red-green-refactor cycle to ensure code reliability and maintainability.
Software developmentClaude CodeClaude appsOpenAI Codex+14 more
MITGitHub stars of the source repository113.9k
Browser Testing With Devtools
Addy Osmani· Community
Integrate Chrome DevTools to enable live browser inspection, debugging, and automated UI verification for your AI agent.
Software developmentClaude CodeClaude appsOpenAI Codex+14 more
MITGitHub stars of the source repository113.9k