Una especificación formal es una descripción matemática de software o hardware que se puede usar para desarrollar su implementación. Describe qué debe hacer el sistema, pero no necesariamente cómo debe hacerlo. Dada una especificación, es posible usar técnicas de verificación formal para demostrar que el modelo de un sistema candidato se ajusta a ella. Esto tiene la enorme ventaja de que se detectan sistemas candidatos incorrectos y se pueden revisar antes de invertir en su implementación. Un enfoque alternativo consiste en usar etapas de refinamiento para transformar una especificación en un modelo completo y, finalmente, en una implementación concreta. Es importante señalar que un modelo (o implementación) nunca puede declararse "correcto" de forma aislada, sino solo "correcto con respecto a su especificación". Determinar si una especificación formal describe correctamente el problema a resolver es un problema aparte. También es un problema difícil de resolver, ya que consiste en construir una representación formal abstracta de un dominio de problema informal y concreto, y este paso de abstracción no es ni responsable ni suficiente para constituir una prueba formal por sí solo. Sin embargo, es posible validar una especificación demostrando teoremas relacionados con las propiedades que el sistema debe poseer. Si estos teoremas resultan ser correctos, refuerzan la comprensión de la especificación y su relación con el dominio del problema. De lo contrario, probablemente sea necesario modificar la especificación para que refleje mejor la comprensión del dominio por parte de quienes participan en su elaboración (e implementación).