Smart contracts are programs that are executed in a blockchain, mapping contracts and other real-world agreements to program logic and executing the contract conditions in an automated and transparent manner. Typical use cases range from business relationships, with the blockchain acting as a secure database and fraud protection, to voting, where security and privacy can be guaranteed by blockchain technology.
Smart contracts require a high degree of reliability. They manage financial goods, rights, and other real-world values, making them a potential target for attackers. Therefore it is necessary to use formal methods when designing smart contracts, so that their functional correctness can be proven.
The goal of this project is to pave the way for specification and formal verification of smart contracts. Building on existing verification tools and technology, we establish a base for describing and proving functional properties of smart contracts. The overall goal is that blockchain/smart-contract technology, with all its advantages, can be confidently employed.