As a follow-up to An Introduction to Formal Verification Techniques and Tools, we will analyze 4 different examples in order to learn how to use formal verification and symbolic execution tools
I just wanted to point out to the possible issue with a first example (the one with the code similar to the ERC-4626).
In case of `deposit` function, if `totalAssets` has a value of 0, is should also revert, therefore the issue is not only with `mint` function. Any of the other tools you were testing, where during setup the values are not explicitly 0 for `totalSupply` and `totalAssets` should revert (every tool except `hevm`, which as explicitly set these to non-zero value).
Hi Secoalba,
Great article!
I just wanted to point out to the possible issue with a first example (the one with the code similar to the ERC-4626).
In case of `deposit` function, if `totalAssets` has a value of 0, is should also revert, therefore the issue is not only with `mint` function. Any of the other tools you were testing, where during setup the values are not explicitly 0 for `totalSupply` and `totalAssets` should revert (every tool except `hevm`, which as explicitly set these to non-zero value).