Property-Based Testing skill for Codex

A property test states a rule that must hold for every valid input, lets the library search for a counterexample, and when one is found reports the smallest input that breaks the rule, reproducible by seed. Done well, each property encodes a real requirement and generators produce the inputs production actually sees.

Inspect first

1. Read AGENTS.md and check whether fast-check (and @fast-check/vitest or @fast-check/jest) or hypothesis are already dependencies. Adding them needs network access to install.
2. Find the unit’s contract: types, validation rules, documented invariants. Properties come from the contract, not from the implementation.
3. Look for existing example-based tests; keep them. Properties complement examples.

Finding properties

Pattern	Property	Typical target
Round-trip	decode(encode(x)) == x	serializers, parsers + printers, compression, URL encoding
Invariant	output always satisfies a rule	sorted output is ordered and a permutation of input; totals never negative
Oracle / differential	fast(x) == reference(x)	optimized vs naive implementation, new vs legacy code path
Idempotence	f(f(x)) == f(x)	normalization, formatting, dedupe, upserts
Metamorphic	changing input in a known way changes output predictably	adding an item never lowers the cart total; filtering more never returns more
Commutativity / associativity	order of operations does not matter	merging CRDTs, set operations, money arithmetic
Never crashes	arbitrary input yields a value or a typed error	parsers, request validators

Avoid properties that re-implement the function under test. If the only way to state the expected output is the same algorithm, use an oracle that is simpler (brute force) or a different pattern.

fast-check

import fc from "fast-check";
import { describe, it, expect } from "vitest";
import { encodeQuery, decodeQuery } from "./query";

describe("query string codec", () => {
  it("round-trips any flat string map", () => {
    fc.assert(
      fc.property(fc.dictionary(fc.string(), fc.string()), (params) => {
        expect(decodeQuery(encodeQuery(params))).toEqual(params);
      }),
    );
  });

  it("never makes the total smaller when an item is added", () => {
    const item = fc.record({
      priceCents: fc.integer({ min: 0, max: 1_000_000 }),
      qty: fc.integer({ min: 1, max: 99 }),
    });
    fc.assert(
      fc.property(fc.array(item, { maxLength: 30 }), item, (cart, extra) => {
        expect(total([...cart, extra])).toBeGreaterThanOrEqual(total(cart));
      }),
      { numRuns: 500 },
    );
  });
});

• Async code: fc.asyncProperty and await fc.assert(...).
• @fast-check/vitest (or @fast-check/jest) offers test.prop([fc.integer()])("...", (n) => ...) for tighter integration.
• Useful arbitraries: fc.integer, fc.double({ noNaN: true }), fc.string, fc.uniqueArray, fc.record, fc.oneof, fc.constantFrom, fc.option, fc.date, fc.emailAddress, fc.uuid, fc.letrec for recursive structures.
• Restrict with .filter() sparingly; heavy filtering wastes runs. Build valid values directly with .map() or fc.record instead.
• On failure fast-check prints seed and path; replay exactly with fc.assert(prop, { seed: <seed>, path: "<path>", endOnFailure: true }). Then copy the shrunk counterexample into a plain example test so it runs forever.

Hypothesis

from hypothesis import given, example, settings, strategies as st

money = st.integers(min_value=0, max_value=10_000_000)
line = st.builds(LineItem, price_cents=money, qty=st.integers(min_value=1, max_value=99))

@given(st.lists(line, max_size=30), line)
def test_adding_an_item_never_lowers_total(cart, extra):
    assert total(cart + [extra]) >= total(cart)

@given(st.dictionaries(st.text(), st.text()))
@example({"": ""})                       # pinned edge case, always runs
def test_query_round_trip(params):
    assert decode_query(encode_query(params)) == params

Composite strategies for dependent values:

from datetime import date, timedelta

@st.composite
def date_ranges(draw):
    start = draw(st.dates(min_value=date(2000, 1, 1), max_value=date(2100, 1, 1)))
    days = draw(st.integers(min_value=0, max_value=365))
    return start, start + timedelta(days=days)

@given(date_ranges())
def test_nights_is_never_negative(rng):
    assert nights(*rng) >= 0

• st.from_type(MyDataclass) and st.builds(...) infer from type hints.
• assume(cond) discards an input; if many inputs are discarded, Hypothesis raises a health check error. Fix the strategy instead.
• Hypothesis stores failing examples in .hypothesis/ and replays them first on the next run. Add .hypothesis/ to .gitignore; pin important ones with @example.
• Profiles for speed vs depth:

# conftest.py
import os
from hypothesis import settings
settings.register_profile("ci", max_examples=500, deadline=None)
settings.register_profile("dev", max_examples=50)
settings.load_profile(os.getenv("HYPOTHESIS_PROFILE", "dev"))

deadline=None avoids false failures on slow CI machines; keep the default deadline locally to catch accidental slowness.

Stateful (model-based) testing

Compare the real system against a simple model across random command sequences.

from hypothesis.stateful import RuleBasedStateMachine, rule, invariant
import hypothesis.strategies as st

class CartMachine(RuleBasedStateMachine):
    def __init__(self):
        super().__init__()
        self.cart = Cart()
        self.model: dict[str, int] = {}

    @rule(sku=st.sampled_from(["A", "B", "C"]), qty=st.integers(1, 5))
    def add(self, sku, qty):
        self.cart.add(sku, qty)
        self.model[sku] = self.model.get(sku, 0) + qty

    @rule(sku=st.sampled_from(["A", "B", "C"]))
    def remove(self, sku):
        self.cart.remove(sku)
        self.model.pop(sku, None)

    @invariant()
    def matches_model(self):
        assert self.cart.quantities() == self.model

TestCart = CartMachine.TestCase

fast-check has the same idea with fc.commands([...]) and fc.modelRun(setup, cmds). Use stateful tests for caches, queues, undo stacks, connection pools and anything with an API where call order matters.

Generators that match reality

• Bound sizes and ranges to the domain (quantities 1-99, prices in cents up to a cap). Unbounded integers find overflow bugs that cannot happen, which wastes time.
• Do include the nasty edges the domain allows: empty strings, unicode, zero, maximum values, duplicate keys, leap days, DST transitions.
• Floats: decide whether NaN and infinities are valid inputs; exclude them explicitly if not, and compare with tolerances.
• Share generators in one module (tests/strategies.py, test/arbitraries.ts) so domain constraints stay consistent across properties.

Gotchas

• A property that passes on the first run may be vacuous. Break the implementation on purpose and confirm the property finds it and shrinks to a small input.
• Shrinking needs generators built from library combinators; values produced through external randomness (Math.random() inside the test) cannot shrink or replay.
• Do not catch broad exceptions inside the property; a swallowed error passes.
• Tests that hit a database or network per example are slow; lower numRuns / max_examples or test the pure core with properties and the edges with examples.
• Properties do not replace coverage-guided fuzzing for parsers of untrusted input; for that, hand off to $fuzz-testing.

Verification

1. Each property fails against a deliberately broken implementation and reports a shrunk counterexample.
2. Every counterexample found during the work is pinned as an example test.
3. Runtime per property stays under a few seconds in the default profile.
4. CI runs with the deeper profile (more examples) at least nightly.