Re: [RFC] Property-based testing for Postgres

On Monday, November 2nd, 2026 at 5:33 PM, Jeff Davis <pgsql(at)j-davis(dot)com> wrote:

> On Mon, 2026-11-02 at 21:28 +0000, Greg Burd wrote:
> > I would rather present a small, sound, reproducible core and grow it
> > from there if there is interest.
> >
> > So, is there appetite for a PBT framework in the tree on these terms?
> > If
> > this is a non-starter, that is useful to know now. If it's worth
> > pursuing, I'd like to hear from you.

Hey Jeff,

> Thank you for including a README, that's helpful.

Thanks for taking a look at the README.

> Right now it's about 4KLOC, which seems reasonable for a new testing
> approach, if it's useful.

Agreed, the first intro on the list was intentionally "bite-sized" so as
to test the waters.

> I'd suggest that we try to control the scope here. Some of these seem
> like property testing for the sake of property testing.

Again, just a demo at this point. None of the examples given were meant
to illustrate how PBT pays off in practice within Postgres. The intention
was to have very small examples to educate people on the concepts without
distracting them with too many details. The sqrt bound is exactly the kind
of thing I would drop before proposing a real set: it is a contrived
property on a scalar function, and the README itself warns against inventing
a formula to check a function. Point taken that the demo blurred the line.

> +/*
> + * sqrt bound: S = sqrt(abs(X)) is non-negative and, since numeric
> sqrt rounds
> + * to a scale, S*S must not exceed abs(X) by more than a small
> relative-plus-
> + * absolute tolerance. This is a sound one-sided bound: an exact sqrt
> gives
> + * S*S = X, and the only slack is the rounding of the last digit, well
> within
> + * abs(X) * 1e-10 + 1e-10. (The symmetric lower bound is scale-
> dependent and
> + * fiddly to state soundly, so we assert only the clean upper side
> plus the
> + * sign.)
> + */

Yep, all those PBTs were basic examples I'd remove before offering up a
solid set of real tests for commit.

> It seems much more valuable to test, say, data structure invariants,
> where we are likely to get creative with optimizations and might break
> something. Is this property testing system good for that?

Yes, and that is one area where I think it earns its place. I kept those
areas out of the first cut to keep it bite-sized, but they already exist
in the larger tree and are a better advertisement than the scalar ones:

- binaryheap: build a heap from random inserts, then assert pop order is
sorted, the first element is the minimum, and an incrementally-built heap
matches one built in a batch. That is a pure data-structure invariant on
binaryheap.c, no SQL involved.

- btree / index scans: a differential oracle, an index scan must return
the same rows as a sequential scan, over random tables, predicates, and
index kinds (btree, gin, gist, partial, expression, multicolumn). This is
exactly the "we got creative with an optimization and broke something"
case you describe: the property doesn't know the right answer, it only
knows the two paths must agree, so any divergence is a bug by construction.

The three live bugs I cited in the first mail are all of that shape: an
optimization computing a different result than the unoptimized path (SSI
serialization, outer-join selectivity, MCV selectivity). Differential
oracles over data structures and plans are the strong suit; the scalar
round-trips are the warm-up.

> Also, how do you see this affecting the dev process? Do most people
> need to be aware of this framework, adding new tests along with
> features? Or would most of the value come from adding lots of new
> property tests in a big batch, hoping to catch some longstanding bugs?

Good question, mostly the former. Today we have a few models for testing:
regression tests pin exact output for a known case, TAP scripts a scenario,
and isolation tests pin an interleaving. A PBT is a fourth model that sits
alongside them, it pins a property that must hold across an input space the
author can't enumerate by hand. It doesn't replace any of those; the README
is explicit that a PBT belongs only where a disagreement is unambiguously a
bug, and that a good unit test beats a contrived property.

So no, most people would not need to think about it for routine work. The
value concentrates where someone is doing something risky (a new scan
optimization, a data-structure rework, a selectivity change) and wants a
standing net under that specific area. The person making that change adds
the property, the same way they'd add a regression test, because they know
what invariant their change must not break. The big-batch "mine for
longstanding bugs" mode does happen (that's how the three bugs surfaced), but
I'd treat that as a bonus, not the pitch; the durable value is the standing
differential net on the tricky areas, maintained by the people who work in
them.

> The timing of your proposal is not ideal, because AI is already finding
> a lot of bugs, so finding more might be a thankless exercise until this
> wave passes. So, if it doesn't get a lot of attention that may be the
> reason why.

I'd argue the opposite.

This style of testing fits AI well: the properties are easy for an agent to
write, cheap to run, and the counterexample the engine shrinks to is exactly
the artifact an agent can consume to produce a fix, a minimal input plus a
seed that replays it.

An LLM alone can find bugs, but it does so by reading and reasoning, which
burns tokens fast and doesn't reproduce, a property test is the opposite.
The engine does the searching deterministically and cheaply, and the agent
spends its tokens only on the one minimal case that actually failed. So I
see PBT less as "more bugs to triage during the AI wave" and more as the
scaffolding that makes the AI wave efficient, reproducible, and long-term
helps collapse and manage that wave..

What I'm actually hoping people latch onto is using this as the foundation
for harnesses that eliminate *categories* of bugs in tricky code, not one
test per bug, but one property that rules out a whole class of bugs.

Ideally the division of labor is: humans and LLMs write ordinary regression
tests for the specific things they know a change must get right, and they
write a property for the invariant that change must never violate. Then the
engine, not the person, finds the input that breaks it. The human states
the law; the machine hunts down the counterexample. That split is where I
think the leverage is, and it's why I'd rather land a small sound core now
and grow it than wait for the wave to pass.

> Regards,
> Jeff Davis

best.

-greg