Формальна специфікація

Форма́льна специфіка́ція — математичний опис програмного забезпечення або обладнання, яке може бути використане для розробки реалізації. В ній описується, що має робити система, але не (обов'язково) вказується як. Маючи таку специфікацію, можна, використовуючи техніку формальної верифікації продемонструвати, що запропонований проєкт системи є правильним, по відношенню до специфікації. Такий підхід має перевагу в тому, що запропоновані невірні проєкти систем можуть бути переглянуті до того як буде зроблено основні витрати на власне саму реалізацію. Альтернативний підхід полягає в тому, аби, виконуючи кроки по уточненню специфікації, вірність яких можна довести, перетворити специфікацію на реалізацію, яка буде вірною через побудову.

Важливо зазначити, що проєкт (або реалізацію) ніколи не можна вважати «вірним» окремо, але, лише «вірним по відношенню до вказаної специфікації».