A smart contract is hard to patch for bugs once it is deployed, irrespective of the money it holds. A recent bug caused losses worth around 50millionofcryptocurrency.WepresentZEUS—aframeworktoverifythecorrectnessandvalidatethefairnessofsmartcontracts.Weconsidercorrectnessasadherencetosafeprogrammingpractices,whilefairnessisadherencetoagreeduponhigher−levelbusinesslogic.ZEUSleveragesbothabstractinterpretationandsymbolicmodelchecking,alongwiththepowerofconstrainedhornclausestoquicklyverifycontractsforsafety.WehavebuiltaprototypeofZEUSforEthereumandFabricblockchainplatforms,andevaluateditwithover22.4Ksmartcontracts.Ourevaluationindicatesthatabout94.60.5 billion) are vulnerable. ZEUS is sound with zero false negatives and has a low false positive rate, with an order of magnitude improvement in analysis time as compared to prior art.