We have modeled and formally analyzed a simple external memory manager (EMM) system loosely based on the memory management strategies of Mach. The modeling was carried out via a series of refinements from a very abstract model to a simple concrete model. Each successive model is an implementation of the next more abstract level. We have stated theorems that describe formally the relationships among these models; these theorems have been proven for a subset of the functionality of the system. The result is a stack of progressively more realistic and complex systems (partially) proven to satisfy an implements relation with a simple high-level design.