About the New CPSA® – Advanced Level Module FM: Formal Methods

On February 27, 2025, the iSAQB intro­duced the new Advanced Level module Formal Methods (FM) .

The “FM — Formal Methods” module teaches software archi­tects how to ensure the correctness of a system’s design and imple­men­tation through mathe­matical proofs. Focusing on safety-critical, sensitive, or econom­i­cally vital systems, this module goes beyond tradi­tional architecture and testing methods, offering formal techniques to verify that software adheres to its requirements. By integrating formal methods early in the design phase, archi­tects can create verifiable models, ensuring a higher level of software quality and reliability.

We conducted an interview with the curators, Michael Sperber and Lars Hupel, where they provide deeper insights into the module.

Why do you believe the topic of “Formal Methods” is important enough to warrant its own module in the CPSA Advanced program?

Software systems control an increasing number of aspects of our lives, and this makes their safety and security ever more relevant: These software systems need to keep our lives and health safe, and be resistant against sabotage and data exfil­tration. With such software we want guarantees that they actually fulfill certain requirements. Automated tests are not suffi­cient for that, as they only cover certain scenarios — but we want the system to behave correctly in all scenarios. This requires applying mathe­matical techniques — so-called formal methods. So far, this was a gap in the Advanced portfolio, and we have now closed it.

What specific advan­tages do formal methods offer compared to tradi­tional software devel­opment approaches, especially in safety-critical areas?

They achieve something that tradi­tional techniques don’t: They give us guarantees, instead of a mere promise that the “next update” will fix the current security problem.

How does the module help software archi­tects ensure system accuracy and correctness in complex projects?

The first important aspect is to identify those parts of the system where applying formal methods pays off. The second one is to pick the right method depending on the requirements — there is a large collection of such methods. Finally, the training is about making the system architecture amenable to applying formal methods effectively.

Formal methods are known for their mathe­matical approach – how can this be applied in practice without compro­mising the agility of development?

In principle, formal methods are not in opposition to agility. However, software archi­tects need to give formal methods some basic consid­er­ation at the outset of a project. Otherwise, applying them later may be much more costly. For example, to prove the correctness of a piece of code, it has to be written in a certain way — the programming language also plays a role. Therefore, it is much more effective to use formal methods concomi­tantly with the devel­opment process, and to integrate its tooling into CI. That makes formal methods quite agile.

What impact do formal methods have on the long-term maintain­ability and scala­bility of software architectures?

Conal Elliott, a prominent computer scientist, coined the phrase “only correctness composes”: If a building block is guaranteed to have a certain property, it does not matter how it does that, and it is safe to combine it with other such building blocks without worrying about their inner details. This fosters decou­pling the building blocks and is great for the architecture.

What prereq­ui­sites should one have for this module, partic­u­larly regarding mathe­matical knowledge and experience in software architecture?

High-school math is enough. In principle, the training is independent from other Advanced trainings, but it is a partic­u­larly good fit for FUNAR and EMBEDDED: FUNAR because formal methods in practice build on functional programming, and EMBEDDED because embedded systems often have heightened requirements on qualities where formal methods can help.