Does your smart contract do what you wanted it to do?

Check

About Helmholtz — Verifier for Tezos Smart Contracts

Helmholtz is a formal verifier of smart contracts written in the Michelson language for the Tezos blockchain. The specification of a smart contract is described as a refinement type.