程度問題だよ
少なくとも俺にとってはVDMとりわけVDM++は
仕様を記述するには気が利かないし面倒くさ過ぎる
そのくせ証明による検証も大して期待できない

勿論そう思わない人もいるだろう
そういう人は是非とも形式仕様記述を活用して普及に努めてもらいたい