AI can generate the code. We can verify the behavior. But who decides
what correct means?
I wrote recently about a coding agent that built me a password reset
flow with a reset link that worked more than once.
The bug survived because nobody had written down that a reset link
should be single use. It was obvious right up until it wasn't.
My argument was that as AI makes implementation cheaper, verification
becomes the bottleneck. The feature request said "build password reset."
The agent built password reset. The happy path worked. The tests passed.
The implementation looked finished.
What nobody had asked was whether the same reset link should work twice.
So I added an independently written behavioral specification. The agent
implemented against it. The verifier rejected the reusable token. The
agent fixed the implementation. The verifier passed it.
That seemed like a useful pattern:
Then I published the article, and the comments started finding things my
specification didn't say. That exposed a harder problem.
The specification wasn't finished either
One reader asked what would happen if two password reset requests using
the same token arrived at the same time.
I hadn't tested that. My test covered sequential reuse:
But concurrent reuse is different:
Both requests check the token while it is still unused. Both proceed.
If validation and consumption are not a single atomic operation, "single
use" can still produce two successful resets.
The original invariant was incomplete.
That doesn't make the specification useless. It makes the specification
provisional.
The interesting part is where the new knowledge goes.
Once somebody discovers that "single use" also means competing attempts
cannot both succeed, that should stop being knowledge held by the person
who noticed it. It belongs in the durable definition of correct
behavior.
The specification changes.
Which means the loop is really closer to this:
That is messier than the first diagram.
It is also much closer to engineering.
Separate tests can share the same mistake
Another reader described an integration builder where an agent wrote
both a connector and the tests for that connector.
Everything passed.
Both were wrong.
The connector and its tests encoded the same incorrect assumption about
OAuth token refresh. The mistake only surfaced when a customer's token
expired during a live session.
The implementation and test suite were separate artifacts. They were not
independent in the way that mattered.
They shared an assumption.
That distinction matters because "independent verification" can sound
like an organizational property:
- different file
- different test suite
- different agent
- different step in the pipeline
None of those necessarily provides independence.
If the implementation and verifier derive their definition of correct
behavior from the same incomplete prompt, they can agree perfectly and
still be wrong.
The student is no longer literally grading the same exam.
Two students have simply studied from the same incorrect answer key.
Generating more tests doesn't discover the missing rule
Another commenter asked whether property-based testing or giving an
agent an adversarial security persona might do a better job uncovering
these unstated constraints.
I think both are interesting, but they expose the same boundary.
Property-based testing can explore a stated invariant extremely well.
If I tell a framework:
A successfully consumed reset token must never produce another successful reset.
it can generate combinations and sequences I would never think to
hand-author.
But it cannot tell me that single use was a requirement if nobody
expressed it.
An adversarial agent has a similar problem. Asking a model to "try to
break this" may produce better tests than asking it to "write tests for
this feature." But if the adversary shares the same context, model
assumptions, and incomplete understanding of the requirement, how
independent is it really?
The question starts shifting from who writes the tests? to a more
difficult one: where does the definition of correct behavior come
from?
The verifier can be wrong too
One of the most interesting examples in the discussion came from a
verification harness rather than generated application code.
A capability test timed out.
The harness recorded the result as a failure.
But a timeout did not establish that the capability failed. It
established that the harness did not obtain a result within the allotted
time.
Those are different claims.
FAILED
and
NOT TESTED
are not interchangeable.
The verifier had turned an observation failure into an assertion about
capability.
That's a useful warning for any architecture built around deterministic
verification: deterministic does not mean correct.
A verifier can enforce the wrong invariant with absolute consistency.
So can a specification.
The goal isn't to replace an unreliable agent with an infallible
verifier. There is no infallible verifier.
The goal is to make the definition of correctness explicit enough that
it can be inspected, challenged, tested, and revised independently of
the implementation.
So who writes the contract?
This was the question that pushed the argument furthest for me.
If humans have to write complete behavioral specifications before agents
can implement anything, haven't we simply moved the bottleneck back to
humans?
Probably.
And worse, the concurrency example demonstrates that humans don't
necessarily know the complete specification beforehand either.
So "humans write the contract" isn't much of an answer.
An agent could propose it.
That sounds circular at first. If the agent proposes the implementation
and proposes the contract, aren't we back to the student grading the
exam?
Only if proposing the contract and accepting the contract are the same
operation.
They don't have to be.
An agent might generate a candidate operating contract:
reset token:
may be used once
competing attempts cannot both succeed
expires after N minutes
cannot authorize a different account
A human, another system, or some combination can then challenge that
much smaller artifact.
The question being reviewed becomes:
Is this an adequate definition of correct behavior?
rather than:
Is this entire implementation correct?
That doesn't solve the trust problem, but it reduces its surface area.
Reviewing four lines is a different activity than reviewing four hundred.
One is a conversation about intent. The other is an audit.
But this runs straight back into the answer key problem.
If the same model that will implement the feature also proposes the
contract, they share assumptions. An agent that doesn't know single use
matters won't propose single use as an invariant. It will produce a
confident, well-formatted contract with the same hole in it, and now the
hole has been written down and approved.
So accepting a contract has to do more than approve it. It has to
introduce something the proposing agent didn't have.
That might be a person who has debugged this class of bug before. It
might be a genuinely different model, though I'm unsure how much
independence that buys. It might be a checklist derived from past
incidents, which is really institutional memory in a form an agent can
read. For a reset token, somebody's list somewhere already says: single
use, expiry, no account substitution, no concurrent success, session
invalidation.
The value comes from the independence of the source, not from the
ceremony of the review.
That may be a more tractable thing to build tooling around than
verification itself.
Maybe verification isn't the deepest bottleneck
This is where the comments changed my framing.
I started with:
I'm less sure that's where it stops.
Once implementation is cheap and verification is increasingly
automatable, the harder problem may become discovering the invariants
worth verifying.
Call it contract discovery.
The requirement says:
Reset my password.
Somebody has to discover:
The link works once.
Then:
Two concurrent attempts cannot both succeed.
Then perhaps:
The token cannot authorize a different account. A token issued before another successful reset may no longer be valid. A reset invalidates existing sessions.
Some of those are product decisions. Some are security properties. Some
are implementation-independent behavioral invariants. Some may not apply
at all.
The difficult work is deciding which ones belong to the definition of
correct.
AI can help propose them.
Property-based testing can explore them.
Deterministic systems can enforce them.
Production incidents will unfortunately discover some of them for us.
But none of those eliminates the need to decide which claims actually
define correctness.
This gets harder when agents start acting
There is another reason I think this matters beyond generated code:
agents don't just write things anymore. They call things.
An agent calls an API. The response is 200. The agent moves on.
But a 200 says the request was processed. It doesn't say the
constraint the agent's plan depended on was enforced. Maybe the call
timed out after the write succeeded, so the retry performed the effect
twice. Maybe the operation was legitimate the first time and should have
been rejected the second.
That second one should look familiar. It's the reset link, one layer
out.
A bad implementation leaves an artifact somebody can inspect later.
A bad tool call already happened.
It sent the email. Charged the card. Revoked the access. Posted the
message.
There is no diff to read.
This is where the contract-discovery problem becomes more consequential.
The system needs some definition of what the agent is permitted to cause
and what evidence would establish that the intended effect actually
happened.
I don't think I have the architecture for that yet, but one boundary is
becoming clearer:
The specification can be agent-readable without being agent-owned.
The agent should be able to see the invariant. Withholding the
requirement only makes the work guesswork.
But the agent shouldn't be able to quietly redefine the invariant when
satisfying it becomes inconvenient.
Whatever accepts, stores, and evaluates the contract needs some
independence from the reasoning that produced the implementation or
action.
Where that boundary belongs remains a harder question.
The specification is durable because it can change
Calling the specification a durable artifact can sound like calling it
an immutable one.
I don't mean that.
A durable specification should change when we learn something about what
correct behavior actually requires.
What makes it durable is that the knowledge survives the implementation
that taught us the lesson.
The reset implementation may be rewritten next month.
The framework may change.
The agent may change.
The database may change.
But once we've established that two competing reset attempts cannot both
succeed, that invariant should survive all of them.
The same applies to an integration. Once a production failure teaches us
what token refresh must guarantee, that knowledge should not remain
attached to the incident report or the engineer who debugged it.
It should become part of what "correct connector" means.
The implementation may be disposable. The accumulated definition of
correctness is not.
I still don't think this is solved
There are plenty of uncomfortable questions left.
How independent does a verifier have to be?
Can two agents using different prompts but the same underlying model
provide meaningful independence?
Who accepts an agent-proposed contract?
How do you distinguish a genuine product invariant from an
implementation detail that shouldn't survive the current code?
What happens when two valid invariants conflict?
How do contracts evolve without quietly weakening previous guarantees?
And how do we verify effects in external systems where state is delayed,
partially observable, or distributed?
I don't have good answers to all of those. That's partly why I don't
think the answer is simply "write better tests." The tests are
downstream of the harder question.
Write down what you mean by correct
The original password-reset bug happened because a rule existed in
someone's head and nowhere else.
The comments on that experiment showed the next problem: writing down
one rule doesn't mean you've found all the others.
That's fine. The specification doesn't have to arrive complete. It has
to provide somewhere for discovered invariants to go, and that somewhere
has to be a place with a history: versioned, reviewable, and attached to
the behavior rather than to the incident that revealed it.
Maybe an agent proposes them. Maybe a human notices them. Maybe
property-based testing exposes them. Maybe an independent reviewer asks
the annoying question nobody else asked. And sometimes production will
teach us the expensive way.
The important part is that each discovery makes the durable definition
of correct behavior better.
AI is making it remarkably cheap to turn an instruction into working
code.
Verification asks whether the code did what we said. Contract discovery
asks whether we said enough. I'm starting to think that's the harder
problem.
Top comments (14)
This makes the specification problem concrete: the behavior people call obvious is usually absent from the artifact that code and tests actually consume. I like the idea of treating those negative cases as first-class requirements, because they give reviewers something precise to challenge before implementation hardens around an assumption.
Glad to see the concurrent-reset case in this follow-up. One detail I’d want to keep is the contract version attached to each verification result. After adding that concurrency rule, an older green run would still tell us something useful—just not that the stronger contract had been checked.
Yes. I think that's an important consequence of calling the specification durable and allowing it to evolve.
An old green result shouldn't become false when the contract changes. It remains evidence that implementation X satisfied contract version Y at that point in time. It cannot establish compliance with the stronger version Y+1.
So the verification result probably needs to bind together at least the implementation, contract version, result, and time of verification. Otherwise "passed" loses the context necessary to know what was actually proven.
And now we've wandered rather directly into provenance. :)
The reset case may be less about the specification being incomplete than about the shape the invariant was written in. "A second attempt is rejected" is a per-request predicate, and I ran the race to see what it actually binds to: across 200 trials of a non-atomic check-then-set, all 200 produced two successful resets, and in not one of them was any request rejected. So under concurrency that sequential assertion does not fail, it has nothing to assert on, because there is no second attempt that ever observes a used token. Write the same sentence as a count over the token's lifetime instead,
successes <= 1, and it fails on the first trial, while the atomic version passed 200 of 200 with exactly one rejection each. That bears on the property-based question you close with, since a count-shaped invariant does not require anyone to have thought of concurrency first, whereas the predicate form is quietly satisfiable by both branches of the race.That's a really useful distinction, and I think you're right that it puts pressure on how I framed the missing invariant.
successes <= 1describes the property I actually care about across the token's lifetime without requiring the specification author to predict concurrency as the failure mechanism. "A second attempt is rejected" accidentally embeds a sequential model into the requirement.That also makes the property-based testing question more interesting than I gave it credit for. The framework still can't invent an unstated requirement, but the shape of a well-stated invariant can expose failure modes the author never anticipated.
And 200/200 is a fairly persuasive way to make the point. :) Thanks for actually running it.
The line I keep rereading is where you say the system needs a definition of what the agent is permitted to cause and what evidence would establish that the intended effect actually happened, and that you don't have the architecture for it yet. I don't either, but I have two production scars that mark where the hole is.
For generated code the evidence channel is free: the artifact is sitting there and you can rerun it. For an action, the record IS the artifact. That makes the emitting path load-bearing, and it fails in two directions that both look fine.
Evidence without execution. Our onboarding wizard generated a reporter that posted outcome: success on a 30-minute timer whether or not the agent had run. Weeks of clean, continuous, well-formed, entirely fictional evidence. Every contract you could write over that data was satisfied. Nobody flagged it, because flagging requires a reason to look and a green record gives you none.
Execution without evidence. Our run attestations were bound to (repository, workflow filename). Someone renamed a workflow, and reporting began 404ing after the work had already been done. Authorised, executing, invisible. A quiet agent is indistinguishable from an idle one.
Those are fantastic counterexamples because they fail in opposite directions, even though both produce apparently reasonable system states.
The first one especially breaks a naive version of what I wrote. If evidence can be emitted independently of execution, then no contract over the evidence can prove the action occurred. You can have perfectly valid, well-formed, cryptographically pristine evidence of something that never happened.
And the workflow rename gives you the inverse: execution occurred, but the evidence path was detached from it, so the action becomes invisible.
That makes me think the missing architectural requirement is stronger than "produce evidence after an action." Evidence generation has to be causally bound to the execution path somehow. The system shouldn't be able to produce an execution receipt without executing, and ideally shouldn't be able to execute without producing the corresponding receipt.
Which immediately raises harder questions about partial failure, of course. What happens if the action commits and evidence emission fails? At that point, the evidence path itself starts looking like part of the transaction rather than downstream observability.
These are exactly the kinds of production scars I hoped somebody would bring up in the part where I admitted I didn't have the architecture yet. Thanks for sharing them.
The concurrency case has a mechanical fix that also sharpens the spec: make consumption atomic in the store instead of in the application protocol.
UPDATE reset_tokens SET consumed_at = now() WHERE token = $1 AND consumed_at IS NULL, then reject if affected_rows is 0. "Single use" stops being a rule the app has to remember and becomes an invariant the database enforces on every competing request at once — two simultaneous attempts can't both succeed, because the second UPDATE matches zero rows. The spec sentence and the mechanism collapse into one statement.The harder problem in your article is the shared answer key. Independence has to come from the definition of correct behavior being written down before the implementation exists. Otherwise the verifier and the implementation are two students who studied from the same incomplete notes, and their agreement carries no information.
Yes, push enforcement down to the store. An atomic conditional update is a much stronger mechanism than asking application code to remember the rule correctly across competing requests.
I'd keep one small separation, though: I don't think the specification and mechanism quite collapse into the same statement.
successes <= 1is the behavioral invariant; the conditionalUPDATEis one implementation that can enforce it. If I replace the database tomorrow, I still want the invariant to survive even though that mechanism disappears.And I agree that the shared answer key remains the harder problem. The database can enforce single use beautifully once we've decided single use belongs in the definition of correct. It can't tell us that we forgot to require it.
Honestly, I feel like LLMs promised us a less painful future and I find myself entangled into a higher abstraction layer of how to know the ins and outs functionally and more importantly error-prone wise of huge chunks of "foreign" code.
Ughhh
I feel some of that tension too. :) We were promised less time wrestling with implementation, and in some ways we've gotten it. But the work hasn't necessarily disappeared. Some of it has moved upward into understanding behavior, boundaries, failure modes, and code we didn't personally write.
What worries me is when generation speed outruns our ability to build a mental model of what was generated. At that point we're not really maintaining code we understand so much as auditing an increasingly large foreign artifact.
Maybe the win isn't eliminating that higher-level reasoning, but making sure we're spending human attention on judgment and invariants rather than boilerplate. I'm not convinced we've figured out that balance yet either.
The independence of the spec is doing all the work here. If the spec gets written from the same conversation that produced the prompt, spec and implementation share the same blind spot - you end up with two artifacts that agree with each other and are both wrong, which is worse than one. The single-use reset link is the perfect example because "single use" lives in security policy, not in the feature request. Nobody asks for it because it feels obvious, and it stays obvious right up until the day it isn't. We started writing acceptance criteria from the ticket before touching the prompt at all, specifically so the spec can't absorb the implementation's assumptions. The closer the spec writer's information source is to the generator's, the less the verification step buys you.
Yes, and I think your last sentence gets closer to the real independence requirement than simply saying “use a different agent” or “write the tests separately.”
Two artifacts can be produced independently and still inherit the same blind spot if their information lineage is effectively identical. In that case, we've separated the work without introducing any new knowledge.
Writing acceptance criteria from the ticket before constructing the implementation prompt is interesting because it deliberately creates some distance between those paths. I'd still want other sources feeding the contract too, especially security policy, known domain invariants, previous incidents, and the accumulated “obvious” constraints that rarely make it into feature requests.
I'm increasingly thinking independence needs to be evaluated by where the knowledge came from, not simply who or what produced the artifact. Thanks for sharpening that distinction.
Some comments may only be visible to logged-in visitors. Sign in to view all comments.