In this tutorial, we will cover the basics of the Certora Prover and reach some of the most advanced features available that the Prover offers. You will learn about common specification patterns, diagnosing violations reported by the Prover, and troubleshooting wrong configurations of the Prover. Our running example will be a smart contract implementing a Map. Initially, we will implement a map that doesn’t provide much beyond the standard primitive mapping type of Solidity, but as we progress, we will support iteration over the map’s keys (slightly akin to OpenZeppelin’s EnumerableMap contract).