In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.
Formal methods employ a variety of theoretical computer science fundamentals, including logic calculi, formal languages, automata theory, control theory, program semantics, type systems, and type theory.Monin, pp.3-4
History Reasoning mathematically about programs predates the discipline's name. Alan Turing sketched a correctness argument for a routine in 1949, and in the late 1960s Robert W. Floyd and Tony Hoare established the axiomatic tradition of program proof that became Hoare logic. Edsger W. Dijkstra's weakest-precondition calculus gave a systematic way to derive programs from specifications, and model-oriented specification languages such as VDM and the Z notation were developed during the 1970s.
A second tradition grew out of temporal logic. Amir Pnueli proposed it in 1977 as a language for specifying the behaviour of reactive programs, and model checking was introduced independently by Edmund M. Clarke and E. Allen Emerson and by Jean-Pierre Queille and Joseph Sifakis in the early 1980s, work for which the three shared the 2007 Turing Award. Symbolic model checking with binary decision diagrams raised the size of systems that could be analysed by orders of magnitude, and bounded model checking built on SAT solvers extended it further.
Industrial interest was sharpened by costly defects such as the 1994 Pentium FDIV bug, which prompted processor vendors to invest heavily in hardware verification. From the 2000s onwards, maturing SMT solvers and proof assistants made it practical to verify complete systems rather than isolated components.
Uses
Formal methods can be applied at various points through the development process.
Specification
Formal methods may be used to give a formal description of the system to be developed, at whatever level of detail desired. Further formal methods may depend on this specification to synthesize a program or to verify the correctness of a system with respect to its specification.
Alternatively, specification may be the only stage in which formal methods are used. By writing a specification and attempting to prove properties that should follow, ambiguities in the informal requirements can be discovered and resolved. Additionally, engineers can use a formal specification as a reference to guide their development processes.
The need for formal specification systems has been noted for years. In the ALGOL 58 report, John Backus presented a formal notation for describing programming language syntax, later named Backus normal form then renamed Backus–Naur form (BNF).Knuth, Donald E. (1964), Backus Normal Form vs Backus Naur Form. Communications of the ACM, 7(12):735–736. Backus also wrote that a formal description of the meaning of syntactically valid ALGOL programs was not completed in time for inclusion in the report, stating that it "will be included in a subsequent paper." However, no paper describing the formal semantics was ever released.
Synthesis
Program synthesis is the process of automatically creating a program that conforms to a specification. Deductive synthesis approaches rely on a complete formal specification of the program, whereas inductive approaches infer the specification from examples. Synthesizers perform a search over the space of possible programs to find a program consistent with the specification. Because of the size of this search space, developing efficient search algorithms is one of the major challenges in program synthesis.
Verification
Formal verification is the use of software tools to prove properties of a formal specification, or to prove that a formal model of a system implementation satisfies its specification.
Once a formal specification has been developed, the specification may be used as the basis for proving properties of the specification, and by inference, properties of the system implementation.
Sign-off verification Sign-off verification is the use of a formal verification tool that is highly trusted. Such a tool can replace traditional verification methods (the tool may even be certified).
Human-directed proof Sometimes, the motivation for proving the correctness of a system is not the obvious need for reassurance of the correctness of the system, but a desire to understand the system better. Consequently, some proofs of correctness are produced in the style of mathematical proof: handwritten (or typeset) using natural language, using a level of informality common to such proofs. A "good" proof is one that is readable and understandable by other human readers.
Critics of such approaches point out that the ambiguity inherent in natural language allows errors to be undetected in such proofs; often, subtle errors can be present in the low-level details typically overlooked by such proofs. Additionally, the work involved in producing such a good proof requires a high level of mathematical sophistication and expertise.
Interactive theorem proving Proof assistants occupy a middle ground between wholly human-directed and wholly automated proof. The user directs the argument, typically by applying tactics, while the tool records each step and mechanically checks the resulting proof. Because the finished proof is checked by a comparatively small and stable kernel, the much larger body of search and automation surrounding it need not itself be trusted. Systems in common use include Isabelle/HOL, the Rocq Prover (named Coq until 2025), Lean, Agda, HOL4, PVS and ACL2. Interactive proof underlies most of the largest verified software artifacts, including the seL4 microkernel and the CompCert compiler, and is increasingly combined with automated back ends so that routine obligations are discharged by solvers while difficult ones are proved by hand.
Automated proof In contrast, there is increasing interest in producing proofs of correctness of such systems by automated means. Automated techniques fall into four general categories: Automated theorem proving, in which a system attempts to produce a formal proof from scratch, given a description of the system, a set of logical axioms, and a set of inference rules. Model checking, in which a system verifies certain properties by means of an exhaustive search of all possible states that a system could enter during its execution. Abstract interpretation, in which a system verifies an over-approximation of a behavioural property of the program, using a fixpoint computation over a (possibly complete) lattice representing it. Deductive verification, in which a program annotated with preconditions, postconditions and loop invariants is translated, in the tradition of Hoare logic, into logical verification conditions whose validity is then discharged automatically by an SMT solver or interactively in a proof assistant.
Some automated theorem provers require guidance as to which properties are "interesting" enough to pursue, while others work without human intervention. Model checkers can quickly get bogged down in checking millions of uninteresting states if not given a sufficiently abstract model.
Proponents of such systems argue that the results have greater mathematical certainty than human-produced proofs, since all the tedious details have been algorithmically verified. The training required to use such systems is also less than that required to produce good mathematical proofs by hand, making the techniques accessible to a wider variety of practitioners.
Critics note that some of those systems are like oracles: they make a pronouncement of truth, yet give no explanation of that truth. There is also the problem of "verifying the verifier"; if the program that aids in the verification is itself unproven, there may be reason to doubt the soundness of the produced results. Some modern model checking tools produce a "proof log" detailing each step in their proof, making it possible to perform, given suitable tools, independent verification.
The main feature of the abstract interpretation approach is that it provides a sound analysis, i.e. no false negatives are returned. Moreover, it is efficiently scalable, by tuning the abstract domain representing the property to be analyzed, and by applying widening operatorsA. Cortesi and M. Zanioli, Widening and Narrowing Operators for Abstract Interpretation . Computer Languages, Systems and Structures. Volume 37(1), pp. 24–42, Elsevier, (2011). to get fast convergence.
Techniques Formal methods includes a number of different techniques.
Specification languages
The design of a computing system can be expressed using a specification language, which is a formal language that includes a proof system. Using this proof system, formal verification tools can reason about the specification and establish that a system adheres to the specification.
Binary decision diagrams
A binary decision diagram is a data structure that represents a Boolean function. If a Boolean formula expresses that an execution of a program conforms to the specification, a binary decision diagram can be used to determine if is a tautology; that is, it always evaluates to TRUE. If this is the case, then the program always conforms to the specification.
SAT solvers
A SAT solver is a program that can solve the Boolean satisfiability problem, the problem of finding an assignment of variables that makes a given propositional formula evaluate to true. If a Boolean formula expresses that a specific execution of a program conforms to the specification, then determining that is unsatisfiable is equivalent to determining that all executions conform to the specification. SAT solvers are often used in bounded model checking, but can also be used in unbounded model checking.
Satisfiability modulo theories
Satisfiability modulo theories (SMT) generalises Boolean satisfiability to formulas interpreted over background theories such as fixed-width bit vectors, linear arithmetic, arrays, algebraic data types and uninterpreted functions. Because those theories correspond closely to the constructs of real programming languages, SMT solvers such as Z3 and cvc5 have become the automation engine behind most contemporary deductive verifiers, as well as behind symbolic execution and program synthesis tools.
Deductive program verification Deductive verifiers translate an annotated program into verification conditions using a predicate transformer such as the weakest precondition, and then discharge those conditions with automated provers. Intermediate verification languages, among them Boogie, Why3 and Viper, allow several front ends to share a single verification-condition generator and solver interface. Tools of this kind include Dafny, Frama-C, SPARK, VeriFast and F*.
Separation logic extends this style of reasoning to programs that manipulate pointers and the heap, by making the disjointness of memory regions part of the assertion language. It underpins both interactive frameworks for verifying low-level code and automatic analysers that run on very large code bases.
Applications