Wired reports that MIT have used formal verification to write a file system that to probably will not lose data in the event of a crash.
Making sure that the file system can recover from a crash at any point is tricky because there are so many different places that you could crash. You literally have to consider every instruction or every disk operation
They used Coq, a proof assistant that enabled them to build the system from the ground up in a logically consistent manner.
musingstudio 