Last night, Nada and I had the privilege of speaking to a brilliant San Francisco crowd about Midspiral’s approach to building verified software from the ground up.
There isn’t really a blueprint for this technology. Integrating formal verification into engineering AI workflows is a gigantic open question mark in terms of how. There are so many angles we could take to harden codebases and the foundation of what AI works with.
But one thing is crystal clear to us — and to that room of people: now that AI has taken care of speed, volume, and the expertise gap, we can and should focus on correctness.
Living Ten Years in the Future
In my head, I live ten years in the future. And in that future, bug-chasing is down by 90% because software is written correctly the first time.
That future doesn’t arrive on its own. For most of software’s history, correctness has been a tax — something you pay for with slow, expensive, expert labor that most teams simply can’t afford at scale. So we tested a little, shipped, and chased the rest in production. AI has quietly removed the three constraints that made that tradeoff feel inevitable: it’s fast, it’s tireless, and it closes the expertise gap. What’s left is the part we kept deferring — proving the code actually does what we meant.
That’s the shift we walked the room through. The point isn’t to ask an LLM to write code and certify it’s correct — that’s asking the same non-deterministic system to be both author and judge. The point is to put a deterministic verifier in the loop: the AI proposes implementation candidates, and an external checker decides whether they hold. The model gets to be creative; the proof gets to be the authority. When those roles are separated, “it compiles” and “it’s correct” stop being the same sentence.
The questions afterward made it obvious how ready people are for this. The room pushed on the hard parts — where verification stops and testing has to take over, how you write specs precise enough to be worth proving against, what happens to all the existing code that was never built this way. Those aren’t skeptical questions. They’re the questions you ask when you’ve already accepted the premise and started thinking about the work.
The Wave Is Growing
We had a blast talking about our approach to software correctness at the Antithesis HQ in SF. The crowd was brilliant and the conversations that flowed afterwards were energizing.
Thank you to everyone who came, asked questions, and challenged us. The wave of software correctness is growing larger and approaching faster than most realize — we’re lucky to meet people along the way who understand this well and are down for the ride.
If the ideas from the talk resonated, the work behind them is open and out in the world. For this workshop we focused on LemmaScript. Other tools we’ve released include lemmafit, an npm package that adds a verifier-in-the-loop workflow into a single dev tool you can install today. claimcheck helps make sure verified code actually matches intent, and Dafny-replay is the broader methodology underneath it all. Our previous posts go deeper on each.
Thank You
Thank you so much to Akshay Shah and Antithesis for providing the space, the logistics, and delicious snacks — and to everyone who came and made us feel like we’re on the right track.
Until next time, San Francisco!