在硬件和軟件系統的上下文中，形式驗證是使用形式數學方法證明或反駁系統下針對特定形式規范或屬性的預期算法的正確性的行為。

形式驗證可以幫助證明系統的正確性，例如：密碼協議、組合電路、帶有內部存儲器的數字電路以及表示為源代碼的軟件。

這些系統的驗證是通過對系統的抽象數學模型提供正式證明來完成的，數學模型與系統性質之間的對應關系通過構造已知。 經常用于對系統建模的數學對象的例子有：有限狀態機、標記轉換系統、Petri 網、向量加法系統、時間自動機、混合自動機、過程代數、編程語言的形式語義，例如操作語義、指稱語義、公理化 語義和霍爾邏輯。

一種方法和形式是模型檢查，它包括對數學模型的系統詳盡探索（這對于有限模型是可能的，但對于一些無限模型也是可能的，其中無限狀態集可以通過使用抽象或利用 對稱）。 通常，這包括探索模型中的所有狀態和轉換，通過使用智能和特定領域的抽象技術在單個操作中考慮整個狀態組并減少計算時間。 實現技術包括狀態空間枚舉、符號狀態空間枚舉、抽象解釋、符號模擬、抽象細化。 要驗證的屬性通常在時態邏輯中描述，例如線性時態邏輯 (LTL)、屬性規范語言 (PSL)、SystemVerilog 斷言 (SVA) 或計算樹邏輯 (CTL)。 模型檢查的xxx優點是它通常是全自動的； 它的主要缺點是它通常不能擴展到大型系統； 符號模型通常僅限于幾百位狀態，而顯式狀態枚舉則需要探索的狀態空間相對較小。

另一種方法是演繹驗證。 它包括從系統及其規范（以及可能的其他注釋）生成數學證明義務的集合，其真實性意味著系統符合其規范，并使用證明助手（交互式定理證明者）履行這些義務（ 例如 HOL、ACL2、Isabelle、Coq 或 PVS）或自動定理證明器，尤其包括可滿足性模理論 (SMT) 求解器。 這種方法的缺點是它可能需要用戶詳細了解系統為何正確工作，并將此信息以要證明的定理序列的形式或規范的形式傳遞給驗證系統（ 系統組件（例如函數或過程）和可能的子組件（例如循環或數據結構）的不變量、前提條件、后置條件）。

軟件程序的形式驗證涉及證明程序滿足其行為的正式規范。 形式驗證的子領域包括演繹驗證（見上文）、抽象解釋、自動定理證明、類型系統和輕量級形式方法。 一種有前途的基于類型的驗證方法是依賴類型編程，其中函數的類型包括（至少部分）那些函數的規范，并且類型檢查代碼確定其針對這些規范的正確性。 功能齊全的依賴類型語言支持演繹驗證作為一種特殊情況。

另一種補充方法是程序推導，其中通過一系列正確性保持步驟從功能規范中生成高效代碼。 這種方法的一個例子是 Bird-Meertens 形式主義，這種方法可以看作是另一種形式的構造正確性。

這些技術可以是可靠的，這意味著可以從語義中邏輯推導出已驗證的屬性，也可以是不可靠的，這意味著沒有這樣的保證。 一項完善的技術只有在覆蓋了所有可能性的情況下才會產生結果。 不健全技術的一個例子是僅涵蓋可能性的子集，例如僅涵蓋特定數量的整數，并給出足夠好的結果。 技術也可以是可判定的，這意味著它們的算法實現保證以答案終止，或者是不可判定的，這意味著它們可能永遠不會終止。 通過限制可能性的范圍，當沒有可判定的可靠技術可用時，可以構建可判定的不可靠技術。