As embedded systems and critical software components become increasingly complex and interconnected, ensuring their correctness and reliability has become a central concern in both safety and cybersecurity domains. While conventional verification techniques are often limited in their ability to offer guarantees, formal methods provide a mathematically grounded approach to prove system properties or detect specification violations. Despite their power, these methods are sometimes misunderstood or perceived as inaccessible. This article offers a clear and structured overview of formal methods—how they work, what they bring, and why their adoption is gaining traction in industrial settings.
What are Formal Methods?
Formal methods are a set of rigorous automatic technics based on mathematical abstraction to elaborate on software or hardware systems.
They replace or complement human reasoning on these systems with three main objectives:
- to synthesize (generate) the system implementation from a formal description,
- to verify the correctness of the system with respect to its formal description,
- to prove (verify) that the system implementation satisfies (conform) to its specification (properties).
Formal methods accelerate system development and make the implemented systems more reliable than manual methods. This document focuses on formal methods used to “prove the absence of” or “detect” violations of the specification, functional, safety or cyber security properties.
The advantages of using formal methods with respect to manual proof are:
- error free: formal methods are not subject to reasoning errors as human beings are,
- reproducible: formal methods give the same results each time the proof is launched,
- accessible: using a proof tool requires less expertise than producing proof by hand.
The main advantage of using formal methods with respect to semi formal or informal methods is the insurance that all violations are detected: all target properties are checked for on all system states for all possible inputs. The soundness and completeness of the results increase the reliability of the system.
The formal methods fall into three main categories:
- theorem proving: producing formal proofs from a description of the system, a set of axioms and a set of inference rules,
- model checking: proving that the system description satisfies the properties (or raises a counter example) for all system states.
- abstract interpretation: verifying properties on the system description for all execution paths and all possible values of variables (lattices).
In proof mode, formal methods conclude with:
- “True”: if the property is valid for all system states,
- “False”: if there exists at least one system state that violates the property.
In proof mode, model checking and abstract interpretation offer a supplementary “MayBe” conclusion if the formal reasoning cannot conclude. Such a conclusion does exist with theorem proving.
In detection mode, formal methods identify states that violate a property. Such mode is only available with model checking and abstract interpretation. It helps debug the system: one can detect a first violation, correct it then relaunch to get the next violation until no violation is detected then launch the proof mode.
The scaling of formal methods on industrial size and complexity systems may require human intervention. When the proof reasoning does not reach “True” or “False” but run for too long or produce a “MayBe”, human intervention is required to add information to the initial description:
- theorem proving: axioms or inference rules,
- model checking: lemmas,
- abstract interpretation: restricted input variables domains or assertions.
Why and how to use Formal Methods?
Formal methods contribute greatly to the reliability and robustness of the software or hardware system thanks to the underlying mathematical analysis. They are implemented in proof tools that hide the mathematical foundations. For example, proof assistants are based on theorem proving, model-based design (MBD) tools are based on model checking, and a few static analysis tools are based on abstract interpretation. For model checking and abstract interpretation the final user does not have to know the theories inside; he is left with the charge of the system description. For theorem proving, the initial description combines system and proof theory description. As a result, the level of mathematical knowledge required from the theorem proving tool end user is larger. Note that the three categories of methods can either be used independently or sequentially in a proof tool chain.
Running the proof tool requires a configuration that combines system description and proof control. On the initial run, the tool may not be able to conclude on the validity of the system property. This is in general due to incomplete configuration. The final user must complete the configuration to set out the system and environment description (model checking or abstract interpretation) or the proof theory (theorem proving), until the tool is able to conclude. As a result, several proof tool launches may be necessary before proving valid or invalid the system property. Finally, when the configuration is achieved for the system, it will be used for all further versions of this system but also for all “equivalent” systems.
Proof tools based on formal methods produce only conclusions such as “True” or “False”, but do not produce any demonstration of these conclusions. If the conclusion is “False”, some tools produce (on request) one representative set of data that triggers the property violation. But if the conclusion is True, no detail is automatically supplied to the user because the property holds for a large set of data (each value of input data and all execution paths) difficult to summarize.
The proof results verification may be achieved by a “double proof chain” based on the idea that if a property is proven on a system by two different chains, then the conclusions can be trusted. This method requires proof of the equivalence of the configurations, and of the independence of proof tools (different technological strains).
Another way for the end user to demonstrate that proof results are correct is first to choose a certified proof tool with a qualification kit available and then demonstrate that the proof tool is used in conformance with its use case.
Proof tools have been used for a long time to check communication protocols, or safety properties on embedded systems. The use of proof tools based on formal methods is recommended or required by more and more standards, increasing “de facto” the number of industrials that use them but also domains they are used in (crypto, avionic, automotive, energy, defense, railway …).
When a proof campaign has been launched for one revision of the system, it can easily be relaunched for all further revisions. If the initial campaign is in general performed with the assistance of an expert of the system, the next ones can be done without any assistance because the properties have been finalized on the initial one. Moreover, if the proof campaign covers the entire system, behavioral differences between revisions are captured. They are automatically detected and can be accepted by correcting the property or rejected by correcting the system.
The choice of the proof tool or its configuration may be carried out by experts to fit the proof objectives on the system description for the selected proof tool.
Conclusion
Formal methods are no longer confined to academic settings or niche applications. With the rise of formal verification tools and increasing regulatory pressure in domains like avionics, automotive, and cybersecurity, their industrial deployment has become both viable and valuable. Beyond their technical rigor, their real strength lies in the reproducibility, reliability, and depth of analysis they offer. When properly configured and integrated into the development lifecycle, they help organizations detect critical defects early, reduce certification risks, and improve long-term system maintainability. As tool maturity increases and best practices emerge, formal methods are poised to become a cornerstone of trusted software engineering.
