Elrond Initiates Cooperation With Runtime Verification — A Research and Development Company Specializing in Formal Methods
14th of July, 2019 — Elrond — the sharding-based public blockchain network is proud to announce a cooperation agreement with Runtime Verification for research and development in core areas of formal verification methods.
Elrond 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.
The Elrond research and development team will work closely with Runtime Verification to further develop the K framework and its capability to generate correct-by-construction Virtual Machines for the blockchain. Through the research and development initiative between Elrond and Runtime Verification we aim 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 or supporters include Ethereum, Algorand, IOHK, Casper, Maker DAO, Gnosis, Toyota and others.
“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.” says Grigore Rosu, CEO of Runtime Verification.
“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.” says Beniamin Mincu, CEO of Elrond.
About Elrond
Elrond is a new blockchain architecture, designed from scratch to bring a 1000-fold cumulative improvement in throughput and execution speed. To achieve this, Elrond introduces two key innovations: a novel Adaptive State Sharding mechanism, and a Secure Proof of Stake (PoS) algorithm, enabling linear scalability with a fast, efficient, and secure consensus mechanism. Thus, Elrond can process upwards of 10,000 transactions per second (TPS), with 5-second latency, and negligible cost, attempting to become the backbone of a permissionless, borderless, globally accessible internet economy.
Elrond is built by a team of experienced entrepreneurs along with 13 engineers and researchers with significant blockchain backgrounds and technical experience at Microsoft, Google, Intel, and NTT DATA. The team includes two PhDs in CS & AI, multiple math, CS, and AI Olympiad champions, and a former member of the NEM core team.
About Runtime Verification
Founded by Professor Grigore Rosu, Runtime Verification provides cutting-edge technology to design safe and secure systems and languages based on mathematically-grounded principles. Its technology not only detects the rarest, trickiest and most costly bugs lurking in existing codebases or specifications, but also stimulates the design and development of better programming and specification languages, where such costly bugs cannot exist by design or can be detected cheaply.
For more information, please visit us:
