From Rockets To Blockchains: Formal Verification Pioneered At NASA Applied At Elrond Via Runtime Verification

Blockchains are verifiable computation platforms that lend themselves optimally to enabling the future of finance, business, and governance. This multi-trillion-dollar opportunity will however manifest fully only once it is predictably safe for complex processes to move on-chain.

Situations starting with the Ethereum DAO fork, to the present day frequent DeFi exploits, show that bugs, errors and insufficient testing present a very high risk to smart contract based processes. Mitigation is possible with proactive and reactive methods. Testing for instance, is great but is a rather reactive method. Exhaustive testing in complex scenarios is either impractical or impossible. The question is, can we create a development process which ensures correctness and security by design?

This is where formal methods come in. Formal methods allow for specifications for any process to be defined with mathematical precision and rigor. Once defined, the process goes through validation that formal expressions reflect what is actually desired, and verification that what is desired is secure, sound, and maps to the desired outcome.

Thus, formal verification can eliminate subtle bugs and logic flaws even from the design phase, provably demonstrating correspondence between requirements and specifications, creating the premise for a secure-by-design development process.

Enter Runtime Verification and Elrond

We are excited to announce that we are working with Runtime Verification to complement the Elrond dev toolkit with a set of formal tools based on K Framework.

“Formally verified smart contracts deployed on top of one another will add up to a virtuous stack of compelling DeFi primitives. By empowering its developers with such tools from the beginning, Elrond will establish better standards for security, and will hopefully accelerate the entire blockchain adoption process at scale.” said Beniamin Mincu, Elrond CEO.

The K Framework was pioneered by our friend and advisor, Grigore Rosu, Computer Science PhD, during his time as a NASA researcher, serving in the safety-critical environments specific to rockets and spacecraft. Grigore then went on to found Runtime Verification and is working with his team on making these rocket science tools usable by blockchain developers.

The goal of our collaboration is to create a toolset that allows developers to better write their code, immediately see and increase testing code coverage, and ultimately, add symbolic execution and even formally verify their Elrond smart contracts. Formal methods are relatively complex and difficult for the average developer, but our work together will focus on adding significant granularity to these tools, and lowering the barrier for immediate usage as much as possible.

“Elrond’s hardcore spirit is refreshing. They keep finding ingenious solutions to complex problems while moving forward with high speed. Adding formal tools to their internet-scale blockchain, seems like an important necessary step forward for adoption. It’s great to see our team collaborate and make this happen.” said Grigore Rosu, Runtime Verification Founder & CEO.

Progress milestones and next steps

After several months of working together, we already were able to create a K-Framework replica of our Arwen VM dubbed KArwen. Arwen is a WASM VM so Runtime Verification was able to expand their KWasm semantics for WASM to accommodate our virtual machine.

The resulting KArwen is a fully formalized auto-generated virtual machine that can execute Elrond Smart contracts. This lays the groundwork for advanced formal tooling to be used for the Elrond smart contracts. An important outcome is also that Mandos testing using the K Framework already allows developers to perform code coverage testing at a lower level than previously possible.

Runtime Verification’s tooling was able to help us reduce the footprint of Smart Contracts written in Rust by up to 40%, by identifying and removing unused functionality that the Rust compiler adds automatically.

The next steps of our collaboration will focus on more coverage tools for developers, and integrating the new tools with erdpy and our Elrond IDE to make them more easily accessible.

The Elrond semantics developed by Runtime Verification is already available in this repository: https://github.com/runtimeverification/elrond-semantics

The collaboration is critical for our teams. Elrond developers will soon be able to use formal tools to write more secure smart contracts, with Runtime Verification opening perhaps a new era for widespread usage of more granular formal tools available for all developers.

With these tools in place, the Elrond ecosystem will stand out as a prime candidate for the vast majority of startups and companies looking to deploy secure high-value use cases, at internet scale performance.

We are ready to welcome the massive wave of adoption that is coming.