Formal verification is not ready for the revolution. Can we catch up?

AI is pushing software into an industrial age, but formal verification infrastructure is still operating like a guild craft.

For decades, formal verification thrived in university basements and research labs. We wrote arcane Rocq tactics, built bespoke proofs, and spoke in theorem provers few outsiders could understand. Verified systems are still rare, expensive, and mostly isolated from one another. Projects like DeepSpec recognized the problem early: formal verification produced islands of trust, not a connected trust infrastructure.

The guild era must end. AI makes proof abundant; formal methods must make trust abundant. For that, we now have to build the infrastructure that makes trust composable: across provers, languages, compilers, hardware, and legacy systems. We do not need more isolated proofs. We need a connected trust stack for the AI age.

The formal tower of Babel 

I should be clear: The guild era was also a heroic era.

Formal verification has achieved incredible feats. CompCert proved realistic optimizing compilers could be machine verified. seL4 showed kernels could carry end-to-end proofs. VST connected C verification to compiler semantics. HACL* demonstrated that high-performance cryptographic libraries could be both verified and practical.

The problem is not failure. The problem is Formal Babel: a world where proof frameworks fail to communicate.

Proofs compose inside carefully engineered ecosystems, but rarely across them. Even though VST builds on CompCert semantics, the field still contains dozens of incompatible formalizations of C semantics, memory models, concurrency semantics, and intermediate representations. Every prover and framework develops its own abstractions, proof idioms, and trusted infrastructure.

This became a running joke in the field: “The Next 700 Semantics,” “The Next 700 Separation Logics,” and eventually, “The Next 700 Proof Ecosystems.”

Moreover, real software lives at the intersection of languages, compilers, operating systems, and hardware, where many behaviors are difficult to model formally. Existing verification frameworks each capture part of this reality, but none captures all of it. To reason about production systems, we need guarantees that span the entire stack.

Taming formal Babel

‍The answer to Formal Babel is a universal framework that connects across languages, analysis types, abstraction levels, through compilation and (why not?) down to hardware. 

The goals are interoperability and cooperation.

The future formal methods stack must make trust portable. Guarantees should survive translation across provers, compilers, operating systems, networks, and hardware targets. Formal verification cannot remain a collection of isolated proofs and bespoke pipelines. It must become infrastructure: invisible, composable, and ambient across the entire computing stack.

Allow yourself to dream: verified transpilers everywhere. Compilers shipping with proofs of correctness by default. Operating systems whose guarantees survive optimization and hardware translation. Automatically verified patching. AI agents rewriting infrastructure while preserving formal invariants across the stack.

 A connected fabric of trust.

The Path Forward

This vision is ambitious, but it is not science fiction. The pieces already exist. Our task now is to complete them, scale them to the full complexity of production software, and connect them into a coherent trust infrastructure.

First, it's time to finish the foundations of formal semantics. Every major language should have a single, extensible semantic foundation that supports the full complexity of production software, including the long tail of behaviors that real systems depend on. Let's be ambitious: those semantics should extend across the entire stack, from source code, through intermediate representations, to operating systems and hardware. There are both theoretical and engineering challenges ahead, but AI gives us an unprecedented opportunity to tackle them at a pace that was previously impossible.

Second, it's time to finish verified translation. Every compiler should carrying machine-checked guarantees and match the performance of today's production toolchains. Verified transpilers should make it possible to migrate legacy infrastructure across languages, preserve behavior, and bridge abstraction layers with confidence. Projects like TRACTOR already show that AI can make large-scale software translation practical. Now we must make it verifiable, preserving semantics across even vastly different programming languages.

Third, it's time to finish the foundations of formal verification. Verification frameworks, logics, and semantic foundations should share common foundations, allowing proofs to compose across languages, tools, and abstraction layers. Efforts such as CSLib point in this direction, but we should accelerate them dramatically. The next wave of progress should come less from building new proof ecosystems than from converging on shared foundations, porting and unifying mature tools instead of continually reinventing them.

None of these challenges is beyond our reach. We already know how to formalize languages, verify compilers, prove operating systems, and reason about hardware. The work ahead is to finish those foundations, extend them to the realities of production software, and connect them into a common trust infrastructure. The age of abundant proof has begun. Now we must build the infrastructure that turns it into trust.