軟體開發中一般使用「測試」來找bug，這種方法只能找到bug，不能證明程式沒有bug。
形式化驗證是用邏輯來驗證程式的可靠性，就是把一段程式用邏輯的方法證明一遍，證明它能得到預期的結果，沒有bug。一般這類研究主要應用於昂貴的航天器材的作業系統、危險的醫療裝置的程式之中。因為航天器材、醫療裝置牽扯到人的生命，如果作業系統出現錯誤，那麼很危險，又不能用測試一遍一遍的測，所以用形式化驗證來做。比如美國航天局nasa就會僱傭大批形式化驗證的專家來驗證他們作業系統的正確性。
學習這個方向，最好有比較好的邏輯知識（數理邏輯、拉姆達驗算），最好比較了解程式（比如作業系統的設計、編譯器的設計等）。
這個方向是比較犀利的研究方向，但不大容易出**，需要長時間積累才能發一篇好**。
這個方向只是科研方向，不適合找工作，如果你讀完碩士打算找工作而不做研究，這個方向不適合。因為企業沒人用形式化驗證來驗證程式。
formal verification（形式驗證)
在計算機硬體（特別是積體電路）和軟體系統的設計過程中，形式驗證的含義是根據某個或某些形式規範或屬性，使用數學的方法證明其正確性或非正確性。
形式驗證是乙個系統性的過程，將使用數學推理來驗證設計意圖（指標）在實現(rtl)中是否得以貫徹。形式驗證可以克服所有3種**挑戰，由於形式驗證能夠從演算法上窮盡檢查所有隨時間可能變化的輸進值。
形式驗證的出現
由於**對於超大規模設計來說太耗費時間，形式驗證就出現了。當確認設計的功能**是正確的以後，設計實現的每乙個步驟的結果都可以與上個步驟的結果做形式比較，也就是等價檢查，如果一致就說明設計合理，不必進行**了。
形式驗證主要是進行邏輯形式和功能的一致性比較，是靠工具自己來完成，無需開發測試向量。而且由於實現的每個步驟之間邏輯結構變化都不是很大，所有邏輯的形式比較會非常快。這比**的時間要少很多。一般要做形式驗證的步驟有：rtl和rtl。
ic設計驗證方法
形式驗證（formal verification）是一種ic設計的驗證方法，它的主要思想是通過使用形式證明的方式來驗證乙個設計的功能是否正確。形式驗證可以分為三大類：等價性檢查（equivalence checking）、形式模型檢查（formal model checking）（也被稱作特性檢查）和定理證明(theory prover) 。
等價性檢查的驗證用於驗證rtl設計與門級網表、門級網表與門級網表是否一致。在進行掃瞄鏈重排、時鐘樹綜合等過程中，都可以用等價性檢查保證網表的一致性。等價性檢查已經融入ic標準設計流程中。等價性檢查在檢查eco時非常有用。例如，設計者在修改門級網表時，由於手誤，錯將乙個或門寫成或非門，等價性檢查工具通過比較rtl設計與門級網表，可以很容易地發現這種錯誤。
模型檢查用時態邏輯來描述規範，通過有效的搜尋方法來檢查給定的系統是否滿足規範。模型檢查是目前研究的熱點，但其驗證的電路規模受限制這一問題還沒有得到很好的解決。
定理證明把系統與規範都表示成數學邏輯公式，從公理出發尋求描述。定理證明驗證的電路模型不受限制，但需要使用者的人工干預和較多的背景知識。
軟體設計驗證方法
形式化驗證過程可以證明乙個系統不存在某個缺陷或符合某個或某些屬性。軟體測試無法證明系統不存在缺陷，也不能證明它符合一定的屬性。系統無法被證明或測試為無缺陷，這是因為不可能形式地規定什麼是「沒有缺陷」。所有可以做的，就是證明乙個系統沒有任何可以想到的缺陷，並且滿足所有的使系統符合功能要求的和有用的屬性。
形式驗證工具：
synopsys的formality
cadence lec(logic equivalence check)
形式驗證的優點
1. 由於形式驗證技術是借用數學上的方法將待驗證電路和功能描述或參考設計直接進行比較，因此測試者不必考慮如何獲得測試向量。
2. 形式驗證是對指定描述的所有可能的情況進行驗證，而不是僅僅對其中的乙個子集進行多次試驗，因此有效地克服了模擬驗證的不足。
3. 形式驗證可以進行從系統級到門級的驗證，而且驗證時間短，有利於盡早、盡快地發現和改正電路設計中的錯誤，有可能縮短設計週期。
驗證實現工作包括將多種輸進條件定義為測試計畫的一部分、建立功能覆蓋模型、開發測試平台、建立輸進激勵發生器、編寫指導性測試以及執行測試、分析覆蓋率指標、調整激勵發生器以面向未驗證的設計部分，然後反覆這一過程。
形式驗證補充了模擬驗證的不足，二者各有優勢，互為補充，缺一不可。
**是一種基於經驗的模擬驗證方法，通過反覆試驗試圖查明缺陷，這要花相當多的時間嘗試所有可能的組合，因此永遠不會完整。另外，由於工程師必須定義和產生大量輸進條件，他們的工作重點將是如何在非設計目標基礎上分解設計。
形式驗證是窮盡式數學技術，使工程師僅關注設計意圖。純形式驗證技術與**驗證相反，專注於證實模組的端到端、直接對應微架構規範的高層要求，幫助使用者戲極大進步專案的設計和驗證產能，同時確保正確性。
區塊鏈時代 形式化驗證的應用
區塊鏈時代，智慧型合約的安全性被無限放大，乙個小小的bug就能導致上億美元的損失。美鏈 bec 近日被爆出安全漏洞，被黑客用以太坊erc 20智慧型合約中batchoverflow漏洞攻擊，引發 閃崩，當日幣價幾乎歸0。除了美鏈，據英國和新加坡的研究人員統計，超過34000個智慧型合約都有可被利用的...
形式化驗證工具之離線免費版Beosin VaaS
形式化驗證工具之離線免費版beosin vaas 儘管筆者認為離線免費版beosin vaas的功能已足夠強大，但根據官方發布的訊息，對於一些複雜型別的業務合約 以及對安全性要求高的業務合約，比如數字金融類 如defi 物流 鏈類 跨境支付類 防偽溯源類等等，還是建議選擇企業版beosin vaas...
區塊鏈智慧型合約及形式化驗證平台 VaaS 講解
2017年7月20號，parity 的多簽名錢包合約被曝漏洞，導致3200萬美元的數字貨幣被盜，甚至連 dao bec 這樣的著名專案市值也出現了一夜歸零的慘痛事件，而所有代幣都由智慧型合約生成，所以，毫無疑問，智慧型合約是區塊鏈生態安全中最重要的一環，越來越多的人逐漸意識到區塊鏈智慧型合約安全的重...