Smart contracts can handle large numbers of virtual coins worth hundreds of dollars apiece, easily making financial incentives high enough to attract adversaries. Unlike traditional distributed application platforms, smart contract platforms such as Ethereum operate in open (or permission-less) networks into which arbitrary participants can join. Thus, their execution is vulnerable to manipulation by random adversaries—a threat that is restricted to accidental failures in traditional permissioned networks such as centralized cloud services.

Although users in Ethereum have to follow a predefined protocol when participating in the network, it has been shown that there is considerable room for manipulation of a smart contract’s execution by the network participants. For example, Ethereum (and Bitcoin) allows network participants (or miners) to decide which transactions to accept, how to order transactions, set the block timestamp, and so on. Contracts which depend on any of these sources need to be aware of the subtle semantics of the underlying platform and explicitly guard against manipulation.

In contrast to classical distributed applications that can be patched when bugs are

detected, smart contracts are irreversible and immutable. There is no way to patch a buggy smart contract, regardless of its popularity or how much money it has, without reversing the blockchain (a formidable task). Therefore, reasoning about the correctness of smart contracts before deployment is critical, as is designing a safe smart contract system.

More detail: https://www.linkedin.com/pulse/formal-verification-smart-contracts-raghuram-madabushi/