Verification Is Cheap Now. Validation Isn't.

In [AI for Research](@/blog/AI for research.md) and The Loop Gets Shorter I wrote about how fast I can now get from an idea to working code. I said much less about checking that the code is right, and that is where my own field comes in.

I think formal methods does well out of this. Generating models and proofs for a problem is a lot cheaper than it was. You can have a model draft a small language or tool around your problem and test the hypothesis right away, instead of first becoming fluent in whatever proof language your subfield settled on. AI-written code also needs a lot of checking. It makes assumptions nobody asked for, and it is often wrong in ways that look right on a skim, which is the kind of output formal methods people already know how to check.

I don’t do much of that checking myself, though. Most days, reviewing AI-generated code comes down to a skim. I read it, nothing jumps out, I move on.

Developers in general don’t trust this code much either. In DORA’s 2024 State of DevOps report, 87.9% of respondents reported some level of trust in the quality of AI-generated code, though for most of them that trust was low, with 39.2% reporting little (27.3%) or no trust (11.9%). 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 wrote about this in a thread from May 2022, half a year 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.

A few tweets later he wrote “AI moves the problem from generation to recognition/validation. My own work has been building toward this in many ways… We need MUCH more.” For the code I generate, the one doing the recognizing is mostly me, without much tool support.

Barry Boehm put the difference 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 quickly. Fernanda Graciolli and Nada Amin explain why in their ACM Queue piece, “You Don’t Know Jack About Formal Verification”: “By eliminating the cost of writing proofs, AI is removing the biggest barrier to formal verification.” The guarantee you get from a proof is a strong one:

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 be mostly for 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 one company that changed its mind. Yaron Minsky writes that for 25 years he told people Jane Street was just not interested in formal methods, apart from special cases like hardware synthesis. Now they are building a team for it, because “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 what agentic coding 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.”

A proof only tells you that the code matches its spec, though. Leslie Lamport said something close to this years ago, in a video interview with Erik Meijer quoted in a piece on TLA+. He was talking about people in specification and verification looking 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.

A model that drafts my spec and closes my proof obligations helps with the expressing, not the understanding.

NASA’s page on formal methods also admits a practical limit. 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 has not solved that complexity. The ACM Queue piece says as much about scope: “verification makes the core airtight but doesn’t guarantee end-to-end correctness.”

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

So the proof doesn’t tell you whether the spec was the right thing to want. That is validation, and for my own code that part is on me.

Ryan Wright’s “Dialectical Review” describes how I review. A reviewer reading a diff can’t easily rebuild the author’s intent from it, so in practice “[t]hey pattern-match, skim, and then ‘LGTM’, approved.” His fix is to withhold the author’s tests and have the reviewer write their own adversarial tests, from their own idea of what the code should and shouldn’t do.

Verification is getting cheaper fast. Validation isn’t, and I don’t see anything coming that will do it for me. Maybe that’s fine.