當且僅當大多數驗證者將 B0 與其 K 代子孫檢查點 Bk 關聯起來，則 B0 獲得 K 階終局性（k > 0），且 B0 與 Bk 之間的所有檢查點都被終局化。注意，創世區塊本身被認為既已得到合理化，又有終局性。下圖演示了 Gasper 中的合理化和終局化概念。
罰沒條件（Slashing Conditions）
如果驗證者嘗試偏離協議要求、提交自相矛盾的投票，則該驗證者會被懲罰：其保證金會被扣除一大部分。Gasper 定義了兩個條件（也稱罰沒條件）來定義何謂自相矛盾的投票：
1.雙重投票（Double-voting）：驗證者釋出了兩個截然不同的投票，但兩個投票的目標高度是同一個高度。
2.環繞投票（Surround-voting）：驗證者釋出的一個投票所關聯的兩個檢查點恰好在自己所釋出的另一個投票的兩個檢查點高度範圍內。
發起雙重投票的驗證者被認為違反了第一罰沒條件；而發起環繞投票的驗證者則違反了第二罰沒條件。不論是哪種情況，違反規則的驗證者都會被扣除大量保證金。
正確性（Correctness Properties）
與其它拜占庭容錯型（Byzantine Fault Tolerance，BFT）協議相同，Gasper 協議的一個關鍵底層假設是絕大多數驗證者（超過 2/3，以保證金數量定義）是誠實的、會遵循協議的要求。在此假設下，Gasper 有兩大基本屬性：
· 可追責的安全性（Accountable Safety）：不會有兩個屬於不同分叉的區塊都被終局化，除非有至少 1/3 的驗證者（以保證金數量計）被罰沒；
· 似然活性（Plausible Liveness）：無論區塊鏈過往發生了什麼事，區塊的終局化程序永遠不會陷入僵局。
此外，在驗證者集合會動態變化的環境（因為驗證者會離開網路，也會有新驗證者加入，活躍驗證者集合可能會發生改變）中，第三種屬性量化了在有人違反協議規則時可被罰沒的保證金體量：
· 可罰沒下限（Slashable bound）：只要能夠使用協議外條件來控制驗證者的啟用和退出引數條件，就能證明（在打破安全性時）可被罰沒的保證金數量有一個下限。
動態驗證者集合（也即信標鏈協議所實現的）引入了另一個有挑戰性的問題：系統不再那麼能夠可靠地懲罰惡意驗證者，因為他們可能會在作惡之後、保證金被實際罰沒之前離開網路。而可罰沒下限屬性使得調整活躍驗證者集合的可變幅度、維持最低水平的可追責性成為可能。
驗證 Gasper 的終局性
Gasper 旨在為終局性提供一個數學化的、精確的、可用來形式化地證明其正確性的描述；這種正確性也是證明信標鏈協議安全性的關鍵。以太坊平臺正日漸被用作大型金融交易系統的股價，更突出了安全性保證的前所未有的重要性。
與以太坊基金會通力合作，我們已經使用 Coq 證明助手，形式化了 Gasper 在動態驗證者集合一般條件下的終局性機制。我們在這一條件下指出並證明了 Gasper 的所有三種關鍵屬性：可追責的安全性、似然活性以及可罰沒下限；所有證明都使用了同一個 Coq 模型。
對協議的演繹論證給了我們對相關主張正確性和安全性的極大信心，因為演繹論證保證沒有未經指明的假設，也沒有無效的演繹推理步驟。它也明確了為使論點成立所需的所有假設。形式化過程也能反哺協議的描述，使協議的描述能更準確、更完整。
這裡我們僅對這一成就給出概要的說明。完整的細節可見：
1. 該專案的技術報告
2. 該專案的 Github 程式碼庫
建模及驗證方法
第一步是開發一個協議的模型，讓我們能夠表達出所有我們希望形式化地指出並證明的關鍵屬性。這個模型建立在我們之前驗證 Casper FFG 的安全性和活性的工作基礎上（此前的模型已經定義了 Gasper 終局性機制的早期版本）。
這一模型有三個主要的結構化模組：
驗證者和團體（Validators and quorums）。驗證者被抽象地表示為一個有限型（finite type）的成員（成員數量有限，而且可以列舉），寫為 Validator : finType 。每個驗證者都有一份保證金；這一事實我們建模成一個未解釋的函式 stake : {fmap Validator -> nat}，儲存驗證者與其保證金數量（一個自然數）的對映。此外，給定一個驗證者集合，其權重 wt 定義為該集合中所有驗證者保證金數量的總和：
\sum 是求和運算子；stake.[st_fun v] 則給出了相應於驗證者 v 的保證金數量（st_fun 即假設每個驗證者都必須在系統中有一份保證金）。
wt 函式的幾個屬性源自其定義，例如：空驗證者集的權重必然為 0，兩個互不相交的集合的合集的權重就是各自權重的和。這些屬性在涉及可罰沒下限屬性中關於權重的推理時會派上用場。
此外，因為我們要模擬動態的驗證者集合，也就是活躍驗證者的集合可能會隨區塊發生改變，我們宣告瞭一個抽象的（有限）對映 vset : {fmap Hash -> {set Validator}}，給出一個區塊處的活躍驗證者集合。現在，使用 vset 和 wt，我們就能定義什麼是絕對多數集合：
在某個區塊處，如果活躍驗證者集合的一個子集的權重超過整個集合權重的 2/3，則該子集就是一個絕對多數集合。
區塊樹。我們用區塊雜湊的有限型來模擬一個區塊 Hash:finType，另外，用 genesis 代表創世區塊。我們使用符號 h2 <~ h2 這樣的符號來表示區塊父子關係（ h2 就是 h2 的父輩），以此模擬檢查點區塊樹。
接下來我們使用 h2 <~* h2 來定義祖先關係，h2 就是 h2 的祖先，而 h2 就是 h2 的後代（h2 和 h2 可以是同一個區塊）。至於祖先關係的屬性，比如祖先的祖先也是祖先，與父子關係的屬性類同。
全域性狀態。狀態可表示為由合理化投票組成的有限集合，投票的形式是 (v, s, t, s_h, t_h)，而 v 是發起投票的驗證者，s 和 t 是 TA 支援的來源區塊和目標區塊，而 s_h 和 t_h 是它們的見證高度（attestation height）。某一個投票是否有人發起過可透過一個布林成員斷言確定：
例項規範
基於這些定義以及它們相應的屬性，我們定義出了模型中的所有其它結構和屬性，包括罰沒條件、團體交集屬性（quorum intersection property），還有合理化以及終局化。舉例而言，在一次違反協議的事件中，罰沒某個團體的屬性可使用如下的抽象成員約束而得到定義：
該命題指出，罰沒一個團體意味著，在某些區塊 bL 和 bR 處存在著兩個絕對多數團體 vL 和 vR，這兩個團體的交集就是被罰沒驗證者（發起了雙重投票或者環繞投票）的完整集合。注意，在活躍驗證者集合一直固定的特殊條件下，這些絕對多數集合的交集的權重至少是所有保證金的 1/3。
另一個例子是一個終局化分叉（即違反安全性的情形）的定義：
該命題指出兩個相互矛盾的區塊 b1 和 b2 都被終局化了（因為 b1 和 b2 都不是對方的祖先區塊）。這兩個區塊可以是在任意合理化高度的時候被任意長的鏈終局化的。
這些定義和結果組中被用來指出和證明可追責的安全性、似然活性以及可罰沒下限三種定理。為清楚起見，我們還用下式重新定義了可追責安全性定理的表述：
這個定義很簡單，只是說：如果安全性被打破（出現了任何被敲定的分叉），那必定意味著某個驗證者集合會被罰沒。這個證明機械化了 Gasper 給出的非正式論證，並展示了為什麼分叉獲得終局化就意味一定有兩個絕對多數團體違反了其中一條罰沒條件，因此其交集可被罰沒。
我們的技術報告描述了形式化過程以及這些屬性的證明，而我們的專案程式碼庫提供了完整的詳述。
繼續前進
在本文中，我們講解了 Runtime Verification 與以太坊基金會合作成就的第一部分。這第一部分乃是（在驗證者集合會動態變化的條件下）形式化 Gasper 並證明其關鍵的三種屬性：可追責的安全性、似然活性以及可罰沒下限。我們成就的第二部分，在本文中還未涉及的，是展示如何將這些結果代入更加精細的模型（用 K 框架寫就）中，給出一個信標鏈狀態轉換函式的抽象版本。我們後面會用另一篇文章來展示這一成果。
完成這個里程碑還意味著我們向這場合作的終極目標（形式化地證明信標鏈協議滿足所有三種關鍵屬性、並能清楚地宣告一個非常接近於協議詳述的抽象版本所需的所有假設）邁出了重要的一步。
我們期待在這項工作上與以太坊基金會繼續合作。在這次接觸中，我們對以太坊基金會的幾位專家深為感激：Danny Ryan、Carl Beekhuizen、Martin Lundfall、Yan Zhang 以及 Aditya Asgaonkar。
