形式的仕様記述の有効性について、語るスレです。

プログラムやプロトコルの仕様の、
フォーマルな記述方法っていくつかありますが、
どれくらい有効なんでしょうか？

形式的仕様記述を有効活用するには、
どんな知識が必要なんでしょうか？

おめぇーら、知っていることを書け！