proof-drivenlisted

# Proof-driven development Prove properties from requirements before writing code. Proofs guide implementation, not the reverse. Zero unproven properties in final code. **Modern insight (2025)**: PBT + example tests pairing is the standard -- properties discover edge cases, example tests prevent regressions and serve as documentation. Counterexamples from shrinking should always become permanent regression tests. AI-assisted PBT (Anthropic 2025) can generate properties from docstrings, but human judgment for property selection remains essential. See [frameworks](references/frameworks.md) for language-specific PBT and stateful testing tools. See [examples](references/examples.md) for brief property test patterns per language. See [formal-tools](references/formal-tools.md) for theorem provers and bounded model checkers. --- ## Property Categories | Category | Description | Example | |----------|-------------|---------| | **Postcondition** | Output satisfies contract | `sorted(sort(xs))` | | **Invariant** | Property preserved by operation | `len(xs) == len(sort(xs))` | | **Idempotence** | `f(f(x)) == f(x)` | `deduplicate(deduplicate(xs))` | | **Inverse / Round-trip** | `g(f(x)) == x` | `decode(encode(x)) == x` | | **Model-based** | Implementation matches reference | `my_sort(xs) == stdlib_sort(xs)` | | **Commutativity** | Order doesn't matter | `a + b == b + a` | | **Metamorphic** | Relationship between outputs | `sin(-x) == -sin(x)` | **Most effective** (OOPSLA 2025): Mo