形式驗證（formal verification）是不像模擬那樣給予輸入圖樣來確認電路正確性，而是以數學手法加以證明之驗證方法的總稱。代表性的是等價性驗證（Equivalence Checking），例如全面證明 RTL（電路的行為描述）與其經邏輯合成後的閘級網表，對任何輸入都回傳相同輸出。其特長是即使是模擬無法在現實時間內測試所有輸入的大規模電路，也能進行毫無遺漏的確認。
等價性驗證在設計流程中會多次使用。（1）RTL 對閘級：確認邏輯合成工具在最佳化過程中沒有改變功能。（2）閘級對閘級：確認在插入掃描鏈、佈局繞線中插入緩衝器或替換元件、投片前修正（ECO）的前後，功能沒有改變。代表性工具有 Synopsys Formality、Cadence Conformal。
形式驗證還有另一種：屬性驗證（模型檢查）。描述「發出請求後必定回傳回應」「2 個訊號不會同時為 1」等應滿足的性質（屬性），並證明其在所有可到達的狀態下都成立。若找到反例，會直接顯示導致違規的輸入序列，因此擅長發現模擬中難以重現的深層邊界情況（corner case）錯誤。使用 Cadence JasperGold 等工具。
形式驗證並非萬能。要一次證明狀態數爆炸性增加的大規模電路整體相當困難，因此屬性驗證一般以區塊為單位套用。此外，能證明的是「是否符合所寫的規格」，無法找出規格本身的錯誤。因此實際的驗證會結合模擬（UVM 等）、形式驗證與硬體模擬（emulation）進行。