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.

Course Instructors

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.