Formal verification provides certain mathematical guarantees that a smart contract does what it is supposed to do, at least according to how it is programed. This is usually done by creating an abstract mathematical model of the smart contract that can be proved to be equivalent to the specifications provided. Thus, it is possible to establish an equivalence between the smart contract and the specifications, so that as far as the specifications are accurate, the smart contract will also be accurate. This eliminates many common forms of bugs in smart contracts. The Tezos smart contract platform aims to implement formal verification.