Verification Without Inspection
A week ago I finished up at Westpac NZ. I was fortunate to spend the last few years there as a Distinguished Engineer, a role with an unusually wide and undefined remit. It was the perfect playground for a curious mind, giving me the freedom to think deeply about all sorts of interesting questions. The trouble is that there are only so many hours in the day, and it’s never enough for all the curiosities tugging at my mind. So I made the difficult decision to leave so I could create more time, at least for a while, to scratch a few of those itches. This post focuses on the one that I’m most passionate about.
AI is fundamentally changing what it means to be a software engineer. As coding agents take over more of the writing, verification is quickly becoming where much of our time and focus is spent - and it isn’t the job most of us engineers signed up for. For the last eighteen months I’ve been wondering what could take some of that weight, and my gut keeps pointing back to something I fell in love with at university twenty-three years ago but never once got to use.
Twenty-three years ago
As a child I loved maths for its purity, and computers and programming for their power. These two passions stuck with me as I grew older, so when I went to university I naturally chose to study both mathematics and computer science.
If I’m honest, the papers I enjoyed most were the maths ones, especially those built on logic and proof - discrete mathematics, mathematical logic, combinatorics. The process of working out a proof was immensely satisfying - step by step, each move following logically from the last until the whole thing fit together like a puzzle. What a nerd, right? But when I realised that those same proofs could be applied to programs and code… well, now we’re talking!
The formal methods papers at Victoria University of Wellington were where that realisation happened for me - specifically, COMP425 (Computational Logic), COMP426 (Formal Software Development), and COMP473 (Formal Aspects of Concurrent Systems). There were only two or three of us in those classes so they almost didn’t run them, but I’m so glad Lindsay Groves did anyway.
I loved that work in a way that’s hard to explain. Formal methods is the umbrella for a lot of things - specification languages, computational logic, refinement - and I loved all of it. But it all comes together in verification: proving that a program does what its specification says.
Back in those days, we did this type of work by hand. I don’t remember using any software or tooling to help at all, actually. Derivations, proofs, refinement steps, all worked out on paper. It took a while to get right, but when you did, it was right. Not “the tests pass” right. Not “it worked in staging” right. Provably, mathematically right. And that’s where the satisfaction came from. I kept those assignments for years afterwards and would occasionally reopen them just to marvel at that certainty.
Some of the material I’ve held onto all these years - handwritten weakest-precondition derivations alongside the papers we studied, from proving parallel programs correct to I/O automata.
There are two words that appear often in these papers: specification and verification. I find it fascinating, and somewhat serendipitous, that these are the same words our industry now reaches for as AI writes more and more of our code. Is it just a coincidence? I don’t think so.
Taking a punt
About eighteen months ago I saw Erik Meijer posting about formal methods in the context of AI on X. I didn’t know Erik personally, but I took a punt and messaged him about it. If you’ve been in this industry a while you’ll know his work even if you don’t know his name - LINQ, Rx, decades of programming-language contributions at Microsoft and Meta.
To my surprise, he replied almost immediately, with kindness and reading material. Erik saw the opportunity early and started building a language and a runtime that put formal methods to work on AI-generated logic - Universalis and Automind. How awesome is that?
I’ve been tracking Erik’s work carefully ever since. With that foundation in place, he’s now going after the risks that agents bring with them: Guardians of the Agents makes a great case for why agentic AI needs proof, not just guardrails, and his newest, In Code They Think; In Proof We Trust, shows how to prove an agent’s plan safe before a single tool executes. All of this makes perfect sense to me, even if the details feel frustratingly out of reach - I haven’t had the chance to work with formal methods since those papers at university twenty-three years ago.
Then earlier this year, I got to meet Erik in person. We were both speaking at IT Revolution’s Enterprise AI Summit in San Jose, and during one of the breaks I went and found him, laptop in hand. I wanted to show him my COMP473 assignments - proof, of sorts, that once upon a time I knew how to do this stuff, and that I just needed a way back in. His response was: “Why don’t we try something. Do you have Claude Code? Open it up.” So we did. We pointed it at one of the hand proofs from 2003 and watched it re-prove the whole thing with today’s tools - model checkers, solvers, the lot. Pages of careful hand-worked reasoning, mechanically verified in the space of a coffee break. I’ll never forget it - I was like a kid in a candy shop, vibe-verifying with Erik Meijer himself!
And I wasn’t the only one at that summit starting to think this was becoming viable, maybe even required.
The signals
There are more and more signs that formal verification might finally be earning its place in mainstream software development. Amazon recently announced that they’re investing in the Lean Focused Research Organization, and their reasoning is the clearest statement I’ve seen of why this matters more now than it ever has:
As AI agents increasingly make decisions that move money, approve claims, and operate critical infrastructure, the standard approach to software testing is no longer sufficient. Testing checks the cases you thought of, but there is a fundamentally different approach: mathematical proof, which shows with certainty that a system cannot behave incorrectly, no matter what inputs it gets.
Startups are forming around the idea. Midspiral describes itself as “the correctness layer for AI-generated software”, which is about as direct a statement of the thesis as you’ll find. Their open-source lemmafit puts a verifier - built on Dafny - right in the Claude Code loop, so the AI has to prove its code correct before anything compiles. I took it for a spin recently, and watching a solver prove a small theorem from a one-sentence prompt brought back that old feeling of certainty. Very cool, and well worth a play in your next Claude Code session.
Well-known voices in tech are turning their attention to it too. Martin Fowler’s notes from the second Thoughtworks Future of Software Development retreat recently described property-based testing and formal methods as the “computational sensors” of harness engineering. And just this week, Gergely Orosz had Hillel Wayne on The Pragmatic Engineer for a full episode on formal methods.
And away from the spotlight, I keep coming across individuals who are reorienting their careers toward this space, some going as far as leaving industry jobs for PhDs. The group is still small, but it is growing.
Why now
You can think of the software development lifecycle as a system. With AI, we’ve massively increased the inflow of generated code into the system, and it’s now piling up at the next step - code review. Review has become the new bottleneck, but not only because there’s far more to review. When engineers no longer write the code themselves, review is the first real opportunity they get to understand the system being built. So the pressure on that one phase is enormous: much more code, needing to be read much more carefully, both for errors and for understanding. Organisations and researchers alike are trying to work out what to do about it, and if we somehow manage to fix that bottleneck, testing will be the next one.
The constraints in the system are still there, they’ve just moved downstream.
One common response is to ask engineers to simply review more, and more carefully. But Deming told us long ago that you cannot inspect quality into a finished product, and Lisanne Bainbridge told us in 1983 why asking humans to sustain vigilance over an automated process is a losing game: we’re bad at monitoring, and the skills we aren’t practising atrophy while we watch. In any case, a tsunami of code review - and, worse, review of AI-generated slop - is not the job any software engineer signed up for. It’s not creative, it carries enormous responsibility, and we have forty years of human-factors research saying we can’t do it well.
Nor can the answer simply be more tests. Faros AI’s “Acceleration Whiplash” report found that the probability of a production incident per merged code change has more than tripled - and that’s with all the unit and integration tests we already write, plus the ones AI now writes for us. We seem to have hit a threshold where throwing more tests at the problem isn’t materially shifting the needle.
There’s an accountability squeeze in here too, and it’s the productivity-experience paradox all over again: organisations are pressing engineers to use AI to go faster, then holding them accountable for code they can’t possibly review at the level being expected of them. Responsibility without the means to discharge it - no wonder anxiety is rising. That’s the experience cost hiding underneath the speed.
Every response to this new bottleneck currently available is a trade-off against something else. Inspect harder, and you buy vigilance failure and skill atrophy. Slow the pipeline down to review properly, and you hand back the throughput gains. Wave it through, and you get the quality decline that’s already showing up in the data. There is no free option inside the current equation. The only way out is to change it - not the same steps faster, but a different kind of step.
Proof as a first-class citizen
I think that step is formal verification - correctness established by proof rather than by sampling - as a legitimate, first-class citizen of the software development lifecycle.
There are two ways I think formal verification can help make agents more trustworthy, and I’m interested in both.
Agentic engineering
The first is in agentic engineering: using agents to produce code as an artefact, which a human still reviews, ships and stands behind. The case here is one of quality assurance. As more code is generated by AI, proof is the only assurance mechanism that scales with the machines producing it. Instead of asking engineers to review more carefully, or piling yet more tests onto the problem, verification becomes a step in the build, a bit like static analysis but with proof behind it, and the closer that step is to where the code is generated, the better. That’s exactly where lemmafit sits.
The thing about proofs is that they are complete in a way that review and test suites can never be. As Edsger Dijkstra put it over fifty years ago, “program testing can be used to show the presence of bugs, but never to show their absence!”. A proof shows their absence, for every possible input at once.
But it’s not a silver bullet (because silver bullets don’t exist). People working in this space are quick to point out that while AI can help generate the proofs, coming up with the right specification is still hard, as it always was. Deciding what “correct” means assumes you understand the domain, the problem and the solution well enough to say so. That judgement - that we’re building the right thing - is basically validation by another name, and that has to stay human. I’d argue it’s one of the responsibilities we must keep, or we’ve really missed the point of building any of this at all.
Beyond the assurance itself, I’m just as interested in what proof could do for the eroding developer experience of the engineers supervising all that code generation. If proof carries the assurance, accountability becomes dischargeable again, resting on something sturdier than how carefully a tired human read the diff. That’s the side I may have something distinctive to say about, having spent the last three years studying what AI is doing to the lived experience of software engineers.
Agentic workflows
The second way reaches beyond the software development lifecycle altogether, into runtime. In agentic workflows, an LLM controls the flow of logic itself, generating code that gets executed on the fly by the harness it’s running in.
The problem there is more about security and governance: there’s real cyber risk in unsupervised, unverifiable agents taking actions in the world, and a serious governance question when nothing checks those actions at runtime. Periodic risk assessments and control checks were designed for organisations that change at human pace, and they don’t stand a chance against agents acting in milliseconds, thousands of times per hour. It’s exactly the angle Erik’s recent papers take aim at, and the reason I’ve become so interested in agentic control planes and governing agentic systems at scale. Machine-speed actors need machine-speed controls, and proof is the only one I can see keeping up.
Why it never caught on
Two things kept this work at the margins all these years, and neither was any doubt that it worked.
The first is the name. Put the word “formal” in front of anything and eyes glaze over. It sounds like quantum physics, people assume you must be an academic or a theorist, and they pretty much stop listening. It’s part of why the group of believers has stayed so small for so long.
There are people fixing that, though. At VUW, James Noble - one of my Honours supervisors - and his colleagues recently redeveloped their software correctness course around Dafny so that verification feels like a specially intense kind of programming rather than mathematics. Student retention went up, and the course earned its best evaluations in at least a decade. They make the case that formal methods are critical to the future of software engineering, and so must be an essential part of how we teach it. Either they were ahead of their time, or their timing was perfect - I must ask James which.
The second, and the real reason I never got to use any of this throughout my career, is pure economics. Everywhere I’ve worked - like most of the industry - the maths never stacked up. Testing and code review get you most of the way there for a fraction of the effort, classic 80/20, and chasing that last stretch of certainty the formal way would have cost more than it ever saved. That’s not a criticism, it was the right call. Formal verification stayed confined to the domains where failure is unthinkable: avionics, rail signalling, nuclear systems, verified kernels and compilers.
But the economics are what’s changing, and from two directions at once. The cost of not verifying is compounding, as agents pour out code at machine speed. And the cost of verifying is collapsing, because AI can now help write the proofs themselves. What remains tricky is getting the specs right, but AI is starting to help with that too. For the first time in my career, the maths might actually stack up.
From creation to verification, and back again
What we need is verification and governance that run at the same speed as the machines they’re checking, and I’m convinced proof can supply both. So my aim is to help make agentic work provable - what agents produce and what they do - in a form the industry can actually adopt.
In practice, that means building the machine that builds the machine - the harnesses we develop with, and the runtimes our agents operate in - with provable rigour baked right in, especially where the stakes are high. You could say this is just “shifting left”, and in a way it is. Verification stops being inspection after the fact and becomes part of the act of creation itself. Specifying what must hold, and proving it holds, become central to what it means to be a software engineer. And the spec stops being the kind of document that just drifts into fiction and becomes something the software can actually be held to.
None of that happens at scale while the rigour stays locked away with theorists and mathematicians though, so a big part of the work is making formal methods accessible to everyday working software engineers.
Get that right and the creation-to-verification shift my research found might start to reverse. Engineers get to create instead of inspect, keeping control of what they build, just in a different way to how we have in the past. And organisations may finally start to see the benefits they’ve been promised, because the use cases requiring more rigour become trustworthy enough to ship.
We keep saying that software engineering is being transformed, that we have to fundamentally reimagine it. So let’s actually do that!
An invitation
So that’s what I’m rekindling: a twenty-three-year-old love of proof, at a moment when the industry might finally need it. For what we ship, and for the people carrying the weight of it.
The first step I want to take is to scan in that whole box of old notes and assignments. I want to give it all to Claude Code and get it to help me re-learn what still holds, as a springboard into everything that’s changed since. I quite like the circularity of that - the technology making verification matter again is the same one helping me find my way back to it.
If you’ve read this far and haven’t been put off by the “f-word”, I’d love to hear from you. Whether you’re thinking about this too, building in this space, wrestling with these questions inside your own organisation, or just quietly curious like I was eighteen months ago, please reach out. Every time I’ve taken a punt and messaged someone in this space, I’ve been met with generosity - it’s that kind of community. So let’s talk, and maybe even build something awesome together.