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