Formalish Verification: How software changes
LLMs write code faster and better than me now, but I still can't fully trust what they build. Part 1 of me digging into how we exhaustively verify what our apps actually do.
It started with LLMs generating code faster than humanly possible. It was shitty code, but damn, LLMs could churn out a lot of it. Now “faster than human” is really just a property of computers in general - not LLMs - but it was still an exciting new party trick since it was the first time computers were spitting out semi-reasonable, non-deterministic code.
Next LLMs became better than the average human developer. This is where we’re at currently in 2026, and it’s a pretty jarring reality for me, an average human developer. I find myself constantly oscillating between feeling deliriously empowered and overwhelmed with existential dread. I think a lot of people assumed that once LLMs could generate code faster and better than humans, the jig would be up and we’d all be replaced… but most of us are still here collecting a paycheck every other week.
So what’s holding back the paradigm shift? It all boils down to one thing - trust. More specifically, “how can I trust that this code does exactly and only what I want it to do.” This is not a new problem, in fact it is arguably the oldest problem that every new level of software abstraction has to answer. People love to describe LLM-first development as “just a new higher level of abstraction”… but it actually isn’t… at least not yet. There are two parts to every new level of abstraction: (1) it makes it faster and easier to build stuff, and (2) it gets rid of some of the footguns. JavaScript is faster to build with than C, but think of how terrifying your average React app would be if we got all the speed ups of dynamic typing and a large standard library of convenience methods, but didn’t get automatic memory allocation or garbage collection. It wouldn’t matter that we could ship things faster if we were crashing people’s computers left and right. It’s true that LLMs have made code generation wildly easier, faster, and more accessible… but so far it isn’t fundamentally safer than when humans were coding by hand. At this point we aren’t at a higher level of abstraction or a new paradigm… we’re at that awkward transition phase where software being buggy and flaky is the norm and it’s no longer news when a company discovers that their LLM dropped their prod database or caused an embarrassing security incident.
You might be surprised that in the human coding era, trust did not fundamentally come from test coverage, but from the fact that we were shipping human sized features at human speed. If you’re only shipping a couple features a week, and you and a colleague check the code and think it’s reasonable, and any user reported bugs or edge cases that come up in the days after launch get addressed (ideally with a few test cases added to codify the desired behavior), then you can have reasonably high trust that things are good to go. Now imagine you are trying to ship a couple hundred features a week - you’re going to quickly run into a choice: either limit your throughput to how much you can review and vet (which will give you a nice albeit incremental output boost), or lower the review bar and implicitly turn your users into your QA team. Both of these options are bad.
This is how software changes: humans stop writing code, they specify their intent and desires and an LLM generates a solution (this is already happening). This is how software changes: humans stop reviewing code, they verify that the exhaustive list of actual behavior aligns with their intent and desires (this needs to happen).
We can only fully delegate implementation to LLMs if we can completely trust that the code being generated does exactly and only what we want it to do. This is not possible if we abdicate review to other LLMs since that is just kicking the can down the line and shifting the trust problem to this review LLM. It’s also not possible if humans continue to be responsible for reviewing the code since there is just way too much of it. It only works if we come up with a new pattern that exhaustively verifies all actual behavior happening in our apps. I think this need for fully verified & trustable code aligns with Kleppmann’s Prediction: AI will make formal verification go mainstream, I just think FE apps are going to end up with something like normalizing chaos engineering practices instead of trying to figure out how to come up with a formal proof for if my button is the right color. As far as I can tell, this isn’t a solved problem, but there seems to be a dozen or so overlapping bits from prior art that might help us find a solution. I’ll be digging into this and documenting my findings. If you’re also interested in this space or have any leads you think would be useful, please shoot me an email at will@lotherington.me