Formal Verification: The 40-Year Overnight Success

From chipmakers and cloud infrastructure to mathematical proofs, AI agents, and human intent.

*Disclaimer this is a short mostly auto-generated post from one of my social media talks.

Formal verification is suddenly fashionable. Apparently, the world has discovered that testing something and proving something about it are two different things.

Only took forty years.

It didn't start with AI

Chip designers were using formal methods decades before anyone was talking about vibe coding. The 1986 breakthrough in binary decision diagrams helped bring formal verification into practical hardware design. Then Intel's infamous 1994 Pentium FDIV bug came with an estimated $475 million price tag. That was the cost of a mistake, not verification spending. An expensive distinction.

The story kept moving. Microsoft's SLAM checked properties of Windows drivers. In 2009, seL4 became the first operating-system kernel with a machine-checked, code-level functional-correctness proof. AWS has used TLA+ since 2011 to reason about cloud infrastructure. Facebook acquired Monoidics in 2013 and put separation logic to work finding bugs with Infer. In 2014, Cadence agreed to pay about $170 million for Jasper.

Not exactly a fringe hobby. Just not much of a dinner-party topic.

The money has entered the chat

Harmonic raised $295 million and has now taken Aristotle from mathematics into C software and Verilog hardware. &Truth emerged with $70 million in seed funding to pursue large-scale software verification. Pramaana raised $27 million to apply formal methods to high-stakes AI.

That's funding for companies working in and around verification, not a measure of annual formal-verification spending. The broader trend is harder to count. The expanding range of systems worth checking is harder to miss.

Next up: intelligence itself

Verified code is one flavor. Others include hardware specifications, cloud designs, AI guardrails, agent actions, and checking claims against trustworthy facts. They don't all call for the same kind of proof.

If AI is going to dominate future “useful output generation,” I suspect individuals will be most interested in having their intent autoformalized, so swarms of agents can produce useful work at scale and offer independently checkable evidence that they stayed within scope.

But here's the catch. Formal verification can prove a system satisfies its specification. It cannot, by itself, prove that the specification faithfully captured what a person meant.

A perfectly verified proof of something you never meant is still pretty useless.