Lessons from Formally Verified Deployed Software Systems (Extended version)

TL;DR

The paper assesses the practicality of formal verification by surveying deployed, formally verified software across domains, languages, and verification techniques. It synthesizes a wide set of case studies to extract patterns about verification approaches, tooling, and project contexts, highlighting how verification was achieved, what was proven, and how unverified components were managed. The findings show that formally verified systems are deployed in industry beyond safety-critical domains, with notable successes in compilers, microkernels, cryptographic libraries, and OS kernels, though adoption remains constrained by the need for specialized expertise and integration costs. The study concludes that formal verification can yield meaningful benefits, including defect discovery and certification gains, and argues for strategic adoption, reuse, and incremental verification to broaden industry impact. It also emphasizes the importance of tooling maturity, verification reuse, and early-stage specification work to improve practical viability and maintainability of verified systems.

Abstract

The technology of formal software verification has made spectacular advances, but how much does it actually benefit the development of practical software? Considerable disagreement remains about the practicality of building systems with mechanically-checked proofs of correctness. Is this prospect confined to a few expensive, life-critical projects, or can the idea be applied to a wide segment of the software industry? To help answer this question, the present survey examines a range of projects, in various application areas, that have produced formally verified systems and deployed them for actual use. It considers the technologies used, the form of verification applied, the results obtained, and the lessons that the software industry should draw regarding its ability to benefit from formal verification techniques and tools. Note: this version is the extended article, covering all the systems identified as relevant. A shorter version, covering only a selection, is also available (see https://doi.org/10.1145/3785652).

Figures (9)

• Figure 1: Verification tool stack of EiffelBase 2
• Figure 2: The specification style of HACL*.
• Figure 3: HOL specification for scheduler
• Figure 4: The calculus of abstraction layers. The ticket acquire/release example.
• Figure 5: Property 5 in code contracts.