使用模型檢測技術來進行系統設計的驗證包含三個步驟：
建模：第一步需要將設計轉化為能被模型檢測器接受的形式。在許多情況下這只是簡單的編譯過程，但在這些時候，由於驗證時間和計算機內存的限制，可能還需要使用抽象技術約簡不相關或不重要的細節來得到設計的形式化模型。
規約：在驗證前，需要聲明設計必須滿足的性質。性質規約通常是以某種邏輯的形式表示。對硬件與軟件系統驗證而言，通常使用時序邏輯規約系統的性質，這種邏輯體系能表示系統行為隨時間的變化。性質規約過程中最重要的問題是完備性。雖然模型檢測提供了檢測模型是否滿足給定性質的一套方法，但是這套方法並不能保證性質規約確切地表達了待驗證系統所需要滿足的所有性質。
驗證：理想中驗證過程應該是完全自動的。但是實際上它常常需要人的協助，其中之一就是分析驗證結果。當得到失敗的結果后，通常可以給用戶提供一個錯誤軌跡，可以把它看成所有檢測性質的一個反例，從而使設計者能夠跟蹤錯誤發生的具體位置。當分析錯誤軌跡並改正系統設計后，需求再次進行模型檢測，重新驗證，直到驗證通過。
錯誤軌跡也可能由模型建模或刻畫性質規約過程的失誤導致（常常稱為假否定），錯誤軌跡也能用於確定和修復兩類錯誤。另外，由於計算機的內存限制，當驗證過程需要大量內存時，驗證可能不會在有限實際內正常終止而產生錯誤軌跡。這種情況下，需要改變模型檢測器的若干參數或直接約簡模型，然后重新做驗證。