Property-Based Tests: Derive Invariants From the Spec, Let the Framework Hunt

Tier: Advanced · Workflow area: Testing & Quality

AI is unusually good at exactly that step: reading a spec or a function and proposing candidate properties ("output is always sorted," "encode∘decode is identity," "total is preserved across splits"). You judge the invariants; Hypothesis or fast-check does the hunting; the shrinker hands you a minimal counterexample.

When to use

• •
  Parsers, serializers, encoders — anything with a round-trip (decode(encode(x)) == x).
• •
  Money/quantity math where conservation laws exist (splits sum to the original, no penny lost).
• •
  Functions with rich input spaces (date ranges, unicode, nested structures) where example tests visibly undercover.
• •
  Reimplementations and migrations: property "new(x) == old(x)" over generated inputs is the cheapest correctness harness available.

Skip for thin CRUD glue and I/O orchestration — there is no invariant to state, and PBT adds runtime for nothing.

Prerequisites

• •
  Hypothesis (Python), fast-check (JS/TS), or jqwik (JVM) installed — all free.
• •
  The spec, docstring, or ticket describing intended behavior — properties come from intent, not from the implementation.
• •
  An AI assistant with the function and spec in context.

The workflow

1. 1.

   Elicit candidate invariants. Prompt with the spec, not just the code:

   Copy

   Here is the spec for split_invoice(invoice, ratios) and its implementation.
   Propose 6-10 candidate properties that must hold for ALL valid inputs.
   For each: state the property in one sentence, classify it
   (round-trip / invariant / conservation / oracle / metamorphic), and flag
   any property that the implementation might currently violate.
   Do not propose properties that merely restate the implementation line by line.
   

2. 2.

   Cull to the strong ones. Keep properties that would catch a real bug class; discard tautologies ("returns a list") and spec-restatements. Three sharp properties beat ten weak ones. This judgment step is yours — a wrong property becomes a permanent false alarm.

3. 3.

   Generate the harness. Ask for the test with explicit generator constraints:

   Copy

   Write Hypothesis tests for the 3 approved properties. Constraints:
   - ratios: lists of 1-10 Decimals in (0,1] that sum to 1 (build a composite strategy).
   - invoice amounts: Decimal, 2 places, 0.01 to 10_000_000.
   - Property 1 (conservation): sum of split amounts == invoice.total exactly.
   - Property 3 (metamorphic): permuting ratios permutes outputs identically.
   - Use @settings(max_examples=500) and add an explicit @example for the
     known edge: single ratio of exactly 1.
   

4. 4.

   Run and read the shrunk counterexample. When a property fails, Hypothesis shrinks to a minimal case — e.g. ratios=[Decimal('0.333...'), ...] exposing a rounding-remainder bug. Paste the counterexample back to the AI for a fix proposal, but decide yourself whether the code or the property was wrong. Both happen.

5. 5.

   Pin regressions. Every real counterexample becomes a permanent @example(...) so the exact case replays forever, independent of random generation.

Tool variants

• Claude / reasoning-tier models: best at invariant elicitation from prose specs; use extended thinking for metamorphic-property brainstorming.
• Copilot / Cursor inline: fine for step 3 (strategy and harness code) once you hand it the approved property list.
• schemathesis: if the input space is an API schema, skip hand-rolled generators — see pb-31.

Verification

• •
  Each property fails when you deliberately break the code (mutate a + to -); a property that never fails verifies nothing.
• •
  Generators produce genuinely valid inputs — print 20 samples and eyeball them; over-constrained strategies silently test a toy domain.
• •
  Shrunk counterexamples are reproducible via the printed seed or pinned @example.
• •
  Suite runtime stays in budget (tune max_examples; 100–500 covers most CI budgets).

Pitfalls

• Properties derived from the implementation. Ask the AI for properties from the spec before it reads the code, or it will faithfully encode the current bugs as law.
• Filtering instead of constructing.assume(sum(ratios) == 1) throws away almost every generated input; build a strategy that constructs valid ratios directly.
• Floating-point equality in conservation properties. Use Decimal or integer minor units; otherwise you will chase phantom failures.
• Treating a failing property as always a code bug. Sometimes the property is over-strong; adjudicate against the spec, not against whichever artifact is easier to change.

Restricted-environment variant

Invariant elicitation works on redacted material: paste the spec with product nouns neutralized ("ledger entry" → "record") and the function signature only. Local Qwen-Coder-class models via Ollama produce serviceable Hypothesis harness code from an explicit property list, though invariant brainstorming quality drops — compensate by mining properties from the spec's own "must/always/never" sentences yourself and using the local model just for strategy code. Everything else (running, shrinking, pinning) is fully local anyway.

Success criteria

• •
  At least three non-tautological properties are in CI with constructive generators.
• •
  One property, at some point, produced a shrunk counterexample that changed the code or sharpened the spec — the payoff event.
• •
  Regression @example pins exist for every counterexample found.
• •
  You can explain each property's bug-class in one sentence to a reviewer.