在硬件和軟件系統的背景下，形式化驗證是使用數學的形式化方法，證明或反駁系統所依據的預定算法在某種形式化規范或屬性方面的正確性的行為。形式化驗證有助于證明系統的正確性，例如：加密協議、組合電路、帶有內部存儲器的數字電路以及以源代碼形式表達的軟件。這些系統的驗證是通過在系統的抽象數學模型上提供形式化證明來完成的，數學模型和系統的性質之間的對應關系是通過構造知道的。經常用于系統建模的數學對象的例子有：有限狀態機、標記過渡系統、Petri網、向量加法系統、定時自動機、混合自動機、過程代數、編程語言的形式語義，如操作語義、指稱語義、公理語義和Hoare邏輯。

一種方法和形成是模型檢查，它包括對數學模型進行系統的詳盡探索（這對有限模型來說是可能的，但對一些無限模型來說也是可能的，因為無限的狀態集可以通過使用抽象或利用對稱性而有效地被有限地表示）。通常，這包括探索模型中的所有狀態和轉換，通過使用智能和特定領域的抽象技術，在一次操作中考慮整組狀態并減少計算時間。實施技術包括狀態空間枚舉、符號狀態空間枚舉、抽象解釋、符號模擬、抽象細化。要驗證的屬性通常用時間邏輯描述，如線性時間邏輯（LTL）、屬性規范語言（PSL）、SystemVerilog斷言（SVA）或計算樹邏輯（CTL）。模型檢查的xxx優點是它通常是全自動的；它的主要缺點是它一般不能擴展到大型系統；符號模型通常被限制在幾百比特的狀態，而顯式狀態枚舉要求被探索的狀態空間相對小。另一種方法是演繹驗證。它包括從系統和它的規范（可能還有其他注釋）中生成數學證明義務的集合，這些義務的真實性意味著系統符合其規范，并使用證明助手（交互式定理證明器）（如HOL、ACL2、Isabelle、Coq或PVS）或自動定理證明器來履行這些義務，特別是包括可滿足性模數理論（SMT）解決器。這種方法的缺點是，它可能需要用戶詳細了解系統正確工作的原因，并將這些信息傳達給驗證系統，其形式可以是有待證明的定理序列，也可以是系統組件（如函數或程序）和可能的子組件（如循環或數據結構）的規范（不變量、前提條件、后置條件）。

軟件程序的形式化驗證包括證明一個程序滿足其行為的形式化規范。形式化驗證的子領域包括演繹驗證（見上文）、抽象解釋、自動定理證明、類型系統和輕型形式化方法。一個有前途的基于類型的驗證方法是依賴類型的編程，其中函數的類型包括（至少是部分）這些函數的規范，類型檢查代碼根據這些規范建立其正確性。全功能的依賴類型語言作為一種特殊情況支持演繹驗證。另一種補充方法是程序推導，通過一系列保持正確性的步驟，從功能規范中產生有效的代碼。這種方法的一個例子是Bird-Meertens形式主義，這種方法可以被看作是另一種形式的構造正確性。

這些技術可以是健全的，也就是說，被驗證的屬性可以從語義中邏輯推導出來，或者是不健全的，也就是說，沒有這樣的保證。健全的技術只有在覆蓋了整個可能性的空間之后才會產生結果。一個不健全的技術的例子是，它只覆蓋了可能性的一個子集，例如只覆蓋了某個數字以下的整數，并給出了一個足夠好的結果。技術也可以是可判定的，也就是說，它們的算法實現可以保證以一個答案結束，或者是不可判定的，也就是說，它們可能永遠不會結束。通過限定可能性的范圍，當沒有可判定的健全技術可用時，可判定的不健全技術就能夠被構造出來。