· 如果該區塊不屬於主鏈，則驗證者將對該區塊的分片投票。直觀上，分片是連結到信標鏈的獨立鏈，可以透過系統中的驗證者子集與狀態中的其他分片並行處理，從而顯著提高了系統一次處理更多交易的能力，從而提高了它的可擴充套件性（請參閱sharding和crosslinks）。
最後，遵循協議並做出明智決策的驗證者將獲得以太坊獎勵，以紅利形式分配，以鼓勵適當的行為。另一方面，偏離協議或行為不正常的驗證者可能會因拒絕或在某些情況下因削減其抵押的以太幣而受到處罰。這種獎勵懲罰系統有助於使惡意使用者在經濟上不可行，無法在該系統上發起成功的攻擊（請參閱《 Serenity設計原理》註釋）。
信標鏈當前由以太坊基金會開發的Python“以太坊2.0階段0 –信標鏈”的參考實現定義。
定義協議操作的實現的主要元件是信標鏈狀態轉換函式state_transition。該函式實現的相關部分的摘錄如下所示：
處理從創始狀態（已處理的創始信標區塊的狀態）開始。給定要處理的下一個信標區塊，並假定該區塊有效，信標鏈狀態轉換功能將給定的信標鏈狀態（前狀態）轉換為新狀態（後狀態）。此後狀態反映了以下結果：
· 考慮（可能）丟失的區塊； （process_slots）;
· 處理區塊的內容（process_block）。
在K中建模信標鏈
我們在這項工作中的目標是建立一個信標鏈的形式模型，該模型儘可能與“以太坊2.0階段0規範”給出的參考實現相對應，從而實現以下功能：
· 模擬或設定信標鏈狀態轉換函式的執行。
· 從信標鏈測試套件執行現有測試。
· 分析現有測試套件的程式碼覆蓋率，並透過新測試進行改進。
K是實現此目標的非常合適的框架，因為它能夠開發信標鏈的形式模型，其特徵是：
1. 可透過K工具中的模式重寫來執行，因此可以直接從規範中獲取信標鏈狀態轉換函式的直譯器（無需任何額外費用）。
2. 具體而言，其規範直接對應於系統的Python實現（對某些特定的抽象進行模化，例如簽名驗證）。
K模型也為更復雜的驗證任務（例如可達性分析和演繹驗證）奠定了基礎，但這是正在進行的工作和將來的工作的一部分，將在其他地方進行介紹。
該專案的github儲存庫中提供了k中模型的完整規範，以及一份更詳細地描述這項工作的技術報告。https://github.com/runtimeverification/beacon-chain-spec
信標鏈是如何用k建模的？
通常信標鏈在K中建模為狀態轉換系統，其狀態為信標鏈狀態，其轉換由主信標鏈狀態轉換函式定義。
在K中，信標鏈狀態被指定為由（可能巢狀的）單元組成的配置，其中每個單元代表定義協議所需的配置的語義元素。 例如下面的摘錄顯示了<beacon-chain />配置的兩個單元：<k />單元是用於儲存要執行的程式（計算）的一個特殊的單元，而<state />單元是包含信標鏈狀態的所有結構元素（下面僅顯示三個，三個點表示省略的單元格）：
信標鏈狀態轉換功能由K中的運算子指定，該函式將由當前信標鏈配置建模的信標鏈前狀態轉換為由結果K配置建模的信標鏈後狀態。 運算子宣告如下：
如上所述，涉及兩個主要的連續步驟：process_slots和process_block。命令在k中的排序自然指定為使用運算子~>，將計算疊加在一個連續項上。例如使用以下k規則定義狀態轉換函式：
只有當process_slots成功終止時，才會進行由process_block定義的下一次計算，該計算將捕獲預期的語義。
在開發轉換函式的語義規範時，我們面臨的挑戰之一是python語義豐富的表示式和大多數指令式程式設計風格與k語言定義的構造和宣告式規範風格之間的不匹配。在這一發展過程中，我們已經確定了一些模式以及如何在k中優雅地指定它們，例如如上所述的用於排序的堆疊計算結構。其他模式更復雜，不匹配更明顯，例如列表理解表示式，它們在Beacon鏈的引用實現中被大量使用。在這些情況下，這種編碼通常相當冗長，但如果不用k定義中間語言結構，就無法避免。然而，其優點是，這種編碼容易實現更詳細的覆蓋率分析。
驗證模型
以太坊基金會為信標鏈提供了豐富的測試套件。 除了用作Python實現的除錯工具之外，第三方生產客戶開發人員還使用測試套件來確保與參考實現一致。 該測試套件包含3,000多種不同的單元測試。
在給定的開發K模型抽象級別，可以在模型中直接執行信標鏈的標準測試套件中的測試，而無需任何工具。這證明是非常有價值的，因為它提供了一種機制來驗證模型，並確保模型符合參考實現，就像驗證其他生產實現一樣,按照專案資源庫中的說明，所有測試都可以自動執行。
擴充套件測試覆蓋範圍
標準信標鏈測試套件的設計使程式碼覆蓋率最大化，可以使用Python的可用程式碼覆蓋率分析工具。 但是Python的覆蓋範圍通常比較粗略。它不會區分執行語義豐富的Python構造（例如列表理解表示式）的各個分支。
K提供了不同的基於規則的覆蓋率分析工具。它檢測執行中是否應用了規則（如果適用，則應用了多少次）。 使用這種基於K的工具進行語義覆蓋已經證明在其他語言（例如JavaScript）的環境中很有用，我們在所有瀏覽器中都發現了新的錯誤（這些結果在PLDI’15論文中進行了描述）。
因此該計劃是評價標準的Python程式碼覆蓋率如何確保語義覆蓋面，看是否基於規則的覆蓋分析可能暴露不是由標準的Python程式碼覆蓋工具檢測到任何未覆蓋的功能。 確實分析顯示測試未涵蓋或未充分涵蓋的執行路徑，而Python覆蓋率未檢測到這些執行路徑 這些檢測中的大多數都屬於複雜行為的規範，例如列表理解表示式和複雜迴圈中通常遇到的行為。
以下是K覆蓋率工具生成的覆蓋率分析報告的快照，顯示了未在測試套件的任何測試中應用的規則。
繼續向前
信標鏈的可執行k模型是實現正式驗證信標鏈的基本安全性和活性特性及其參考實現這一最終目標的第一步，但也是至關重要的一步。事實上，如果沒有一個可信的、形式化的系統模型來驗證，形式化驗證的問題是沒有意義的。除了能夠執行狀態轉換函式、執行測試和分析測試覆蓋率之外，本文提出的k形式化模型還可以用來描述和驗證在這種低抽象級別上可表示的低階別不變數。
但是信標鏈是一個非常複雜的協議。在這種較低的抽象級別上直接驗證高階屬性（如安全性和活動性）通常是不可行的。相反，通常使用抽象細化技術。因此我們的計劃如下：
· 建立此具體模型的抽象，該模型保留協議的核心共識機制；
· 在抽象模型上證明所需的屬性；
· 表明這些屬性保留在具體模型中；
