How can software be implemented correctly—and where do traditional testing methods reach their limits? Lars Hupel provides insights into the use of formal methods and explains when their use is particularly worthwhile.
Correctness sounds obvious, yet in practice it often plays only a minor role. Why is that – and in which cases does it become truly critical?
Of course, no one wants to deliver “incorrect” software. However, in most projects, there simply isn’t the budget to ensure full correctness.
This is because the methods required to achieve or approximate correctness increase development costs. For the critical parts of a system, teams need to write detailed specifications and verify that the implementation conforms to those specifications.
The term “critical” is typically used in contexts where software failures are unacceptable, for example in aerospace, healthcare, or financial services. In these domains, it is not an option for software to fail to meet its requirements, as the consequences can be severe.
You argue that testing alone is not sufficient to ensure correctness. Where do traditional testing approaches fall short – and what do formal methods provide beyond that?
Edsger Dijkstra famously said that testing can show the presence of bugs, but not their absence. By their very nature, tests cannot cover the entire possible input and output space of a system.
Most of us have encountered bugs that hide in edge cases. For example, YAML interprets “no” as “false”, which can be quite problematic when dealing with country codes.
Formal methods go beyond this by providing guarantees rather than just a promise. Instead of executing a finite set of test cases, they make universal statements about certain properties of a system.
Formal methods are often seen as complex or difficult to apply. How can they be used pragmatically and effectively in real-world projects?
There is probably no silver bullet.
The first important step is to identify the parts of a system where the use of formal methods actually makes sense.
The second is to choose the right technique based on the requirements. There is a wide spectrum of options, ranging from lightweight approaches (such as modeling state machines) to heavyweight ones (such as full program verification).
Take a banking app as an example: it may not be a big issue if the app crashes occasionally (no formal methods needed). However, it must never lose or duplicate a transaction (formal methods are essential).
What requirements do formal methods impose on software architecture? What should architects keep in mind when designing verifiable systems?
Verifiable code needs to be designed and implemented in a specific way.
For example, external interactions such as database or network access should be isolated as much as possible. Components should have a clear, single responsibility and communicate only through well-defined interfaces.
Fortunately, these are also characteristics of good software architecture in general. In other words, anyone who takes the principles of iSAQB modules such as DDD or DSL seriously will already be in a strong position to apply formal methods effectively.
You mentioned practical examples in your talk: where do you currently see the most important application areas for formal methods? Where do they provide the most value?
A common example in software engineering is compiler construction. Compiler bugs are often difficult to debug and can lead to highly undesirable behavior.
“CompCert” is an academic project that has produced a production-ready C compiler. It can be used in safety-critical environments to ensure that the compiled code faithfully reflects the semantics of the source code.
Just last month, it was announced that CompCert is being used in aircraft developed by the manufacturer ATR.
You can learn more about this topic at the Software Architecture Forum 2026: In his session, Lars Hupel will demonstrate how formal methods can be applied in practice in software architecture.
