Property-based testing for agent-written code

Property-based testing checks agent-written code against invariants taken from spec.md, such as “the instalments sum to the total”, on 100 or more generated inputs per run. Because the library picks the inputs, an agent cannot overfit the tests by choosing examples. fast-check, Hypothesis and proptest shrink each failure to a small input that becomes a permanent regression test.

An agent implements “split an invoice total into instalments” and ships four example tests. splitCents(1000, 3) returns [333, 333, 334], the tests expect exactly that, and CI is green. The spec said earlier instalments are never smaller than later ones, so that example already breaks the spec’s ordering rule, yet the test expects it, because the agent read the expected value off its own code. Worse, splitCents(2, 4) returns [1, 1, 1, -1]: a negative payment. This page is for the developer who approves agent pull requests on evidence and wants a test suite the agent cannot quietly fit to its own code.

What you get from property tests on agent code

• A method for turning spec requirements into invariants, with a table of the eight property shapes that cover most business logic.
• Working property tests in three stacks (fast-check with Vitest, Hypothesis with pytest, proptest with Cargo), with the real failure output each library prints.
• A regression-pinning routine that turns every shrunk counterexample into a test that runs on every commit, forever.
• Four copy-paste prompts: extract invariants from a spec, write property tests in a test-only task, triage a counterexample, and audit existing properties for tests that assert nothing.
• CI settings for a fast per-pull-request run and a deep nightly sweep, including the Hypothesis CI profile trap.

Why do example tests fail as an oracle for agent code?

An example test checks one input the author chose. When the agent writes both the implementation and the examples, it chooses inputs its implementation already handles, and it reads the expected values off its own code. The suite then describes the code rather than the requirement. This is the “grading its own homework” problem that oracle strength measures after the fact.

A property removes the choice. It states a rule that must hold for every valid input, and the library generates the inputs, including the awkward ones: zero, one, the maximum, totals smaller than the number of parts. When a rule fails, the library shrinks the input, repeatedly simplifying it while it still fails, and reports a small counterexample you can read.

Properties do not replace examples. Keep a few examples as documentation of typical behaviour; let properties carry the rules. Kiro builds the same idea into its spec workflow, using property-based tests to “check that the code matches the spec” (Kiro README on GitHub, read 2026-09-26); see Kiro compared.

Where do properties come from in spec.md?

Each property is a sentence in the spec rewritten as “for all valid inputs, …”. Start from requirements written as observable outcomes, in the format from spec-driven development:

### BILL-4: Split an invoice total into instalments
- The instalments sum exactly to the total, in minor units (cents).
- No two instalments differ by more than 1 cent.
- Earlier instalments are never smaller than later ones.
- The total is 0 to 10,000,000 cents and the count is 1 to 24;
  anything else is rejected with a RangeError.

Four bullets give four properties. Most requirements fall into one of these shapes:

Shape	Spec sentence looks like	Property	Example
Conservation	“adds up to”, “nothing is lost”	An aggregate of the output equals one of the input	Instalments sum to the total; ledger debits equal credits
Bounds	“at most”, “never negative”, “within”	Every output value lies in a range	Spread of at most 1 cent; discount never exceeds the price
Ordering	“sorted by”, “earlier … never smaller”	Adjacent outputs respect an order	Instalments non-increasing; search results sorted by score
Round trip	“can be exported and re-imported”	decode(encode(x)) equals x	CSV export and import; URL building and parsing
Idempotence	“normalised”, “applying twice changes nothing”	f(f(x)) equals f(x)	Address normalisation; migration re-run
Reference model	“behaves like”, “same result as the old system”	Output equals a simple, slow, obviously correct version	New pricing engine against the legacy function
Metamorphic	“adding a filter never adds results”	A related input changes the output in a predictable way	Narrower date range returns a subset
Rejection	“anything else is rejected”	Invalid inputs raise the named error	Totals out of range throw RangeError

A requirement that fits no shape is often vague. “Instalments should be fair” has no property; “no two instalments differ by more than 1 cent” does. When extraction stalls, fix the spec, not the test.

How do you run property-based testing on agent-written code?

The order matters: invariants are approved and property tests exist before the implementation task starts, and the implementing agent cannot edit them. Otherwise the agent fits the properties to the code as easily as it fits examples.

1. Extract the invariants. Give an agent the requirement and ask for invariants only, no code (first prompt below). You approve the list. This is the one place you read carefully, and it is a few lines of English, not a diff.

2. Write the property tests in a test-only task. A separate session writes one property per approved invariant, tagged with the requirement ID ([BILL-4]) so the traceability check finds it. Generators follow the spec’s input ranges exactly.

3. Record a negative control for each property. Break the behaviour on purpose in a scratch branch and confirm the property goes red. A property that stays green against a wrong implementation asserts nothing. The routine is on oracle strength.

4. Lock the property files. Add them to the agent’s deny rules and to CODEOWNERS, as described in protecting the oracle. From now on they are pre-existing checks.

5. Run the implementation loop against the properties. The implementing agent iterates until the suite is green. It may add example tests; it may not touch the properties.

6. Triage every shrunk counterexample. Each failure is one of three things: a wrong property, an ambiguous spec, or a real bug. Only the third is fixed in code; the first two go back to steps 1 and 2 with a human decision.

7. Pin the counterexample, then fix. Add the exact failing input as a permanent regression case in the same pull request as the fix, so the evidence shows it red before and green after.

Write the properties in fast-check, Hypothesis or proptest

The three libraries share the model: generators (fast-check calls them arbitraries, Hypothesis strategies, proptest strategies), a property body, a run count, and shrinking. Versions below were checked on 2026-09-26: fast-check 4.10.2 with @fast-check/vitest 0.5.0 and Vitest 5.0.2, Hypothesis 6.168.2 with pytest 9.1.1, and proptest 1.11.0. Every failure shown was produced by running these tests against the agent’s first implementation, which rounds total / parts and gives the remainder to the last instalment.

TypeScript (fast-check)

Install with npm i -D fast-check @fast-check/vitest. test.prop runs the body 100 times by default (numRuns).

tests/billing/split.property.test.ts

import { describe, expect } from 'vitest';
import { fc, test } from '@fast-check/vitest';
import { splitCents } from '../../src/billing/split';

const total = fc.integer({ min: 0, max: 10_000_000 });
const parts = fc.integer({ min: 1, max: 24 });

describe('BILL-4 splitCents', () => {
  test.prop([total, parts])('[BILL-4] instalments sum exactly to the total', (t, n) => {
    expect(splitCents(t, n).reduce((a, b) => a + b, 0)).toBe(t);
  });

  test.prop([total, parts])('[BILL-4] no two instalments differ by more than 1 cent', (t, n) => {
    const out = splitCents(t, n);
    expect(Math.max(...out) - Math.min(...out)).toBeLessThanOrEqual(1);
  });

  test.prop([total, parts])('[BILL-4] earlier instalments are never smaller', (t, n) => {
    const out = splitCents(t, n);
    for (let i = 1; i < out.length; i++) expect(out[i - 1]).toBeGreaterThanOrEqual(out[i]);
  });

  test.prop([fc.oneof(fc.integer({ max: -1 }), fc.integer({ min: 10_000_001 })), parts])(
    '[BILL-4] rejects totals out of range',
    (t, n) => {
      expect(() => splitCents(t, n)).toThrow(RangeError);
    },
  );
});

The run against the first implementation:

× [BILL-4] no two instalments differ by more than 1 cent (with seed=191597017)
Error: Property failed after 1 tests
{ seed: 191597017, path: "0:1:0:0:0:2:1:1", endOnFailure: true }
Counterexample: [2,4]
Shrunk 7 time(s)
Caused by: AssertionError: expected 2 to be less than or equal to 1

To replay exactly that failure, pass the printed object as the second argument: test.prop([total, parts], { seed: 191597017, path: '0:1:0:0:0:2:1:1', endOnFailure: true }).

Python (Hypothesis)

Install with pip install hypothesis. @given runs 100 examples by default (max_examples), each with a 200 ms deadline.

tests/billing/test_split_properties.py

from hypothesis import given, strategies as st
from billing.split import split_cents

totals = st.integers(min_value=0, max_value=10_000_000)
parts = st.integers(min_value=1, max_value=24)


@given(totals, parts)
def test_bill_4_sum_is_exact(total, n):
    assert sum(split_cents(total, n)) == total


@given(totals, parts)
def test_bill_4_spread_at_most_one_cent(total, n):
    out = split_cents(total, n)
    assert max(out) - min(out) <= 1

Python’s round rounds half to even, so the same bug surfaces differently:

E       assert (2 - 0) <= 1
E        +  where 2 = max([0, 0, 0, 2])
E        +  and   0 = min([0, 0, 0, 2])
E       Failing test case: test_bill_4_spread_at_most_one_cent(
E           total=2,
E           n=4,
E       )

Locally, Hypothesis saves failing inputs in .hypothesis/examples and replays them first on the next run. Its documentation allows committing that directory only if you also pin Hypothesis to an exact version, because the stored entries are opaque. @example is the durable form.

Rust (proptest)

Install with cargo add --dev proptest. Each proptest! test runs 256 cases by default, overridable with PROPTEST_CASES.

src/billing.rs

#[cfg(test)]
mod tests {
    use super::*;
    use proptest::prelude::*;

    proptest! {
        #[test]
        fn bill_4_sum_is_exact(total in 0u64..=10_000_000, parts in 1u32..=24) {
            let out = split_cents(total, parts).unwrap();
            prop_assert_eq!(out.iter().sum::<u64>(), total);
        }

        #[test]
        fn bill_4_spread_at_most_one_cent(total in 0u64..=10_000_000, parts in 1u32..=24) {
            let out = split_cents(total, parts).unwrap();
            let (max, min) = (*out.iter().max().unwrap(), *out.iter().min().unwrap());
            prop_assert!(max - min <= 1, "spread {} in {:?}", max - min, out);
        }
    }
}

The run against the first implementation:

# paths shortened
proptest: Saving this and future failures in .../proptest-regressions/billing.txt
Test failed: spread 2 in [29740, 29740, 29740, 29738] at src/billing.rs:27.
minimal failing input: total = 118958, parts = 4

“Minimal” means proptest could not simplify further along its shrinking path, not that no smaller failing input exists. fast-check and Hypothesis found 2, 4; proptest stopped at 118958, 4. Both are valid regression cases.

All three libraries caught a bug that four passing example tests hid. In the TypeScript run, a second property (ordering) also failed, with a counterexample of [791421, 14] after 24 shrinks. One root cause often trips several properties; triage the smallest counterexample first.

Turn every shrunk failure into a permanent regression test

A random run finds a bug once. Unless you pin the input, the next run may not generate it again, and a later agent change can reintroduce the bug unnoticed. Pin every real-bug counterexample in the same pull request as the fix, and write the date and the observed wrong output in a comment.

Library	Pin the input with	Where it lives	Trap
fast-check	examples: [[2, 4]] in the test.prop options; examples run before the generated inputs	The property test file	Seed and path replay a run only while the arbitraries are unchanged; examples survive any refactor
Hypothesis	@example(total=2, n=4) above @given	The property test file	The .hypothesis database is local by default, and in CI Hypothesis disables it (see below), so only @example travels reliably
proptest	Commit proptest-regressions/*.txt; proptest replays those cases first	In proptest-regressions/ at the crate root, mirroring the source path (for example proptest-regressions/billing.txt)	The file stores seeds, as its own header says, so a changed strategy can replay a different input. Add a plain #[test] with the literal values as well

A pinned case must assert the rule it broke: [791421, 14] failed the ordering property, so a pin that checks only sign and spread would pass on the buggy code. The fast-check and Hypothesis forms of the pinned case:

// Shrunk counterexamples from failed runs, 2026-09-26. Never delete.
// [2, 4] returned [1, 1, 1, -1]; [791421, 14] returned a larger last instalment.
test.prop([total, parts], { examples: [[2, 4], [791421, 14]] })(
  '[BILL-4] pinned counterexamples stay fixed',
  (t, n) => {
    const out = splitCents(t, n);
    expect(out.every((c) => c >= 0)).toBe(true);
    expect(Math.max(...out) - Math.min(...out)).toBeLessThanOrEqual(1);
    // [791421, 14] broke the ordering rule, so the pin must assert ordering too.
    for (let i = 1; i < out.length; i++) expect(out[i - 1]).toBeGreaterThanOrEqual(out[i]);
  },
);

from hypothesis import example, given

@given(totals, parts)
@example(total=2, n=4)  # 2026-09-26: returned [0, 0, 0, 2]
def test_bill_4_no_negative_or_lopsided_instalments(total, n):
    out = split_cents(total, n)
    assert min(out) >= 0 and max(out) - min(out) <= 1

Treat pinned cases as oracle files: they sit under the same deny rules and CODEOWNERS entry as the properties, and a pull request that removes one needs a human reason.

How many runs belong in CI?

The defaults (100 for fast-check and Hypothesis, 256 for proptest) keep a pull-request run to seconds, and that is the right gate for every change. Add a nightly sweep with far more runs and a fresh seed each night, so the search keeps covering new inputs without slowing pull requests down.

Hypothesis needs one extra step. When it detects a CI environment (CI, GITHUB_ACTIONS and similar variables), it loads its built-in ci profile: derandomize=True, database=None, deadline=None and print_blob=True (checked in Hypothesis 6.168.2 source). Derandomized runs generate the same inputs every time, so a nightly job that only raises the example count searches the same corner every night. Register a nightly profile that turns randomisation back on:

conftest.py

from hypothesis import settings

settings.register_profile(
    "nightly",
    settings.get_profile("ci"),
    max_examples=5_000,
    derandomize=False,
)

For fast-check, set the count in a Vitest setup file (listed in test.setupFiles in vitest.config.ts) with fc.configureGlobal({ numRuns: Number(process.env.FC_NUM_RUNS ?? 100) }); FC_NUM_RUNS is a name this setup file defines, not a fast-check variable. proptest reads PROPTEST_CASES directly.

.github/workflows/property-sweep.yml

name: property-sweep
on:
  schedule:
    - cron: '17 3 * * *'
  workflow_dispatch:
permissions:
  contents: read
jobs:
  sweep:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
        with:
          persist-credentials: false
      - uses: actions/setup-node@v7
        with:
          node-version-file: .node-version
      - run: npm ci
      - name: Deep fast-check run
        run: FC_NUM_RUNS=10000 npx vitest run property
      # Python: pytest --hypothesis-profile=nightly tests/
      # Rust:   PROPTEST_CASES=20000 cargo test

A red nightly run prints the seed (fast-check), the @reproduce_failure blob (Hypothesis, because the ci profile sets print_blob=True) or a new regressions line (proptest). The sweep reports; a developer or a test-only agent task pins the case and opens the fix.

Copy-paste prompts for property-based testing

Copy-paste prompt: extract invariants from the spec

Read specs/billing/spec.md, requirement BILL-4 only. Do not write code.

List every invariant the requirement implies, one per line, as
"For all <inputs within the stated ranges>, <rule>". Use these shapes where
they fit: conservation, bounds, ordering, round trip, idempotence, reference
model, metamorphic, rejection of invalid input.

For each invariant give:
- the spec sentence it comes from (quote it),
- the exact input ranges the generator must cover, taken from the spec,
- one input you expect to be hard for a naive implementation.

Then list every sentence in BILL-4 that you could NOT turn into an invariant
and say what is missing. Do not invent rules the spec does not state.

Copy-paste prompt: write property tests in a test-only task

Write property-based tests for the approved BILL-4 invariants below, using
fast-check with @fast-check/vitest (test.prop) in
tests/billing/split.property.test.ts.

Rules:
- One test.prop per invariant. Prefix each test name with [BILL-4].
- Generators cover exactly the spec's ranges. No .filter() that discards more
  than a small fraction of inputs; build the range into the arbitrary instead.
- Never reimplement splitCents inside a test. Assert the rule, not the result
  of a second copy of the algorithm.
- You may create or edit files under tests/ only. Do not touch src/.
- Run `npx vitest run tests/billing` and report which properties fail, with
  the counterexample and seed. Do not change a property to make it pass.

<paste the approved invariant list here>

Copy-paste prompt: triage a shrunk counterexample

The property "[BILL-4] no two instalments differ by more than 1 cent" failed
with counterexample [2, 4] (seed 191597017). Do not edit any file yet.

1. Call splitCents(2, 4) and show the output.
2. Quote the BILL-4 sentence the property encodes.
3. Classify the failure as exactly one of:
   WRONG PROPERTY - the test asserts something the spec does not say,
   AMBIGUOUS SPEC - the spec allows more than one reading,
   REAL BUG - the output violates a clear spec sentence.
4. For REAL BUG: name the line in src/billing/split.ts that causes it and
   propose the fix. Also list which other BILL-4 properties the same root cause
   would break.
Stop after the classification and proposal. I decide the next step.

Copy-paste prompt: audit existing properties for tests that assert nothing

Review every property-based test under tests/ (test.prop, fc.assert, @given,
proptest!). Do not edit files. For each one report:
- the requirement ID it cites, or NONE,
- whether it reimplements the code under test (a test that recomputes the
  expected value with the same algorithm),
- whether its generator is narrower than the spec's input ranges,
- whether any .filter()/assume() discards most generated inputs,
- whether it could pass against an implementation that always returns an
  empty or constant result.
Finish with a table: test, verdict (KEEP / STRENGTHEN / DELETE), one-line reason.

How do you run this in Claude Code, Codex and Cursor?

The libraries, tests and prompts are the same in all three tools. What differs is how you install the property-testing skill, how you keep the implementing agent out of the property files, and how you run the extraction headless. Commands were checked against Claude Code 2.1.283, Codex CLI 0.157.1 and the skills CLI 1.7.0 on 2026-09-26.

Trail of Bits publishes a property-based-testing plugin (1.2.2) whose skill writes and reviews property tests for Hypothesis, fast-check, proptest and more, and triages a shrunk counterexample into “a wrong property, an ambiguous spec, or a real bug” (plugin README, read 2026-09-26). That is the same triage as step 6 above. It is one skill, so its context cost is its description until the agent invokes it.

Claude Code

Install the skill.

claude plugin marketplace add trailofbits/skills
claude plugin install property-based-testing@trailofbits

Extract invariants headless, with read-only tools, and save the result for your approval:

# Terminal or CI, from the repository root
claude -p "$(cat prompts/extract-invariants.md)" \
  --allowedTools "Read,Grep,Glob" \
  --max-budget-usd 2 --output-format json > bill-4-invariants.json

Lock the properties during implementation. Add deny rules to .claude/settings.json; they apply in every permission mode:

{
  "permissions": {
    "deny": [
      "Edit(**/*.property.test.ts)",
      "Edit(**/test_*_properties.py)",
      "Edit(**/proptest-regressions/**)"
    ]
  }
}

Deny rules do not stop a script that writes files itself; add the sandbox denyWrite paths from protecting the oracle for that.

Codex

Install the skill.

codex plugin marketplace add trailofbits/skills
codex plugin add property-based-testing@trailofbits

Extract invariants headless. A read-only sandbox is enough, because extraction writes no files:

# Terminal or CI, from the repository root (Codex CLI 0.157.1)
codex exec --sandbox read-only -o bill-4-invariants.md "$(cat prompts/extract-invariants.md)"

Implementation loop. Use /goal with a condition such as every [BILL-4] property in tests/billing passes and no file under tests/ or proptest-regressions/ is modified. Do not rely on the condition alone: fail the task in CI if git diff --name-only origin/main... -- tests/ '**/proptest-regressions/**' (the CI checkout needs fetch-depth: 0, or fetch origin/main first) lists anything in an implementation pull request. Enforcement that runs before the edit is on protecting the oracle.

Cursor

Install the skill with the cross-agent skills CLI:

npx skills add trailofbits/skills --skill property-based-testing --agent cursor

Extract invariants by pasting the first prompt into the agent in Plan Mode, so it reports before it writes anything.

Implementation loop. Run the implementing agent in a separate chat from the one that wrote the properties, so it starts without the test author’s reasoning. Before you accept its result, confirm that git diff --name-only -- tests/ is empty, and put the property files under CODEOWNERS so a pull request that edits them needs a named reviewer. Cursor’s own hooks can block the edit earlier; the setup is on protecting the oracle.

How do you know the properties are strong enough?

Nobody reads every generated input, so the evidence has to be mechanical:

• Every invariant maps to a property with a requirement ID, and the traceability check fails the build when a requirement has no test.
• Every property has a negative control: a deliberate violation that turned it red, recorded in the pull request.
• Mutation score on the module clears the team’s threshold. A property suite with many surviving mutants is asserting less than it appears to; see oracle strength.
• Pinned counterexamples are present and untouched, verified by the provenance check on oracle files.
• The nightly sweep is green, or its failures are triaged within a working day.

The developer who owns the change approves the invariant list and the triage of each counterexample. The tech lead owns the oracle paths and the nightly sweep. Record all five items in the evidence bundle so a reviewer reads evidence instead of the diff.

What breaks when you use property-based tests with agents?

The property reimplements the code. The agent writes expect(splitCents(t, n)).toEqual(mySplit(t, n)), where mySplit is the same algorithm. Both share the bug and the test always passes. Recovery: assert rules, not outputs. A reference model is legitimate only when it is simpler and independently correct, such as a legacy function or a brute-force version.

The generator is narrower than the spec. fc.integer({ min: 1, max: 100 }) for a total that may be zero or ten million never tests the edges. Recovery: copy the ranges from the spec into the generator, and include the endpoints in examples or @example.

Filters throw away most inputs. .filter(t => t % n === 0) keeps only easy totals, and the library gives up or tests almost nothing. Recovery: build valid inputs directly (generate n and a quotient, multiply) instead of filtering.

The agent weakens a property to go green. It loosens <= 1 to <= 2, narrows a range, or deletes a pinned example. Recovery: the property files are oracle files under deny rules and CODEOWNERS; a same-change edit to them fails the provenance check.

Hypothesis fails on deadlines, not logic. The default 200 ms deadline turns a slow first call into DeadlineExceeded locally, while CI passes because the ci profile sets deadline=None. Recovery: fix genuine slowness, or set an explicit deadline for that test with @settings.

The nightly sweep keeps finding nothing. In Hypothesis this is usually the derandomized ci profile repeating the same inputs. Recovery: load a profile with derandomize=False, as shown above.

A replayed failure does not reproduce. A fast-check seed and path, or a proptest seed, stop matching once someone changes the generator. Recovery: pin the literal input values, not only the seed.

Where to go next with property-based testing

Spec-driven development Requirements with IDs and a traceability check: the source every property is taken from.

How strong is your oracle? Mutation score and negative controls that show whether your properties catch bugs.

Protecting the oracle Deny rules, sandbox paths and CODEOWNERS that keep agents out of property files.

Model-graded checks Rubric judges for behaviour that no invariant can express.

Characterization tests Pin legacy behaviour first, then use it as the reference model for properties.

The evidence bundle Where the invariant map, negative controls and pinned cases go in each pull request.