Example Application: Verification of Smart Contracts and Clients

As an example application, we can use Stainless in automated verification of smart contracts. We have created the following fork of Stainless:

https://github.com/epfl-lara/smart

which shows how to:

• write smart contracts in Scala;
• specify and prove properties of such programs, including precise reasoning about Uint256 data types;
• generate Solidity source code from Scala, which can then be compiled and deployed using the usual tools for the ethereum software ecosystem.

For example, we have modeled and verified a voting smart contract developed by SwissBorg using Scala and Stainless (check the corresponding benchmark).

For more information, check the README.md, as well as the online documentation including the page on smart contracts in Stainless.

Our verification efforts may prove useful in the future for companies such as AXONI as well. A this stage, our open source implementation of generator for Solidity is a proof of concept, which helps understand the verification challenges as well as differences and similarities of Solidity and Scala programming models.

Beyond verifying individual smart contracts, we are excited about the potential of Stainless to establish properties of clients and wallets for blockchain networks, such as the Mantis client written in Scala as well as Bitcoin-S.

Finally, we are also interested in new programming models for smart contracts and understanding how they can further increase the reliability and efficiency of decentralized systems.

This direction of work with Stainless is inspired by discussions within the EPFL Center for Digital Trust of which our research group is a member.

Stainless is the result of work of many contributors, see the main Stainless repository. Smart contract support is in particular due to the work of Jad Hamza and Romain Jufer. For more information about Stainless for blockchain technologies, please contact Jad and Viktor.