形式化方法是一種基於嚴格數學基礎的系統開發方法，它通過使用數學和邏輯證明的手段對計算機系統進行建模、規約、分析、推理和驗證。這種方法旨在保證設計的正確性，提高系統的可信度和正確性，並使系統具有良好的結構、易維護，並能較好地滿足用戶要求。形式化方法的主要內容包括形式化規約和形式化驗證技術。
形式化規約是對系統需要達到的功能和性質的數學描述，它是系統設計的出發點，也是驗證系統是否正確的依據。通過形式化描述，可以儘早發現需求和設計中的錯誤。形式化規約的方法主要可分為兩類：一類是對系統建模，該方法的目的是用合適的數學工具建立系統模型，藉此精確地刻畫系統的行為特徵；另一類是性質描述，該方法的目的是用合適的數學工具來描述系統的性質，藉此對系統進行深入的研究。
形式化驗證技術則是通過數學邏輯證明來驗證系統是否滿足形式化規約中的要求。它包括定理證明、模型檢測等技術，用於確保系統設計的一致性和正確性。
形式化方法的套用逐漸融入軟體開發過程的各個階段，從需求系統分析、功能描述、體系結構/算法設計、編程、測試直至維護。它主要包括形式化規約和形式化驗證技術，以及定理證明、模型檢測等技術。形式化方法的主要研究方向包括定理證明、形式模型、形式語義與形式建模、形式規約、形式驗證技術等。