Property-Based Testing §

Pattern: A named solution to a recurring problem.

State a rule that must hold for every valid input, let a generator search for an input that breaks it, and treat the smallest failing case as the bug report.

Also known as: Generative Testing, QuickCheck-Style Testing

You ask an agent for a function and its tests. It comes back with six example tests, all green. Look at those six inputs. Every one is a case the agent thought of while it was writing the code, so the tests and the implementation share the same blind spots. The suite tells you the agent agrees with itself. It doesn’t tell you what happens on the input nobody imagined.

Understand This First §

Context §

This is a tactical pattern for the moment you decide how to check code, whether you wrote it or an agent did. You already have Tests and know what a test oracle is. The question is where the inputs come from.

In example-based testing, a person (or an agent) picks each input and its expected output. In property-based testing, you write a rule that relates inputs to outputs, and a tool generates the inputs. Koen Claessen and John Hughes introduced the approach with QuickCheck for Haskell in 2000. Libraries now exist for most mainstream languages: Hypothesis for Python, fast-check for JavaScript and TypeScript, jqwik for Java, and proptest for Rust among them.

Agentic coding changes what the pattern is for. When a model writes both the code and its tests in one pass, the tests tend to encode whatever the model just built. Properties give you a check written against intent.

Problem §

Example tests cover the cases their author anticipated. When the author is also the implementer, the gaps reflect the same blind spots as the code. Typical omissions include the empty list, the one-cent remainder, the timestamp at midnight, and the string with a combining accent. An agent makes this worse because it produces green example suites quickly and confidently, and a green suite reads as evidence.

How do you check code against the inputs nobody thought to write down, without hand-writing thousands of cases?

Forces §

Solution §

Write properties from the specification, run them against generated inputs, and adjudicate every counterexample before changing anything.

Describe the input space with a generator. A generator (also called a strategy or an arbitrary) produces valid inputs of a given shape. It might produce integers in a range, lists of customer records, or sequences of API calls. Good generators reach the edges on purpose, so empty collections, zero, maximum values, and unusual Unicode show up far more often than pure chance would allow.

State properties, not answers. A property is a rule that holds for every input the generator can produce. A few shapes recur:

Let the tool search and shrink. The framework runs the property against hundreds or thousands of inputs. When one fails, it shrinks the input: it keeps simplifying the failing case while the failure persists, and reports the smallest version it can find. A 300-element list that broke your merge function might shrink to two elements. That minimal case is usually enough to see the bug at a glance.

Here’s what that looks like with Hypothesis, for a function that splits an invoice total, in integer cents, into equal installments:

from hypothesis import given, strategies as st

@given(total=st.integers(min_value=0, max_value=10_000_000),
       parts=st.integers(min_value=1, max_value=48))
def test_installments_add_up(total, parts):
    shares = split_into_installments(total, parts)
    assert len(shares) == parts
    assert sum(shares) == total
    assert max(shares) - min(shares) <= 1

The test never names an expected output. It says three things any correct answer must satisfy: the right number of installments, nothing gained or lost, and no installment more than a cent larger than another. Those rules come from the billing requirement, not from the code.

For agentic work, add three disciplines.

Derive properties from intent, separately from the implementation. Have the agent read the specification, the Acceptance Criteria, or the documentation. It should write properties before it writes the code, or in a separate session that never sees the code. Some Spec-Driven Development tools now build this in: Kiro extracts properties from requirements written in EARS (Easy Approach to Requirements Syntax) and runs them against the implementation.

Adjudicate before you fix. A counterexample means the code, the property, and the specification disagree. One of them is wrong, and it isn’t always the code. Sometimes the property is too strict. Sometimes the specification never said what should happen. Decide which one is wrong before anyone edits anything, and treat a change to a property or a spec as a decision that needs human review. An agent that “fixes” a failure by relaxing the property is committing Reward Hacking one level up from editing an assertion.

Feed the shrunk case back as the repair signal. A minimal counterexample plus the violated property is a much better prompt than a stack of failing tests. It gives the agent’s Verification Loop one small, concrete fact to explain. Researchers building LLM repair loops have measured the difference. A violated property plus the simplest failing input fixed more bugs than input-output mismatches from generated test cases. Once the bug is fixed, pin that input as a permanent example so it runs on every build. Record the random seed too, so any failure replays exactly; Determinism matters as much here as anywhere.

Example Prompt: “Read docs/billing.md, not the source. Write Hypothesis properties for split_into_installments that follow from the requirements there, then run them. Don’t edit the implementation, and don’t weaken a property to get a pass. If the docs leave a case undefined, list it as a question instead of guessing.”

How It Plays Out §

An agent implements split_into_installments and adds four example tests: 10,000 cents in four parts, 9,000 in three, and so on. All pass. The developer adds the three properties above, written from the billing spec, and runs them. Hypothesis fails within a second and shrinks to total=1, parts=2: one cent split two ways returns [0, 0]. The implementation computed every share as total // parts and dropped the remainder, which no round-number example would ever expose.

The developer hands the agent the counterexample. Its first attempt changes the second assertion to abs(sum(shares) - total) < parts. The test goes green, and the review catches the edit because the property file is supposed to be read-only for the agent. On the second attempt the agent leaves the properties alone and distributes the remainder cents across the first installments. The total=1, parts=2 case becomes a pinned example.

A team building a room-booking service writes its requirements in EARS form. One requirement says, “WHEN a user moves a booking, THE booking service SHALL reject the move if the new time overlaps another booking for the same room.” Their spec tool derives a stateful property: no sequence of create, move, and cancel operations may leave two live bookings overlapping in one room. An agent writes a fresh implementation. The first run fails on two back-to-back bookings, 10:00 to 11:00 and 11:00 to 12:00, which the property calls an overlap.

Nothing is wrong with the code. The generated property treated end times as inclusive, while the product treats them as exclusive, so a person reviews and approves a fix to the property. The next run fails differently, shrinking to three operations: book 10:00 to 11:00, book 11:00 to 12:00, move the first to 10:30 to 11:30. The move is accepted. The move handler only checked whether the new start time fell inside another booking, so this one is a code bug, and the agent fixes it.

A third question surfaces while the team is adjudicating: can a booking have zero length? The requirements never say. That one goes back to the product owner as a specification change, not to the agent.

Warning: Don’t let the agent that writes the implementation also edit the properties in the same session without review. The easiest way to make a failing property pass is to make it say less, and a weakened property stays green forever. Review property and spec changes as their own diff.

Consequences §

Benefits. Properties find the failures example tests are structurally bad at finding: boundaries, empty and extreme values, odd encodings, and unexpected orderings of operations. Shrinking turns a random failure into a minimal, readable bug report, which is close to the ideal input for an agent’s repair loop. Because a property describes intent rather than one output, it’s harder to satisfy by tailoring code to the test. Writing properties also forces a useful conversation about what the code is supposed to guarantee, and the questions the specification can’t answer surface early.

The evidence for agent use is real but recent. In 2025, Muhammad Maaz, Liam DeVoe, Zac Hatfield-Dodds, and Nicholas Carlini ran an agent that inferred properties from code, docstrings, and documentation, then wrote and ran Hypothesis tests across 100 popular Python packages. Maintainers merged resulting fixes in NumPy, aws-lambda-powertools, and Hugging Face’s tokenizers. The aws-lambda-powertools bug, a dictionary-chunking helper that kept returning its first chunk, fell to a round-trip property: slicing a dictionary and reassembling the pieces should give back the original.

Liabilities. False alarms cost real time. The same agent produced 984 bug reports. The authors hand-checked 50 of them and judged 56% to be real bugs, and only 32% worth sending to maintainers. A scoring rubric helped: among the 21 top-ranked reports, 86% were valid. Before reporting anything, they sent the highest-priority candidates to three expert reviewers, at an average of an hour of review per bug.

Even a real find needed judgment: the agent located a genuine bug in NumPy’s random.wald but proposed the wrong fix, and the actual cause was a numerically unstable calculation. And sometimes the property is what’s wrong. The agent flagged python-dateutil’s Easter calculation for returning non-Sunday dates under the Julian calendar, and the maintainers explained that was intended. Adjudication is part of the pattern, not an afterthought.

Good generators take work. Inputs that must satisfy many constraints, such as a valid order with consistent line items, taxes, and currency, can take longer to generate than the code takes to write. Stateful properties over sequences of operations are harder still, for people and for agents. Property runs are slower than example runs, so teams usually run a modest number of cases on every commit and a larger search on a schedule.

A passing property is evidence, not proof. The generator samples the input space; it doesn’t cover it. Kiro’s documentation makes the same distinction. When you need a guarantee over every input, that’s Formal Verification, and the properties you’ve already written are a good first draft of its specification. Properties also don’t replace a pinned output check like Approval Testing, which asks “did anything change?” rather than “is this rule still true?” To check that a property can fail at all, break the implementation on purpose, as Mutation Testing does, and confirm the property goes red.

Related Articles §

Sources §