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 for language-specific PBT and stateful testing tools. See examples for brief property test patterns per language. See formal-tools for theorem provers and bounded model checkers.

Property Categories

sorted(sort(xs))

len(xs) == len(sort(xs))

f(f(x)) == f(x)

deduplicate(deduplicate(xs))

g(f(x)) == x

decode(encode(x)) == x

my_sort(xs) == stdlib_sort(xs)

a + b == b + a

sin(-x) == -sin(x)

Most effective (OOPSLA 2025): Model-based properties (~80% bug detection), postconditions (~65%). Least effective: properties that reimplement the logic under test.

Anti-pattern: Don't reimplement the function in the property. Properties should be simpler than the code they test.

When to Apply

• Critical algorithms (sort, search, crypto, compression)
• Financial calculations (rounding, currency conversion)
• Consensus/distributed protocols (invariants across nodes)
• Safety-critical systems (medical, automotive, aerospace)
• Data structure invariants (balanced tree, heap property)
• Serialization round-trip (encode/decode fidelity)
• Stateful systems (databases, queues, caches) -- via stateful PBT

When NOT to Apply

• UI rendering, visual layout
• Simple CRUD endpoints
• Configuration management
• Non-critical utility code
• Rapidly changing requirements (properties are expensive to maintain)

Anti-patterns

• Happy-path-only properties: Properties must cover edge cases -- that's their primary value
• Skipping stateful testing for stateful systems: Use model-based stateful PBT (Hypothesis RuleBasedStateMachine, jqwik stateful)
• Ignoring counterexamples: Shrunk counterexamples are gold -- always convert to permanent regression tests
• Properties that test the framework:

  assert fast_check works

  is not

  assert my_code works

• Permanently skipped/pending properties: Zero-skip policy -- skip = unfinished work
• Conflating PBT with unit testing: PBT explores input space; unit tests verify known examples. Use both.
• Not using shrinking: If counterexample is 500-line input, it's useless. Shrinking finds minimal failing case.
• Reimplementing logic in properties: Property should be simpler than the code. If property is as complex as implementation, it adds no confidence.

Shrinking

Shrinking transforms a failing complex input into the minimal input that still fails. This is the most valuable feature of PBT frameworks.

• Integrated shrinking (Hypothesis, Hedgehog): Generates shrink tree during generation. Preserves generator invariants. Superior approach.
• Type-based shrinking (QuickCheck): Separate shrinker functions. Can violate generator constraints.
• Always investigate shrunk counterexamples: They reveal the essential failure, stripped of noise.

PBT vs Fuzzing (decision guidance)

Proof Strategies

• Simplification: Reduce by known rules, use shrinking to find minimal counterexamples
• Arithmetic: Generate numeric edge cases (0, 1, MAX, negative, overflow boundaries)
• Case analysis: Split on constructors/variants, test each branch independently
• Induction: Recursive/sequential properties via stateful testing
• Fuzzing: Empirical exploration when properties are hard to specify formally
• Metamorphic relations: When oracle is unknown, test relationships between outputs

Theorem Hierarchy

Main Property (Goal)
|-- Supporting Property 1
|   +-- Helper Property 1a
|-- Supporting Property 2
+-- Edge Case Property 3

Workflow (language-neutral)

1. PLAN -- Identify correctness, safety, invariant, and termination properties. Design hierarchy. Choose property categories.
2. CREATE -- Write property test files. One property per concern. Tag by category (postcondition, invariant, inverse, etc.).
3. VERIFY -- Run all properties. Count unproven (skipped/pending). Analyze counterexamples via shrinking.
4. REMEDIATE -- Fill in each skipped property using proof strategies. Convert every counterexample to a permanent regression test.

Constitutional Rules (Non-Negotiable)

1. CREATE First: Generate all property test artifacts from plan design before verification
2. Complete All Proofs: Zero skipped/pending properties in final code
3. Totality Required: All definitions must terminate
4. Target Mirrors Model: Implementation structure corresponds to proven model
5. Iterative Remediation: Fix proof failures, don't abandon verification

Validation Gates

Exit Codes