cs.PL cs.LO cs.SE
solc verify A Modular Verifier for Solidity Smart Contracts. We present solc verify, a source level verification tool for Ethereum smart contracts. Solc verify takes smart contracts written in Solidity and discharges verification conditions using modular program analysis and SMT solvers. Built on top of the Solidity compiler, solc verify reasons at the level of the contract source code, as opposed to the more common approaches that operate at the level of Ethereum bytecode. This enables solc verify to effectively reason about high level contract properties while modeling low level language semantics precisely. The contract properties, such as contract invariants, loop invariants, and function pre and post conditions, can be provided as annotations in the code by the developer. This enables automated, yet user friendly formal verification for smart contracts. We demonstrate solc verify by examining real world examples where our tool can effectively find bugs and prove correctness of non trivial properties with minimal user effort.