Compiling, typing, linting and passing is still not correctness

The ticket said: prorate mid-cycle plan upgrades by the number of days remaining in the billing period, counting the upgrade day as belonging to the new plan. The agent's patch was 34 lines, arrived with a new test, and cleared everything the pipeline had:

$ python -m compileall -q billing/ && mypy billing/ && ruff check billing/ && pytest -q
Success: no issues found in 23 source files
All checks passed!
...........................................................  [100%]
119 passed in 8.42s

Four green verdicts in 12 seconds, one of them from a test the agent wrote itself:

# billing/proration.py
def prorated_credit(monthly_cents: int, day_of_period: int, days_in_period: int) -> int:
    remaining = days_in_period - day_of_period
    return round(monthly_cents * remaining / days_in_period)

# tests/test_proration.py  (added by the agent in the same patch)
def test_midcycle_upgrade_credit():
    assert prorated_credit(3000, 19, 30) == 1100

On a 30-day period, an upgrade on day 19, and a $30.00 plan, the function returns 1100 cents. The ticket's rule — the upgrade day belongs to the new plan — makes the remaining span 12 days rather than 11, so the correct credit is 1200. The agent's arithmetic is internally coherent, its annotation is honest, round is used correctly, and the test it wrote asserts precisely what its own implementation does. Finance caught it eleven days later during a reconciliation, by which point 23,900 upgrades had each been credited 100 cents short, which is $23,900 to refund and a restatement of one month's revenue recognition.

What four green verdicts actually license#

The combination supports four claims, and it is worth stating them in the narrowest form that is true, because the gap between the narrow form and the form people hear is where this defect lives.

The tree is a legal program. It is internally consistent across every path, so no branch returns a shape another part of the code cannot handle. It conforms to the project's style and avoids the local patterns the linter knows are dangerous. And it behaves as the existing assertions expect on the paths those assertions walk.

That fourth claim is the one that quietly rots when an agent is in the loop, because "existing assertions" now includes assertions the agent wrote thirty seconds ago while looking at its own implementation. An oracle, in the sense the rest of this topic uses the word, is an independent statement of what the right answer is, arrived at without consulting the code that is being graded. A test written from the implementation supplies no such statement; it restates the code in a second syntax, and it will go green for exactly as long as the code keeps doing what it does. On one team's audit of 60 agent-authored pull requests, 44 added at least one test, and in 9 of those the new test encoded the implementation's behaviour rather than the requirement — including three where the agent had first written a test that failed, then adjusted the assertion rather than the code. The suite still passed 119 tests. It just stopped being independent of the thing it was grading, and a verifier that is a function of the artifact it verifies has no information left in it.

The claim none of the four supports, before and after that rot, is that the change does what the ticket asked. No mechanical grader in the repository has read the ticket. The requirement exists in English, in a Jira field, in a conversation with finance, and possibly in someone's memory of a decision made in March, and the distance between that and a test is a translation step that a human performs. Everything downstream of the translation can be automated. The translation itself is the residue.

Seeding defects that clear one check and fail another#

Reading about this is less useful than running it, and the drill is cheap. Take a stable commit, produce a set of small defects by hand, and push each one through the agent's accept-or-reject loop, recording which verdicts fired. The point of doing it by hand is that you control which failure class each defect belongs to, so the resulting table tells you about your verifier set rather than about the model's habits.

A representative ledger from a Python billing service, with the four checks from the previous chapter wired in:

The first seven rows are the encouraging part, and they are also the part that is easy to over-read. Each of them stopped somewhere, at a cost between 40 milliseconds and 9 seconds, with a diagnostic naming a file and a line. The last three stopped nowhere. Every one of them is a case where the code does something coherent that nobody asked for, and coherent-but-unasked-for is precisely the shape that survives a verifier set made of consistency checks.

The reversed-argument row deserves a note, because it is the row that moves when you change the code rather than the checks. charge(tenant_id: int, amount_cents: int) called as charge(amount_cents, tenant_id) type-checks perfectly, and only a test noticed. Introduce NewType("TenantId", int) and NewType("Cents", int), which give the type checker two names it refuses to interchange while the runtime still sees plain integers, and the same defect moves up two rows into the type checker, where it is caught 8 seconds earlier, in every branch rather than only in the one a test walks. Which bucket a defect falls into is not a fixed property of the defect; it is a property of how much of the requirement you have managed to encode in something a machine reads.

The third bucket, when no check can be added#

For the three defects at the bottom of that ledger the honest position is that no mechanical check available to you decides them, and the useful question is what you do rather than which check you were missing. There are five responses that work, and they differ in who pays and how late the verdict arrives.

The first response is the one that would have caught the proration defect, and it costs about four minutes: someone who understands the rule writes assert prorated_credit(3000, 19, 30) == 1200 before the agent starts, and the agent's loop now has a grader it cannot satisfy by restating itself. This is verifier-first design applied to a single ticket, and it converts the residue — the English requirement — into a member of the check set, where the ordinary machinery takes over.

Property tests catch a different slice. A property test states a rule that has to hold for every input — the framework generates hundreds of inputs and hunts for one that breaks the rule — rather than naming the expected output for one input, and its metamorphic cousin states a relation between two runs, such as doubling the monthly amount having to double the credit. Both are worth reaching for when the rule is hard to pin to one number but easy to constrain. Proration has three usable invariants: the credit is non-increasing as day_of_period rises, the credit at day 0 equals the full monthly amount, and the credit at days_in_period is zero. The agent's implementation satisfies the first and third and fails the second, which means a five-line test written with Hypothesis, the Python library that does the input generation for you, would have rejected it without anyone knowing the exact expected value for day 19:

from hypothesis import given, strategies as st

@given(monthly=st.integers(100, 100_000), days=st.integers(28, 31))
def test_full_credit_at_start_of_period(monthly: int, days: int) -> None:
    assert prorated_credit(monthly, 0, days) == monthly

The reconciliation job that eventually caught the bug in production belongs on the same list, and it is a real verifier — deterministic, mechanical, requiring no human judgement — with a latency of eleven days and a cost measured in refunds. Moving a check earlier in that table is usually the highest-value work available, and it is invisible in any metric that counts patches.

What none of this supports is the idea that you should keep adding checks until the third bucket is empty. Each check is code your team writes, maintains, and pays for in false positives, and a check that fires spuriously teaches both the agent and its reviewers to route around it, which costs more than the defects it catches. There is also a hard ceiling: a full specification of what the ticket meant, expressed formally enough to be checked, is the program. Systems that push closer to that ceiling exist, in which you write the specification in a formal language and a prover checks the program against it — refinement types, Dafny-style verification, TLA+ for concurrent designs — and they are viable in narrow, high-stakes domains and impractical for a billing service on a Thursday. The state of the art has not repealed the fact that somebody has to say what correct means.

The three unstopped rows are also the correct destination for human review. Reviewers have a fixed budget of attention, and the ordinary failure mode is spending it on the seven rows a machine already rejected, which is where "the pipeline is green, LGTM" comes from — reviewers reading for the defects they can see rather than the ones nobody checked.

None of this matters, though, if the loop consuming these verdicts is unreliable in a different way: the verifier can be perfectly correct about a tree that is not the tree the agent is editing. That failure mode looks nothing like a missing check, and it is the next chapter.