Preface¶

The most common practice when writing tests is to manually craft a few examples: empty strings, maximum values, a piece of JSON that “looks like production data”. Even as coverage numbers go up, edge cases may still slip through: isolated surrogate pairs, 65536-byte alignment, floating-point underflow, malformed UTF-8. Property-Based Testing (PBT) shifts the framing: instead of asking “are these few inputs correct?”, it asks “does a certain property hold true for all inputs in this category?” Libraries automatically generate a large number of test cases, and when a failure occurs, shrink the input down to the smallest possible counterexample.

The catch is that the barrier to entry is not trivial. Judging where PBT is appropriate, which properties to assert, how to constrain generators, and whether a failure is a code bug or a poorly written test often relies on experience. Trail of Bits has packaged this methodology into the Agent Skill property-based-testing: when encountering serialization pairs, parsers, normalization functions, or smart contract invariants, it guides the programming assistant to write, review, and interpret tests following a consistent workflow, rather than ad-hoc improvisation.

What It Is¶

One-sentence positioning: property-based-testing is a cross-language property-based testing guide Skill that also covers smart contracts. It does not replace libraries like Hypothesis, fast-check, proptest, or Echidna. Instead, it tells the Agent: when to use PBT, which properties to test, which reference documents to consult, and not to immediately flag a failure as a bug.

It is maintained by security firm Trail of Bits, hosted in the public Skills marketplace repository trailofbits/skills, and categorized as a Verification plugin. The plugin metadata .claude-plugin/plugin.json specifies:
- name: property-based-testing
- version: 1.1.1
- description: Property-based testing guidance for multiple languages and smart contracts
- author: Henrik Brodin (affiliated with Trail of Bits)

The overall repository license is CC BY-SA 4.0. The official README describes it as a Claude Code plugin marketplace; the same README notes that Codex can load it directly via the Claude marketplace compatibility layer without additional sidecar metadata. The Skill itself is a standard SKILL.md file, which can be used by any programming assistant that can recognize skill directories; the exact installation path depends on the installer’s output, and will not be guessed here.

The SKILL.md file defines the trigger conditions: use it when writing tests, reviewing code with serialization/validation/parsing patterns, designing features, or determining that PBT will provide stronger coverage than example-based tests.

The repository structure is more complete than a standalone SKILL.md. The entry file handles pattern detection and routing; detailed content is split into the references/ directory:

property-based-testing/
├── SKILL.md
├── README.md
└── references/
    ├── generating.md              # How to write runnable property tests
    ├── strategies.md              # Input generators
    ├── design.md                  # Property-Driven Development
    ├── refactoring.md             # Refactoring for testability
    ├── reviewing.md               # Quality checklist for existing PBT tests
    ├── interpreting-failures.md   # Failure analysis and bug classification
    └── libraries.md               # PBT libraries listed by language (including contract tools)

There are also agents/ and assets/ directories in the repository. The Skill’s decision tree is based on the references/ directory: the current task determines which document to load, rather than dumping the entire methodology into the context at once.

Core Features and Highlights¶

The following capabilities are consistent across the official SKILL.md, plugin README, and the same Guide on the Trail of Bits website.

1. Automatically determine whether to use PBT based on code patterns¶

The Skill requires active activation when high-value patterns are detected, rather than waiting for the user to mention “property-based testing”. The detection list includes:
- Serialization pairs: encode/decode, serialize/deserialize, toJSON/fromJSON, pack/unpack
- Parsers: URLs, configurations, protocols, string-to-structured data conversion
- Normalization: normalize, sanitize, clean, canonicalize, format
- Validators: is_valid, validate, check_* (especially when paired with normalization)
- Data structures: Custom collections with add/remove/get methods
- Mathematical/algorithmic: Pure functions, sorting, comparators
- Smart contracts: Solidity/Vyper, token operations, state invariants, access control

The priority table marks roundtrip encode/decode, pure functions, contract state invariants as HIGH priority; validating “still valid after normalization”, idempotence and ordering of sorts, normalization idempotence as MEDIUM priority; output invariants of builders/factories as LOW priority.

The repository README includes sample prompts that can be used directly for explicit invocation:

Write property-based tests for this JSON serializer
Review this Hypothesis test for quality issues
Help me design this feature using properties first
This function is hard to test - how can I refactor it?
Write Echidna invariants for this token contract

2. Property catalog, rather than “write a few more examples”¶

The core is not randomly throwing inputs, but first selecting a property that should always hold true. The cheat sheet from SKILL.md is as follows (formulas as originally written):

Property	Formula	Use Case
Roundtrip	`decode(encode(x)) == x`	Serialization, conversion pairs
Idempotence	`f(f(x)) == f(x)`	Normalization, formatting, sorting
Invariant	A property preserved before and after transformation	Any transformation, contract state
Commutativity	`f(a, b) == f(b, a)`	Binary/collection operations
Associativity	`f(f(a,b), c) == f(a, f(b,c))`	Associative combination operations
Identity	`f(x, identity) == x`	Operations with an identity element
Inverse	`f(g(x)) == x`	Encryption/decryption, compression/decompression
Oracle	`new_impl(x) == reference(x)`	Optimization, refactoring comparisons
Easy to Verify	e.g. `is_sorted(sort(x))`	Algorithms with hard-to-write implementations and easy-to-verify results
No Exception	Valid inputs do not crash	Weakest baseline

The strength order from weakest to strongest is explicitly defined as:

No Exception → Type Preservation → Invariant → Idempotence → Roundtrip

The Skill explicitly opposes stopping at “no exceptions thrown”: that is the weakest property, and stronger properties should be prioritized. It also rejects common excuses such as “example tests are sufficient”, “the function is very simple”, “no time to write generators” — the official stance is that when the input domain is complex (strings, floating points, nested structures), simple functions are actually more suitable for PBT; most libraries include built-in strategies, and custom generators are not a prerequisite.

3. Route to different reference documents based on the task¶

The entry SKILL.md is brief, with truly actionable content in the references/ directory. The decision tree branches by task:
- Writing new tests → generating.md, read strategies.md only if generators are complex
- Designing new features → design.md (write executable specifications first before implementation)
- Code is hard to test (I/O mixed with logic, missing inverse operations) → refactoring.md
- Reviewing existing PBT tests → reviewing.md
- Interpreting test failures → interpreting-failures.md
- Looking up libraries → libraries.md

This differs from “pasting an entire testing manual into the prompt”: the Agent only loads the document required for the current step.

4. Provide constrained recommendations, avoid pushing PBT unconditionally¶

When high-value patterns are detected, the Skill requires presenting it as an option first, rather than directly changing the test style. The official sample phrase is:

I notice encode_message/decode_message is a serialization pair. Property-based testing with a roundtrip property would provide stronger coverage than example tests. Want me to use that approach?

If the repository already uses Hypothesis, fast-check, proptest, or Echidna, the recommendation can be more direct: “This codebase uses Hypothesis. I’ll write property-based tests for this serialization pair using a roundtrip property.” If the user declines, proceed to write example tests as requested, and do not continue to push the topic.

It also lists red lines: do not recommend PBT for trivial getters/setters; do not discuss roundtrip properties when only an encode function exists without a corresponding decode function; do not present more than 5–10 candidate properties at once; do not pester the user after they decline.

5. Language coverage for application code and EVM contracts¶

Tutorials link to secure-contracts.com, and the full manual for contract tools is not embedded into the Skill.

Installation and Activation¶

The official installation has two paths: one for the Trail of Bits plugin marketplace (Claude Code / Codex), and one for the universal skills CLI (directory page officialskills.sh). Installation counts and security scan scores on third-party directories are not official data; use the commands from the GitHub README and this directory page as authoritative.

1. Claude Code: Add marketplace first, then select the plugin (repository recommendation)

/plugin marketplace add trailofbits/skills
/plugin menu

Select property-based-testing from the menu.

2. Claude Code: Install directly via plugin path
Both the Trail of Bits website and the plugin README provide this command:

/plugin install trailofbits/skills/plugins/property-based-testing

The website notes: Enable this Skill after running it in Claude Code.

3. Codex: Use the same Claude marketplace
From the repository root README:

codex plugin marketplace add trailofbits/skills
codex plugin list
codex plugin add property-based-testing@trailofbits

The placeholder <plugin-name>@trailofbits corresponds to this plugin’s name field property-based-testing.

4. Universal Agent Skills CLI (for tools like Cursor that can recognize SKILL.md)

npx skills add https://github.com/trailofbits/skills --skill property-based-testing

You can also paste the GitHub directory address to the programming assistant and have it install via the Agent Skills workflow:
https://github.com/trailofbits/skills/tree/main/plugins/property-based-testing

This installs the guidance documentation, and does not install Hypothesis or Echidna for you. You still need to install the corresponding library per libraries.md to actually run tests, for example:

pip install hypothesis

npm install fast-check

[dev-dependencies]
proptest = "1.0"

Echidna requires crytic-compile, with binaries available from crytic/echidna; Medusa can be installed with go install github.com/crytic/medusa@latest. Use the latest version numbers from each library’s documentation; the pins in libraries.md are only for reference.

Typical Usage Examples¶

The following prompts, code, and settings are all from the official SKILL.md / generating.md / libraries.md, and can be reproduced according to the project’s language.

1. Trigger this Skill in the assistant
Use phrasing close to the description:

This code has a matching encode/decode pair.
Please use property-based-testing: first determine whether PBT is appropriate,
then write tests using the roundtrip property; if the repository does not already have Hypothesis / fast-check, first explain which library to install.
Do not stop at "valid inputs do not crash".

When reviewing existing tests, rephrase to “Review this Hypothesis test for quality issues”; for contracts, use “Write Echidna invariants for this token contract”.

2. Roundtrip: Encoding then decoding should return the original object
Full Python/Hypothesis example from generating.md (core assertions excerpted):

from hypothesis import given, strategies as st, settings, example
from myapp.codec import encode_message, decode_message, Message, DecodeError

messages = st.builds(
    Message,
    id=st.uuids(),
    content=st.text(max_size=1000),
    priority=st.integers(min_value=1, max_value=10),
    tags=st.lists(st.text(max_size=50), max_size=20),
)

class TestMessageCodecProperties:
    @given(messages)
    def test_roundtrip(self, msg: Message):
        """Encoding then decoding returns the original message."""
        encoded = encode_message(msg)
        decoded = decode_message(encoded)
        assert decoded == msg

    @given(messages)
    def test_encode_deterministic(self, msg: Message):
        """Same message always encodes to same bytes."""
        assert encode_message(msg) == encode_message(msg)

    @given(st.binary())
    def test_decode_invalid_raises_or_succeeds(self, data: bytes):
        """Random bytes either decode or raise DecodeError."""
        try:
            decode_message(data)
        except DecodeError:
            pass

The shortest roundtrip template from the same document is:

@given(valid_messages())
def test_roundtrip(msg):
    """Encoding then decoding returns original."""
    assert decode(encode(msg)) == msg

3. Idempotence: Normalizing twice should equal normalizing once

@given(st.text())
def test_normalize_idempotent(s):
    """Normalizing twice equals normalizing once."""
    assert normalize(normalize(s)) == normalize(s)

4. Sorting: Assert length, elements, order, and idempotence together

@given(st.lists(st.integers()))
@example([])
@example([1])
@example([1, 1, 1])
def test_sort(xs):
    result = sort(xs)
    assert len(result) == len(xs)
    assert sorted(result) == sorted(xs)
    assert all(result[i] <= result[i + 1] for i in range(len(result) - 1))
    assert sort(result) == result

@example is explicitly required by the official guidelines to cover edge cases: empty input, single-element input, duplicate elements, rather than relying solely on random generation.

5. Embed constraints into generators, not via post-hoc assume()
The principle from design.md: the generator itself is the specification. Define valid ranges in st.integers(min_value=1, max_value=100); using @given(st.integers()) followed by assume(1 <= x <= 100) will increase the rejection rate, which is a pattern that should be fixed.

Hypothesis sample size recommendations (from generating.md):

# Development: Fast feedback
@settings(max_examples=10)

# CI: More thorough coverage
@settings(max_examples=200)

# Nightly / release: Most thorough
@settings(max_examples=1000, deadline=None)

Run tests:

pytest test_file.py -v
pytest test_file.py --hypothesis-seed=0 -v
pytest test_file.py --hypothesis-show-statistics

6. Contracts: Echidna invariant naming convention
Minimal example from libraries.md:

function echidna_balance_invariant() public returns (bool) {
    return address(this).balance >= 0;
}

Function names must start with echidna_ and return bool. This is a tool convention, not a complete template for business invariants; total token supply, balance upper bounds, and other invariants should be written based on the contract’s documentation.

7. Classify failures first before deciding whether to report a bug
interpreting-failures.md divides failures into three categories: poorly written tests (incorrect property, generated invalid inputs), ambiguous specifications, and true violations of documented guarantees. The workflow is: reproduce the minimal failing input separately → anchor the property against type annotations, docstrings, existing unit tests, and external specifications

# Property-Based Testing: Trail of Bits Turns Property Testing into Reusable Agent Skills