A Joke Prompt Beat TDD, Lean, and Verus Across 4,800 Agent Runs

TL;DR

Dan Luu ran roughly 4,800 agentic coding runs building a Zstd implementation in Rust and varied exactly one thing: the sentence telling the agent which testing or verification technique to use. Thirty conditions, about 160 runs each, on GPT-5.6 Sol via Codex at medium and xhigh effort. Correctness was scored as the fraction of runs passing 100% of a hidden test suite.

The condition with no testing instructions at all scored well above average. A control condition whose entire addendum was "Make no mistakes" scored slightly higher still. Every named technique got used, and almost none of them changed a single line of code.

Agents did the ritual. Every time.

The first thing to kill is the theory that agents ignore the instruction. They do not. Compliance was close to total.

Now the other half of the same data.

159 of 160 runs in the TLA+ condition produced a state-machine model of Zstd. Luu reports finding no instance where a TLA+ issue caused an actual change to the Rust. In the differential testing condition, 135 of 160 runs did something you could call differential testing, and zero built two independent implementations to compare, which is the entire point of the technique. When agents did try, they wrote the same thing twice and encoded the same bug in both.

Kani caught one real bug in 160 runs. Fuzzing generated structured random inputs in only 10 of 160 runs, but when it did, it found real bugs about half the time. That 5-in-160 is the single most encouraging number in the whole study, which tells you something about the rest of it.

The proofs were real. They just proved nothing.

The formal methods conditions (Verus, Lean 4, Alloy, Creusot, ACL2, Spin, SMT solvers) uniformly failed to outperform. Not because the tools are bad, but because agents pointed them at the wrong things. Verus can prove that your code matches a specification; agents mostly used it to prove abstract arithmetic facts, and sometimes wrote proofs of the shape A implies A. An actual example from the runs:

requires
    0 < a <= window,
    0 < b <= window,
    0 < c <= window,
ensures
    0 < c <= window,
    0 < a <= window,
    0 < b <= window,

Think of it as hiring a building inspector who files a spotless report certifying that every doorknob turns, while the foundation is cracked. The certificate is genuine. It is also worthless, because nobody aimed it at the load-bearing part.

The SMT condition has the cleanest illustration. Zstd needs a computation that should be byte1 + (byte2 << 8) + 0x7F00. Agents frequently wrote byte1 + (byte2 << 8) | 0x7F00 instead. They used the solver to prove properties related to that computation, and then still shipped the wrong operator.

TDD did not just fail. It changed behavior for the worse.

Luu pre-registered a 55% guess that test-driven development would underperform. It did, on the Zstd eval and again on a separate IMAP RFC eval. The prompt visibly worked: agents produced roughly twice as many tests and adopted an iterative test-code-test loop. Agents had one or more failing tests before substantial implementation in 67 of 160 runs, against 0 of 160 in the default condition.

More tests, worse correctness. Zstd uses a jump table when there are four Huffman streams, and TDD agents were more likely to fail the hidden test for it while writing more tests overall. The reason is depressingly human: they made all four streams identical, so a bug that transposes streams passes cleanly. Yossi Kreinin's explanation, quoted in the post, is that writing tests first pushes you toward black-box testing, and for intricate machinery you do not yet know where the hard cases are.

Explicitly asking for the built-in Rust test framework produced double the tests on medium and 25% more on xhigh, and no correctness gain either. Volume of tests is not the variable.

The published skills were worse than nothing, and they billed you for it

This is the part that should worry anyone maintaining a shared skills directory. Four testing skills were tested: the official Hegel skill, the Rust testing skill from ECC (a skills collection with over 250,000 GitHub stars), the Trail of Bits property testing skill, and a five-bullet skill Luu wrote in about two minutes.

The three published skills underperformed. Luu's throwaway got the highest correctness score in the study.

The Hegel skill is the cautionary tale. It is 34k characters plus a 45k-character Rust reference, over 20k tokens, loaded at the start and re-read repeatedly. Correctness came out slightly worse. Cost came out 26% higher on medium and 41% higher on xhigh. Even at a 99.85% cache hit rate after the first read, raw token usage rose by an average of 900k on medium and 1.8M on xhigh.

The ECC skill has an exposure gradient that is hard to read as anything but damning: the earlier an agent read it, the worse the run went. Its headline score looked fine only because 7 agents never opened it and scored 100%, and 9 more opened it late and also scored 100%. The Trail of Bits skill was opened in just 108 of 160 runs, and its recommendation to use proptest was dead on arrival because it asks for approval before adding a dependency, and these were single-turn autonomous runs.

That workflow is the mechanism behind every result above. The agent implements, tests the way it always tests, then goes and reads the docs for whatever you asked for, then adds one to four decorative checks. The technique never touches the design of the implementation, which is where its value would have come from.

What actually moved the needle

Not much, and none of it is a one-liner you can paste into AGENTS.md.

• Property-based testing scored above average. proptest and the generic property-based testing condition both did well. Luu credits shrinking, the machinery that reduces a failing input to a minimal one, as providing real value even when the properties themselves were weak.
• Agents can identify risk correctly. In the audit and fuzz conditions, they consistently picked the right danger zones: FSE, Huffman, bit readers, state. Knowing where the bugs are and writing a test that catches them turn out to be different skills.
• Auditing is real but expensive. 152 of 160 agents audited when told to, and 151 claimed a finding, but they usually audited in the same context that produced the bug and repeated the mistake. Spinning off an independent auditor happened in 42 runs and scored worse, though Luu notes that may be selection rather than causation.
• Luu's own five-bullet skill won, and he is the first to say it did not work as designed. Its instruction to re-derive results in a fresh context was almost never followed. He calls it a first draft not ready to use.

His practical answer is not a prompt at all: set up a reasonable test and triage structure yourself, then let agents extend it. Jamie Brandon, quoted in the post, got usable end-to-end tests only after moving them into a separate crate and writing rules into AGENTS.md about not touching the public interface. Structure beats instruction.

Caveats worth holding

One task family (Zstd, plus an IMAP RFC eval at 40 runs per condition), one model, one harness. Luu explicitly warns against reading the ordering of conditions as meaningful, and demonstrates why with ECC: even 160 runs was not enough to separate a bad skill from a neutral one without reading the transcripts by hand. ACL2 runs that hit the 192 GiB memory limit were dropped, which biases that arm in an unknown direction. And the whole thing is a snapshot of publicly available agents in September 2026, on a curve that moves fast.

What survives all of that is the qualitative finding, and it is the one that matters: naming a technique in a prompt does not transfer the technique. It transfers the vocabulary.

Key Takeaways

• Compliance is not competence. Agents used the named tool in 108 to 159 of 160 runs depending on condition, and the tool changed the outcome in 0 to 5.
• No instruction beat almost every instruction. The default condition scored well above average, and "Make no mistakes" scored fractionally higher, which Luu reads as noise around the same result: a no-op beats pushing agents into useless work.
• Telling an agent to do TDD makes it write more, worse tests. Twice the volume, failing tests up front in 67 of 160 runs versus 0 in default, and lower correctness.
• Audit your skills directory for cost, not just quality. A 20k-token testing skill raised cost 26% on medium and 41% on xhigh while making correctness slightly worse. Skills written as human tutorials do not modify agent behavior, they just occupy context.
• Property-based testing and structured fuzzing are the only techniques with a pulse here, and only because shrinking and structured inputs do work the agent otherwise skips.
• Small-N skill evaluations are worthless. 160 runs was not enough to correctly rank a skill that turned out to be actively harmful. If you tried a skill five times and liked it, you learned nothing.

Sources: Dan Luu, How well do agents use test/verification techniques?, Dan Luu, the original Zstd language eval, ECC skills collection, Hegel SKILL.md, Trail of Bits property-based testing skill, OpenAI GPT-5.6 Sol model card