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%。