區塊鏈技術與智慧合約的結合提供了誘人的前景：為具有嚴格安全要求的應用程式（如財務，安全訊息傳遞等）啟用分散式，可信任且可驗證的計算平臺。不幸的是，人們不必很難看出，區塊鏈的實現道路還是充滿很多不知因素，例如Gox，DAO，對以太坊經典版的攻擊以及智慧合約bug。儘管從理論上講區塊鏈系統可能聽起來不錯，但在實踐中，區塊鏈系統和智慧合約仍然很容易出現開發人員bug。
區塊鏈系統的支持者必須捫心自問的問題是：我們如何才能挽救（a）區塊鏈技術在構建新一類分散式系統方面的承諾，以及（b）它在警惕的公眾眼中的聲譽？顯然，這是一個多方面的問題，不能在一篇文章中完全解構。但是在本系列文章中，我們將論證形式驗證（以下更多內容）將在應對這兩個挑戰（a）-（b）中發揮越來越重要的作用。
該系列文章涉及適用於區塊鏈系統和智慧合約的形式驗證。在第一篇文章中，我們希望對形式化驗證（沒有具體提及區塊鏈或智慧合約）以及為什麼需要它提供一個概括而溫和的介紹。在以後的文章中，我們將詳細介紹技術細節。除了介紹之外，讓我們開始吧！
無論是建立業務，產品還是軟體系統，您都必須回答以下問題：我們的系統是否滿足我們的基本要求？這個問題涉及兩部分：
1. 待驗證的系統
2. 需求清單
我們稱此為回答問題驗證的過程。完整的驗證意味著檢查系統是否滿足其所有要求，即透過檢查所有可能的情況，檢查系統是否完成了它應該做的所有事情，而沒有做不應該做的事情。這就引出了一個重要的問題：我們如何驗證我們的系統？
如果您向大多數軟體開發人員詢問此問題，他們將透過一些不同的測試來回答。什麼是測試？測試是我們採用系統並詢問自己是否的過程。如果我們從某些初始條件開始（例如，我們的Web伺服器具有1 GB的RAM），我們能否達到預期的效果？答案當然取決於我們正在研究的系統。不幸的是，透過新增更多的測試用例來擴充套件測試功能只能確保對最簡單的系統進行完整的驗證，因為這些系統對複雜性有固定的限制。
作為一個簡單的例子，考慮必須為許多使用者服務的Web應用程式，例如銀行網站。理論上可能有多少套初始條件？顯然，同時服務5個使用者不同於同時服務6個使用者。無限期地應用此引數，請注意由於單個輸入變數（即同時使用的使用者數），我們已經可以考慮無數種情況。
這正是驗證（特別是形式驗證）可以提供幫助的地方。
形式驗證通常不使用顯式狀態（如我們上面所使用的那樣），而是使用符號輸入變數（例如如果我們的網站有n個同時使用者怎麼辦？）以及相關係統的精確數學模型。從本質上講，我們將驗證問題轉化為精確的數學命題，然後使用數學證明來證明該命題的正確性。
這是形式驗證的主要優點：當一個命題被正式證明時，您就可以透過有限的測試步驟來驗證無限數量的測試用例。我們將從以下圖表開始調查如何（針對軟體系統）執行此操作：
在圖中，方框表示在驗證過程中產生的不同工件，而連線線表示從一種工件到另一種工件的轉換。實線表示保留所有基本資訊的轉換，而虛線表示有損轉換，可能丟失基本資訊。所有行均由執行所需轉換所需的實體註釋。在常規軟體開發中，開發人員（通常也是編譯器）一起將系統需求轉換為可執行程式碼。然後（可能是不同的）開發人員將採用相同的系統要求，並編寫掛接到可執行程式碼中的測試，以確保某些程式碼路徑返回期望的結果。這些測試有助於顯示我們的程式碼正確，但是我們已經知道測試還不夠。儘管測試可以證明存在bug，但是通常無法證明沒有缺陷。形式驗證的好處在於，我們可以證明我們的要求與系統規範之間的對應關係，即我們可以證明我們的原始碼沒有bug。
我們在此過程中使用的關鍵工具是語義。您可以將語義視為將程式碼對映為其數學含義的編譯器。我們使用的另一個關鍵工具是定理證明器，它只是一個計算機程式，可以幫助我們證明數學命題並避免粗心大意的bug。由於我們的形式化需求和形式化系統規範都是數學陳述，因此我們可以使用定理證明者來討論它們之間的關係。因此要回答這個問題：
我們怎麼知道我們的系統實現滿足我們的系統要求？
我們將思維轉移到形式化的數學領域，而是問：
定理證明者可以證明我們的形式化系統規範滿足我們的形式化要求嗎？
在接下來的三篇文章中，您將學習形式驗證如何將系統正確性問題從非正式的人類推理轉變為形式化的數學推理。結果，您將能夠在實踐中理解並享受採用正式驗證的好處：
精確。系統，形式和數學推理為我們提供了思考系統設計的精確語言；
自動化。許多重要的正式驗證任務都可以由計算機自動執行。這意味著我們可以考慮非常棘手的問題，這些問題對於人類來說是難以解決的。
置信度。當使用複雜的舊系統時，尤其是在不受信任的環境中（例如IoT /嵌入式系統等），正式驗證可以高度確保您沒有做錯事。
速度。 在設計新系統時，我們認為基於語義的形式驗證可以透過減少代價高昂的設計錯誤來加速系統設計和編寫良好程式碼的過程。
我們希望您對正式驗證有一個簡單的概述，並且您將加入我們的系列文章的下三篇文章，其中將放大基於語義的正式驗證過程的三個階段，如上圖所示，以及它們如何應用於區塊鏈系統：
（i）形式化需求
（ii）用於形式化驗證的定理證明工具
（iii）形式化系統語義。
