Santiago Mansilla.

The verification ladder: when the domain writes its own code

When the domain generates its code with AI, reviewing it doesn't scale. The verification ladder: let the cheapest verifier check each claim.

Santiago Mansilla 8 min read

Generating code is now nearly free; verifying it isn’t. That asymmetry — cheap to generate, expensive to verify — was the ceiling on agents in production, and when the domain expert — the accountant, the support lead, whoever knows the rules — starts generating their own modules with an AI assistant, it becomes the team’s central problem: the volume of code grows faster than anyone can read it.

The answer isn’t to review more. It’s to move up a layer: stop competing by writing the code AI generates in seconds, and start owning the domain’s invariants — the rules that can’t be broken — and the cheapest verifiers that enforce them on their own. The tool that organizes that work is a ladder.

Code gets commoditized; invariants don’t

Forward Deployed Engineer postings — the engineer who deploys product glued to the client’s domain, writing code that ships to real production — went from 643 in April 2025 to 5,330 a year later: a 729% year-over-year jump (Indeed data via Business Insider). It’s no accident: the software bottleneck in a regulated domain moved from writing the code to knowing which code is correct.

AI commoditizes writing code. It doesn’t commoditize knowing which journal entry is legal under Spanish accounting law, or keeping a system alive in production for years, or — the new one — owning the dataset that measures whether an agent does the job well. Ramp’s CTO puts it this way: “your code is the LLM now… plus instructions and an infinite loop” (interview). The product stops being only deterministic code and starts including agents with instructions; an agent without a test that measures it is an agent you don’t know works.

In practice: write the list of which invariants in your domain live only in the head of whoever knows them, and not in a verifier that blocks violations. That list is your real backlog.

Review surfaces, not diffs

Reviewing 100% of the diffs AI generates doesn’t scale, it burns you out, and it turns you into the department of “no.” Not all code weighs the same: a broken reporting dashboard gets fixed Tuesday; a wrong journal entry is a misfiled tax return.

The line is drawn by blast radius — how far the damage reaches if something breaks. Hot zone: money, the general ledger, tax calculation. Cold zone: listings, read-only reports, internal dashboards. The hot zone demands the strict verifiers; in the cold zone, let anyone (human or agent) generate whatever they want, because breaking is cheap. And the line is architectural, not procedural: cold-zone code doesn’t write to the accounting collections, and that’s enforced in the system, not trusted to good faith.

In practice: mark which modules touch the ledger or money, review only the surfaces of those, and let the rest break without your eyes on it.

The verification ladder

Fewer than 5% of diffs should reach your eyes; the rest is covered by a cheaper verifier. The ladder orders those verifiers from free to scarce, and the engineer’s job is to push each check as far down as it will go:

  • N1 · Type or schema — the shape contract of the data: amount as Decimal, calendar-date as its own type. Free, on every keystroke. What’s impossible to represent doesn’t need verifying.
  • N2 · Domain semantic lint — rules that read the syntax tree and block forbidden patterns. Seconds, on every PR. It catches the error before it exists, and the integration point matters: Google set as a threshold tolerating up to ~10% false positives in a code-review check, but demanding ~0% at compile time (study).
  • N3 · Deterministic and property-based tests — generate thousands of valid cases and assert a universal property: for every invoice, its entry balances. Minutes, on every PR. The technique is old (QuickCheck, 2000); for outputs with no correct answer to compare against, like those of an AI parser, its cousin is metamorphic testing: asserting a relationship between two outputs instead of an exact value.
  • N4 · Integrity check on real data — the invariants run against production every night by a cron. Nightly. It catches the mismatch before the client does; inferring and watching invariants over real executions is what Daikon has done since 2001.
  • N5 · Agentic benchmark (pass@k) — hits in k attempts: the only possible verifier for the probabilistic, like an AI parser or a model swap. Hours, per release.
  • N6 · Human judgment — design, modeling, domain decisions. Expensive and scarce. The one thing you can’t delegate.

Human judgment is the team’s most expensive resource, so it’s reserved for what no lower rung covers. This is the structural answer to the asymmetry: AI inflates the volume of generated code, and your ladder decides whether verification scales with it or drowns you (Willison on the rebalancing).

In practice: take a check that today only your eye does (N6) and drop it down a rung — the rule you repeat in every review becomes a lint (N2) that runs on its own.

Every incident drops a rung

Every failure you catch at one rung should produce, in under 5 days, a verifier at a lower rung that catches it next time. A mismatch a client found — N6, the most expensive and embarrassing rung — becomes a nightly check (N4), a regression test (N3), and, if it touches a parser, a benchmark task (N5).

It’s a compound-interest mechanism. Every incident leaves the system cheaper to operate, not more expensive, and within a year the platform knows more about the domain than any single person. The key is to record the learning twice: in human form — a note, a logged decision — and in executable form — the check. Recorded only in one head, it leaves with the person; recorded only as a check, no one remembers why it exists and it ends up deleted.

Ramp measured it and found what nobody expects: most of its skills subtracted performance from the agent, and one of them could have its context cut by 64% without barely moving the score — proof that almost all of that context was noise (benchmarking of its accounting agent). Without the rung that measures, every one of those decisions is made blind.

In practice: take the last incident a client reported to you — not you — and write the cheapest verifier that would have stopped it. Move it down from your eye to a machine.

None of this is new: the ladder’s lineage

Fitness functions — the genre that turns any architectural property into a CI check — were named in 2017 (Building Evolutionary Architectures, by Ford, Parsons, and Kua), but the ladder fuses three rather older traditions.

The test pyramid, stretched at both ends. Mike Cohn drew it — many cheap tests at the bottom, few expensive ones at the top — and Martin Fowler fixed it; Kent C. Dodds rotated it into the testing trophy, adding static analysis as the base and reasoning by confidence/cost return. The ladder stretches it further: downward, to the type that makes the illegal state unrepresentable — “parse, don’t validate” by Alexis King, the invariants of Bertrand Meyer’s Design by Contract (1992) —; and upward, to the invariant watched in production and the agentic benchmark, which the classic pyramid didn’t have. The root of the “cheap and early” principle is the shift-left of 2001.

Formal methods, in a light version. You don’t need to prove the code: AWS specifies the design in TLA+ to catch concurrency bugs no test instantiates — “prevent serious but subtle bugs from reaching production”. The type (N1) is the cheapest version of that same idea: a proof the compiler checks for free — in a double-entry ledger, the type that keeps an unbalanced entry from even compiling.

Toyota’s poka-yoke, for rule 3. “Every incident drops a rung” wasn’t born in software: it’s jidoka — stopping the line at the first defect and fixing the cause, not the symptom — and poka-yoke — designing the process so the error can’t recur — from Toyota’s factory floor in the 1960s. Google SRE’s blameless postmortem and Fowler’s “a regression test for every bug” are the same move: turning the failure into a permanent, cheap guard. And “record the knowledge twice” has a name too — specification by example (Gojko Adzic) and living documentation (Cyrille Martraire): the example that is at once prose for the human and a test for the machine.

Review your ladder and give each rung the name of its ancestor: the one with none is probably not a rung, it’s an unverified habit.

To go deeper

The type as proof (N1):

  • Parse, don’t validate — Alexis King, 2019. Validation throws away what it learned; parsing fixes it in the type. Post
  • Applying “Design by Contract” — Bertrand Meyer, IEEE Computer, 1992. Precondition, postcondition, and class invariant as code. PDF
  • Designing with types: making illegal states unrepresentable — Scott Wlaschin, 2013. Business rules as compile-time unit tests. Post

The verification strategy:

  • Building Evolutionary Architectures — Ford, Parsons, Kua, 2017. The origin of fitness functions (book, O’Reilly).
  • TestPyramid — Martin Fowler, 2012. Bliki
  • The Testing Trophy — Kent C. Dodds, 2017. Adds static analysis as the base of the pyramid. Post
  • Lessons from Building Static Analysis Tools at Google — Sadowski et al., CACM 2018. Why the check has to arrive in the developer’s flow. PDF

Properties and formal methods:

  • QuickCheck — Claessen and Hughes, ICFP 2000. The founding paper of property-based testing (ACM Digital Library).
  • How Amazon Web Services Uses Formal Methods — Newcombe et al., CACM 2015. TLA+ to verify the design, not the code. PDF
  • Dynamically Discovering Likely Program Invariants (Daikon) — Ernst et al., IEEE TSE 2001. Inferring invariants from real executions. Summary

Executable knowledge and incidents:

  • Specification by Example — Gojko Adzic, 2011. The example that is spec, test, and living documentation at once (book).
  • Documenting Architecture Decisions — Michael Nygard, 2011. The ADR: recording the why, not just the what. Post
  • Postmortem Culture: Learning from Failure — Google SRE, 2016. The blameless postmortem. Chapter
  • Poka-yoke — Shigeo Shingo, Toyota Production System. Designing the process so the error is impossible. Reference

The code you write today will probably be rewritten by a better model in six months. The ladder you build around it — the cheap rungs that verify your domain — stays and runs on its own. It’s not about defending yourself from AI: it’s about being the person thanks to whom everyone else’s AI works in production.

How many of the rules you repeat in every review still live only in your head, and not in a rung that checks them for you?

Subscribe to the newsletter

AI engineering in production — one email a week, no noise.

Subscribe →