ConsenSys, a blockchain company that works on improving the Ethereum network, has announced the release of Elle, a formally-verified code compiler that builds a secure link between the Ethereum Virtual Machine (EVM) and higher-level smart contract code.
Ethereum and other blockchain technology are inherently built on smart contracts, the trustless system that allows the network to be secure and prevent discrepancies between transactions. It is the rule of law in blockchain transactions, as it “exists on the blockchain to correctly encode the transaction logic of our trusted transactions”. As an exemplification of the “code is law” principle of blockchain, if it contains errors, it can lead to unintended and harmful consequences.
However, they argue, smart contracts can contain bugs and errors, but once it is coded and established on the Ethereum network, it cannot be changed, putting people subject to the contract vulnerable to attacks and mismanaged transactions. This has occurred in the Ethereum network before, most notably with the DAO hack resulting in a hard fork and the creation of Ethereum Classic, along with serious monetary losses.
Errors in smart contracts could have serious implications for whatever is established on those contracts, as was seen when a bug was found (and fixed) in Solidity, a programming language used for implementing smart contracts on Ethereum. The bug could have caused “severe consequences for whatever cryptoeconomic system might have been built on top of that token.”
ConsenSys thus developed Elle-Core, or “Elle” for short. In simple words, it is a structured programming language that can formally verify smart contracts, protecting users from bugs in smart contracts’ implementations. According to the developers, it is a “very exciting direction for Ethereum smart contract development”.
According to the developer, Mario Alvarez:
Elle helps take the security of compiled smart contracts to the next level because Elle comes with a proof that the output EVM program will have the same meaning as the source.
Elle will thus simplify the time, effort and money spent on audits of smart contract code.