Whether it is our smart phone, our car or even our medical devices - everyone knows that software is an integral part of our everyday life and regularly gets more sophisticated and complex. We most of the time readily share our sensitive information to a maze of complex systems where safety and security are critical. We also know how catastrophic the repercussions can be when such systems are insecure. 

Just recently, a seemingly simple piece of software practically used on every computing machinery - Log4j - has made the news with the bug of the century. Log4j is a Java-based logging software, better say it’s the logging software. From Apple to Nasa everyone who uses Java as a programming language, will most likely use Log4j. A major security flaw was now made public that could account for damage beyond imagination. One of the victims was the well-known game Minecraft where attackers exploited the vulnerability to take over a whole world-building server from Microsoft - the owners of the game. This shows that even with meticulous software testing routines, the smallest inconsistencies can be exploited to gain access or control over whole systems. 

So what can we do to make systems safer? Well, we have to go back to basics and mathematically prove that software is doing what it is supposed to do, in other words that software is correct. Just like a builder works off an architect’s blueprint for construction, programmers rely on specifications mapping how a system should and should not perform. Such specifications are translated into code. However, it is often the case that specifications and code do not match up causing systems to have potential flaws and vulnerabilities. A tiny bug can lead to system faults, breakdowns and offer attackers easy access to obtain data or control. 

With formal methods we can analyse such pieces of software to check that nothing is lost in translation and software does what it is intended to do. To do so, we need to translate the code and specifications into a mathematical representation - in our case first-order logic, specifically trace logic. Such mathematical models can now be checked by mathematical proof: can we prove the specification correct for the given program in terms of a logical calculus? In case that program and specification do not match, formal methods allow to analyse the root of the cause of such discrepancies and to correct it. 

Given how complex software nowadays is and how many possible paths each program can contain, with conventional testing it would never be possible to cover all execution paths - even worse a critical one might be missed. With mathematical abstraction and logic we can nicely represent many execution paths. Formal methods in fact allow us to investigate all possible paths at once. Automated proving techniques such as first-order reasoners and SMT-solvers can be leveraged to help us mathematically verify program correctness. We can wipe out whole classes of bugs and dramatically improve security and safety of critical systems while cutting down costs for avoided security breaches. Formal verification is thus an indispensable tool for code bases that millions of people, companies or governments depend on.