We developed SCV, a verification tool geared towards contracts implemented in Michelson, the smart contract language of the Tezos blockchain. SCV utilizes symbolic execution to derive verification conditions that can be checked automatically against user specifications using an SMT solver. These specifications are written in a domain-specific language. We present the fundamental principles behind the design and development of SCV. By pruning states during symbolic execution, SCV effectively addresses the problem of state explosion. This approach has enabled us to conduct two case studies on real-life contracts, demonstrating the expressiveness of our tool.