We previously noted that, while it's easier than ever to hit a particular quality bar by having coding agents use effective test techniques, software quality seems to be getting worse：/ai-coding/, indicating that whatever defaults developers are using may not work very well. Here, we test if simple instructions to agents to use particular techniques or libraries improve implementation correctness, as a kind of test to see how effective agents are when guided by someone with no expertise in testing who's maybe heard that you should apply certain techniques or use certain libraries.

We'll re-use the Zstd implementation eval discussed in this comparison of agentic programming language effectiveness：/pl-tokens/ and, instead, compare different testing techniques and testing libraries when agents are given a prompt to implement Zstd with different addendums, such as "Use test-driven development", "Use Lean 4", "Use QuickCheck", "Use property-based testing", etc. I also ran some other evals, such as on the IMAP RFC, which are briefly discussed.

I pre-registered some guesses on how conditions will do:

Below, we have a very messy graph which shows the results for the conditions tested (codex with GPT-5.6 Sol, with medium and xhigh efforts). When looking at data, I tend to prefer much denser and messier graphs than most people, such as the first graph here：/android-updates/. Because most people find these kinds of graphs unreadably messy, I tend to split information out into a series of graphs, each of which shows less information, when presenting information to others. For reasons discussed elow, I'm not going to do this here and am just going to present this extremely messy graph where we have cost on the x axis and the fraction of runs that passed 100% of the (hidden) tests on the y axis, average of 80 runs from each condition and effort (mousing over items shows bootstrap covariance, 50% uncertainty：https://statmodeling.stat.columbia.edu/2016/11/05/why-i-prefer-50-to-95-intervals/, and there's some attempt at making like things similar colors, e.g., blue-ish for formal methods, green-ish for property-based testing, etc.):

One thing we can see is that nothing really wildly outperforms. However, Default (no additional instructions) does well above average. Looking at xhigh, on average, the fuzzing and PBT-related conditions did a little better than formal methods on average, with the situation being a lot more mixed at medium. The testing-related skills codex recommended we try underperformed, although our quick custom skill did ok (a major difference is that our skill is designed to nudge away from their default behavior towards more productive behaviors whereas the other skills seem more like tutorials). TDD didn't do well, as predicted (one skill also suggested that agents used TDD, and that skill also fared poorly in the cases where agents attempted to follow the instruction).

If we actually look at what agents did, it quickly becomes apparent that, in general, agents don't know how to use these tools or techniques very well. As we noted here：/ai-coding/, and as everybody I've talked to has also noted, agents are really bad at testing and don't seem to understand how to test reasonably "by default". For example, here's a comment by Gary Bernhardt：https://x.com/garybernhardt/status/2067002665427775613:

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.

On xhigh, agents were generally able to get the tests they wrote to pass, but they wrote poor tests (e.g., they'd submit four identical bitstreams into a test of a feature that uses four bitstreams and miss any bug that would occur because they transposed bitstreams). And as we noted previously on the Zstd eval with respect to languages：/pl-tokens/#appendix-medium-in-a-loop-vs-ultra, running at a lower effort level in a naive loop gets worse results (agents do even more of this and stall out with lower correctness).

Below we'll look at how agents did things for each condition, ordered from worst correctness to best, but I would caution anyone against drawing any kind of strong conclusions from the ordering.

A lot of the failures here seem analogous to the failures we saw when we looked at the impact of programming language on token usage and correctness：/pl-tokens/, in that the failures are often idiosyncratic. For example, with programming languages, we saw that agents had a fairly high rate of getting the semantics of byte conversion incorrect in Clojure but not Java, even though agents "should" (and probably sort of do) know that they can get Java byte conversion semantics by converting with unchecked-byte instead of byte .

Verus：https://github.com/verus-lang/verus uses an SMT solver and various types of reasoning to prove that the code matches specifications.

Although Verus can prove that code matches specifications, agents didn't do that. Instead, they made proofs about various abstract properties relating to Zstd. I've not used a tool like Verus myself, so I can't speak to what an expert or even a beginner user would normally do, but from reading the tutorial, I find it a bit odd that agents didn't attempt to use Verus to verify any of the actual code and only used it to do abstract reasoning, as it seems designed to make it easy to prove properties about the actual code.

Additionally, if we look at the properties proved, there were generally few properties proved and the properties that were proved were uninteresting. For example, agents would prove things like "given a valid cursor/index/distance, the resulting operation remains in bounds", which isn't bad to prove, but wasn't really a source of bugs. Also, agents would frequently write vacuous proofs that were effectively A => A . An actual Verus proof of this form was:

In cases where agents actually proved something, they generally proved something relatively simple and avoided proving properties about the parts that were likely to have a bug (for example, agents often failed to reverse the bitstream order for encode and decode and would write tests that failed to detect this because the tests were palindromic; perhaps some kind of proof of reversal here might get agents to "think" about this in a different way).

It doesn't seem that agents were getting value out of Verus when just provided with Verus and the Verus docs.

If we look at the result, the aggregate xhigh Verus results are fine (slightly lower correctness than average, but much cheaper). The medium results had average cost and the lowest percentage of correct runs as well as the lowest average number of correct tests. Because agents didn't really get value out of Verus, what they actually did for correctness was mostly just traditional tests (built-in Rust #[test] functions with unit tests). When going from medium to xhigh, agents spend much more effort on traditional testing and only a bit more effort on using Verus, which allowed the xhigh result to be ok.

Looking at the actual tests, for one of the two features which agents using Verus did much worse on (the four stream jump table：https://github.com/facebook/zstd/blob/dev/doc/zstd_compression_format.md), Verus agents wrote a test for this in 89 out of 160 cases, coincidentally the exact same number as Default agents, but Verus agents were much more likely to write bad tests. They were more likely to encode incorrect results in the tests as well as make easy to pass tests that don't cover the space well, such as making all four streams identical. This kind of thing is what I meant when I said that the failures were idiosyncratic. There's nothing about Verus that necessarily makes one write poor tests when not using Verus and we wouldn't, in general, expect a human who's used Verus to write bad unit tests, in the same way that we wouldn't expect a human using Clojure to make more byte conversion mistakes, but this happened here for whatever reason (possibly a coincidence).

I don't know if folks inside AI labs can get access to better information on why things happened, but here on the outside it's generally quite difficult to tell why something like this happened (even when we formed a plausible hypothesis for the language issue, it required running many samples of many languages, and papers we looked at which studied the same thing didn't observe the language popularity / agentic effectiveness correlation because they either looked at too few languages to be able to reason about such a weak correlation or they looked at problems that were too small and too trivial).

Alloy is often called a bounded model checker. This is maybe not quite right with Alloy 6 since that introduces some extra features, but this is way outside of my area of expertise. My understanding is that, with Alloy, you normally prove properties about your model (as opposed to proving that your code works).

Alloy got the 2nd worst correctness score and, unusually, scored generally poorly on both medium and xhigh. Although it isn't shown (because it doesn't seem to add anything), in general, results were highly correlated between max and xhigh, which were quite different from medium results.

As we saw with Verus, agents using Alloy pretty much relied on standard Rust #[test] for correctness and mostly faffed about with Alloy. Once again, using a formal tool poorly did not help with correctness.

There were individual cases of Alloy use that were close to finding an issue or risk, but even then, only a small number. In one case, Alloy found a counterexample which then caused the agent to implement the Rust version with a mitigation for the potential bug. Unfortunately, the counterexample relied on an 8-bit overflow that couldn't happen in practice because the actual implementation used 64-bit usize with no possibility of overflow given the inputs, so it just made the code more complex without preventing an actual bug.

In another case, the Alloy specification was incorrect and a related test failed. After the test failed, the agent fixed the Alloy specification. Had the specification been correct, perhaps the agent would've written the correct code without the failure. There were some cases where it's possible the good version of this happened, but it's not clear if an actual potential bug was prevented.

Alloy agents did model things that were more closely related to the Zstd algorithm than Verus agents (which mostly checked things like arithmetic), but it was still the wrong modeling.

Differential testing is a technique where you give the same inputs to multiple implementations and then compare results to find issues. In principle, this seems like a reasonable thing to try with LLMs as we often get different results from different rolls of the dice, and as we noted here：/pl-tokens/#appendix-medium-in-a-loop-vs-ultra, having an agent iterate more on an implementation (which might be only part of the entire thing, perhaps even only part of a function) often works worse than having the agent restart from scratch.

But this gave us the third worst results. In this case, we had slightly above average results on xhigh and far below average results on medium. None of the agents created two full implementations to compare. Out of 160 runs, 135 did something you might call differential testing, but like the other conditions we've seen, these were generally trivial and effectively useless. And, in the cases where differential testing might've caught a bug, instead of implementing things in independent ways, agents just did the same thing twice and encoded the same bug in both versions.

I sometimes tell agents to do things independently and get them to launch with separate contexts, but this was not done effectively for differential and agents would generally just write the same thing twice.

It makes sense to discuss how the official Hegel skill changes Hegel behavior, but in reverse correctness order, Hegel Skill appears above Hegel because the result was worse on correctness. See the Hegel section below for discussion of this skill.

Lean 4 can maybe be described as an interactive theorem prover：https://en.wikipedia.org/wiki/Proof_assistant.

Although I didn't pre-register a guess about Lean, if I had pre-registered guesses on which formal tools would do well, I would've put Lean on the list of things I'd expect to do well because it's relatively hot/trendy and therefore seems relatively likely to have good performance due to synthetic data from RL envs.

The Lean agents did prove properties, like the Verus condition, agents mostly did arithmetic proofs that didn't hit the bug-prone or risk surface areas.

Like the other formal conditions, Lean agents relied heavily on standard Rust tests. As with the formal conditions so far, doing a few proofs of things that don't matter didn't help with correctness.

QuickCheck is a property-based testing library：https://en.wikipedia.org/wiki/Property_testing, probably the best known such library for a long time, although Hypothesis might currently hold that crown.

Unfortunately, agents were about as effective at using property-based testing as they were at using the formal tools we've seen so far. When using QuickCheck, agents mostly wrote very simple "smoke tests" that didn't check much. They also used random inputs, which, when fully randomized, are pretty poor for testing something like Zstd (because they just go down one of a few failure/rejection code paths).

Also, relatively few properties were checked. Although all agents used QuickCheck, 63 out of the 160 runs only checked a single property. Agents once again mostly relied on traditional testing, although they technically did use QuickCheck. For whatever reason, agents actually wrote more traditional tests than under the Default condition or most other conditions, but did fewer test-fix iterations (which resulted in this condition coming in with below average cost).

TDD underperformed here as well as in the IMAP RFC eval.

The TDD prompt seemed to cause large changes to agent behavior. Agents produced twice as many tests, and worked in a much more iterative test-code-test-code-etc. workflow, although a TDD advocate would probably say that agents didn't actually use TDD. There were only a few instances of agents doing some kind of fine-grained iterative TDD.

Overall, agents wrote more tests up front; for example, agents had one or more failing tests in 67 of 160 cases before doing substantial (non-stub) implementation, vs. 0 of 160 for the Default condition.

For broad test classes, TDD had more tests of every kind. There were more small, trivial tests and there were also more integration and end-to-end tests. Any kind of obvious high-level "agents did too much or too little of X" doesn't seem to fit the data. If we look at specific failures and how they were missed by tests, we can observe that the TDD condition had a number of these. For example, Zstd uses something called a jump table when there are four Huffman streams .

TDD agents were more likely to fail the eval test for this although they wrote more tests that cover the general case. For whatever reason, TDD agents were more likely to write tests that don't cover hard cases (e.g., making all four streams identical and then also making them trivial, like we saw with Verus). This is another case where I'd be curious what kind of visibility people at AI labs have since it's not obvious from the outside why priming agents with TDD made them write worse tests and worse implementations.

If we only had TDD and a few test conditions to go on, a hypothesis might be that TDD'd code often seems to have a lot of small tests that aren't very good, so maybe priming agents with TDD causes them to write more of these sorts of ineffective tests. But it's not clear why we should see the same pattern with Verus. Maybe we could tell whether or not this is true for TDD if there's a shared reason for the Verus (or other) behavior by re-running the experiment on an open model and inspecting what's actually going on inside the model at some level?

Two of the skills also caused agents to run in a more iterative approach, perhaps on the theory that executing more frequently would give better results, and both of those skills also underperformed. In general, across all conditions, agents were able to get the tests they wrote to pass on xhigh and max (not shown, but max had slightly better correctness than xhigh at substantially better cost). Getting their own tests to pass more iteratively tended to get agents to write more incorrect tests that would enforce incorrect behavior.

Yossi Kreinin had this thought for why TDD might result in worse tests:

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

Was my guess that TDD would underperform correct? Strictly on the result, the answer is yes. On my reasoning (not explicitly pre-registered in writing, but I do know what I was thinking), I think it's not clear. My thinking was something like, as we've recently：/benchpocalypse/ discussed：/ai-coding/ in a variety of contexts：/pl-tokens/, getting agents to actually do something like the right thing and not just overfit is a key part of achieving good performance or correctness with agents. Speaking to the methodology in general and not how this instruction changed agent behavior, TDD seems primed to cause overfitting.

Agents did write worse tests and sometimes used a relatively expensive and ineffective iterative workflow, but I don't know that the failure mode I'd expect from a human using TDD and then directing agents to implement was the real problem here, and that problem was where my intuition came from. I would rate the reasoning here as perhaps and perhaps not in the right vicinity; I think more evals and investigation would be necessary to decide this and I would guess that the result of additional data would be that my original reasoning is wrong.

Now we're getting into the range where results weren't far from average. Spin did moderately worse than average on both medium and xhigh, at below average cost. As we saw with the other formal tools, usage of Spin was generally ineffective. In this case specifically, using Spin to model a certain class of behavior had no correlation to passing or failing the hidden tests covering that behavior. Usage of Spin was superficial and not productive.

Hegel is a property-based testing library based on Hypothesis：https://github.com/hypothesisWorks/hypothesis/.

As we might expect by now, agents didn't use Hegel effectively. To the extent they used it, they used it superficially, and they generally used it after heavily relying on ordinary testing. Since just saying that agents didn't really meaningfully do the thing is repetitive, I'll make these sections short and only highlight particular curiosities.

The actual workflow agents used was generally

As noted above, the Hegel skill didn't improve correctness. Correctness was worse (though it was close enough that this could've been random). What was more striking was that cost was much higher (26% higher on medium and 41% on xhigh), for reasons which seem causal.

The skill caused agents to generate more tests. The additional tests were mostly checks that malformed inputs don't cause a panic and round-trip tests. The former is something that agents were already inclined to do an excessive amount of for all of the property-based and fuzzing conditions, so additional effort there wasn't useful. The latter doesn't seem like an inherently bad idea (I even often explicitly instruct agents to create round-trip tests and they seem to be useful to check specific properties), but it wasn't done in any of the most bug-prone areas. Without additional instruction, agents were inclined to create round-trip tests for relatively trivial properties that were already likely to be correct.

As for the cost, there are multiple reasons for the cost. One is that the skill is fairly large (34k characters for the skill, which also loads a 45k Rust-specific reference, which ends up being more than 20k tokens). This was loaded at the start of the run and was re-read on many subsequent actions. This resulted in an average additional dollar cost of 16% for medium and 18% for xhigh (by raw tokens, the average increase was 900k on medium and 1.8M on xhigh; although the cache hit rate on these was very high, 99.85% after the initial read, they were re-read enough that this was still a substantial fraction of total cost).

A multiplicative cost (this multiplier is included in the previous numbers) is that the skill also specified a structured set of operations that cause a lot more work to get done. This work didn't increase correctness, so this increased cost without a concomitant benefit.

One thing to note is that the skill was "only" used in 157 out of 160 cases. As is generally the case when using LLMs, the actions and results are random. If you have a skill available that you think an agent should use for a particular task, it may or may not use it depending on factors that seem opaque to people outside of AI labs.

In this case, only 108 out of 160 runs actually opened the skill：https://github.com/trailofbits/skills/blob/d3323cefbcf645678b8dc481de204b02ad3d02dc/plugins/property-based-testing/skills/property-based-testing/SKILL.md to read it. The skill suggests using proptest in Rust, but the skill suggests approval is required to add a dependency and these were all single-turn autonomous runs, so this wasn't done.

As with the other property test cases seen so far, property testing was rudimentary and not done in a helpful way.

Rstest is a fixture-based：https://en.wikipedia.org/wiki/Test_fixture#Software test library.