ETHERLive delivers real-time price and volume data across 16+ exchanges to users in a clear and easy-to-understand package. Users can get up-to-the-second updates for each exchange/currency pair, as well as aggregated market averages for each exchange, currency, and the market as a whole. It also provides a global converted average of all the currency pairs monitored by ETHNews, converted to USD.


24hr ---

The Basics

Learn the basics of Ethereum and various cryptocurrency technologies

Learn More

What is Ethereum?

Understand the underlying principles of the Ethereum Platform

Learn More

The Blockchain

Discover the revolutionizing technology known as the blockchain

Learn More

Press Release

Submit a press release for consideration on ETHNews

Submit Press

Story / Dapp

Submit a story or DAPP to be considered for publication on ETHNews.

Submit Story


Submit "Ethereum Explainer" content for consideration to be featured on ETHNews

Submit Topic
ETHNews Logo
Ether Price Analysis
Contact Us

IC3 Bootcamp Winners




The KEVM project team was declared the winner of the IC3-Ethereum Crypto Bootcamp for creating a human-readable model of reference for Ethereum Virtual Machine programs that is reliant on the K-framework.

IOHK, a self-described blockchain engineering company, has revealed that a research project in conjunction with the University of Illinois at Urbana-Champaign (UIUC) has generated a fully-executable formal semantics model of the Ethereum Virtual Machine (EVM), called KEVM.

As per the announcement, KEVM assists in the execution, analysis, and verification of EVM executable distributed code contracts (EDDCs). It also has the distinction of being selected as the winner of the IC3-Ethereum Crypto Bootcamp, which the Ethereum Foundation hosted in partnership with the Initiative for Cryptocurrencies and Contracts (IC3). Prof. Grigore Rosu and PhD student Everett Hildenbrandt competed alongside nine other teams, rising to the top with their KEVM project, the funding for which stems from IOHK. The team’s first place prize included bragging rights, and $256 USD in Ether.

Runners up included second place winner Phil Daian of Cornell, with a project called “Writing Secure Smart Contracts,” for which 10,000 Dogecoins were awarded. An undisclosed quantity of Useless Ethereum Tokens were awarded to third place winners Nate Rush of Berkeley and Loi Luu, founder of SmartPool and developer of Oyente, from National University of Singapore, for their “ETH-ETC Peace Relay.” A similar award of UET was given to the recipients of an honorable mention, Haseeb Qureshi and Preethi Kasireddy, for their “Frontrunning Bancor” project.

Rosu expressed his delight in announcing KEVM as “the first complete and fully executable formal semantics of the Ethereum Virtual Machine." He went on to say:

"KEVM, which allows us to formally verify properties of EVM-based smart contracts in a correct-by-construction and cost-effective manner, is significant because Ethereum users need the guarantees of formal verification to safeguard against financial losses due to software bugs. This work serves as a foundation for the development of new smart contract analysis tools; more importantly, it gives us invaluable insight on how to design better programming languages for smart contracts."

KEVM is built upon the rewrite-based executable semantic K-framework. It passed the official 40,683-test stress test suite which was designed to ready EVM implementations, and exposes errors present in paper representations of EVM semantics, according to IOHK.

“KEVM has demonstrated that our unique approach based on K formal executable semantics is feasible and not computationally restrictive," said Rosu. "We hope our work serves as a strong basis for the development of a wide range of useful, formally-derived tools for Ethereum, like model checkers, certified compilers, and program equivalence checkers.”

According to the whitepaper, KEVM reduces the probability of bugs that can arise from encoding semantic models in existing software by creating a wide range of tools from the same reference semantics, reinforcing the team's "semantics first" development approach. The authors affirm a commitment towards contributing to the secure development of a bug-free EDCC ecosystem.

According to IOHK some of the advantages of the K-framework that drew the company’s attention included its language independent nature, an ability to meet a wide range of applications, and academic adoption. The framework has already been utilized in the formalization of JavaScript, Java, C, Python, and PHP. The K-framework also boasts an extensive toolkit that includes a semantic debugger, symbolic execution engine, and a verification infrastructure.

IOHK CEO Charles Hoskinson made comments on the next steps for IOHK, based on the groundwork his team has done.

"This research has given us a great degree of insight into what one should do to redesign the EVM to make it more secure, faster, and more efficient. It will now be easier to build tooling for the EVM, such as verified compilers. This white paper is the result of our first wave of research into this area. Based on this research, IOHK will begin building prototypes and our hope is to have an EVM 2.0 ready next year, as part of Cardano, a product we are currently building.”

As an open source project, KEVM will continue to be developed in the public realm, and ETHNews will continue to provide coverage of new innovations the team brings to light.

Jeremy Nation

Jeremy Nation is a writer living in Los Angeles with interests in technology, human rights, and cuisine.

ETHNews is committed to its Editorial Policy

Like what you read? Follow us on Twitter @ETHNews_ to receive the latest KEVM, IOHK or other Ethereum ecosystem news.