Solidity Verification Mini-course
The mini-course is aimed at those interested in the topic of Solidity Verification. It is free of charge and requires no previous knowledge on the subject. The course is organised by the Exactpro Sri Lanka team. See the course agenda below.
The mini-course included 3 lectures:
Lecture 1. Formal Verification of Software
- Formal proving, axioms and rules of inference
- Hoare logic, preconditions, postconditions
- Automated proving with Microsoft Z3 theorem prover
Homework: theory test, statements to formalise, Z3 basics.
Lecture 2. Decentralised Finance on the Ethereum Blockchain
- Blockchain, Bitcoin, Ethereum
- ERC-20, ERC-721, DeFi, DAO
- Solidity syntax, EVM
Homework: theory test, smart contract to implement with Solidity.
Lecture 3. Formal Verification of Solidity Contracts
- Typical vulnerabilities: Stack Overflow, arithmetic bugs, timestamp dependance, costly loop, reentrancy
- Overview of existing tools
- Known issues and challenges of formal verification
Homework: theory test, tool practice.
Rostislav Yavorski, Head of Research, Exactpro
Andrey Novikov, Syndata.io, Managing Partner
The recordings of the course lectures are available on the Exactpro YouTube channel via the link below.