Formal Verification

This blogpost is the second part of a trilogy of formal verification on computer systems. Here we will take a quick tour of what formal verification means, with a particular focus on verifying systems software and examples of verifying some file system. If you have not read the previous post on system verification, feel free to jump there first for an introduction! Case studies CompCert CompCert1 is probably one of the first and most famous verified compilers (and perhaps also computer systems). It is itself a significant piece of work which took around 15 years. It is a rather important corner stone, however, that is achieved by the verification community, with tools/frameworks available in 2009, it is already possible to formally verify a complex system such as a compiler. ...

This blogpost is the first part of a trilogy of formal verification on computer systems. Here we will take a quick tour of what formal verification means, with a particular focus on verifying systems software and examples of verifying some file system. What do you mean by formally verified systems? Sometimes we hear people say we have built this formally verified system that is provably correct, and does all sorts of amazing things without bugs. But what we mean by having a system formally verified? At a high level, a formally verified system often has a formal specification which mathematically stipulates what the system ought (and ought not) to do, followed by a proof that such a concrete realisation of the system meets such a spec. ...