Property-Based Testing - Trail of Bits Skills

Property-based testing (PBT) generates hundreds of random test cases to verify code properties hold across the entire input space, catching edge cases that example-based tests miss.

Overview

This plugin provides intelligent guidance for writing property-based tests when Claude Code detects suitable patterns in your code. Instead of writing individual example tests, PBT tests properties that should always hold:

Roundtrip properties - decode(encode(x)) == x
Idempotence - f(f(x)) == f(x)
Invariants - Properties preserved across transformations
Commutativity - f(a, b) == f(b, a)
Oracle comparison - new_impl(x) == reference(x)

The plugin automatically suggests PBT when it detects high-value patterns like serialization pairs, parsers, validators, or smart contract invariants.

When to Use

Automatic Detection Patterns

The plugin activates when detecting:

Serialization Pairs

encode/decode, serialize/deserialize, toJSON/fromJSON, pack/unpack

Parsers

URL parsing, config parsing, protocol parsing, string-to-structured-data

Normalization

normalize, sanitize, clean, canonicalize, format

Validators

is_valid, validate, check_* (especially with normalizers)

Data Structures

Custom collections with add/remove/get operations

Smart Contracts

Solidity/Vyper contracts, token operations, state invariants, access control

Priority Matrix

Pattern	Property	Priority
encode/decode pair	Roundtrip	HIGH
Pure function	Multiple	HIGH
Smart contract	State invariants	HIGH
Validator	Valid after normalize	MEDIUM
Sorting/ordering	Idempotence + ordering	MEDIUM
Normalization	Idempotence	MEDIUM
Builder/factory	Output invariants	LOW

When NOT to Use

Do NOT use property-based testing for:

Simple CRUD operations without transformation logic
One-off scripts or throwaway code
Code with side effects that cannot be isolated (network calls, database writes)
Tests where specific example cases are sufficient and edge cases are well-understood
Integration or end-to-end testing (PBT is best for unit/component testing)

Supported Languages

The plugin provides language-specific guidance for:

General Purpose
Smart Contracts

Python - Hypothesis
JavaScript/TypeScript - fast-check
Rust - proptest, quickcheck
Go - rapid, gopter
Java - jqwik
Scala - ScalaCheck
Haskell - QuickCheck
F# - FsCheck
Erlang/Elixir - PropEr, StreamData

See the plugin’s references/libraries.md for complete library documentation.

Property Catalog

Core Properties

Roundtrip

Formula: decode(encode(x)) == xWhen to use: Serialization, conversion pairs, compress/decompressExample:

@given(st.text())
def test_json_roundtrip(data):
    assert json.loads(json.dumps(data)) == data

Idempotence

Formula: f(f(x)) == f(x)When to use: Normalization, formatting, sorting, deduplicationExample:

@given(st.lists(st.integers()))
def test_sort_idempotent(lst):
    assert sorted(sorted(lst)) == sorted(lst)

Invariant

Formula: Property holds before and after transformationWhen to use: Any transformation that preserves certain propertiesExample:

@given(st.lists(st.integers()))
def test_filter_preserves_length(lst):
    filtered = [x for x in lst if x > 0]
    assert len(filtered) <= len(lst)

Commutativity

Formula: f(a, b) == f(b, a)When to use: Binary operations, set operations, merge functionsExample:

@given(st.integers(), st.integers())
def test_addition_commutative(a, b):
    assert a + b == b + a

Oracle

Formula: new_impl(x) == reference(x)When to use: Optimization, refactoring, algorithm replacementExample:

@given(st.lists(st.integers()))
def test_fast_sort_matches_builtin(lst):
    assert fast_sort(lst) == sorted(lst)

Inverse

Formula: f(g(x)) == xWhen to use: encrypt/decrypt, compress/decompress, add/removeExample:

@given(st.binary())
def test_encryption_inverse(plaintext):
    ciphertext = encrypt(key, plaintext)
    assert decrypt(key, ciphertext) == plaintext

Property Strength Hierarchy

Weakest                                    Strongest
   ↓                                           ↓
No Exception → Type Preservation → Invariant → Idempotence → Roundtrip

Always push for stronger properties:

Start with “no exception” as baseline
Look for invariants that must hold
Identify idempotence opportunities
Seek roundtrip properties for paired operations

Quick Start Examples

Python (Hypothesis)

from hypothesis import given, strategies as st
import json

@given(st.dictionaries(st.text(), st.integers()))
def test_json_roundtrip(data):
    """JSON serialization preserves data"""
    serialized = json.dumps(data)
    deserialized = json.loads(serialized)
    assert deserialized == data

@given(st.text())
def test_normalize_idempotent(s):
    """Normalizing twice gives same result as once"""
    once = normalize(s)
    twice = normalize(normalize(s))
    assert once == twice

JavaScript/TypeScript (fast-check)

import fc from 'fast-check';

test('URL parser roundtrip', () => {
  fc.assert(
    fc.property(fc.webUrl(), (url) => {
      const parsed = parseURL(url);
      const rebuilt = buildURL(parsed);
      return normalizeURL(rebuilt) === normalizeURL(url);
    })
  );
});

Rust (proptest)

use proptest::prelude::*;

proptest! {
    #[test]
    fn test_serialize_roundtrip(data: Vec<u8>) {
        let serialized = serialize(&data)?;
        let deserialized = deserialize(&serialized)?;
        prop_assert_eq!(data, deserialized);
    }
}

Solidity (Echidna)

contract TokenTest {
    Token token;
    
    // Invariant: total supply equals sum of all balances
    function echidna_supply_invariant() public view returns (bool) {
        return token.totalSupply() >= token.balanceOf(address(this));
    }
    
    // Invariant: balance never exceeds total supply
    function echidna_balance_bounded() public view returns (bool) {
        return token.balanceOf(msg.sender) <= token.totalSupply();
    }
}

How Claude Suggests PBT

Existing PBT Library Detected

If the codebase already uses a PBT library, Claude will be direct:

“This codebase uses Hypothesis. I’ll write property-based tests for this serialization pair using a roundtrip property.”

No PBT Library

If no library is detected, Claude offers it as an option:

“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?”

User Declines

If you decline, Claude will write good example-based tests without further prompting.

Advanced Topics

Custom Generators

For complex domain types, the plugin provides guidance on writing custom generators that produce valid inputs while maintaining coverage.

Shrinking

When tests fail, PBT libraries automatically find the smallest failing input. The plugin includes guidance on interpreting and acting on shrunk failures.

State Machine Testing

For stateful systems (databases, caches, smart contracts), the plugin provides patterns for modeling state transitions as properties.

Performance Properties

Beyond correctness, test performance properties like:

Output size bounded by input size
Linear time complexity
Memory usage within limits

Antipatterns to Avoid

Common mistakes the plugin helps you avoid:

Testing implementation details - Test observable behavior, not internals
Weak properties - Don’t settle for “no exception” when stronger properties exist
Non-deterministic tests - Generators should produce deterministic results from the same seed
Testing trivial properties - x == x is always true, not useful
Ignoring shrinking output - Shrunk examples reveal root cause, don’t ignore them

Rationalizations to Reject

The plugin enforces quality by rejecting these shortcuts:

“Example tests are good enough” - If serialization/parsing/normalization is involved, PBT finds edge cases examples miss
“The function is simple” - Simple functions with complex input domains benefit most from PBT
“We don’t have time” - PBT tests are often shorter than comprehensive example suites
“It’s too hard to write generators” - Most libraries have excellent built-in strategies
“No crash means it works” - “No exception” is the weakest property; push for stronger guarantees

Integration with Other Plugins

Spec-to-Code Compliance - Verify implementation matches specification with property tests
Testing Handbook Skills - Combine with fuzzing for comprehensive coverage
Constant-Time Analysis - Test timing properties in crypto code

Resources

The plugin includes detailed reference documentation:

references/generating.md - Test generation patterns and examples
references/strategies.md - Custom input generator guidance
references/design.md - Property-Driven Development approach
references/refactoring.md - Making code testable with properties
references/reviewing.md - Quality checklist for existing tests
references/interpreting-failures.md - Failure analysis and debugging
references/libraries.md - Complete library documentation by language

Examples from the Wild

Parser Testing

URL parser tested with 10,000 random URLs finds edge case with IPv6 zone IDs that example tests missed

Serialization Bug

MessagePack encoder/decoder roundtrip test finds corruption on 65536-byte boundary

Smart Contract

Token invariant testing discovers reentrancy vulnerability in balance update logic

Normalization

Unicode normalization tested with random strings finds non-idempotent case with combining characters

Author: Henrik Brodin (Trail of Bits)Version: 1.1.0

Get Started

Core Concepts

Smart Contract Security

Code Auditing

Static Analysis Tools

Verification & Testing

Specialized Tools

Development

Infrastructure & Tools

Other

​Overview

​When to Use

​Automatic Detection Patterns

Serialization Pairs

Parsers

Normalization

Validators

Data Structures

Smart Contracts

​Priority Matrix

​When NOT to Use

​Supported Languages

​Property Catalog

​Core Properties

​Property Strength Hierarchy

​Quick Start Examples

​Python (Hypothesis)

​JavaScript/TypeScript (fast-check)

​Rust (proptest)

​Solidity (Echidna)

​How Claude Suggests PBT

​Existing PBT Library Detected

​No PBT Library

​User Declines

​Advanced Topics

​Custom Generators

​Shrinking

​State Machine Testing

​Performance Properties

​Antipatterns to Avoid

​Rationalizations to Reject

​Integration with Other Plugins

​Resources

​Examples from the Wild

Parser Testing

Serialization Bug

Smart Contract

Normalization

Build docs developers (and LLMs) love

Overview

When to Use

Automatic Detection Patterns

Priority Matrix

When NOT to Use

Supported Languages

Property Catalog

Core Properties

Property Strength Hierarchy

Quick Start Examples

Python (Hypothesis)

JavaScript/TypeScript (fast-check)

Rust (proptest)

Solidity (Echidna)

How Claude Suggests PBT

Existing PBT Library Detected

No PBT Library

User Declines

Advanced Topics

Custom Generators

Shrinking

State Machine Testing

Performance Properties

Antipatterns to Avoid

Rationalizations to Reject

Integration with Other Plugins

Resources

Examples from the Wild