Organised by the Exactpro Sri Lanka team, our Solidity Verification mini-course features such topics as Formal Verification of Software, Decentralised Finance on the Ethereum Blockchain and Formal Verification of Solidity Contracts.

 
Lecture 1

Lecture 1. Formal Verification of Software
✅Formal proving, axioms and rules of inference
✅Hoare logic, preconditions, postconditions
✅Automated proving with Microsoft Z3 theorem prover

Q&A Session for Lecture 1

We discussed Formal Verification of Software and answered questions on the following topics:
✅Formal proving, axioms and rules of inference
✅Hoare logic, preconditions, postconditions
✅Automated proving with Microsoft Z3 theorem prover

Lecture 2

Lecture 2. Decentralised Finance on the Ethereum Blockchain
✅Blockchain, Bitcoin, Ethereum
✅ERC-20, ERC-721, DeFi, DAO
✅Solidity syntax, EVM

Q&A Session for Lecture 2

We discussed Decentralised Finance on the Ethereum Blockchain and answered questions on the following topics:
✅Blockchain, Bitcoin, Ethereum
✅ERC-20, ERC-721, DeFi, DAO
✅Solidity syntax, EVM

Lecture 3

We discussed 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

Q&A session for Lecture 3

We discussed Formal Verification of Solidity Contracts and answered questions on the following topics:
✅Typical vulnerabilities: Stack Overflow, arithmetic bugs, timestamp dependance, costly loop, reentrancy
✅Overview of existing tools
✅Known issues and challenges of formal verification