Lessons Learned From Microkernel Verification -- Specification is the New Bottleneck

TL;DR

This paper discusses the challenges in verifying large software systems, emphasizing that specification complexity is a key bottleneck despite advances in verification tools, based on lessons from microkernel verification.

Contribution

It identifies specific issues hindering the widespread adoption of formal verification in large-scale software development, derived from practical experience with microkernel verification.

Findings

Specification complexity is the main bottleneck in large-scale verification.

Verification tools have advanced but are underutilized due to process issues.

Lessons from microkernel verification highlight key challenges and potential solutions.

Abstract

Software verification tools have become a lot more powerful in recent years. Even verification of large, complex systems is feasible, as demonstrated in the L4.verified and Verisoft XT projects. Still, functional verification of large software systems is rare - for reasons beyond the large scale of verification effort needed due to the size alone. In this paper we report on lessons learned for verification of large software systems based on the experience gained in microkernel verification in the Verisoft XT project. We discuss a number of issues that impede widespread introduction of formal verification in the software life-cycle process.