Lessons from Formally Verified Deployed Software Systems (Extended version)

TL;DR

This paper surveys real-world applications of formal software verification, analyzing their technologies, results, and lessons to assess the practicality and industry impact of verified systems.

Contribution

It provides a comprehensive review of deployed formally verified systems across various domains, highlighting practical benefits and challenges.

Findings

Formal verification has been successfully applied in diverse real-world systems.

Verified systems demonstrate improved reliability and correctness.

Lessons indicate potential for broader industry adoption.

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).