proof-driven

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

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): 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)

Aspect	PBT	Fuzzing
Input generation	Guided by properties	Guided by code coverage
Oracle	User-written property assertions	Crashes/exceptions/timeouts
Best for	Correctness, algorithms, contracts	Security, memory safety, crash detection
Convergence (2025)	Hybrid tools (Bolero, Antithesis) combine both approaches

---

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

Gate	Pass Criteria	Blocking
Framework	PBT framework available and configured	Yes
Properties	All property tests pass	Yes
Unproven	Zero skipped/pending properties	Yes
Coverage	>= 80% line coverage	If present

Exit Codes

Code	Meaning
0	All properties pass, zero unproven/skipped
11	Property testing framework not available
12	No property tests created
13	Property tests failed or proofs incomplete
14	Coverage gaps (properties missing)