Formal Methods Practice and Theory

Traditional software development and testing methodologies aren’t sufficient for safety and security-critical software. It needs to be free of defects to avoid costly and potentially life-threatening software failures. A software failure could crash an autonomous car, leak a confidential key, or bring down a major cloud service.

This is where formal methods come into play.

Formal methods are a powerful way to connect software with its required behavior. Starting from a formally defined requirement, designers can check the model for correctness and properties such as liveliness or the absence of deadlock. That model can then be refined and connected to a formal model at the code level. While this methodology does not guarantee the absence of errors, it does provide a very high level of confidence during the design process.

Formal methods can be used to prove properties of software, either at the implementation level, where it can prove, for example, the absence of run-time errors in software, or at a higher level. As an example, it could find problems in a communication protocol bridging separate design elements.

At the code level, traditional testing workflows try to stress a codebase to exercise all code paths and prove that they behave correctly. This means a) the absence of runtime errors and b) functional correctness. However, testing all paths is simply not possible for real-world software. Worse, the gap in test coverage is usually unknown and greatly underestimated. Formal methods take a different approach: it allows the software developer to statically prove the absence of runtime errors - and even functional correctness - for a set of properties, even if those properties themselves don’t cover full functional correctness.

The formal methods field has made tremendous progress in the past decade, enabling the use of formal methods in real-world applications and projects. Popular technologies include CBMC, TLA+, and Ada/SPARK. AdaCore is an active participant in this field, as are NVIDIA, Oracle, AWS, Microsoft, and others.

The report “Back to the Building Blocks: A Path Toward Secure and Measurable Software” makes the case that we have to get better at building the software-intensive systems we depend on. It refers to formal methods as one of the technologies to drive that improvement across requirements and implementation.

At the code level, an often quoted data point from Microsoft in 2019 is that 70% of all security vulnerabilities are due to memory errors. Based on real-world data, when using Ada/SPARK, this drops down to sub 10%, with no vulnerabilities in the Ada/SPARK code, but there may still be still vulnerabilities in the SPARK-to-C binding

One aspect that is slowing down the adoption of formal methods is that the barrier of entry is substantial. Building a formal model representation of a requirement requires someone to be fluent in the formal method language being used. Similarly, proving the absence of runtime errors in a piece of software requires effort on the side of the programmer.

In this area, there is still much progress to be made in the formal methods field. There are a lot of improvements in modeling languages (such as TLA+), programming languages (such as Ada/SPARK), the use of AI/LLM, and more being worked on by different research teams. The use of AI to translate a requirement into a formal model or to translate a piece of code from C into Ada/SPARK is promising.

Collaboration in this field is very important, especially collaboration with actual practitioners. From the AdaCore perspective, this feedback from practitioners is key to help us find ways to make the application of formal methods easier, both in the area of writing green-field code, but also in the area of migrating a piece of logic from an existing code base in C or C++ into Ada/SPARK, proving the absence of runtime errors, proving functional correctness and then integrating it back into the larger software project.

We discussed a wide array of topics from both practitioners and researchers, covering topics such as:

• How to use AI in the authoring and proving of algorithms and code
• Ada/SPARK, TLA+, CBMC, Rust, and other tools and languages, and formal methods
• Best practices for mixed language systems
• How formal methods help resolve defects in requirements
• How formal methods help developers become better programmers
• What type of programs are best suited for the usage of formal methods

Everybody took heavy notebooks with learnings away from the event. Now it is time to collate our notes, reflect on them, and determine how we can apply them in our future plans.