There have already been two file system verification projects, this year's OSDI best paper is the most recent example, http://locore.cs.washington.edu/papers/sigurbjarnarson-yggdr..., and last year as SOSP FSCQ: http://sigops.org/sosp/sosp15/current/2015-Monterey/013-chen...