有界模型檢查（Bounded Model Checking, BMC）

有界模型檢查是形式驗證的務實折衷：它不問「這性質會不會在無窮多週期的任何一個出錯？」，而是問「它會不會在接下來 k 個週期內出錯？」k 是某個固定深度。工具把設計邏輯連續展開 k 次——像把 k 份電路影本首尾相接攤開——將整體化成一條巨大的布林公式，交給 SAT 求解器。若求解器找到一組滿足解，那就是你的臭蟲，附帶確切輸入序列；若找不到，該性質至少在深度 k 之內是安全的。

BMC 擅長快速地找出淺層臭蟲——多數真實設計臭蟲在數十個週期內就會現形，而 BMC 會給出最短的反例。它的限制是「k 個週期內無臭蟲」並非完整證明；更深處、第 k+1 週期的臭蟲仍可能潛伏。要把 BMC 升級成完整證明，工程師會加入「k 階歸納法」（證明若性質連續 k 週期成立，下一週期就必成立），或把 k 推到設計的直徑——其狀態空間中最長的最短路徑——超過此值便不會出現新狀態。