社会におけるソフトウェアの重要性が高まり，開発における効率および信頼性がより強く求められている中，形式仕様に対する注目が産業界でも高まってきている．形式仕様においては，「作りたいシステム」を厳密な文法・意味論の定まった言語で記述することにより，曖昧さや不完全さが排除されるとともに，特にツールによる科学的・系統的な分析・検証が可能となる．本稿においては，形式仕様の基本的な考え方を解説する．この解説においては特に，抽象的な仕様モデルから「正しいことがわかっているプログラム」を導出する手法であるBメソッドの記述例を示す．本稿ではさらに，他の手法や適用事例，研究事例，最近の動向についても俯瞰する．