1月7日消息，分片項目Elrond宣布正在使用運行驗證（Runtime Verification）來完成一組基於K框架的正式工具來補充和完善Elorand開發工具包。 K框架是由Elrond顧問Grigore Rosu首創的，他是計算機科學博士，在美國國家航空航天局(NASA)擔任研究員期間，服務於火箭和航天器的安全關鍵環境。 Grigore隨後發現了運行驗證，並與他的團隊一起致力於讓這些火箭科學工具能夠被區塊鏈開發者使用。經過幾個月的合作，Elrond團隊已經能夠創建一個名為KArwen的ArwenVM的K-Framework副本。 Arwen是一個WASM虛擬機，因此運行驗證能夠為WASM擴展其KWasm語義以適應Elrond的虛擬機。此外，使用K框架的Mandos測試已經允許開發人員在較低的級別上執行代碼覆蓋測試。運行時驗證工具通過識別和刪除Rust編譯器自動添加的未使用的功能，能夠幫助將用Rust編寫的智能合約的佔用空間減少40%。