There is actually already fledgling support for this in Solidity (the prevailing language that Ethereum developers use to write smart contracts).

https://forum.ethereum.org/discussion/3779/formal-verificati...