Posted on October 19, 2017 by Philip Daian
Runtime Verification, Inc. (RV) along with the Formal Systems Lab at the University of Illinois (FSL) are announcing a joint initiative targeting the full formalization of the Viper smart contract programming language, using the K Framework to create a full formal definition of this research-oriented smart contract programming language. We believe this effort will yield a number of useful tools and artifacts, and can lay the foundation for the future of principled and formally rigorous smart contract development.
At both RV and FSL, we believe strongly in a semantics-first approach to language development. This semantics-first approach means establishing a rigorous, mathematically formal, and human-readable definition of a programming language early in development. We believe this approach has several advantages.
In short, we do not believe it is desirable to cater such tools directly to the target language. The target language may change, requiring frequent changes to the surrounding tools and introducing massive inefficiencies. Language-specific tools may also bake in language-specific hacks or shortcuts that are often difficult to understand or detect. And, language-specific tools require the duplication of core language-independent infrastructure across projects, a major inefficiency in software quality tool development.
Our semantics-first approach, on the other hand, allows for an executable (can be used as an interpreter) semantics to evolve with the language, providing the above tools through a language-independent semantic framework and allowing the reuse of such core tool infrastructure across programming languages and language versions. This approach also provides developers with an interpreter usable as a reference implementation for testing and compiler development, and provides a clear human-readable yet precise language definition that can be independently useful.
We believe the creation of such formal tools from our semantics of Viper will be practically useful towards developing sophisticated analysis and verification tools that directly bolster smart contract rigor and security, an obvious gain for the Ethereum community and all smart-contract enabled blockchains.
There are several reasons that we've chosen Viper as a target of formalization. They include:
Overall, we are incredibly excited about the future of Viper in smart contract development and verification and the opportunity to build a principled and secure smart contract programming language, and look forward to building rigorous guarantees and usable tools for Viper smart contracts.
As part of this new Viper-based project, the following work is planned:
We reserve the right to make changes to this schedule as we receive input from the community and the stakeholders in this project, including the developers of Viper. We are aiming for maximum utility and impact for the Ethereum community, and will iterate rapidly to see what works and where we can apply this semantics-based technology effectively.
We will also be in close contact with the Viper team and developers, providing any feedback that we believe useful to enhancing the security of contracts built on Viper, making Viper easier to model, or making Viper contracts easier to verify.
We encourage any interested parties to engage us, ask questions, contribute code, or build experience with our tools. We are also always looking for contributors able to work on documentation, efficient install/quickstart process for new developers, and more proof examples. We are hiring, and will be sure to keep an eye open for helpful contributors!
We will also be posting updates on our brand new Twitter page @rv_inc, which we hope any interested developers will follow and interact with.
Let's build more secure smart contracts for everybody, together!
This research and development project will be made possible by a grant from the Ethereum Foundation.