One of the specialties of HENSOLDT Cyber is *formal verification*. This may sound very sophisticated, but what is it exactly? In this blog, we will endeavor to explain. In general, whenever we write a computer program, we would like it to behave exactly the way we want it to. But how to be sure? Generally, the way software developers do this is by *testing*; running a program under specific circumstances and checking that it then does the right thing.

However, testing is not entirely foolproof. The main drawback is that it is only run on a limited number of test cases: if you do not include a particular test case, any bugs that test case might reveal will only show up when your program is actually in use (with dire consequences ensuing…)

The approach of formal verification is different: we use mathematical methods (either automatic, such as model checking, or manual, like interactive theorem proving) to *prove* properties of the program, for example that its output is what we expect it to be, or that it doesn’t keep running forever. Since we’re checking properties of the program as a whole, we’re not dependent on whether we’ve covered everything with test cases.

Of course, formal verification is not perfect either: since we are reasoning about the program, we must have some sort of idea of how it behaves—in other words, we need to have a mathematical model of the programming language our program is written in. And if this model is different from how the program behaves on a real machine, errors might still occur.

So, while formal verification cannot replace testing, it does offer another way of checking a program for errors that is highly complementary to testing. And therefore, it allows you to be more confident about the correctness of your program – and that’s what it’s all about in the end!