Our great sponsors
-
As an example, taken from Certora's tutorials (most examples in this article will be copied or adapted from it), let's say we have a Bank contract that receives and stores deposits from users. We want to verify that, after every deposit, the total funds deposited are greater than every individual user balance.
-
The main challenge is dealing with non-view functions. The default behavior of the prover is to assume that an external call can alter all state on every contract but the caller, noted as HAVOC_ECF. This can lead to state changes in external contracts that are unreachable, making verification more difficult. Furthermore, it assumes that the call is non-reentrant, which in reality is a frequent source of attacks. This last issue can be avoided by indicating that calls can re-enter, noted as HAVOC_ALL, but this means that an external call can mutate any state in any contract, caller included. This leaves the contract being verified in a state where we don't know anything about it after an external call is made. This severely limits what we can prove.
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
Understanding a smart contract as a finite-state machine (obligatory mention to Yoichi's bamboo, my favorite smart contract programming language that never happened) allows us to define clear rules on:
-
Let's grab some examples from OpenZeppelin's TimelockController spec. In a Timelock, operations can have different states. We can write a rule that checks, for instance, that calling execute is the only way for moving an operation from ready to done state.
-
Certora's tutorial on github is also a great starting point for the basic concepts, though the lessons for more advanced ones are still under development. The documentation provides a good overview and reference for many concepts, though it's also a work in progress, and redirects to an older set of docs for the more advanced ones. A multi-contract example repo is a good complement to see the documented concepts in action.
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
Related posts
- Fork mainnet using hardhat to test and build on DeFi protocols and more
- Generating Decentralized identifier using ERC725 and ERC735
- “Every company will have an nft strategy” - Gary Vee Gary V explains why every company will implement in nft strategy in the next decade. Not every nft will be the next big then but they will still be very useful because the technology is so great. Do you agree with Gary?
- Implementing a Token Contract using Solidity
- Question about implementing a UUPS proxy