Unification is an important concept. It is used in Prolog, resolution, term rewriting and natural language understanding. As the use of formal methods increases, unification will be part of formally developed systems. Hence a theory of unification is desirable. This paper demonstrates the use of VDM to develop a theory of unification. Substitution application is defined recursively, a theory of non-circular substitutions is developed, and an implicit specification of unification is written. A proof of a particular unification algorithm is outlined with respect to this specification. The algorithm considered is more space-efficient than that which Manna and Waldinger prove correct. The theory developed is also compared with that of Manna and Waldinger.