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 can be drawn for the software industry at large and its ability to benefit from formal verification techniques and tools. Note: a short version of this paper is also available, covering in detail only a subset of the considered systems. The present version is intended for full reference.

翻译：形式化软件验证技术已取得显著进展，但它对实际软件开发究竟有多大助益？关于构建具有机械校验正确性证明的系统的实用性，学界仍存在较大分歧。这种前景是仅限于少数昂贵、关键任务型项目，还是能够应用于软件产业的广泛领域？为解答这一问题，本综述审视了多个应用领域内已构建形式化验证系统并投入实际使用的项目。它考察了所采用的技术、验证形式、取得的成果，以及可为整个软件行业从中汲取的经验教训，特别是如何利用形式化验证技术与工具。注：本文另有精简版，仅详细涵盖部分受检系统。当前版本旨在提供完整参考。