This gist shows how formal conditions of Solidity smart contracts can be automatically verified even in the presence of potential re-entrant calls from other contracts.
Solidity already supports formal verification of some contracts that do not make calls to other contracts. This of course excludes any contract that transfers Ether or tokens.
The Solidity contract below models a crude crowdfunding contract that can hold Ether and some person can withdraw Ether according to their shares. It is missing the actual access control, but the point that wants to be made
