Формальная спецификация - математическое описание программы или оборудование, которое может быть использовано для разработки реализации. В ней описывается, что должно делать система, но не (обязательно) указывается как.
Имея такую спецификацию, можно, используя технику формальной верификации продемонстрировать, что предложенный проект системы является правильным, в отношении спецификации. Такой подход имеет преимущество в том, что предложенные неверные проекты систем могут быть пересмотрены до того как будут сделаны основные расходы на собственно саму реализацию.
Альтернативный подход состоит в том, чтобы, выполняя шаги по уточнению спецификации, верность которых можно доказать, превратить спецификацию на реализацию, которая будет верна путем построения.
