Experiences with formal specification of fault-tolerant file systems