Метод анализа спецификаций и проектных решений систем с использованием моделей и свойств, поддающихся логической проверке.
Hillel Wayne представляет принципы формальных методов для обнаружения дефектов проектирования до реализации системы, уделяя внимание силе свойств, исследованию пространства состояний и предположениям о среде. Примеры показывают, как упрощённый анализ параллелизма, отказов и повторных попыток может заранее выявить дорогостоящие ошибки.