形式驗證(formal verification)是一種基於數學技術的驗證方法，用於確保設計的正確性和功能的完整性。
這種驗證方法主要應用於硬件和軟件設計領域，通過使用數學推理和靜態分析來證明設計實現是否滿足其規格和要求。形式驗證的主要技術包括等價性驗證、模型檢驗和定理證明。等價性驗證用於確認設計實現與設計規格是否等價；模型檢驗通過檢查模型的所有可能狀態來證明系統是否滿足某些屬性；定理證明則基於更廣泛的數學原理來驗證設計的正確性。
形式驗證的優點包括能夠進行全面覆蓋，發現設計中的歧義和邊界條件下的隱藏問題，且不需要創建仿真平臺和測試向量，從而縮短驗證週期。然而，由於其複雜性和計算成本，形式驗證通常適用於較小或較簡單的系統，對於大型軟件程序如操作系統來說，形式驗證的實施非常困難。