K Framework Enables Verification of Smart Contracts


The age of cryptocurrency is here. A high percentage of cryptocurrency transactions are taking place on the Ethereum blockchain, which uses a computer program or “smart contract” to execute them. In December, Ethereum became the first cryptocurrency to amass one million transactions in a single 24-hour period.

However, any programming mistakes create openings for the theft of the virtual currency. While there are many safeguards to protect against security breaches, to date there hasn’t been a way to guarantee the formal verification of these contracts. For instance, last month hackers in Tokyo broke into the Coincheck, Inc. and stole $500 million in digtal tokens.

In a fruitful collaboration with Prof. Grigore Rosu's Formal Systems Laboratory (FSL) at UIUC, Runtime Verification (RV) has used the K framework to successfully build and test a mathematical model of the Etherem Virtual Machine, which makes it possible to formally verify the accuracy of smart contracts.
Continue reading