合約的形式化驗證方法

首先我們來個小科普——你知道什麼是形式化驗證方法嗎？

　　所謂形式化驗證方法，即指在計算機科學領域，特别是軟體工程和硬體工程中，一種特殊的基于數學的技術，用于規範、開發和驗證軟體和硬體系統，以提高系統的安全性、可靠性和魯棒性。形式化方法可以形容為建立在相當廣泛的理論計算機科學基礎上的應用，特别是邏輯演算，形式語言、自動機理論、離散事件動态系統和程式的語義，還包括類型系統和代數資料類型等理論。一般這類研究主要應用于昂貴的航空、航天、軍事器材的作業系統、危險的醫療裝置的程式之中。

形式化驗證的原理是什麼？

　　形式化驗證是一種基于數學和邏輯學的方法。具體來講，在智能合約部署之前，對其代碼和文檔進行形式化模組化，然後通過數學的手段對代碼的安全性和功能正确性進行嚴格的證明，可有效檢測出智能合約是否存在安全漏洞和邏輯漏洞。該方法可以有效彌補傳統的靠人工經驗查找代碼邏輯漏洞的缺陷。形式化驗證技術的優勢在于，用傳統的測試等手段無法窮舉所有可能輸入，而我們用數學證明的角度，就能克服這一問題。

形式化驗證跟傳統網際網路安全公司的做法有什麼不同？

　　傳統的網際網路安全公司是「以攻促防」，而形式化驗證是直接從代碼自身安全角度出發，來防止不安全事件發生。通俗舉個例子，就像一個是西醫，有病的時候給你治病，而一個是中醫，強調自身抵抗力的提升，自己身體更健康了，就很難生病了。

形式化驗證産品