This is a topic that any post-2022 software engineer has to take seriously. So here is my take on things. First let's review what the dangers are that we are trying to avoid here.
- LLMs hallucinate, and frequently have a shallow (yet very confidently stated) understanding of the problem domain.
- LLMs become easily confused when navigating complex structures, such as deeply nested JSON structures.
- LLM-generated code is produced quickly and in large volume, and it becomes a coma-inducing wall of text. We need a way to stay in control, make sure it's doing what it's supposed to do, while allowing the LLM to play to its strengths.
Here is what I've got for guardrails.
- Borrow correctness practices from functional programming. Use rigorous typing wherever possible. For Python that means leaning heavily on frozen Pydantic models and mypy validation.
- We can loosen our grip on the code itself as long as our test suite is bullet-proof. By "bullet-proof" what I mean is that the tests are clearly understood and vetted by at least one human, they all pass, they are comprehensive in covering everything that can go wrong, and in summary, they guarantee that when they are all satisfied, the software is correct. If we are confident on all these points then we don't need to understand the code completely.
- Automate your CI as much as possible. If it takes effort to do things correctly, people will cut corners.
- Constrain the blast radius. Make the LLM work in small, reviewable units. A 40-line function you fully understand beats a 400-line module you skimmed. Enforce this structurally: small PRs, tight function scope, clear module boundaries.
- Make illegal states unrepresentable. The functional-programming complement to your typing point. Don't just type
things rigorously — design types so the wrong thing can't be constructed. Use enums/
Literalinstead of strings,NewTypefor IDs that shouldn't be interchangeable, validators on your frozen models that reject bad data at construction. The LLM can't wire together a nonsensical state if the type system forbids it. - Property-based testing (1, 2). Human-written example tests share the human's biases and blind spots. Hypothesis generates adversarial inputs you didn't think of, which is exactly the coverage gap that matters when you're not reading the code closely.
- Maintain a human-authored spec/contract the code must satisfy. The tests verify behavior, but something has to define correct behavior independent of the code the LLM wrote — otherwise the LLM can write code and tests that agree with each other and are both wrong. Docstrings-as-contract, type stubs, or a literate description that predates the implementation.
- Pin and verify dependencies. LLMs hallucinate plausible-looking package names and APIs, a habit exploited by bad actors,
see "slopsquatting" (1,
2). Lockfiles,
pip-audit, and letting import/mypy failures catch fabricated APIs fast. - Track which code was AI-generated so review intensity can scale with risk. Heavier scrutiny on generated security-sensitive paths.
I think you're right that the "avoids your blind spots" framing undersells it. That framing is still example-based thinking with the examples outsourced to a random generator. The deeper thing is a shift in what a test is.
Here's the reframe I'd offer. An example-based test is an existential claim: "there exists an input (this one I wrote) for which the code behaves." A property is a universal claim: "for all inputs in this space, this relation holds." That's not a difference of coverage, it's a difference of logical quantifier. You've stopped asserting points and started asserting a theorem — with a domain of quantification (the strategy) and a predicate that must hold over it.
And once it's a universal claim, the interesting question stops being "did the test pass" and becomes "what is actually true about my function?" That's the part that I think is nagging at you. To write a good property you are forced to articulate an invariant — a law your code obeys — and most of the value is extracted before Hypothesis ever runs, in the act of discovering that the law exists and can be stated. The Semaphore tutorial gestures at this: figuring out the properties gives you deeper insight into the problem, sometimes leading to a better solution. The test suite becomes a byproduct of specification, not the specification a byproduct of tests.
This is why the canonical patterns are the ones they keep listing — round-trip (decode(encode(x)) == x),
idempotence (f(f(x)) == f(x)), commutativity, metamorphic relations (f(x) and f(transform(x)) relate
predictably even when you can't compute the expected output directly). These aren't a grab-bag of tricks.
They're the shapes that algebraic structure takes when projected into test form. A round-trip property
is just saying two functions are inverses. Idempotence is a monoid-ish law. When you reach for these, you're
really asking "what algebra does my function participate in?" — and the reason they recur across every
language's PBT library is that they're the observable consequences of structure that was always there in the
code, whether or not you'd named it.
So the deep idea, if I had to compress it: property-based testing is the executable half of type-driven design. Parse-don't-validate encodes the invariants you can make the compiler enforce; property tests cover the invariants you can't express in the type system but can still state as laws. Same worldview — "make the truth about this program explicit and checkable" — attacking from two sides. The type system proves what it can at compile time; Hypothesis empirically falsifies everything else at test time. QuickCheck came out of the Haskell community for exactly this reason: it's what you build when the types can't quite reach the property but you still want the property checked.
There's a genuinely interesting boundary question lurking here too, which might be the "something more" you're sensing: which invariants belong in the type (parse) versus in a property test (check)? That line isn't fixed — it moves with how much your type system can express, and part of the craft is knowing when to push a law up into the types (making it unrepresentable) versus leaving it as a checked property (making it falsifiable). For a system like yours that's half Pydantic types and half Datalog-style inference rules, that boundary is basically your whole design surface.