← Back to Proof
AgentProof

Skill · Version 1.0.0

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 helps

When 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.

Details…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)

  1. 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.
  2. 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.

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.
  • 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