A manifesto for applicable formal methods

Mario Gleirscher*, Jaco van de Pol, Jim Woodcock

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review


Recently, formal methods have been used in large industrial organisations (including AWS, Facebook/Meta, and Microsoft) and have proved to be an effective part of a software engineering process finding important bugs. Perhaps because of that, practitioners are interested in using them more often. Nevertheless, formal methods are far less applied than expected, particularly for safety-critical systems where they are strongly recommended and have the most significant potential. We hypothesise that formal methods still seem not applicable enough or ready for their intended use in such areas. In critical software engineering, what do we mean when we speak of a formal method? And what does it mean for such a method to be applicable both from a scientific and practical viewpoint? Based on what the literature tells about the first question, with this manifesto, we identify key challenges and lay out a set of guiding principles that, when followed by a formal method, give rise to its mature applicability in a given scope. Rather than exercising criticism of past developments, this manifesto strives to foster increased use of formal methods in any appropriate context to the maximum benefit.

Original languageEnglish
JournalSoftware and Systems Modeling
Early online date18 Aug 2023
Publication statusE-pub ahead of print - 18 Aug 2023

Bibliographical note

© 2023, The Author(s).


  • Formal methods
  • Formal verification
  • Research evaluation
  • Research transfer
  • Software engineering
  • Tools

Cite this