Verification Is Cheap Now. Validation Isn't.

There’s a worry going around that’s hard to dismiss outright: AI is chewing through the problems researchers used to spend careers on, and it’s starting to feel like the job itself is becoming redundant.

I don’t think the research style is over. I think it just got faster. On the applied side, the thing that’s changed isn’t that the ideas come from somewhere else now, it’s that testing an idea used to mean being fluent in whatever proof language your subfield had settled on, and now it doesn’t. You can have a model draft a bespoke language or tool shaped exactly around your problem and throw the hypothesis at it right away, instead of waiting until you’re fluent in someone else’s.

Formal methods specifically, I think, comes out of this ahead. Generating models and proofs for a given problem is a lot cheaper than it was. And there’s a second, less obvious reason: AI-written code tends to be overconfident, full of assumptions nobody asked for, quietly wrong in ways that look right on a skim. Checking that kind of output is exactly the job formal methods people already know how to do, and it’s not a niche concern anymore.

I lived the slower version of this. My PhD tool, MIDES, took the better part of two or three years to build, and most of that time wasn’t spent on the actual algorithm, it was spent fighting Scala. A lot of it went into scaffolding: the boilerplate an experienced programmer sets up in twenty minutes because the thinking is already behind them, embedded in muscle memory they don’t have to think about. Reading code was never my problem. I could spot a pattern and know what structure was missing. Writing it from scratch was.

It’s tempting to describe what’s happening now as having a few master’s students on call. You bring the direction, they implement, you read the output and correct what’s conceptually wrong. The work moves faster than it would alone. But real students surprise you. They go sideways into something you hadn’t considered, ask a question that reframes the problem, and somewhere in the friction of explaining why this approach and not that one, something gets transmitted. The AI doesn’t need to learn from me. It won’t go on to supervise its own students someday.

I believe all of that. I’m less sure I live up to it day to day. Most days, reviewing AI-generated code comes down to a skim for a feeling of plausibility. I read it, nothing jumps out, I move on. There usually isn’t much more rigor to it than that, admittedly.

I’m apparently not alone in that. In DORA’s 2024 State of DevOps report, 87.9% of respondents reported some level of trust in the quality of AI-generated code, but the trust was mostly thin: 39.2% reported little (27.3%) or no trust (11.9%) at all. One participant compared checking and fixing AI output to

the early days of StackOverflow, [when] you always thought people on StackOverflow are really experienced, you know, that they will know exactly what to do. And then, you just copy and paste the stuff, and things explode.

Shriram Krishnamurthi saw this coming in a thread from May 2022, months before ChatGPT came out:

There’s an AI peril we’re not talking about that needs more attention. AI-generated code is great. I’m a fan. BUT: AI code generators are in what I call a Postel mode: permissive in what they accept. That is, no matter what you ask for, they produce something.

Nothing stops at “I don’t know.” And a few tweets later: “AI moves the problem from generation to recognition/validation. My own work has been building toward this in many ways… We need MUCH more.” When generation gets cheap, the problem moves to whoever is supposed to be catching the bad output. Right now that’s mostly me, supplying it out of my own skull, on the fly, without much support.

There’s a distinction from software engineering that’s older than any of this. Barry Boehm put it as two questions: verification asks whether you built the system right, validation asks whether you built the right system. AI is getting good at the first one, fast. Fernanda Graciolli and Nada Amin’s ACM Queue piece, “You Don’t Know Jack About Formal Verification”, lays out why: “By eliminating the cost of writing proofs, AI is removing the biggest barrier to formal verification.” What used to take a PhD and days of coaxing a proof assistant is now something a model can draft and iterate on directly. The guarantee you get out the other side is a real one too:

The guarantee is only as good as the spec, but when the spec is right, the guarantee is absolute: the property holds in every reachable state of the program.

Formal verification used to live mostly in places like avionics, railways and chip design, because few others could afford it. The same article says it’s “no longer just for safety-critical systems with the budget for specialized proof engineers. It’s for anyone who has a property worth proving.”

Jane Street is a useful data point here, mostly because of who’s saying it. Yaron Minsky writes that for 25 years he told people Jane Street was just not interested in formal methods, outside of special cases like hardware synthesis. Now they are building a team for it: “the emergence of agentic coding has changed our perspective, and we’ve gone from being skeptical to being excited about the possibilities.” Part of the reason is a direct complaint about what agentic coding actually produces:

Agentic code is getting better, but is [sic] still tends towards slop: overly complicated, full of weird bugs and corner cases, often not following essential invariants of the codebase that it’s a part of.

Their goal, in Minsky’s words, is “to make formal methods as pervasively useful of a tool for building software as sophisticated type systems are for us today.”

Leslie Lamport made a related point years before any of this, in a video interview with Erik Meijer quoted in a piece on TLA+. He was talking about people in specification and verification hunting for new kinds of math, not about AI:

My feeling is that people are looking for magic bullet in math, [that] there’s this wonderful thing… somehow you discover the right math and that math solves the problem for you. That’s not the way it happens. … When you understand something then you can find the math to express that understanding. The math doesn’t provide the understanding.

An AI model that drafts my spec and closes my proof obligations does the expressing faster. It doesn’t give me the understanding.

NASA’s own writeup on formal methods concedes a limit from the other direction. Checking the entire state space of a design is “rarely done in practice today (except for the critical components of safety critical systems) because of the enormous complexity of real systems.” AI hasn’t solved that complexity, and even a working proof only tells you the code matches its spec. The ACM Queue piece says this too, plainly: “verification makes the core airtight but doesn’t guarantee end-to-end correctness.”

The clearest version of that gap I’ve seen has nothing to do with AI. A piece on the limits of formal verification for AI safety points to the Perseverance rover’s landing on Mars in 2021. JPL used a formal tool, Questa PropCheck, on the FPGA design in the rover’s terrain-relative navigation system, the part that matched camera images to a map during descent. That gave them a real guarantee: the design was bug-free in all legal input scenarios. It said nothing about the physical process of landing, or the mission’s odds as a whole. By one analysis of Mars probe failures, software problems account for roughly a fifth of total mission failure risk.

The proof says nothing about whether the spec was the right thing to want in the first place. That question is still sitting entirely in the human’s lap. Mine, in this case, and I don’t think I do that job especially well.

rrwright’s “Dialectical Review” describes my failure mode. A reviewer reading a diff can’t easily rebuild the author’s intent from it, so in practice “they pattern-match, skim, and then ‘LGTM’, approved.” The fix it proposes is to withhold the author’s tests and have the reviewer write their own adversarial ones, from their own model of what the code should and shouldn’t do. I skim for a feeling of plausibility.

Verification is getting cheaper fast, which is good news. Validation isn’t, and it’s not clear anything is coming to solve it for me. Maybe that’s fine.