Elrond, the recently launched sharding-based public blockchain network, has announced a new cooperation agreement with Runtime Verification for research and development in core areas of formal verification methods.
The Elrond team is using the K Framework, developed by Grigore Rosu while at NASA and the University of Illinois at Urbana Champaign, as the backbone for all of its smart contract languages. Grigore has continued development of K Framework with his team at Runtime Verification which specializes in formal methods.
Building on this, Elrond has developed an in-house GO backend to integrate the IELE VM, which is designed by the Runtime Verification team, and constructed entirely on the K Framework. Elrond is also working to integrate KEVM and WASM in a similar fashion. Having the VMs built using the K Framework gives Elrond access to powerful formal verification tools.
“We at Runtime Verification are very excited to see Elrond’s commitment to not only use, but also contribute to the development of the basic infrastructure of the K Framework. Although “formal verification” is now a buzzword in the blockchain community, in reality, few blockchain companies genuinely understand the critical, almost desperate need of formal specification and verification of smart contracts. And even fewer understand that this starts with the formal modeling of the programming languages and virtual machines, and that formal analysis tools tend to be buggy, too, unless they are derived from such formal models. Elrond takes security at heart and follows the best-known practices to assure safe and secure operation of their blockchain.”
– Grigore Rosu, CEO of Runtime Verification
Through the research and development initiative between Elrond and Runtime Verification, Elrond aims to take smart contracts to the next level, and to make the GO backend developed by Elrond for the K framework, open-source and available to the wide public.
Other Runtime Verification contributors and supporters include Ethereum, Algorand, IOHK, Casper, Maker DAO, Gnosis, Toyota and many others.
“Elrond brings a significant improvement to the blockchain space, setting new performance standards in terms of throughput and execution speed. In addition to performance, we believe dev tools and security measures like formal verification methods are instrumental for developers. Through the partnership with Runtime Verification, we intend to raise the security standard by adding formal verification to our smart contracts, while integrating K framework to support several VMs and smart contract languages at the same time.”
– Beniamin Mincu, CEO of Elrond