Test- and verification-technique guidance for coding agents: a 26-condition eval
An earlier experiment found that while agents can hit a quality bar with effective test techniques, default developer practice isn't working. This follow-up asks a narrower question: if an agent with no testing expertise is simply told to use a technique or a library — "Use test-driven development", "Use Lean 4", "Use property-based testing" — does implementation correctness improve?
The setup reuses the Zstd implementation eval from the earlier comparison of programming language effectiveness. Zstd is implemented under 26 prompt conditions, all in Rust, plus 4 "skill" conditions.
The conditions: ACL2, Alloy, "Audit and fuzz risky areas", "Audit first", Creusot, Default (no additional instructions), Differential testing, Fuzzing, Hegel, Insta, Judgement (agents pick the best technique), Kani, Lean 4, "Make no mistakes", Metamorphic testing, Mutation testing, Property-based testing, Proptest, QuickCheck, rstest, the built-in Rust test framework, SMT solvers (Z3, cvc5 and Yices all installed), Spin, TDD, TLA+, and Verus.
The skills were Hegel's official skill, the ECC Rust test skill (ECC reports 250k GitHub stars and 38k forks), the Trail of Bits property-test skill, and a small skill written for this experiment. Apart from the last, the skills were picked because they were the top hits Codex returned when asked to find relevant ones. Results here come from Codex with GPT-5.6 Sol at medium and xhigh effort, averaging 80 runs per condition and effort. Additional evals were run on the IMAP RFC (40 runs per condition) and on a few other RFCs (a few individual runs each), and results were not materially different.
Pre-registered expectations
Six guesses were registered in advance. TDD would underperform: 55% confidence, and TDD was added to the list precisely because underperformance was expected. Formal methods would not overperform: 52%, on the reasoning that formal methods and good test methods are both effective, so on simple problems formal methods shouldn't pull ahead if used at comparable competence — with low confidence because it's unknown what agents actually do when told to use a technique. "Make no mistakes" would not outperform no instructions: 95%, on the grounds that it's a joke many have tried. The ECC skill would not outperform: 65%, because the skill is large, directs agents toward TDD, and otherwise contains little that looks useful. Hegel's skill would not outperform: 65%, because the SKILL.md plus its linked Rust reference exceeds 20k tokens and reads as a tutorial rather than agent instructions. The Trail of Bits skill would not outperform: 55%, since it looks partly useful but is fairly large.
What the eval found
Nothing wildly outperformed, and Default did well above average. At xhigh, fuzzing- and PBT-related conditions averaged slightly ahead of formal methods; at medium the picture was more mixed. The skills Codex recommended underperformed, while the small custom skill did fine. TDD did poorly, as predicted. An RFC contains a subtle detail: on IMAP, only one run reached a perfect score — "Make no mistakes" at medium — and agents there ran the implementation first and the named technique afterwards in 75 of 80 runs, even for TLA+, which has a natural fit with protocol state and concurrency.
The ordering itself deserves little weight. Inspection of agent behavior shows the underlying pattern: agents largely don't know how to use these tools or techniques well in the first place, consistent with prior reporting and with Gary Bernhardt's characterization of agent testing:
AI agents' approach to testing, more or less:
Take the pathological cases dreamed up by someone objecting to mocks 15 years ago, without ever having actually used mocks. Naive dreams of excessive mocking.
Make those pathologies the backbone of your testing strategy.
The named technique mostly didn't change that approach. Agents either wrote the tests they'd normally write, wrapped in a framework for a different technique, or used the technique so superficially that none of its value materialized. Where a technique was named, they tended to do what Bernhardt describes, restricted to that technique: formal-method conditions proved irrelevant properties, while property-testing conditions leaned on fully random inputs that hit invalid or rejection paths, or found trivial properties and exercised them with low-value random cases.
At xhigh, agents could generally get their own tests to pass, but those tests were poor. One recurring failure: submitting four identical bitstreams to a test of a four-bitstream feature, which misses any transposition bug. Running at lower effort in a naive loop compounds this, as seen in the language eval — agents stall out with lower correctness.
Condition-by-condition observations
Formal methods, with and without code contact
Verus can prove that code matches specifications. Agents proved abstract properties about Zstd instead of verifying the actual code, and proved few and uninteresting ones — for example, that a valid cursor or index keeps an operation in bounds, which wasn't a source of bugs. Vacuous proofs of the form A => A were common; one actual proof was:
requires
0 < a <= window,
0 < b <= window,
0 < c <= window,
ensures
0 < c <= window,
0 < a <= window,
0 < b <= window,
Where agents proved something real, they avoided the bug-prone areas — for instance skipping reversal of bitstream order for encode and decode, and writing palindromic tests that couldn't detect the mistake. Aggregate xhigh Verus results were slightly below average correctness at much lower cost, while medium was average cost and the lowest percentage of correct runs. The correctness that did show up came almost entirely from ordinary #[test] unit tests, with more traditional testing at higher effort. On the four-stream jump table feature, Verus agents wrote a test in 89 of 160 cases — exactly the same count as Default — but were more likely to encode incorrect results or write easy-to-pass tests, such as making all four streams identical.
Alloy, a bounded model checker, scored second worst and did poorly at both effort levels. Agents again leaned on standard Rust #[test] and faffed about with Alloy. One Alloy counterexample led an agent to add a mitigation for an 8-bit overflow that couldn't occur given 64-bit usize with the actual input range, complicating the code without preventing a bug; in another case an incorrect Alloy specification failed a related test, and the agent fixed the specification afterward.
Lean 4, an interactive theorem prover, was not pre-registered but would have been expected to do well as a trendy tool likely covered by synthetic RL data. Lean agents proved arithmetic properties that missed the risk surface and relied heavily on standard Rust tests.
Creusot sits in the same space as Verus and was not used effectively. Spin, a model checker, scored moderately below average at below-average cost; its modeling of one class of behavior had no correlation to passing hidden tests covering that behavior. Kani, a Rust model-checking library, had the best coverage of formal methods actually applied to executing code, though only occasionally and mostly superficially; in one case real Kani use caught a non-trivial bug that changed the Rust code. Its cost was noticeably higher, apparently from repeatedly reading Kani output. ACL2 out-of-memory'd (192 GiB limit) in many cases, and those results were not counted, biasing the numbers opaquely; it mostly proved things that didn't affect correctness. SMT conditions had Z3, cvc5 and Yices installed, but agents used the solvers as a scratchpad for things like FSE state ranges and header arithmetic, and didn't model the right things. One computation should have been byte1 + (byte2 << 8) + 0x7F00; many agents wrote byte1 + (byte2 << 8) | 0x7F00, proved properties about the computation with an SMT solver, and still shipped the wrong code. TLA+ scored above average (more so at xhigh); 159 of 160 agents built some model, usually a state machine, and 30 modeled Huffman/FSE/entropy. Modeling came late, after standard tests and implementation; agents sometimes fixed errors in the TLA+ model, but no TLA+ issue was found to change Rust code, and more sophisticated modeling didn't correlate with better correctness.
Property-based testing and fuzzing
QuickCheck use was slight: mostly simple smoke tests over fully random inputs, which for something like Zstd just walk a few rejection paths. All agents used it, but 63 of 160 runs checked exactly one property. Agents wrote more traditional tests than under Default and did fewer test-fix iterations, landing below average cost.
Hegel, a property-testing library based on Hypothesis, was used superficially and late, generally after heavy ordinary testing, in a workflow of: read the RFC and API/contract, implement Zstd, run normal tests, read the Hegel docs, write 1–4 simple property tests, keep using built-in Rust tests. Hegel's official skill didn't improve correctness and made it slightly worse at a cost increase of 26% on medium and 41% on xhigh, for reasons that look causal. It produced more tests, mostly malformed-input checks — which agents over-produce in every property and fuzzing condition anyway — and round-trip tests in areas that weren't bug-prone. The skill is 34k characters and loads a 45k Rust-specific reference, over 20k tokens, read at the start and re-read on many subsequent actions: an average dollar-cost increase of 16% at medium and 18% at xhigh (900k and 1.8M raw tokens, with a 99.85% hit rate after the initial read) plus a multiplier from a structured workflow that generated more work without more correctness. The skill was used in 157 of 160 cases.
Proptest tests were mostly uninteresting with too-heavy reliance on randomness and poor coverage, but its shrinking — finding a simpler failing input — did sometimes provide value. The Property-based testing condition, with all options installed, saw every agent choose proptest, effectively becoming a second proptest arm; it too scored well above average, with shrinking generating wins.
The Trail of Bits skill was opened and read in 108 of 160 runs. It suggests proptest, but also that adding a dependency requires approval, which these single-turn autonomous runs couldn't obtain; property testing stayed rudimentary.
Fuzzing mostly sent random bytes, which repeatedly exercises invalid-input paths; random variations of valid inputs did the same. When agents generated random structured inputs — 10 of 160 cases — it found real bugs half the time, including non-trivial ones. That is one of the more effective technique uses observed, and it suggests agents could be trained, or directed, to do better here.
Metamorphic testing checked some genuinely reasonable properties — inserting a skippable frame at a frame boundary shouldn't change output, legal block repartitioning shouldn't change output — but they didn't touch the areas agents got wrong, so they didn't help. Curiously, it was used less at xhigh than at medium.
Framework, snapshot and technique conditions
Differential testing came in third worst: slightly above average at xhigh, far below at medium. No agent built two full implementations to compare. Of 160 runs, 135 did something you might call differential testing, but it was generally trivial; where it might have caught a bug, agents wrote the same implementation twice with the same bug in both instead of building independent versions.
TDD underperformed here and on the IMAP eval. The prompt changed behavior substantially: twice as many tests, a much more iterative test-code-test-code loop, though a TDD advocate would say agents still weren't doing TDD. Agents had one or more failing tests before substantial implementation in 67 of 160 cases, versus 0 of 160 under Default. Broad test classes were bigger across the board, both trivial and end-to-end, with no simple over- or under-production of a class. On the Zstd four-stream jump-table feature, TDD agents were more likely to fail the eval test despite writing more tests covering the general case, and more likely to write tests that miss hard cases. Two skills that induced a more iterative workflow also underperformed; across conditions, iterating to make their own tests pass more often led to more incorrect tests that enforce incorrect behavior. Yossi Kreinin's explanation:
fwiw, I think if you write the tests before the code, it's harder to test the harder cases since you know less about what is going to be hard, and even if you do random testing which I don't think "tdd" is associated with, you are less likely to steer the distribution in the direction where the bugs are. if you wrote the code or at least can look at it, you know what seems trivially correct and what might or might not work since it's not easy to understand what it does. in other words, tdd steers you towards black box testing which for complicated machinery seems to me to be less effective than white box testing; pretty sure this is how it works with people, less sure about agents
Rstest, a fixture-based library, was effectively not used: agents wrote standard unit tests inside it, skipping the thing that makes rstest rstest. Insta, snapshot testing, was barely used and likewise saw normal unit tests written in it. Mutation testing, which modifies code to gauge test effectiveness, mostly wasn't done; agents did ordinary testing with a little mutating that doesn't amount to mutation testing, a few cases excepted. Judgement, where agents adaptively chose methods, produced mostly standard Rust unit tests and a little limited fuzzing. Rust test — the built-in framework — doubled tests at medium and added 25% at xhigh when explicitly requested, without better correctness; failures came from untested behavior or tests encoding incorrect behavior, and more tests didn't cover risky behavior or reduce the share of runs with wrong test expectations. Yossi Kreinin on fixed I/O tests:
i think the fixed input/output style of testing encourages this in machines and humans alike. if you generate inputs you need to then have code that classifies output as correct or incorrect, and while this code itself might be buggy, it at least makes you think about what correct means and how to tell if something is correct more easily than running the code and assuming its output is the right answer. with fixed outputs you are quite likely to just encode the output of the code and convince yourself that it makes sense
Auditing, and the remaining conditions
Audit: 152 of 160 agents audited the code, 151 claimed to find an issue and made a change. Audits picked reasonable areas but usually reused the same context and repeated the original mistake; 42 spun off an independent agent and those runs scored worse, possibly because harder cases prompted the extra agent. Audit had the best xhigh correctness but below-average medium results, and increased cost substantially, especially at xhigh. Em Chu's comment:
The results here are consistent with my experience. Auditing code is where most of my tokens go at the moment because I find it quite useful. I always give the two instructions though:
- Don't spawn subagents; read and understand the code/diff yourself
- Don't execute any of the code
because I find the LLM to be significantly dumber if you let it do either of those (though of course I haven't measured...). It really doesn't read or reason about code by default, even if I'm never making a change big enough to exceed its context window.
I also usually include some BS like "be adversarial" "consider all possible combinations of features" "consider the entire input space" but I'm less sure that helps at all.
Audit and fuzz risky areas focused agents on FSE, Huffman, bit readers and state — good choices, better than plain Fuzzing — but agents mostly ignored the instruction at medium and followed it at xhigh. It didn't beat no instructions. One problem: agents generated random inputs that were generally invalid and tested nothing interesting. Human testers target randomization toward interesting inputs; agents didn't. Output checking was weak, often limited to looking for crashes.
Make no mistakes scored technically above Default with indistinguishable behavior and near-identical scores, best explained as random variation. Default, with no test or verification instructions, scored above average — consistent with everything else, since telling agents to do useless work is worse than not telling them. ECC's Rust test skill did okay mainly because much of it was ignored. Agents read it in 153 of 160 runs, and earlier reading correlated with more added tests and worse correctness. Its score came from 7 runs that didn't read it at all (100% correct) and 9 runs that read it late (100% correct), almost all at medium — which is also why medium matched xhigh. Where the skill actually influenced behavior it scored below average, between the built-in Rust framework and Creusot, with large numbers of small, unimplemented-value tests; the skill asks for red-green TDD, and agents write a small test before functionality. There's quite a bit of variance here.
Two of the remaining conditions: TLA+ was already covered above; ACL2 and Kani likewise.
The one skill that scored highest
The custom skill was written after Max Bittker suggested encoding testing knowledge from the author's head. Its contents:
- Think about areas likely to have subtle bugs before implementing; for each, state likely mistakes and plausible alternative interpretations, then come up with a check where the results differ (prefer asymmetric / boundary examples on both sides of the boundary)
- After implementing, for high risk areas, independently re-derive the result without context on production code and compare (fresh context, do not re-use helper functions)
- When feasible, use property-based testing or randomized inputs to try to explore the space, minimizing effort on no-panic or no-crash randomization
- When randomizing, lean towards inputs that will explore interesting state and code paths (don't just naively randomize inputs that all fall into the same error paths); this may require structured random inputs
- If you're unsure about details, use independent reasoning to check what's correct (fresh context, do not re-use helper functions)
It got the highest score but didn't work as intended. The fresh-context re-derivation essentially never happened, so its effect is unknown. Agents did identify risky areas — bitstream reversal for encode versus decode came up — but didn't test them better; in one medium run the agent identified the risk, did independent derivations and an audit, and still failed, because its test input was palindromic and reversal produced the same result. All fuzzing and property testing in this condition was done by hand, so the skill could trivially be improved by pointing agents at proptest. The instructions did directionally reduce the standard "too random" failure mode, but tests remained worse than a human's, or than an agent's with active human guidance. As a first draft it isn't horrible, but it isn't ready to use, and without iterating against many more examples — to avoid overfitting to RFC-like and bit-manipulation-intensive problems — it doesn't capture what a human driving an agent would do.
Takeaways, prediction accuracy, and skills
Risky areas were identified well by agents; the defects were idiosyncratic otherwise, much like the language failures where Clojure agents mishandled byte conversion more than Java agents did despite unchecked-byte being available. There's no clear pattern beyond the headline: agents mostly don't apply test or verification techniques effectively when all they're given is a name.
Every registered prediction held. TDD underperformed; formal methods didn't overperform, though because agents failed to use them at all rather than for the expected reason; "Make no mistakes" didn't beat no instructions, and beat most conditions because a no-op is better than ineffective work; and the ECC, Hegel and Trail of Bits skills didn't outperform. Two implicit guesses were wrong: Lean was expected to do relatively well among formal methods, and the custom skill was expected to be mediocre to bad. Max Bittker guessed the custom skill result in advance and named a consistent reason.
The registered guesses used to be reached by prompting and inspecting a few runs. On this eval's evidence, that intuition transfers to skills reasonably well.
Two experiments on other "official" vendor skills (one from a big AI lab, one from a "small" few-billion-dollar company; details not discussed here) also made results worse. Yet skills for personal use look more promising than before, because the failure modes appear predictable and therefore fixable. A publicly released skill that works well across models and harnesses is probably harder, since Claude and Codex seem to want different prompting styles.
The inspection of the skills here suggests a writing problem: they read like human tutorials that explain how to do something, when the model already has relevant knowledge and a default behavior distribution. What's needed is statements that modify that distribution. Long text doesn't change the fact that defaults differ across harnesses, models and effort levels; much of it gets ignored, in a harness-, model- and effort-dependent way. ECC's TDD instructions were influential but still not followed as written despite being clearly laid out. Prompting that works changed enough between GPT-5.5 and GPT-5.6 to shift how the author works, which argues against one generic testing skill spanning many models and efforts. Generic testing skills also face the problem that there's no workflow independent of the thing being tested and the quality dimensions wanted. Skills do seem a good fit for teaching agents to execute workflows or drive APIs and interfaces — for example Sawyer Hood's skill for driving a web browser, which has a very different style than the testing skills tested here. (That skill hasn't been tried, so it's not an endorsement.)
On getting agents to write good tests: guiding an agent to set up a reasonable test and triage structure, then having it extend that, works okay-ish with light supervision. Jamie Brandon reports the same for snapshot testing — on one project, agents of various models claimed to write snapshot tests and instead wrote unit tests; on another, he got reasonable end-to-end tests with mocked IO only after moving tests into a separate crate and instructing agents via AGENTS.md to keep tests in that crate and not modify the public interface. As before, doing anything remotely reasonable seems to work: light instructions in a CLI produce poor work, but a few more sentences after looking at what the agent did often gets to a good place quickly.
On the state of skills
The author doesn't generally use skills, instead keeping a large scratchpad of prompts to paste in. Thorsten Ball's talk noting he doesn't rely heavily on skills, plus conversations with other effective LLM users who don't either, prompted the question of whether skills matter much. It turned out the intuition from watching agent responses and running small experiments tracked how skills actually behaved; other skills that looked like they'd fail the same way were found too.
One notable response: David R. MacIver said the Hegel skill "sortof sucks right now," and that a common problem is that agents are bad at writing agent skills while everyone uses an agent to write them. A mutual friend mentioned MacIver set up a benchmark confirming the Hegel skill's deficiency and is presumably improving the skill or the Hegel comments and docs so the skill isn't needed. As discussed before, measuring and benchmarking are underrated because publishing a measurement often reveals a problem nobody knew about.
Prediction accuracy, method and closing notes
Prediction outcomes: TDD underperforms — true; formal methods don't overperform — true, but not for the expected reason, since agents failed to use them remotely effectively; "Make no mistakes" doesn't outperform no instructions — true; the ECC, Hegel and Trail of Bits skills don't outperform — all true, with the note that confidence would have been higher if skills were used more, since most of the ECC skill text looks inert and the rest looks counterproductive. Implicit: Lean doing relatively well among formal methods — false.
Prediction outcomes on the walkthrough order: agents often fail in idiosyncratic ways, as with the Clojure byte-conversion case, and there's no clear pattern beyond the headline that naming a library or technique accomplishes little. If the eval's structure looks like an odd result worth splitting into cleaner charts, the reason it isn't is that agents using these tools badly produces no interesting comparison.
Naive thoughts on writing agent skills
The author can't say what a good skill is. But across the skills tested here and in two other experiments, they read like human tutorial instructions — aimed at explaining how to perform the technique. Given a model that already has some knowledge, that's likely wrong: the model already has a default behavior distribution, so the more natural approach is statements that modify that behavior, not instructions that let a human acquire it.
Diffculty of a general skill: what prompting works shifts with model and effort, and different harnesses, models and effort levels have different defaults, which doesn't change when text is added — it only lengthens the push away from the default, and some of the text does unintentional pushing.
There's likely little value in a generic testing skill independent of what's being tested, the quality bar, and which quality dimensions matter. Task-specific work wants task-specific instructions, not generic ones. A skill that asks questions and emits the right instructions could be imagined, but with models improving quickly it doesn't seem worth tweaking for personal use, though it might differ for an agentic product. Skills do look generically useful for executing workflows or interacting with APIs and interfaces, as with the browser skill, which has a different style than the testing skills here.
Footer notes from the original write-up
On the IMAP eval: the earlier planning figures show why it was cheaper to run than the pandoc eval, where some less effective languages exceeded $1k per run and Rust still cost $700 per run to reach only 30% passing tests.
On RL environments for testing, a botched fact-check claims this isn't being worked on; the papers it cites trained agents to write poor tests, effectively unit tests like most programmers write — the opposite of what converges in communities that care about correctness. Some work touches randomized testing (for example, 2509.20384), but given how ineffective models are at PBT, fuzzing and randomized testing absent specific guidance, this doesn't appear to have entered training in a serious way.
On language supremacy claims: they may become true later, but the failures so far look idiosyncratic. If forced to guess, it resembles poker, where confident concepts were invalidated once simulation was powerful enough to outplay humans; if the question is what coding agents are good and bad at, experiments beat cocktail-party concepts, and the experiments to date don't support the abstract reasons people give for language fit. Rust memory safety is the exception, validated by comparing memory safety issues in agent-written C, C++ and Rust in the multi-language pandoc eval.
Where to point agents
The condition set didn't make testing worse consistently; it also didn't make it better. Getting decent tests out of agents looks like an ongoing supervision cost rather than a one-line instruction, at least for the agents available from inception until now (September 2026).
For readers testing that, the practical items the eval supports: randomized and property-based testing with structure, rather than unstructured random input; independent re-derivation with fresh context when it actually happens; and auditing that reads code without spawning subagents or executing it.
The three formal-tool behaviors that showed up most often: proving properties disconnected from the code, modeling the Zstd domain in an abstract space, and treating the Solver as a scratchpad to reason about arithmetic — all consistent with the same failure mode seen under every framework and technique observed here.
Runaway processes
At least one actionable oddity worth reporting: after asking an agent to look something up, it exec'd a perl process that ran for 2 hours and 20 minutes before being killed. A subagent had used perl for a regex search over a 44 kB, 1364-line file; the expression was degenerate under PCRE and did a combinatorially large amount of work. Re-running with the FRE regex engine from an earlier build finished in 0.7s (Rust regex: 0.6s). Three ways this could have been prevented: don't invoke a regex engine that can blow up combinatorially when a safer engine like ripgrep at default settings works; emit the intended pattern instead, since the emitted one returned a uselessly large capture and didn't do the intended thing when it succeeded; and have the subagent or harness kill leftover processes when the subagent finishes, since the subagent stopped after 30s but left the process running indefinitely with no value to a finished subagent. There's already a cleanup process for leaked memory and temporary build artifacts; it wasn't looking for runaway perl. Others have surely hit this, though the author doesn't expect to open source a tool for it, since the major harnesses will probably fix it soon.
Additional notes from the original write-up
The IMAP results are less interesting than expected, since one might think TLA+ fits IMAP state and concurrency naturally. Instead, agents did most implementation in Rust, then pulled out the named tool: 5 of 80 agents used TLA+ before coding, 75 of 80 the other way around. Agents consistently modeled small mailbox mutation and never multple observors, event queues, UIDVALIDITY and mailbox epohcs, where implementation mistakes were common; they modeled CONDSTORE and QRESYNC instead, where Default had a test pass rate above 99.6%, and the TLA+ agents scored lower on those despite modeling them. All evals here use RFCs, which are unrealistically clear and unambiguous compared to the specs programmers give agents; the failure modes here should be the same or worse on most real-world problems.
See the note on RL environments above.
Language supremacy reasoning may become true later, but experiments would show it if so; today's experiments don't.
