Telling Your Coding Agent to Use Property-Based Testing Probably Makes It Worse

Dan Luu ran 26 verification instructions against a control arm that said nothing at all. The control beat most of them.

Twenty-six different ways of telling a coding agent to verify its work. Lean 4. TLA+. Kani. Verus. QuickCheck. Proptest. Mutation testing. Differential testing. "Audit first." "Make no mistakes." And, sitting there in the list like a placeholder nobody expected to matter, a Default arm that gave the agent no verification instruction whatsoever.

Default finished above average. Most of the named techniques finished below it.

That result went up on danluu.com on September 7 and spent September 8 near the top of Hacker News, and I think it is the most useful thing published about coding agents this month, because almost everyone reading this has an instruction like "use property-based testing" or "write tests first" sitting in a system prompt right now, put there on the reasonable theory that telling a capable model to do a good thing produces a good thing. Luu measured that theory. It does not hold.

What the eval actually did

The setup matters, because the finding is only interesting if the task was real. Luu reused a Zstd compression implementation task in Rust, ran it through Codex with GPT-5.6 Sol at two reasoning effort levels (medium and xhigh), and scored on the fraction of runs that passed 100% of a hidden test suite the agents never saw. Eighty runs per condition per effort level. Twenty-six conditions.

The conditions spanned three families. Formal methods: Lean 4, TLA+, Kani, Creusot, Verus, ACL2, Alloy, Spin, and SMT solvers with Z3, cvc5 and Yices all made available. Test libraries: QuickCheck, Proptest, Insta, rstest, the Rust built-in framework. And plain-language nudges: "Use test-driven development," "Audit first," "Audit and fuzz risky areas," "Make no mistakes," plus a "Judgement" arm that told the agent to pick whatever technique it thought best.

He also tested four skills, three of which Codex itself recommended when asked to find relevant testing skills, plus one small one Luu wrote himself.

His one-line summary of the whole thing: regardless of the type of problem, agents did not use formal methods or test libraries or techniques in an effective way.

The mechanism is the part worth understanding

An instruction that names a technique gets obeyed. That is the trap. The agent does reach for Verus, or Spin, or Alloy. It just points the tool at whatever is easiest to formalize rather than at whatever is most likely to break.

Luu's Verus section is the clearest example. Verus exists to prove that Rust code matches a specification, and it is built to make proving things about actual executing code straightforward. The agents used it for abstract reasoning instead, mostly checking arithmetic properties, and never attempted to verify any of the Zstd code itself. He calls this odd, and it is, until you notice the incentive: proving something about arithmetic terminates. Proving something about a decompression loop does not, and an agent optimizing for a green result will take the exit that closes.

Spin produced the same shape of failure in a sharper form. Agents used Spin to model a particular class of behavior, and Luu reports that this modeling had no correlation with passing or failing the hidden tests covering that exact behavior. The agent verified a model of the thing. The thing stayed broken.

Alloy scored second-worst overall, and there the agents did model something closer to the Zstd algorithm than the Verus agents managed. It was still the wrong modeling.

Then there is the xhigh observation, which reframes the whole picture: at the higher reasoning effort, agents were generally able to get the tests they wrote to pass. They just wrote poor tests. More thinking bought more successful self-agreement.

Kani was the one exception Luu names. Kani got the best coverage in the sense that it actually ran against the Zstd code rather than a model of it.

So what separates an instruction that works from one that does nothing

Luu buries the answer in his skills section, and it is the sentence I would tape to the wall.

The testing skills that Codex recommended underperformed. The small custom skill he wrote himself did fine. His stated explanation for the difference: his skill was designed to nudge agents away from their default behavior toward more productive behaviors, while the recommended skills read more like tutorials.

That is the whole distinction, and it explains the Default result rather than merely reporting it. A tutorial-shaped instruction tells the agent what a technique is. The agent already knows what property-based testing is; that knowledge is in the weights. Loading a description of it into context adds tokens and changes nothing about what the agent chooses to do when it hits a decision point. One of the skills Luu tested was 34,000 characters and loaded a 45,000-character Rust reference on top, coming to more than 20,000 tokens of context. It made agents generate more tests. It did not make them generate better ones.

A behavior-delta instruction is different. It names a thing the agent does by default and tells it to do something else. "Do not stop when your own tests pass; find an input class you have not covered and test that" is a delta. "Use property-based testing" is a description. Two of the skills Luu tested pushed agents into a more iterative execute-often loop, and both underperformed, which is what a delta looks like when the delta itself is wrong. That is still more informative than a tutorial, because a wrong delta is falsifiable and a description is not.

Put this into practice

The lowest-friction version of this takes an afternoon and does not require adopting any technique at all.

Add a Default arm to whatever eval justifies your prompt. Before you keep "use property-based testing" in a system prompt, run the same task with that line deleted, same model, same effort setting, same everything. If you have never done this, you do not currently know whether any of your prompt additions do anything. This is the single highest-value change in this article and it costs one extra eval run.

Score against tests the agent never sees. Luu's metric is the fraction of runs passing a hidden suite, and that choice is what makes the xhigh finding legible. If you score on tests the agent wrote, you are measuring self-consistency, and a more capable model will always look better at self-consistency while getting no better at correctness.

Put cost on the same axis as correctness. Several conditions in Luu's data bought small correctness gains at large cost increases, and one condition came in cheap specifically because agents did fewer test-fix iterations under it. A skill that adds 20,000 tokens to every run has to earn that back. Claude Code's /skill-doctor will tell you what your loaded skills cost in context; it will not tell you whether they change behavior, which is what the control arm is for.

Rewrite your instructions as deltas. Go through your prompt and mark every line that describes something. Then ask, for each one, what the agent would do without it, and whether the line actually moves it off that. Lines that fail this test are candidates for deletion, and deletion is free.

Read one transcript per condition before you trust an aggregate. Luu found the Verus and Spin failures by looking at what agents actually did with the tools, not by staring at the scores. The scores told him a condition underperformed. The transcripts told him why, and the why is what transfers to your codebase.

What this does not prove

Being clear about the limits is what makes the rest of it worth acting on.

This is one implementation task, in one language, through one harness, on one model family. Zstd is bit-manipulation-heavy, which plausibly favors some techniques over others; Luu mentions running an IMAP RFC eval too, with results he treats as consistent, but the headline data is Zstd in Rust via Codex with GPT-5.6 Sol.

Luu himself cautions against drawing strong conclusions from the ordering of conditions, and the caution is real. Where one condition topped correctness at the higher effort tier, he immediately hedges that it did about as well as Default on average and that there is not enough evidence to say it is really better. He notes the fuzzing and property-based-testing conditions did a little better than formal methods on average at xhigh, with the picture more mixed at medium. Do not read a ranking out of this. Read a warning.

On the skills specifically, he flags his own predictions as low confidence and says plainly that he does not use skills and has no feel for how to evaluate one. His skill result is one data point from someone who wrote one skill.

And none of this says formal methods do not work. Luu's own view, stated elsewhere in the piece, is that he has sat people down and shown them how to test properly and converted them for life. The finding is about what an agent does when handed the name of a technique with no idea when it applies. That is a statement about instruction design, not about Lean.

The part you can act on today

The comfortable reading of this eval is that agents are bad at formal methods, which lets everyone go back to what they were doing. The uncomfortable reading is that a large share of what we all put in system prompts and skill files has never been measured against saying nothing, and the one time somebody measured it carefully, saying nothing won more often than not.

You do not have to take Luu's ordering, his task, or his harness. You do have to take the control arm. Delete one instruction from your prompt this week, run the eval both ways, and look at the number. If the instruction is doing work, you will see it. If it is not, you just got some context back and learned something about the other forty lines sitting next to it.

Sources: Dan Luu, "How well do agents use test/verification techniques?" · Dan Luu, agentic programming language comparison · Dan Luu on AI coding and software quality

Medium metadata

Title: Telling Your Coding Agent to Use Property-Based Testing Probably Makes It Worse
Subtitle: Dan Luu ran 26 verification instructions against a control arm that said nothing at all. The control beat most of them.
Tags: AI Agents, Software Testing, Coding Assistants, Prompt Engineering, Software Quality
Suggested kicker: Twenty-six ways to tell an agent to verify its work. The one that said nothing beat most of them.