决策财经 IF9.CN 消息，1 月 7 日，分片项目 Elrond 宣布正在使用运行验证（Runtime Verification）来完成一组基于 K 框架的正式工具来补充和完善 Elorand 开发工具包。K 框架是由 Elrond 顾问 Grigore Rosu 首创的，他是计算机科学博士，在美国国家航空航天局 (NASA) 担任研究员期间，服务于火箭和航天器的安全关键环境。Grigore 随后发现了运行验证，并与他的团队一起致力于让这些火箭科学工具能够被区块链开发者使用。经过几个月的合作，Elrond 团队已经能够创建一个名为 KArwen 的 Arwen VM 的 K-Framework 副本。Arwen 是一个 WASM 虚拟机，因此运行验证能够为 WASM 扩展其 KWasm 语义以适应 Elrond 的虚拟机。此外，使用 K 框架的 Mandos 测试已经允许开发人员在较低的级别上执行代码覆盖测试。运行时验证工具通过识别和删除 Rust 编译器自动添加的未使用的功能，能够帮助将用 Rust 编写的智能合约的占用空间减少 40%。