Формальные методы

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

"Термин  формальные методы подразумевает ряд операций, в состав которых входит создание формальной спецификации системы, анализ и доказательство спецификаций, реализация системы на основе преобразования формальной спецификации в программы и верификация программ." [Соммервилл, 2002, стр. 188]

Большой список соответствующих инструментов, теорий приведен здесь.
Наглядная выборка:

• Z notation
  Язык описания программ, не привязан к конкретному ЯП
  
• Coq
  Система для доказательства теорем, синтеза функциональных программ
  
• Java Modeling Language
  Язык описания java программ, привязан к языку java
  
• Leon
  Язык описания и синтеза Scala программ
  

Нестрого, наверное, можно представить шкалу систематичности, на левом конце которой полностью интуитивное программирование, примитивные способы структурирования кода, а на правом - проработанные (но практически пока менее эффективные) теории вроде calculus of inductive constructions, refinement calculus. Так вот, интересуют методы из правой половины (видел, где-то здесь упоминали синтез конечных автоматов, например).