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

翻译：形式化软件验证技术已取得显著进展，但其对实际软件开发的实际效益究竟如何？关于构建具有机械验证正确性证明的系统是否具有实用性，目前仍存在较大分歧。这种前景是否仅限于少数高成本、生命攸关的项目，还是可以广泛应用于软件行业的各个领域？为帮助解答这一问题，本综述考察了在不同应用领域中已产生形式化验证系统并实际部署使用的多个项目。研究涵盖了所采用的技术、应用的验证形式、获得的结果，以及软件行业在利用形式化验证技术与工具方面应汲取的经验教训。注：本版本为扩展文章，涵盖所有被认定为相关的系统。另有仅包含部分案例的简短版本可供参考（详见 https://doi.org/10.1145/3785652）。