Coq

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....