A formal specification is a mathematical description of software or hardware that can be used to develop an implementation of it. It describes what the system should do, and not (necessarily) how it should do it. Given a specification, it is possible to use formal verification techniques to demonstrate that the model of a candidate system conforms to its specification. This has the enormous advantage that incorrect candidate systems are detected and can be revised before investing in their implementation. An alternative approach is to use refinement steps to transform a specification into a complete model, and finally into a concrete implementation. It is important to note that a model (or implementation) can never be declared "correct" in isolation, but only "correct with respect to its specification". Determining whether a formal specification correctly describes the problem to be solved is a separate problem. It is also a difficult problem to solve, since it consists of constructing an abstract formal representation of an informal and concrete problem domain, and this abstraction step is neither responsible nor sufficient to be a formal proof by itself. However, it is possible to validate a specification by proving theorems relating to the properties that the system should possess. If these theorems prove correct, they reinforce the understanding of the specification and its relationship to the problem domain. If not, the specification probably needs to be changed to better reflect the domain understanding of those involved in producing (and implementing) the specification.