Practical guide
Test a rule across many generated examples
Property-based testing replaces a list of expected outputs with a rule checked on generated inputs. The strength of the test comes from the rule and the domain it explores.
Choose a property that rejects a plausible bug
Property-testing libraries such as Hypothesis generate examples and help reduce failures. The framework does not choose the intended behavior for you. A useful property should rule out a concrete incorrect implementation, not merely restate its algorithm or verify that it returned a value.
Illustrative example: sorting records
Weak property: output is ordered
Bug it permits: always return an empty list
Stronger property set:
output is ordered by the agreed key
output preserves every input record and multiplicity
stable order is preserved for equal keys, if required
Idempotence can be a useful additional law, but an empty-output implementation is idempotent too. The properties must work together. Define equality carefully for records with identifiers, duplicate keys or ignored metadata. A multiset check that drops duplicates can silently weaken preservation.
Build a generator for the relevant domain
Include empty lists, one item, duplicate keys, already sorted input and reverse order. Generate equal keys deliberately if stability matters. For numeric keys, define how exceptional values or overflow are handled rather than assuming they cannot occur. Over-filtering the generator can remove precisely the cases the requirement needs to address.
Inspect a failure before repairing the code
A minimized counterexample can reveal an implementation defect, an incorrect property or an unrealistic generator. Decide which artifact is wrong. Preserve the input and its replay information, correct the intended requirement if needed, then retain the case as a regression. Do not weaken a property just because the current implementation violates it.
Keep tests and solver proofs distinct
A successful generated campaign establishes that its property held for executed examples, not for every possible input. In Proof, verify-properties analyzes supported authored models, while proptest can generate model-derived fixtures. Neither command name implies that the production sorting function was exercised. Connect model examples to real tests and retain their execution evidence.
proof verify-properties specs/system ordering
proof proptest specs/system ordering --source z3 --output tests/ordering/
Report the useful scope
Name the property, generator domain, implementation revision and run configuration. Coverage growth can guide further testing, but it does not replace a strong oracle. Keep exclusions and intentionally unsupported inputs visible.
Follow the evidence
Try an intentionally wrong implementation against the property before trusting a passing campaign.
Review one generated-test property. Bring the property and generator so we can assess which plausible defects the oracle rejects and which input classes remain unexplored.