← Back to Proof
AgentProof
Validating property tests
Checks the credibility of property tests by validating independent expectations, meaningful generated cases and sensitivity to known faults.
test-oracle-generator-validation
See how it helpsWhen is it useful?
Use it when generated tests always pass and you suspect their inputs or reference model avoid the behavior under test.
What does it help you do?
- Uses an independent reference instead of copying production logic.
- Inspects generated sample distributions and reachable transitions.
- Injects known defects to check that properties can actually fail.
Try asking this
Validate a balance property suite whose generated withdrawals are all rejected. Inspect generated amounts to ensure both valid and rejected withdrawals occur. Introduce a known balance defect and verify the suite finds a useful counterexample.
Detailed documentation
Read the skill’s original instructions, examples and checks in their authored language.
Show less
Test Oracle & Generator Validation
Use this skill to verify that property-based tests and reference models are genuinely capable of catching bugs, rather than passing vacuously or duplicating production bugs.
Guarding Against Flawed Oracles (Feynman's Falsification Principle)
- Never Copy Production Implementation into the Oracle:
- If the test asserts
expect(calculateFee(x)).toBe(prodCalculateFeeCopy(x)), both sides share the same off-by-one or rounding bug. - Instead, verify using:
- A Radically Simpler Reference Model: An in-memory, unoptimized, obviously-correct data structure (e.g., an append-only array of integer ledger entries compared against a complex SQL/cache service).
- Inverse / Reconstruction Checks: Verify the output by reconstructing the input or checking structural properties (e.g., sum of allocated line-item taxes equals total invoice tax; every output item satisfies the query predicate).
- Algebraic & Domain Laws: Conservation, bounds, idempotency, and state-transition invariants.
- If the test asserts
- Never Mask Failures with Loose Tolerances:
- Never use floating-point tolerances (
toBeCloseTo,abs(a - b) < 0.01) for financial calculations, credit balances, inventory counts, or quota checks. Money and quotas must balance to the exact minor unit, or follow an explicitly specified rounding remainder rule.
- Never use floating-point tolerances (
Eliminating Vacuous Truths & Starved Branches
A property test is vacuously true when it passes 1,000 runs only because the interesting branch was never entered.
- Inspect Sample Distributions: Collect classification statistics (
fc.statistics,event()/target()in Hypothesis, or counters across runs) to verify what percentage of generated runs actually hit:- Approved vs. rejected transitions
- Boundary conditions (zero balance, exact quota exhaustion, multi-step partial refunds)
- Multi-actor / concurrent conflict paths vs. trivial non-overlapping keys
- Assert Non-Trivial Reachability: Require that a test campaign exercises all targeted command types and state transitions at least once; fail the test setup if 100% of generated operations are rejected by preconditions.
Validating Sensitivity via Fault Injection / Mutation
- Before trusting a new property suite, verify that it catches a known or injected defect:
- Temporarily Perturb a boundary (
>to>=, omit an idempotency check, drop a tenant filter, or alter a rounding mode) or run against a known buggy commit/fixture. - Confirm that the property fails quickly and shrinks to a clear counterexample.
- Restore the production code once the test's sensitivity is proven.
- Temporarily Perturb a boundary (
- Clearly state in test reports what the property suite proves within the tested domain and what remains outside its scope (e.g., external payment gateway behavior, real network packet loss, or unmodeled database triggers).
Checklist
- Is the test oracle independent of the production algorithm (simpler reference model, algebraic law, or inverse check)?
- Have vacuous truths been ruled out by verifying that generated samples actually reach and execute the target branches?
- Are financial and quota assertions exact (zero arbitrary floating-point tolerance)?
- Has the property been validated against a known or injected fault to confirm it detects real violations?
Included files 1
SKILL.md
