{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T18:54:49Z","timestamp":1780340089323,"version":"3.54.1"},"reference-count":102,"publisher":"Association for Computing Machinery (ACM)","issue":"8","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2026,6,30]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3785652","type":"journal-article","created":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T20:52:33Z","timestamp":1768596753000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Lessons from Formally Verified Deployed Software Systems"],"prefix":"10.1145","volume":"58","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3531-4045","authenticated-orcid":false,"given":"Li","family":"Huang","sequence":"first","affiliation":[{"name":"Constructor University Bremen","place":["Bremen, Germany"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0957-2844","authenticated-orcid":false,"given":"Sophie","family":"Ebersold","sequence":"additional","affiliation":[{"name":"IRIT CNRS, University of Toulouse","place":["Toulouse, France"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4873-8306","authenticated-orcid":false,"given":"Alexander","family":"Kogtenkov","sequence":"additional","affiliation":[{"name":"Formerly of Constructor Institute of Technology","place":["Schaffhausen, Switzerland"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5985-7434","authenticated-orcid":false,"given":"Bertrand","family":"Meyer","sequence":"additional","affiliation":[{"name":"ETH Zurich","place":["Zurich, Switzerland"]},{"name":"Eiffel Software","place":["Santa Barbara, USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9711-2118","authenticated-orcid":false,"given":"Yinling","family":"Liu","sequence":"additional","affiliation":[{"name":"CRAN, Universit\u00e9 de Lorraine","place":["Nancy, France"]}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,2,11]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/551350"},{"key":"e_1_3_2_3_2","unstructured":"Jean-Raymond Abrial. 2007. Formal methods: Theory becoming practice. Journal of Universal Computer Science 13 5 (2007) 619\u2013628."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3236950.3236962"},{"key":"e_1_3_2_5_2","first-page":"1555","volume-title":"Proceedings of the International Conference on Management of Data","author":"Auerbach Joshua S.","year":"2017","unstructured":"Joshua S. Auerbach, Martin Hirzel, Louis Mandel, Avraham Shinnar, and J\u00e9r\u00f4me Sim\u00e9on. 2017. Handling environments in a nested relat. algebra with combinators and an impl. in a verified query compiler. In Proceedings of the International Conference on Management of Data. ACM, 1555\u20131569."},{"key":"e_1_3_2_6_2","unstructured":"Civil Aviation Authority. 2001. SW01\u2014regulatory objectives for software safety assurance in ATS equipment in part B (generic requirements and guidance) of CAP670\u2014air traffic services safety requirements. (2001)."},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/11415787_20"},{"key":"e_1_3_2_8_2","doi-asserted-by":"crossref","unstructured":"Ezio Bartocci Yli\u00e8s Falcone Adrian Francalanza and Giles Reger. 2018. Introduction to runtime verification. Lectures on Runtime Verification: Introductory and Advanced Topics (2018) 1\u201333.","DOI":"10.1007\/978-3-319-75632-5_1"},{"key":"e_1_3_2_9_2","doi-asserted-by":"crossref","unstructured":"Thomas Bauerei\u00df Armando Pesenti Gritti Andrei Popescu and Franco Raimondi. 2018. CoSMed: A confidentiality-verified social media platform. Journal of Automated Reasoning 61 1 (2018) 113\u2013139.","DOI":"10.1007\/s10817-017-9443-3"},{"key":"e_1_3_2_10_2","doi-asserted-by":"crossref","unstructured":"Christoph Baumann Bernhard Beckert Holger Blasum and Thorsten Bormer. 2012. Lessons learned from microkernel verification\u2013specification is the new bottleneck. arXiv:1211.6186. Retrieved from https:\/\/arxiv.org\/abs\/1211.6186","DOI":"10.4204\/EPTCS.102.4"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603019"},{"key":"e_1_3_2_12_2","volume-title":"Proceedings of the Summit on Advances in Programming Languages","year":"2017","unstructured":"Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pan, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-B\u00e9guelin, Jean-Karim Zinzindohou\u00e9. 2017. Everest: Towards a verified, drop-in replacement of HTTPS. In Proceedings of the Summit on Advances in Programming Languages."},{"key":"e_1_3_2_13_2","doi-asserted-by":"crossref","unstructured":"Karthikeyan Bhargavan C\u00e9dric Fournet and Markulf Kohlweiss. 2016. miTLS: Verifying protocol implementations against real-world attacks. IEEE Security Privacy 14 6 (2016) 18\u201325.","DOI":"10.1109\/MSP.2016.123"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2011.38"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_2"},{"key":"e_1_3_2_16_2","first-page":"2","volume-title":"Proceedings of the Safety-Critical Systems Symposium","author":"Chapman Roderick","year":"2016","unstructured":"Roderick Chapman and N. White. 2016. Industrial experience with agile in high-integrity software development. In Proceedings of the Safety-Critical Systems Symposium. 2\u20134."},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_26"},{"key":"e_1_3_2_18_2","unstructured":"Common Vulnerabilities and Exposures 2025. Common Vulnerabilities and Exposures. (2025). Retrieved January 23 2026 from https:\/\/www.cve.org\/"},{"key":"e_1_3_2_19_2","unstructured":"List of companies using formal verification methods in soft. eng.2021. Retrieved January 23 2026 from https:\/\/github.com\/ligurio\/practical-fm"},{"key":"e_1_3_2_20_2","unstructured":"CompCert 2021. CompCert Webpage. (2021). Retrieved January 23 2026 from https:\/\/compcert.org\/"},{"key":"e_1_3_2_21_2","doi-asserted-by":"crossref","unstructured":"David Costanzo Zhong Shao and Ronghui Gu. 2016. End-to-end verification of information-flow security for C and assembly programs. SIGPLAN Notices 51 6 (2016) 648\u2013664.","DOI":"10.1145\/2980983.2908100"},{"key":"e_1_3_2_22_2","first-page":"344","volume-title":"Proceedings of the International Eurospace-Ada-Europe Symposium","author":"Croxford Martin","year":"1995","unstructured":"Martin Croxford and James Sutton. 1995. Breaking through the V and V bottleneck. In Proceedings of the International Eurospace-Ada-Europe Symposium. Springer, 344\u2013354."},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_24_2","volume-title":"Secure By Design","author":"Deogun D.","year":"2019","unstructured":"D. Deogun, D. B. Johnsson, and D. Sawano. 2019. Secure By Design. Manning. 2019286713"},{"key":"e_1_3_2_25_2","unstructured":"Yli\u00e8s Falcone Klaus Havelund and Giles Reger. 2013. A tutorial on runtime verification. Engineering Dependable Software Systems (2013) 141\u2013175."},{"key":"e_1_3_2_26_2","doi-asserted-by":"crossref","unstructured":"Kathleen Fisher John Launchbury and Raymond Richards. 2017. The HACMS program: using formal methods to eliminate exploitable bugs. Philosophical Transactions of the Royal Society A: Mathematical Physical and Engineering Sciences 375 2104 (2017).","DOI":"10.1098\/rsta.2015.0401"},{"key":"e_1_3_2_27_2","unstructured":"Flover 2021. FloVer: A certificate checker for roundoff error bounds. (2021). Retrieved January 23 2026 from https:\/\/gitlab.mpi-sws.org\/AVA\/FloVer"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3064176.3064183"},{"key":"e_1_3_2_30_2","volume-title":"The seL4 Microkernel\u2014An Introduction","author":"Heiser Gernot","year":"2020","unstructured":"Gernot Heiser. 2020. The seL4 Microkernel\u2014An Introduction. Technical Report. The seL4 Foundation."},{"key":"e_1_3_2_31_2","doi-asserted-by":"crossref","unstructured":"Ronghui Gu J\u00e9r\u00e9mie Koenig Tahina Ramananandro Zhong Shao Xiongnan Wu Shu-Chun Weng Haozhong Zhang and Yu Guo. 2015. Deep specifications and certified abstraction layers. ACM SIGPLAN Notices 50 1 (2015) 595\u2013608.","DOI":"10.1145\/2775051.2676975"},{"key":"e_1_3_2_32_2","first-page":"653","volume-title":"Proceedings of the USENIX Symp. on OS Design and Implementation","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Newman Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertikOS: An extensible architecture for building certified concurrent OS kernels. In Proceedings of the USENIX Symp. on OS Design and Implementation. 653\u2013669."},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_22"},{"key":"e_1_3_2_34_2","unstructured":"hacl 2021. HACL*: A High-Assurance Cryptographic Library. (2021). Retrieved January 23 2026 from https:\/\/github.com\/project-everest\/hacl-star"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-51624-4.50004-6"},{"key":"e_1_3_2_36_2","doi-asserted-by":"crossref","unstructured":"Yann Herklotz James D. Pollard Nadesh Ramanathan and John Wickerson. 2021. Formal verification of high-level synthesis. ACM on Programming Languages 5 (2021) 1\u201330.","DOI":"10.1145\/3485494"},{"key":"e_1_3_2_37_2","first-page":"211","volume-title":"An introduction to the Event-B modelling method","author":"Hoang Thai Son","year":"2013","unstructured":"Thai Son Hoang. 2013. An introduction to the Event-B modelling method. In Industrial Deployment of System Engineering Methods, Alexander Romanovsky and Martyn Thomas (Eds.). Springer Berlin, Heidelberg. 211\u2013236."},{"key":"e_1_3_2_38_2","unstructured":"HOL 2021. HOL Interactive Theorem Prover. (2021). Retrieved January 23 2026 from https:\/\/hol-theorem-prover.org\/"},{"key":"e_1_3_2_39_2","unstructured":"Li Huang Sophie Ebersold Alexander Kogtenkov Bertrand Meyer and Yinglin Liu. 2023 updated 19 January 2026. Lessons from formally verified deployed software systems (extended version of present paper). arXiv:2301.02206. Retrieved from https:\/\/arxiv.org\/abs\/2301.02206"},{"key":"e_1_3_2_40_2","doi-asserted-by":"crossref","unstructured":"Li Huang Sophie Ebersold Alexander Kogtenkov Bertrand Meyer and Yinglin Liu. 2026. Formally Verified Deployed Software Systems: A living review. Retrieved from https:\/\/deployed-verified.org\/","DOI":"10.1145\/3785652"},{"key":"e_1_3_2_41_2","unstructured":"Li Huang Sophie Ebersold Alexander Kogtenkov Alexandr Naumchev Bertrand Meyer and Yinglin Liu. 2021. Questionnaire: Formally Verified Systems. (2021). Retrieved January 23 2026 from https:\/\/docs.google.com\/forms\/d\/e\/1FAIpQLScesACXl8oegnNNHLLPNdBoP9Wj2mK2Fywk-FUoXs2C3jed_Q\/viewform"},{"key":"e_1_3_2_42_2","unstructured":"Isabelle 2021. Isabelle. (2021). Retrieved from https:\/\/isabelle.in.tum.de\/"},{"key":"e_1_3_2_43_2","volume-title":"Language-based Security for Web Browsers","author":"Jang Dongseok","year":"2014","unstructured":"Dongseok Jang. 2014. Language-based Security for Web Browsers. University of California, San Diego."},{"key":"e_1_3_2_44_2","first-page":"113","volume-title":"Proceedings of the USENIX Security Symposium","author":"Jang Dongseok","year":"2012","unstructured":"Dongseok Jang, Zachary Tatlock, and Sorin Lerner. 2012. Establishing browser security guarantees through formal shim verification. In Proceedings of the USENIX Security Symposium. 113\u2013128."},{"key":"e_1_3_2_45_2","unstructured":"Leslie A. Johnson. 1998. DO-178B: Software considerations in airborne systems and equipment certification. Crosstalk October 199 (1998) 11\u201320."},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_11"},{"key":"e_1_3_2_47_2","first-page":"1","volume-title":"Proceedings of the European Congress Embedded Real-Time Software and Systems","author":"K\u00e4stner Daniel","year":"2018","unstructured":"Daniel K\u00e4stner, J\u00f6rg Barrho, Ulrich W\u00fcnsche, Marc Schlickling, Bernhard Schommer, Michael Schmidt, Christian Ferdinand, Xavier Leroy, and Sandrine Blazy. 2018. CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler. In Proceedings of the European Congress Embedded Real-Time Software and Systems. 1\u20139."},{"key":"e_1_3_2_48_2","volume-title":"Guidelines for Performing Systematic Literature Reviews in Software Engineering.","author":"Keele Staffs","year":"2007","unstructured":"Staffs Keele, Barbara Kitchenham, and Stuart Charters. 2007. Guidelines for Performing Systematic Literature Reviews in Software Engineering.Technical Report. Citeseer."},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48118-4_31"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_2"},{"key":"e_1_3_2_51_2","doi-asserted-by":"crossref","unstructured":"Gerwin Klein June Andronick Kevin Elphinstone Toby Murray Thomas Sewell Rafal Kolanski and Gernot Heiser. 2014. Comprehensive formal verification of an OS microkernel. Transactions on Computer Systems 32 1 (2014) 1\u201370.","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_52_2","doi-asserted-by":"crossref","unstructured":"Ramana Kumar Magnus O. Myreen Michael Norrish and Scott Owens. 2014. CakeML: A verified impl. of ML. SIGPLAN Notices 49 1 (2014) 179\u2013191.","DOI":"10.1145\/2578855.2535841"},{"key":"e_1_3_2_53_2","first-page":"1","volume-title":"Proceedings of the International Conference on Interactive Theorem Proving","author":"Lasser Sam","year":"2019","unstructured":"Sam Lasser, Chris Casinghino, Kathleen Fisher, and Cody Roux. 2019. A verified LL(1) parser generator. In Proceedings of the International Conference on Interactive Theorem Proving. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 1\u201318."},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594334"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_51"},{"key":"e_1_3_2_56_2","unstructured":"K. Rustan M. Leino. 2008. This is boogie 2. Manuscript KRML (2008)."},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_58_2","doi-asserted-by":"crossref","unstructured":"Xavier Leroy. 2009. A formally verified compiler back-end. Journal of Automated Reasoning 43 4 (2009) 363\u2013446.","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_59_2","volume-title":"Proceedings of the Embedded Real Time Software and Systems","author":"Leroy Xavier","year":"2016","unstructured":"Xavier Leroy, Sandrine Blazy, Daniel K\u00e4stner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert\u2014a formally verified optimizing compiler. In Proceedings of the Embedded Real Time Software and Systems."},{"key":"e_1_3_2_60_2","volume-title":"Proceedings of the MILS@ HiPEAC","author":"Lescuyer St\u00e9phane","year":"2015","unstructured":"St\u00e9phane Lescuyer. 2015. ProvenCore: Towards a verified isolation micro-kernel. In Proceedings of the MILS@ HiPEAC."},{"key":"e_1_3_2_61_2","first-page":"200","volume-title":"Proceedings of the Int. Workshop on Types for Proofs and Programs","author":"Letouzey Pierre","year":"2002","unstructured":"Pierre Letouzey. 2002. A new extraction for coq. In Proceedings of the Int. Workshop on Types for Proofs and Programs. Springer, 200\u2013219."},{"key":"e_1_3_2_62_2","unstructured":"LMbench 2013. LMbench\u2014Tools for Performance Analysis. (2013). Retrieved January 23 2026 from https:\/\/lmbench.sourceforge.net\/"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451148"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706329"},{"key":"e_1_3_2_65_2","unstructured":"mCertikOS 2021. mCertiKOS Hypervisor. (2021). Retrieved January 23 2026 from https:\/\/flint.cs.yale.edu\/certikos\/mcertikos.html#mcertikos"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/3302424.3303946"},{"key":"e_1_3_2_67_2","unstructured":"NATS. 2013. How technology is transforming air traffic management. (2013). Retrieved January 23 2026 from https:\/\/web.archive.org\/web\/20130801003045http:\/\/nats.aero:80\/blog\/2013\/07\/how-technology-is-transforming-air-traffic-management"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34968-4_23"},{"key":"e_1_3_2_70_2","doi-asserted-by":"crossref","unstructured":"Colin O\u2019Halloran. 2013. Automated verification of code autom. generated from Simulink. Automated Software Engineering 20 2 (2013) 237\u2013264.","DOI":"10.1007\/s10515-012-0116-5"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_26"},{"key":"e_1_3_2_72_2","doi-asserted-by":"crossref","unstructured":"Andrei Popescu Peter Lammich and Ping Hou. 2021. CoCon: A conference management system with formally verified document confidentiality. Journal of Automated Reasoning 65 2 (2021) 321\u2013356.","DOI":"10.1007\/s10817-020-09566-9"},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00064"},{"key":"e_1_3_2_74_2","unstructured":"Quark 2021. Quark: A Web Browser with a Formally Verified Kernel. (2021). Retrieved January 23 2026 from https:\/\/github.com\/Conservatory\/quark"},{"key":"e_1_3_2_75_2","doi-asserted-by":"crossref","unstructured":"Eric Rescorla and Tim Dierks. 2018. The transport layer security (TLS) protocol version 1.3. (2018).","DOI":"10.17487\/RFC8446"},{"key":"e_1_3_2_76_2","doi-asserted-by":"crossref","unstructured":"Talia Ringer Karl Palmskog Ilya Sergey Milos Gligoric and Zachary Tatlock. 2019. QED at large: A survey of engineering of formally verified software. Foundations and Trends\u00ae in Programming Languages 5 2-3 (2019) 102\u2013281.","DOI":"10.1561\/2500000045"},{"key":"e_1_3_2_77_2","unstructured":"Rocq 2025. Rocq Interactive Theorem Prover. (2025). Retrieved January 23 2026 from https:\/\/rocq-prover.org\/"},{"key":"e_1_3_2_78_2","unstructured":"s2n 2021. s2n Github Repository. (2021). Retrieved January 23 2026 from https:\/\/github.com\/aws\/s2n-tls"},{"key":"e_1_3_2_79_2","doi-asserted-by":"crossref","unstructured":"C\u00e9sar S\u00e1nchez Gerardo Schneider Wolfgang Ahrendt Ezio Bartocci Domenico Bianculli Christian Colombo Yli\u00e9s Falcone Adrian Francalanza Sr\u0111an Krsti\u0107 JoHao M. Louren\u00e7o Dejan Nickovic Gordon J. Pace Jose Rufino Julien Signoles Dmitriy Traytel and Alexander Weiss. 2019. A survey of challenges for runtime verification from advanced application domains (beyond software). Form Methods Syst Des 54 3 (2019) 279\u2013335.","DOI":"10.1007\/s10703-019-00337-w"},{"key":"e_1_3_2_80_2","doi-asserted-by":"crossref","unstructured":"Thomas Sewell Felix Kam and Gernot Heiser. 2017. High-assurance timing analysis for a high-assurance real-time operating system. Real-Time Systems 53 5 (2017) 812\u2013853.","DOI":"10.1007\/s11241-017-9286-3"},{"key":"e_1_3_2_81_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_3_2_82_2","doi-asserted-by":"crossref","unstructured":"Youngju Song Minki Cho Dongjoo Kim Yonghyun Kim Jeehoon Kang and Chung-Kil Hur. 2019. CompCertM: CompCert with c-assembly linking and lightweight modular verification. ACM Programming Languages 4 Article 23 (2019).","DOI":"10.1145\/3371091"},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22627-4_21"},{"key":"e_1_3_2_84_2","doi-asserted-by":"publisher","DOI":"10.1145\/2897336.2897344"},{"key":"e_1_3_2_85_2","first-page":"1091","volume-title":"Proceedings of the USENIX Security Symposium","author":"Tao Zhe","year":"2021","unstructured":"Zhe Tao, Aseem Rastogi, Naman Gupta, Kapil Vaswani, and Aditya V. Thakur. 2021. DICE*: A formally verified implementation of DICE measured boot. In Proceedings of the USENIX Security Symposium. USENIX Association, 1091\u20131107."},{"key":"e_1_3_2_86_2","doi-asserted-by":"crossref","unstructured":"Maurice H. Ter Beek Rod Chapman Rance Cleaveland Hubert Garavel Rong Gu Ivo ter Horst Jeroen J. A. Keiren Thierry Lecomte Michael Leuschel Kristin Yvonne Rozier Augusto Sampaio Cristina Seceleanu Martyn Thomas Tim A. C. Willemse and Lijuns Zhang. 2024. Formal methods in industry. Formal Aspects of Computing (2024).","DOI":"10.1145\/3689374"},{"key":"e_1_3_2_87_2","doi-asserted-by":"crossref","unstructured":"Jaroslav \u0160ev\u010d\u00edk Viktor Vafeiadis Francesco Zappa Nardelli Suresh Jagannathan and Peter Sewell. 2013. CompCertTSO: A verified compiler for relaxed-memory concurrency. Journal of the ACM 60 3 Article 22 (2013).","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_3_2_88_2","first-page":"171","volume-title":"Proceedings of the International Conference on Computer Safety, Reliability and Security","author":"Ward N. J.","year":"1993","unstructured":"N. J. Ward. 1993. The rigorous retrospective static analysis of the sizewell \u2018B\u2019 primary protection system software. In Proceedings of the International Conference on Computer Safety, Reliability and Security. Springer, 171\u2013181."},{"key":"e_1_3_2_89_2","doi-asserted-by":"crossref","unstructured":"Neil White Stuart Matthews and Roderick Chapman. 2017. Formal verification: Will the seedling ever flower? Philosophical Transactions of the Royal Society A: Mathematical Physical and Engineering Sciences 375 2104 (2017).","DOI":"10.1098\/rsta.2015.0402"},{"key":"e_1_3_2_90_2","unstructured":"Wikipedia. 2026. Common Criteria. (2026). Retrieved January 23 2026 from https:\/\/en.wikipedia.org\/wiki\/Common_Criteria"},{"key":"e_1_3_2_91_2","unstructured":"Wikipedia. 2026. Kernel (operating system). (2026). Retrieved January 23 2026 from https:\/\/en.wikipedia.org\/wiki\/Kernel_(operating_system)"},{"key":"e_1_3_2_92_2","unstructured":"Wikipedia. 2026. L4 microkernel family. (2026). Retrieved January 23 2026 from https:\/\/en.wikipedia.org\/wiki\/L4_microkernel_family"},{"key":"e_1_3_2_93_2","unstructured":"Wikipedia. 2026. Principle of least privilege. (2026). Retrieved January 23 2026 from https:\/\/en.wikipedia.org\/wiki\/Principle_of_least_privilege"},{"key":"e_1_3_2_94_2","doi-asserted-by":"crossref","unstructured":"Jim Woodcock Peter Gorm Larsen Juan Bicarregui and John Fitzgerald. 2009. Formal methods: Practice and experience. ACM Computing Surveys 41 4 (2009).","DOI":"10.1145\/1592434.1592436"},{"key":"e_1_3_2_95_2","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806610"},{"key":"e_1_3_2_96_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_97_2","unstructured":"Feng Zhang and Wensheng Niu. 2019. A survey on formal specification and verification of system-level achievements in industrial circles. Academic Journal of Computing and Information Science 2 1 (2019)."},{"key":"e_1_3_2_98_2","unstructured":"Qiao Zhang Danyang Zhuo and James Wilcox. A survey of formal verification approaches for practical systems. (n.d). Retrieved from https:\/\/courses.cs.washington.edu\/courses\/cse551\/15sp\/projects\/qz2013-danyangz-jrw12.pdf"},{"key":"e_1_3_2_99_2","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"},{"key":"e_1_3_2_100_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462164"},{"key":"e_1_3_2_101_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_6"},{"key":"e_1_3_2_102_2","unstructured":"Yongwang Zhao David San\u00e1n Fuyuan Zhang and Yang Liu. 2017. High-assurance separation kernels: A survey. arXiv:1701.01535. Retrieved from https:\/\/arxiv.org\/abs\/1701.01535"},{"key":"e_1_3_2_103_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3785652","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T10:24:41Z","timestamp":1770891881000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3785652"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2,11]]},"references-count":102,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2026,6,30]]}},"alternative-id":["10.1145\/3785652"],"URL":"https:\/\/doi.org\/10.1145\/3785652","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2,11]]},"assertion":[{"value":"2023-03-17","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-15","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-02-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}