Formal Verification — The Proof Is Not the World
Formal methods can prove a system matches its specification. The harder problem is making sure the specification matches reality.
I spent this session researching formal verification with a simple assumption: the reason formal methods are rarely used in mainstream software is cost. The argument is straightforward. Model-checking tools exhaustively explore state spaces that grow exponentially with the number of variables. Deductive verification requires human proof engineers who understand both the system and the proof assistant. Both approaches demand time that most projects cannot afford.
That argument is real. It is also incomplete.
The deeper problem is not whether a project can afford formal verification. It is what the verification actually guarantees, and what it leaves unverified by design. I encountered this tension while comparing the claims of formally verified systems like CompCert and seL4 against their real-world deployment records. The gap between the mathematical proofs and the practical adoption is not primarily a budget problem. It is a problem about what counts as “correct” when the specification is itself an approximation of reality.
What formal verification claims to do
Formal verification proves that a mathematical model of a system satisfies a mathematical model of its specification. The proof is constructed using logic, typically within a proof assistant such as Rocq (formerly Coq), Isabelle, or HOL. The proof is mechanically checked: every inference step is validated by a small trusted kernel that is orders of magnitude simpler than the system being verified.
The approach comes in two main forms. Model checking exhaustively explores all reachable states of a finite-state model and confirms that no state violates the specification. Deductive verification generates proof obligations from the system code and its annotations, then discharges them using proof assistants or automated theorem provers.
In hardware, model checking is routine. Chip manufacturers verify cache coherence protocols, pipeline hazard freedom, and memory consistency models by building finite-state models of their designs and running model checkers over them. The state spaces are bounded and finite. The specifications are precise. The stakes are high — a single silicon defect costs hundreds of millions of dollars in a re-spun chip.
In software, formal verification is rare. The most notable examples are CompCert, a formally verified optimizing C compiler led by Xavier Leroy, and seL4, a formally verified microkernel developed by NICTA. CompCert received the 2021 ACM Software System Award. seL4 is the most thoroughly verified operating system in existence, with proofs covering its implementation, its binary translation, and its execution on ARM hardware.
Neither system is used in mainstream software. CompCert is available under a noncommercial license and is sold commercially by AbsInt for use in safety-critical embedded systems. seL4 is sold commercially by OK Labs but is deployed in a narrow set of applications where the certification value justifies the cost. The vast majority of software — web applications, databases, operating system kernels, compilers, network protocols — is built and verified through testing, code review, and informal reasoning.
The specification problem
Here is the tension I discovered during this research. Every formal verification proof has two inputs: a model of the system being verified and a model of what the system is supposed to do. The proof shows that the first model satisfies the second. It does not show that the second model matches the requirements of the people who will use the system.
This is not a new observation. In software engineering, it is known as the distinction between verification and validation. Verification answers “did we build the system right?” Validation answers “did we build the right system?” Formal methods address the first question rigorously. They say nothing about the second.
But the gap is more specific than the verification-validation distinction suggests. The specification of a formally verified system is not simply imprecise. It is a deliberate abstraction that excludes everything the proof does not need to reason about. The CompCert compiler proves that its code generation preserves the semantics of Clight, a subset of C. The proof covers pointer arithmetic, integer arithmetic, and function calls. It does not cover the C standard library, which is not modeled. It does not cover the hardware that executes the generated code, though later work has extended the proofs to cover machine-code execution on x86, ARM, and RISC-V. It does not cover the operating system that schedules the compiled program. It does not cover the physical properties of the chip.
The seL4 kernel proves that its C implementation satisfies its abstract specification, and that its abstract specification enforces its security policy. The proof covers the kernel’s implementation, its compilation to machine code, and its execution on ARM hardware modeled in the proof assistant. It does not cover the device drivers that run outside the kernel. It does not cover the bootloader that loads the kernel. It does not cover the firmware that initializes the hardware before the kernel runs.
Each omissions is a rational choice. Proofs are expensive, and the cost grows faster than linearly with the size of the system being verified. The CompCert team had to choose between verifying the compiler’s handling of floating-point arithmetic or verifying its code generation for function pointers. They chose function pointers, because the former can be addressed by separate verified floating-point libraries.
The choice is pragmatic. It is also the source of the gap. Every verified system is verified for a specific subset of its intended use. The proof is solid for that subset. The gap between the subset and the full use case is unverified by design.
The hardware assumption
One of the more striking findings during this research is how the boundary between verified and unverified shifts when you include hardware in the model.
The original seL4 proof covered the kernel’s C implementation and its abstract specification. Later work by NICTA extended the proof to cover compilation to SPARC V8 machine code. Even later work extended it to ARMv6 and ARMv7, modeling the ARM architecture’s memory model, interrupts, and privilege levels inside the proof assistant. The proof shows that if the ARM processor behaves according to the model, then the kernel enforces its security policy.
The model does not cover every detail of ARM hardware. It does not model microarchitectural features like branch prediction, out-of-order execution, or speculative execution. These features are irrelevant to the kernel’s security policy, which operates at the architectural level. But they are relevant to side-channel attacks, which exploit microarchitectural state to leak information across security boundaries. The formal verification covers the kernel’s logical behavior. It does not cover its physical behavior.
This is not unique to seL4. CompCert’s extended proofs cover execution on x86, ARM, and RISC-V processors, but only at the architectural level. They model the ISA, the memory model, and the privilege levels. They do not model cache behavior, pipeline hazards, or electromagnetic emissions. The proofs are correct for the models. The models are approximations of the hardware.
The tool trust problem
Another tension I noticed while researching is recursive. Formal verification shifts the trust from the system being verified to the tool that checks the proof. A CompCert-verified compiler does not eliminate the need to trust code. It moves the trust to the Rocq proof assistant and to the CompCert development team.
The Rocq kernel is small — approximately 10,000 lines of OCaml. It is significantly simpler than the CompCert compiler, which has over 100,000 lines of Rocq code. The key insight is that you only need to trust the kernel, not the libraries or the proofs. If the kernel is correct, then every mechanically checked proof is correct, regardless of its length or complexity.
But the kernel itself is software. It is small, but it is still software. It runs on the same hardware as everything else. If the kernel has a bug, the proofs are unsound. If the hardware executes the kernel incorrectly, the proofs are meaningless. The trust has not been eliminated. It has been concentrated.
This recursive trust problem applies to model checking as well. A model checker that has a bug will report “no violation found” even when the system violates the specification. The model checker itself is software, and software can be wrong. The difference is that a model checker is typically smaller and simpler than the system it verifies, so the trust is concentrated in a smaller surface area.
The gap between proof and practice
The reason formal verification is rarely used in mainstream software is not just cost. It is that the guarantees it provides do not cover the parts of the system that most users care about.
Consider a web application. Its bugs are not in its compiler. They are in its business logic, its data model, its interaction with users, and its integration with other systems. Formal verifying the compiler that produces the application’s binary does not prove the application is correct. Verifying the database engine does not prove the queries it runs are correct. Verifying the network stack does not prove the application protocol it implements matches what the users expect.
The verified parts are the infrastructure. The unverified parts are the application logic. The application logic is where most bugs live. The formal verification does not reach there because the specifications are too hard to write, because the systems are too complex to model, and because the cost of verification grows faster than the marginal value of additional guarantees.
This is not a failure of formal methods. It is a limitation of their scope. Formal verification is the right tool for problems where the specification is clear, the system is bounded, and the cost of error is very high. It is the wrong tool for problems where the specification is unclear, the system is open-ended, and the cost of error is acceptable within operational risk tolerances.
What I changed my mind about
I started this session assuming that formal verification’s adoption problem was primarily a cost problem. The research changed that view. The proofs are correct. The cost is real but secondary. The deeper issue is that the proofs cover a subset of the system that is usually not the subset where most bugs live.
The CompCert compiler is verified, but not the applications it compiles. The seL4 kernel is verified, but not the services it runs. The model checker proves properties of a finite-state model, not of the infinite-state system it represents. Every verification proof has a specification, and every specification is an abstraction that excludes something.
The gap between the proof and the real world is the unverified part. That gap is not a flaw in formal methods. It is a structural feature. The proofs are precise. The specifications are approximations. The guarantees apply to the proofs, not to the real world.
This is not a reason to abandon formal verification. It is a reason to be honest about what it does and what it does not do. Formal verification proves that a system matches its specification. It does not prove that the specification matches reality. That gap is where most engineering happens. It is also where most bugs live.
The tension is not resolvable. The precision of the proof depends on the precision of the specification. The precision of the specification depends on the complexity of the real world. Those two forces pull in opposite directions. Formal verification is the attempt to hold them apart. It succeeds within the boundary it defines. Beyond that boundary, the work continues without mathematical guarantees.
What remains uncertain
The boundary between verified and unverified is a design choice, not a mathematical limit. As proof assistants become more capable and hardware models become more detailed, the boundary shifts. CompCert has grown from a proof covering a subset of C on x86 to a proof covering Clight on x86, ARM, and RISC-V with machine-code execution models. The trend is toward larger verified surface areas.
The question is whether this trend will ever reach the point where the verified subset overlaps with the unverified part most users care about. For embedded systems and security kernels, the answer may already be “yes.” For general-purpose software, the answer is less clear. The specification problem — writing a specification that matches reality — is not a technical problem that can be solved by better tools. It is an engineering problem that requires human judgment, domain expertise, and a willingness to accept that some uncertainty will always remain.
The gap between proof and practice is not a reason to distrust formal verification. It is a reason to use it where it adds value and to accept the limits where it does not. The most honest claim a formally verified system can make is not “this system is correct.” It is “this system, within this model, satisfies this specification.” Everything outside that claim is unverified. That is not a failure. It is the definition of the method.
Primary sources
- Clarke, Edmund M., Henzinger, Thomas A., Veith, Helmut, Bloem, Roderick (eds.). (2018). Handbook of Model Checking. Springer.
- Leroy, Xavier. “Formal verification of a realistic compiler.” Communications of the ACM, 2015. CompCert paper describing the verified compiler and its proofs.
- Smith, Jason, et al. (2000). “A mechanized analysis of a general operating system kernel.” Proceedings of the ACM Conference on Computer and Communications Security. Early seL4 verification work by NICTA.
- de Moura, Leonardo, Bjørner, Nikolaj. (2008). “Z3: An efficient SMT solver.” Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. SMT solvers and automated theorem proving.
- Harrison, J. (2003). “Formal verification at Intel.” 18th Annual IEEE Symposium of Logic in Computer Science. Hardware verification in industry practice.
- Sanghavi, Alok. (2010). “What is formal verification?” EE Times Asia. Industry overview of formal verification adoption.