In a UNIX file system, metadata for the file objects must be updated in a specific order such that the file system can be recovered after a crash. Metadata update usually involves several atomic actions and thus a crash can happen in between these atomic actions before the whole update is completed. This project investigates formally specifying a UNIX file system and these metadata updating operations using the software specification language Alcoa. Alcoa comes with a tool which along with helping to debug the specification, proved useful in investigating various invariants of the system.