Кто-нибудь пробовал писать формальные спецификации на языках типа Z, EventB, Alloy и т.п.? Мне кажется, что в последнее время наблюдается рост интереса индустрии к этой теме, особенно в областях связанных с security и safety, например:

• seL4 - ядро операционой системы, реализация которого формально верифицирована на соответствие спецификации с помощью Isabelle;
• проекты, использующие Alloy;
• проекты, использующие EventB.

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