The ABI status of filesystem formats

One nice thing about really formal specs (as opposed to careful English specs, which aren't really formal) is that for many specification languages you can find (or write) tools that leverage the specs to do useful work. For example, for a language like Alloy, fuzzing and model-checking tools can automatically generate testcases that are valid according to the spec and exercise all or most of the interesting edge cases (including many that the spec authors didn't think of).

You may also be able to prove useful consistency properties from the spec, e.g. that a "valid" filesystem doesn't have unaccounted-for blocks, etc.